Arithmetic ConnectomeIndependent mathematics research

Research milestone / 25 October 2026

Finite ranges.
Exact boundaries.

A reusable generator and Lean kernel checker now certify Robin’s inequality for a specified canonical family over a complete real interval of cutoff parameters.

FINITE CERTIFICATION · EXPLICIT SCOPE

The problem. Numerical samples alone cannot establish a statement at every real cutoff, especially at exact ties. This track certifies the canonical family across a complete interval. Read the result, its event handling and guarded inputs, then the evidence limits; compare the three research tracks.

What is certified?

For every real cutoff parameter y in the closed interval [100000, 102000], the actual canonical integer N(y) satisfies N(y) > 5040 and

σ(N(y)) < eγ N(y) log log N(y).

Here σ is the sum of positive divisors and γ is the Euler–Mascheroni constant. The canonical family selects the minimizing prime exponents for the calibrated slope λ(y) = log(y/(y−1))/log y, keeping the smaller exponent at a tie. All logarithms on this page are natural.

Exact definition of the canonical family

For each prime p and nonnegative integer exponent a, define the local cost

Cp,y(a) = λ(y)(a − 1) log p − log(1 − p−(a+1)).

Choose ap(y) as the smallest exponent minimizing this cost. Equivalently, it is the first nonnegative integer a for which

λ(y) log p − log((pa+2 − 1)/(pa+2 − p)) ≥ 0.

Then N(y) is the product of pap(y) over all primes. Only finitely many exponents are nonzero in the range discussed here. The first-nonnegative-increment rule chooses the smaller exponent whenever adjacent costs tie; it includes exponent zero for an absent prime.

The interval describes the parameter y. It does not mean every integer N between 100000 and 102000. The theorem covers every real parameter in the interval, rather than a sample grid.

This is finite strict satisfaction of Robin’s inequality. It establishes no Robin exception, no global residual sign and no conclusion about the Riemann hypothesis.

How the finite certificate covers the interval

  1. Certified anchor

    Start from the checked canonical value at y = 100000.

  2. Complete events & exact ties

    Represent every coordinate change; at equality, keep the smaller exponent.

  3. Compensated margin budget

    Check that the certified loss is strictly below the certified starting margin.

  4. Whole real interval

    Conclude N(y) > 5040 and strict Robin satisfaction for every real y in [100000, 102000].

The closed real cutoff interval from 100000 to 102000A continuous segment with two filled endpoints represents every real cutoff y from 100000 through 102000, including both endpoints. For each y, the theorem concerns its canonical integer N(y). No interior event positions, sample grid or values of N are plotted.
100000102000
Every real cutoff y in [100000, 102000] is covered for its canonical N(y), not every integer in that numerical interval.

Complete events, including exact ties

The wider example contains 175 coordinate events: 174 new-prime entries and one increment of the already present prime 439, from exponent 1 to 2. This is not a claim of 175 distinct event times or 176 attainable integers.

Every coordinate event has a unique exact real root. Its increment is active only strictly after that root; equality retains the smaller exponent. Coincident roots are allowed, with all tied coordinates inactive at their common root. Numerical root enclosures do not decide equality or ordering.

The checker verifies complete coordinate-event representation and the actual canonical factorization. A compensated finite margin budget then proves a positive Robin margin uniformly over all active combinations. The certified starting margin is greater than 10−4; the wider example’s total certified loss allowance is less than 10−4. This is a starting-margin and loss comparison, not a claim that the remaining margin is 10−4. The budget may include combinations no real parameter attains; it does not assert that every subset is realized.

A guarded, anchored range class

The reusable workflow is anchored at y = 100000 and accepts an integer upper endpoint. Its implemented domain is 100000 ≤ H ≤ 262144, subject to certified endpoint enclosures, an omitted-layer guard and a sufficient margin budget. Membership in that numerical domain alone does not guarantee certification.

The cutoff guard derives at most one increment per prime within an admitted interval; this is not an arbitrary assumption about all ranges. Unresolved endpoint enclosures or failed guards produce an unsupported or inconclusive result. An insufficient budget gives no sign conclusion; malformed certificates are rejected, and execution failures remain unverified.

Every real closed subinterval of a verified anchored range is covered by restriction. What remains open for extension? A different anchor needs new certified numerical inputs. Extending beyond the cutoff class needs new layer bounds and suitable prime/level masks.

How this fits the wider work

The canonical track also has a checked sharp benefit asymptotic and signed-residual analysis. A benefit asymptotic alone does not determine a residual’s sign: the signed analytic contribution must also be controlled. The finite result above supplies a certified positive margin only on its stated range.

The candidate-counting preprint and the shell/profile construction are separate tracks with their own hypotheses and remaining obligations. The relaxed shell already has checked eventual two-sided bounds under its stated theta estimate, including an unconditional exponent-1/10 instance; an adaptive relaxed shell has a checked lower bound. Those results do not establish actual Robin exceptions, and the full manuscript’s analytic theorem is not formally verified. The prime-pattern laboratory remains a floating-point totient illustration, not this verifier.

Checks and public availability

The recorded private validation includes 198 Robin build targets, 17 exact-statement checks, 107 named declaration axiom audits restricted to Lean’s standard logical axioms, 15 rejection cases and an inconclusive case, and 11 Python regressions. Independent AI-assisted mathematical and protocol reviews were recorded. These are local checks, not a remote CI or independent human-review claim.

Generated rational data are untrusted; the kernel checks the resulting theorem and certificate conditions. The finite example integrates a certified canonical numerical anchor, exact ties, event completeness and the compensated sign budget.

This page is a public summary, not a public reproduction package. Proof sources, generated certificates and raw validation logs remain private and are not downloadable here. Their private existence is not public reproduction evidence. Independent human scrutiny is still sought, and no novelty claim is made.

The September 15 manuscript PDF, its paper-only license and historical companions remain unchanged. Their scope is separate from this October milestone.

Review the statement and its boundaries →Statement fidelity, event completeness, ties and certificate soundness