A Place To Stand: Proof of the Riemann Hypothesis via the SIDE method

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 an off-line zero 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 proof operates entirely within ZFC, and every component theorem is classical (Ostrowski 1916, Tate 1950, Størmer 1897, Artin–Whaples 1945, Cartan 1876/1951). THE PROOF IN TWO FORMS. The argument exists as a human-readable mathematical monograph and as a machine-verified Lean 4 kernel, on the pattern of Hales's Kepler-conjecture proof and its Flyspeck verification: the manuscript proves the mathematics; the kernel compiles the logical architecture through three independent routes and reports its axiom base at named theorems. A reader who does not read Lean can verify the argument mathematically; a skeptic who does not trust informal proof can run lake build at the pinned kernel commit and run #print axioms at the named route theorems (structuralₑxhaustivenessₚroved; SpectralCannonFull. spectralcannon; ConservationBridge. riemannₕypothesis — the third is the compiled implication from the named interface ConservationHypothesis, whose mathematics is the manuscript's Chapter 13 territory and whose ledger is §27. 3). Verification claims in this corpus are made by named theorem at pinned public commits, never by file counts; an earlier version's blanket count is corrected in the enclosed ERRATA. md. WHAT THE MANUSCRIPT ESTABLISHES, AND WHAT IT NAMES AS OPEN. Proved and machine-checked around the argument: the exhaustiveness of the seven-class catalogue over the places of ℚ; Conservation of Spectra from Tate's thesis (Chapter 13) ; the Mechanism Theorem derived from the Independence, Determination, and Symmetry principles (Chapter 10) ; five independent compiled identifications of σ = 1/2 in five machineries; and — new at this version — h1 complete at the witness: all eight per-class coupling facts of Chapter 15 are machine-checked at the one fixed function Φ of the Mellin factorization and conjoined in the named theorem h1completeₐtPhi (SIDE-lv-conservation v0. 6. 0, commit c80bdc2, deposited separately with the completed-zeta and completed Dirichlet L-function growth bounds and a machine-checked countermodel bracketing a retired stronger claim). The final coupling, C₄ (modularity), is recorded in the correction-record voice this monograph keeps throughout: an internal strength audit found the earlier compiled statement weaker than the mathematics it stood for, so the statement was strengthened first — to a holomorphic upper-half-plane lift carrying both PSL₂ (ℤ) generator laws — and only then discharged, with witness jacobiTheta. Section 27. 3, "The One Premise, " names the proof's single premise in five registers with its full literature ancestry (Li 1997; Bombieri–Lagarias 1999; Oesterlé; Voros 2006; Lagarias 2007), locates it at one compiled goal state, and counts exactly what stands certified around it; the C₅-output (Hilbert–Pólya) register is explicitly disclaimed, never claimed. A companion census, Paths to the Critical Line, catalogues the field's completing and non-completing paths in relation, including two machine-checked negative results. CONTENTS. APlaceₜoStand. md — the full manuscript (v5. 8). Six companion papers: ExhaustiveEnumeration, WhichStructureConfines, SpectralInertness, ThirdIdentityElement, SilenceₒfFoundations, SevenMechanismClasses. ONEPAGEPROOF. md — the condensed proof chain. FORMATIONARCHITECTURE. html, PAPERDEPENDENCIES. svg, Visualization assets. ERRATA. md — the standing correction record. PAIRED DEPOSITS. SIDE-kernel v1. 3, DOI 10. 5281/zenodo. 21417776 (all versions: 10. 5281/zenodo. 19674312). SIDE-lv-conservation v0. 6. 0 (commit c80bdc2), deposited separately in this wave. Two Mathlib contributions from this work are merged: PR #36881 (tendstoₘulₗogDerivₛimpleᵦero) and PR #36865 (analyticOrderAtₑqₒneₒfᵦeroderivₙeᵦero). VERSION. v5. 7 (July 2026): the fulcrum reframe — §27. 3 rewritten to five registers with ancestry; §25. 5/25. 7/25. 8/28. 1 reconciled so Chapter 13's theorem is named as the premise's certificate, not its discharge. v5. 8 (July 2026): h1 complete at the witness, with the C₄ strengthening story told in full. No mathematical claim about the open premise is strengthened in either version. v1. 1. 1 (July 2026): companion enrichment in mutual light — the six companion papers, ONEPAGEPROOF, and the FORMATIONARCHITECTURE diagram gain named-terminal grammar where verification is invoked (the three route theorems at SIDE-kernel v1. 3 = 0bc21c0 with #print axioms = propext, Classical. choice, Quot. sound; h1completeₐtPhi at SIDE-lv-conservation v0. 7. 0), the one-premise clause where the exclusion syllogism is narrated (the inter-class conservation step, named in five registers at §27. 3), and cross-references to the companion census Paths to the Critical Line. The in-file version stamp of the manuscript is corrected to v5. 8 (it had lagged the version log; ERRATA E-2026-07-18-1). No mathematical content changed — this is an enrichment point release.