Spectral bounds for the number of Robin candidates

Reading this track. Start with the counting problem below, follow the four links in the argument, then read the verification scope. The three-track comparison separates this manuscript from the shell results and canonical certificate.

The question

Robin’s inequality links the sum-of-divisors function to the Riemann hypothesis. This project asks a quantitative question: how many integers can satisfy its weak reverse inequality?

Here σ(n) is the sum of the positive divisors of n, and γ is the Euler–Mascheroni constant. The manuscript counts all integers 3 ≤ n ≤ X for which σ(n) ≥ e^γ n log log n, including the small initial cases. Under the specified zero-free-region and uniform zero-density inputs, it derives an eventual bound

The rate g is built from an exact weight-two spectral infimum and a specified secondary factor. Classical and Vinogradov–Korobov inputs give unconditional written specializations. The full definitions, quantifiers and imported statements appear in Theorem 1.

Four links in the argument

1. Spectral estimate. Bound a signed integrated tail using a weighted zero sum and a uniform density estimate.
2. Centered inclusion. Use an exact Mertens identity to place candidates in a larger set defined by a common arithmetic cost budget.
3. Finite counting. Encode prime-support changes, control distant and repeated factors, and count the remaining near-cutoff patterns.
4. Aggregation. Combine intervals of unit length in log n, using the proved regularity of the rate function.

Assumptions and verification

The analytic theorem is a written argument relative to its stated classical imports. The zero-free-region and uniform zero-density contract determines the rate; the finite Lean interfaces retain their explicit imported hypotheses. The verification section distinguishes these records from a full analytic formalization.

What remains to be settled?

Independent human review is still sought. The relationship to earlier counting and integrated Mertens results remains under investigation. For the separate shell route, passing from a relaxed benefit set to actual Robin exceptions still requires signed-threshold control.

Read and inspect

October finite results

A follow-up studies a relaxed set defined by a sigma-benefit budget in a unit logarithmic shell. Its lower construction is distinct from the manuscript’s upper count of Robin candidates. Consolidation has brought together the following verified finite ingredients:

• Sigma correction. The prime-factor sum equals the log-ratio deficit. The concrete small-prime multiplier bound is proved; the unfinished historical draft has a verified successor.
• Distinct profiles. Powers-of-two padding preserves distinctness and cardinality for profiles over odd primes with a common positive baseline.
• Shell placement. The natural-floor padding exponent places a positive input in the unit logarithmic shell when its logarithm is at most the target.
• Padding cost. Dyadic padding has an explicit sigma-benefit increment bound. The floor-gap and radius corollaries require a nonnegative cost parameter.

The October checks compiled these ingredients and their statement audits, with actual axiom reports containing only Lean’s standard logical axioms. They do not establish the full shell lower bound, a lower count of Robin exceptions, or the full analytic theorem.

Subsequent checked work implements initial-profile cost accounting, local primewise estimates, finite concentration/counting and conditional assembly, including a concrete multiplier specialization. The old initial-profile task is no longer unimplemented. The full relaxed sigma-benefit shell now has checked eventual two-sided bounds under its stated theta estimate, including an unconditional instance with exponent 1/10. A smaller adaptive relaxed shell also has a checked lower bound. These results do not count actual Robin exceptions; controlling the signed arithmetic threshold remains a separate obligation.

A separate canonical-family track

The October 25 milestone certifies strict Robin satisfaction for the actual canonical N(y), for every real y in [100000, 102000]. It includes complete coordinate events and exact ties in a guarded range class anchored at 100000. It is not a lower count of exceptions or completion of the ENS/shell route.

Verification and scope

Remaining source check. The exact original Montgomery–Vaughan Brun–Titchmarsh theorem number and its precise real-endpoint range/convention remain unchecked. The bound is retained as an explicit classical import; this is a source-verification limitation, not a demonstrated defect in the inequality. Human specialist review and prior-implication assessment remain open.

Selected finite encoding and counting steps have been formalized in Lean. Historical audits checked those modules and their axiom dependencies at recorded source snapshots; the October checks above cover the specified finite follow-up ingredients. These are separate verification records, not a fresh verification of every result in the combined research tree. The Lean prime-partition bound takes Brun–Titchmarsh and Erdős–Nicolas–Sárközy (ENS) Lemma 1 as explicit hypotheses; their published mathematical statements are imported inputs to that formalization. The full analytic counting theorem has not been formalized.