Robin Saddle-Layer Reduction

Author: Jonas Whidden

This repository contains a Lean 4 formalization, computational experiments, and research manuscripts around Robin's inequality and the Riemann hypothesis.

Current status: the repository contains a Lean-checked conditional Robin-to-RH reduction with explicit external theorem and certificate boundaries. The final RH statement follows in Lean from the named external inputs and finite certificate objects, and the project is actively narrowing those inputs into smaller native proof targets. Until the dependency audit is clean of project-local theorem assumptions, the project should be cited as a conditional proof program, not as an unconditional Lean-native proof of RH.

Main Idea

Robin proved that the Riemann hypothesis is equivalent to

sigma(n) < exp(gamma) * n * log(log n)    for all n > 5040.

This project studies the extremal threshold-prefix structure of possible Robin violators through a saddle-layer event calculus. Marginal events for sigma(n)/n are organized by prime layers, producing explicit layer weights

c_j = j * (j^(1/j) - 1)

and a Lyapunov/window accounting system. Earlier versions isolated the remaining analytic input as a canonical half-shell theta-mass tail estimate. The current native branch also contains a direct Dusart/certificate route. Lean verifies that the final RH statement follows from the named external theorem targets and finite certificates, and most of the bridge plumbing around least counterexamples, abundancy records, canonical saddle states, event prefixes, and direct certificate budget witnesses is now native.

Status

What is in place:

• Lean-checked algebraic and order-theoretic reduction infrastructure.
• Lean-checked mass-to-count and finite-to-tail splice theorems.
• A native final socket: Robin.Native.riemannHypothesis_final : Robin.Native.ClassicalRiemannHypothesis.
• Native least-counterexample extraction and the above-cutoff abundancy-record step for Robin counterexamples.
• Canonical arithmetic-profile data for a hypothetical least counterexample: state (log n, log(sigma(n)/n)), scale X = n, frontier cutoff, and threshold-prefix event set.
• A concrete direct survivor budget witness shape (ConcreteSaddleBudget) matching the certificate socket.
• A decomposed saddle-budget bridge layer in Robin/Native/SaddleBudget.lean, including native endpoint atom bounds and an experimental endpoint-room shortcut. That shortcut is not used by the final theorem path because it does not match the paired-excess semantics used by the Abel injection.
• Generated certificate primitive data in Robin/Native/CertificatePrimitives.lean: the direct cell endpoints are now exact generated Lean data, while midpoint/radius and several containment facts are proved natively.
• Source-translation targets for Dusart and Robin's theorem.
• Publication-style manuscripts explaining the conditional reduction/proof program.
• Numerical experiments exploring the saddle-layer and window mechanisms.
• A non-vendored reference-fetch workflow for third-party papers.

What remains external or certificate-backed:

• Dusart's prime-interval theorem, currently decomposed into named source obligations and certificate targets in Robin/Native/Dusart.lean.
• Robin's divisor-sum theorem in the native form NativeRobinInequalityAll <-> ClassicalRiemannHypothesis.
• The arithmetic-profile-to-concrete-saddle-profile semantic bridge: nativeArithmeticProfileProducesConcreteSaddleProfile_source.
• Generated finite certificate objects currently replacing large prose/table verifications.

The broad bridge target,

nativeArithmeticProfileProducesConcreteSaddleProfile_source

is the current final bridge target. The exploratory certificate closes the finite/geometric Abel-injection side; it does not by itself close the survivor-budget semantics.

None of these external inputs are claimed as original to this repository. The goal is to reproduce or certify them in Lean while giving full credit to their authors. RH-conditional estimates are not used as unconditional inputs.

Repository Layout

• Robin/: Lean source for the formal reduction.
• Robin.lean: top-level Lean module.
• src/robin/: Python support code for events and Lyapunov diagnostics.
• experiments/: numerical experiments and exploratory checks.
• papers/: LaTeX manuscript and bibliography.
• notes/: exploratory theorem-target and analytic-lab notes. These are not the authoritative proof surface.
• explorations/: scratch formalizations and failed/successful attack logs. These are public lab notebooks, not final theorem claims.
• data/: generated experiment outputs.
• references/: URL/checksum manifest for third-party reference material.
• scripts/: repository helper scripts.

Papers

The main public-facing manuscript is:

• papers/robin-rh-conditional-traditional.tex
• papers/robin-rh-conditional-traditional.pdf

For a shorter mathematical orientation to the proof mechanism:

