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 skeptic can run lake build at the pinned kernel commit (SIDE-kernel v1.5 = 0e5233f) and #print axioms at the named route theorems (structural_exhaustiveness_proved; SpectralCannonFull.spectral_cannon; ConservationBridge.riemann_hypothesis — 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). All route terminals report {propext, Classical.choice, Quot.sound}. Verification claims are made by named theorem at pinned public commits, never by file counts; the standing correction record is 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; h1 complete at the witness — all eight per-class coupling facts of Chapter 15 machine-checked at the fixed Mellin witness and conjoined (h1_complete_at_Phi, SIDE-lv-conservation); the finite-range Li positivity certificate to the Voros detection threshold, whose finite-set conjunct is now itself proved (lowFinset_mem_iff, v0.10.0); and the step (9) assembly stated in its two-sentence form — the identity reading (every zero participates in the Guinand–Weil prime/zero ledger; classical and shared) separated from the sign reading (participation forces σ = 1/2; the clause). Section 27.3, "The One Premise," names that clause in five equivalent 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 the sign-layer survey (§ANNEX B) and two machine-checked negative results. CONTENTS. A_Place_to_Stand.md — the full manuscript (v5.10.2). Six companion papers: Exhaustive_Enumeration, Which_Structure_Confines, Spectral_Inertness, Third_Identity_Element, Silence_of_Foundations, Seven_Mechanism_Classes. ONE_PAGE_PROOF.md — the condensed proof chain. FORMATION_ARCHITECTURE.html, PAPER_DEPENDENCIES.svg — visualization assets. ERRATA.md — the standing correction record. PAIRED DEPOSITS. SIDE-kernel v1.5, DOI 10.5281/zenodo.21520474 (all versions: 10.5281/zenodo.19674312). SIDE-lv-conservation v0.10.0, DOI 10.5281/zenodo.21539068 (all versions: 10.5281/zenodo.21433177). Two Mathlib contributions from this work are merged: PR #36881 (tendsto_mul_logDeriv_simple_zero) and PR #36865 (analyticOrderAt_eq_one_of_zero_deriv_ne_zero). VERSION. v5.7–v5.8 (July 2026): the fulcrum reframe (§27.3 to five registers with ancestry) and h1 completed at the witness, with the C₄ strengthening story told in full. v1.1.2 / manuscript v5.10.2 (July 2026): the re-articulation release — the monograph's narrative re-articulated end to end in five meaning-preserving passes (spine orientation, seam bridges, canonical homes for repeated stories, voice separation, currency); §25.8 and §25.1 currency to kernel v1.5; §27.3 currency to lv v0.10.0 (the proved finite-set conjunct); step (9) recast into its identity/sign sentences with step (10) carrying the explicit clause tag; the Third_Identity element-level convention caveat; ERRATA entry E-2026-07-23-1 (§18.2 label correction). No mathematical claim changed in any of these releases; the open clause stands exactly as named.