## Main theorem The Riemann Hypothesis: every nontrivial zero of the Riemann zeta function has real part 1/2. ## Method The SIDE Exclusion Principle — Symmetry, Independence, Determination, Exhaustiveness. Applied to zeta, it proves that no off-line zero exists by enumerating the catalogue of mechanism classes from which off-line zeros would have to arise and excluding each one. The seven mechanism classes are proven exhaustive via Ostrowski's classification and the structure of ξ (s). No class produces the algebraic signature of an off-line zero. Independence of the constraints forbids conspiracy among them. Symmetry forces σ = 1/2 as the third identity element. The result follows without new axioms: the proof operates entirely within ZFC, and every component theorem is classical (Ostrowski 1916, Tate 1950, Størmer 1897, Artin–Whaples 1945, Cartan B 1876/1951). ## Both legs complete The proof exists as a human-readable mathematical argument in the monograph (Parts I–IV, each chapter ZFC-valid with classical component theorems) and as a machine-verified Lean 4 kernel that compiles the same conclusion end-to-end via three independent routes. A reader who does not read Lean can verify the argument mathematically; a skeptic who does not trust informal proof can run `lake build` and check that the kernel confirms. ## Contents **Monograph** - `APlaceₜoStand. md` — the full 28-chapter manuscript presenting the proof, its architecture, and its context. **Six companion papers** - `ExhaustiveEnumeration. md` — the mechanism class enumeration- `WhichStructureConfines. md` — structural confinement argument- `SpectralInertness. md` — spectral inertness at σ = 1/2- `ThirdIdentityElement. md` — Trivium and identity structure- `SilenceₒfFoundations. md` — the Silence Principle- `SevenMechanismClasses. md` — the seven-class exhaustion proof **Summary** - `ONEPAGEPROOF. md` — condensed statement of the proof chain. ## Paired deposit This manuscript corpus pairs with the SIDE-kernel v1. 1 Lean 4 formalization at DOI 10. 5281/zenodo. 19937590 (https: //doi. org/10. 5281/zenodo. 19937590) (superseding v1. 0 at 10. 5281/zenodo. 19674313 (https: //doi. org/10. 5281/zenodo. 19674313) ). The kernel verifies the proof end-to-end across 83 active Lean files (Kernel + Bridge + MetaKernel) with zero sorry and zero custom axioms, compiled against Mathlib. Two Mathlib contributions from this work have been merged: PR #36881 (https: //github. com/leanprover-community/mathlib4/pull/36881) (`tendstoₘulₗogDerivₛimpleᵦero`) and PR #36865 (https: //github. com/leanprover-community/mathlib4/pull/36865) (`analyticOrderAtₑqₒneₒfᵦeroderivₙeᵦero`). v1. 0. 1 (April 2026): Orienting paragraph ("How This Monograph Is Organized"), completable-path matrix (§25. 5a), CrossClassExclusion surfaced in §25. 5 Bridge table. No mathematical changes. Formal verification count unchanged (560 declarations, 0 sorry, 0 axioms). v1. 0. 2 (May 2026): Updated paired-deposit cross-reference to SIDE-kernel v1. 1 (DOI 10. 5281/zenodo. 19937590), which adds Bridge/CartanBBridge. lean elevating n₃ = 2 from manuscript claim to Lean-verified theorem and realigns the kernel with current Mathlib API. Manuscript version stamp bumped from v5. 3 to v5. 4. No mathematical changes. Companion papers and visualization assets carried forward unchanged from v1. 0. 1.
J. York Seale (Fri,) studied this question.