• papers/saddle-layer-proof-overview.tex
• papers/saddle-layer-proof-overview.pdf

Related proof-program notes:

• papers/conditional-robin-reduction.tex
• papers/conditional-robin-reduction.pdf
• papers/native-rh-proof-program.tex
• papers/native-rh-proof-program.pdf

To rebuild the main manuscript from the repository root:

cd papers
pdflatex -interaction=nonstopmode robin-rh-conditional-traditional.tex
bibtex robin-rh-conditional-traditional
pdflatex -interaction=nonstopmode robin-rh-conditional-traditional.tex
pdflatex -interaction=nonstopmode robin-rh-conditional-traditional.tex

To rebuild the condensed overview:

cd papers
pdflatex -interaction=nonstopmode saddle-layer-proof-overview.tex
bibtex saddle-layer-proof-overview
pdflatex -interaction=nonstopmode saddle-layer-proof-overview.tex
pdflatex -interaction=nonstopmode saddle-layer-proof-overview.tex

Lean

This is a Lean 4 / Lake project. The toolchain is pinned in lean-toolchain.

Basic check:

lake env lean Robin.lean

Full build:

lake build

Important theorem names include:

• Robin.Native.riemannHypothesis_final
• Robin.Native.nativeDusartPrimeInterval
• Robin.Native.nativeRobinCounterexampleImpliesCASurvivor
• Robin.Native.arithmeticCounterexampleProfile_of_least_record
• Robin.Native.nativeProfileToEventsClosed
• Robin.Native.arithmeticProfileProducesConcreteSaddleProfile_of_budget_targets
• Robin.Native.arithmeticProfileProducesConcreteSaddleProfile_of_fixedScaleBudget
• scaleEnoughWindowCountLowerAbove_of_canonical_half_shell_local_mass
• scaleEnoughWindowCountLowerAbove_of_middleBand_and_canonical_local_mass_tail
• riemannHypothesis_of_zeroState_briggs_prefix_halfCriticalScaleEndpointWindow_gap1724Slack_to_twoPowSixtySix_saddleDesertCriticalAligned_spanEq_from_three

Run #print axioms Robin.Native.riemannHypothesis_final to audit the remaining external theorem and certificate boundaries. A clean unconditional claim should wait until that audit contains no project-local theorem assumptions.

As of the latest native bridge pass, the significant project-local theorem assumptions still visible in the final audit are:

• remaining certificate proof objects under MertensCoupledBudget.directCert...; the endpoint arrays, low-endpoint cutoff, lambda value, lambda bounds, cell/paired excess definitions, cell-base proof, paired representation, and midpoint/radius containment facts have been moved out of the axiom audit;
• Robin.Native.nativeArithmeticProfileProducesConcreteSaddleProfile_source;
• Dusart/Schoenfeld interval source obligations used by the prime interval route;
• Robin.Native.nativeRobinTheorem_source.

Lean now proves the least-counterexample bookkeeping and canonical profile/event alignment around the Robin/CA bridge. The remaining bridge-side trust boundary is the semantic step that turns an actual arithmetic profile into the concrete saddle budget witness consumed by the direct certificate.

Experiments

Most experiments expect src on PYTHONPATH.

Example smoke run:

$env:PYTHONPATH='src'
python experiments/window_test.py --p1-limit 100000

Some larger diagnostics depend on generated CSV files in data/ and may take substantial time. The experiments are evidence and design tools; mathematical steps used in the proof route are represented in Lean before being relied on in the formal reduction.

Third-Party References

Third-party papers and source archives are not vendored. Their URLs and expected SHA-256 checksums are recorded in references/third_party_sources.json.

To fetch local research copies:

python scripts/fetch_third_party_sources.py

Fetched files are ignored by Git and remain under their upstream copyrights and licenses.

This project does not claim authorship of external theorems it cites or is trying to reproduce in Lean, including results due to Robin, Dusart, Schoenfeld, Guth--Maynard, Gafni--Tao, Li, and other cited authors. Any Lean translation of an external theorem is intended as a formal verification of the published mathematics, not as a claim of original discovery of that theorem.

Citation

Citation metadata is provided in CITATION.cff.

License

Copyright (c) 2026 Jonas Whidden.

This repository is dual-licensed:

• Source code, scripts, Lean files, generated certificate checkers, and other software-like files are licensed under the MIT License.
• Mathematical exposition, papers, notes, diagrams, documentation, and research prose are licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0).

See LICENSE and NOTICE for details.