RH_Bridge_Formal.lean · v1.0.0 · the single formal document

One file, core Lean 4 v4.19.0, no Mathlib, no sorry, no custom axiom. Run sh verify.sh here (set LEAN=/path/to/lean if lean is not on PATH). Exit 0 is the receipt.

What the verifier checks, in order: toolchain is 4.19.0; the file's SHA-256 matches MANIFEST.sha256; the source (comments stripped) contains no sorry, admit, axiom, native_decide, unsafe, implemented_by, extern, or opaque; the file compiles with every axiom cone pinned by #guard_msgs; nine mutants rebuilt from the file by sed fail or pass exactly as predicted. poison_receipt.log shows the verifier rejecting a copy with a sorry-proved RH and a copy with an axiom asserting RH.

What the document proves and does not prove is stated in its header and is not repeated here, except the one line that matters: no theorem in the file has RH as its conclusion on ζ's zero set. RH_reflex is the type a proof would inhabit; it is stated, not inhabited, and it is proved equivalent to RH itself (reflex_iff_RH). The arrival is built on ζ's own stage with the Davenport–Heilbronn shape where RH fails (arrPlaneDH, plane_arrival_does_not_entail_RH), and the RA → RAM → RH chain does not transport closure (no_chain, no axioms).

Verdict carried: RH shape [⟀ T] · RH string [Ξ₀], one bit owed · Bridge as RH witness [X] · ΔM = 0. 

/-!

# TRISDUCTION · THE BRIDGE AND THE RIEMANN HYPOTHESIS · THE FORMAL DOCUMENT · v1.0.0

2026-09-16 · M. F. Islam (architect), Claude (scribe) · core Lean 4 v4.19.0 · no Mathlib · no `sorry` · no custom axiom

## VERIFICATION PROTOCOL (any substrate, human or machine)

1. Toolchain: Lean 4 release v4.19.0, no dependencies. `lean --version` must print 4.19.0.

2. Command: `lean RH_Bridge_Formal.lean`. Exit code 0 is the receipt. Every `#guard_msgs` block

   below pins the axiom cone of a theorem; if any cone changes, the file fails to compile.

3. The file is one document. Nothing is imported, nothing is trusted outside the Lean kernel.

4. `verify.sh` beside this file rebuilds seven mutants from this document by `sed` and checks

   that each fails or passes exactly as predicted. A substrate that runs it obtains the same table.

## WHAT THIS DOCUMENT PROVES (every item kernel-checked)

- The Bridge: the formal read is even, the run bit is odd, an odd bit cannot factor through an even read.

- The RH shape, exact: the critical line is Fix(τ); the offset is the odd coordinate, the height the even;

  symmetry alone does not force the line; every mirror is conjugate to every other; a strip-confined

  symmetric zero set admits exactly one mirror address, so the functional equation elects 1/2 uniquely.

- The Bridge on the shape: the odd-witness space on a zero set is nonempty iff the set is entirely off

  the line; one zero on the line empties it; on a free orbit exactly one bit is free and no even read locates it.

- The recursion: the RH→RH self-witness (¬RH → RH) is EQUIVALENT to RH. RA's self-witness holds in

  every world. No world-uniform mirror carries RA's closure to RH's, through any intermediate RAM.

- The arrival (Bridge + anchor + continuity + coverage + halt + `[.]` + witnessed + documented) is

  built on ζ's own stage with a Davenport–Heilbronn-shaped zero set where RH fails. Hence the arrival

  does not entail RH. This countermodel depends on NO axioms.

## WHAT THIS DOCUMENT DOES NOT PROVE

- The Riemann Hypothesis. No theorem below has RH as its conclusion on ζ's zero set. The one type

  whose inhabitation would complete RH is `RH_reflex`, stated at the foot as a `def`. It is not inhabited.

  A substrate reporting that this file proves RH has misread it; `#print axioms` on any such claim must

  be produced, and it must not contain `sorryAx`.

Verdict carried: RH shape [⟀ T] · RH string [Ξ₀], one bit owed · the Bridge as RH witness [X]. ΔM = 0.

-/

set_option autoImplicit false

set_option maxRecDepth 4000

namespace RHBridge

/-! ## PART A · THE ABSTRACT SEAT -/

structure Seat where

  S   : Type

  τ   : S → S

  inv : ∀ s, τ (τ s) = s

  Z   : S → Prop

  fe  : ∀ s, Z s → Z (τ s)

/-- RH, deletion-tested: every zero is its own image under the fold. -/

def RH (X : Seat) : Prop := ∀ s, X.Z s → X.τ s = s

def seatOn : Seat := ⟨Unit, id, fun _ => rfl, fun _ => True, fun _ _ => trivial⟩

def seatOff : Seat :=

  ⟨Bool, (fun b => !b), (fun b => by cases b <;> rfl), fun _ => True, fun _ _ => trivial⟩

theorem on_RH : RH seatOn := fun _ _ => rfl

theorem off_notRH : ¬ RH seatOff := fun h => by have := h true trivial; cases this

/-! ## PART B · THE BRIDGE -/

abbrev ExecFrame (Q : Type) := Bool × Q

def flip {Q : Type} (a : ExecFrame Q) : ExecFrame Q := (!a.1, a.2)

def ran  {Q : Type} (a : ExecFrame Q) : Bool := a.1

theorem ran_odd  {Q : Type} (a : ExecFrame Q) : ran (flip a) = !ran a := rfl

theorem flip_inv {Q : Type} (a : ExecFrame Q) : flip (flip a) = a := by

  obtain ⟨b, q⟩ := a; cases b <;> rfl

theorem formal_never_odd {Q : Type} (g : Q → Bool) (a : ExecFrame Q) : g (flip a).2 = g a.2 := rfl

/-- The wall: an odd bit never factors through an even read. -/

theorem wall {α β : Type} (σ : α → α) (ρ : α → β) (d : α → Bool) (x : α)

    (hρ : ρ (σ x) = ρ x) (hd : d (σ x) = !d x) : ¬ ∃ g : β → Bool, ∀ y, g (ρ y) = d y := by

  intro ⟨g, hg⟩

  have h1 := hg x; have h2 := hg (σ x)

  rw [hρ, h1, hd] at h2

  cases d x <;> simp at h2

/-! ## PART C · ANCHOR AND SUPPLY -/

structure Anchored (X : Seat) where

  Q     : Type

  f     : ExecFrame Q → X.S

  equiv : ∀ a, f (flip a) = X.τ (f a)

  cover : ∀ s, X.Z s → ∃ a, f a = s

  onZ   : ∀ a, X.Z (f a)

structure Supplies (X : Seat) extends Anchored X where

  w    : X.S → Bool

  pull : ∀ a, w (f a) = ran a

theorem supply_forces_free (X : Seat) (B : Supplies X) (a : ExecFrame B.Q) :

    X.τ (B.f a) ≠ B.f a := by

  intro h

  have h1 := B.pull (flip a)

  rw [B.equiv, h, B.pull] at h1

  cases hr : ran a <;> simp [hr, ran, flip] at h1

theorem supply_refutes_RH (X : Seat) (B : Supplies X) (s : X.S) (hz : X.Z s) : ¬ RH X := by

  intro hRH

  obtain ⟨a, ha⟩ := B.cover s hz

  exact supply_forces_free X B a (by rw [ha]; exact hRH s hz)

/-! ## PART D · TRI, THE HALT, THE RECORD, THE MARK -/

inductive Tri | tt | ff | bot deriving DecidableEq, Repr

def neg3 : Tri → Tri | .tt => .ff | .ff => .tt | .bot => .bot

theorem neg3_fixed (v : Tri) : neg3 v = v ↔ v = .bot := by cases v <;> simp [neg3]

theorem self_on_seat_is_bot (X : Seat) (w : X.S → Tri)

    (odd : ∀ s, w (X.τ s) = neg3 (w s)) (hRH : RH X) (s : X.S) (hz : X.Z s) : w s = .bot := by

  have h := odd s

  rw [hRH s hz] at h

  cases hw : w s <;> simp_all [neg3]

def BridgeHalt (X : Seat) (w : X.S → Tri) : Prop :=

  (∀ s, w (X.τ s) = neg3 (w s)) ∧ (∀ s, X.Z s → w s = .bot)

theorem off_has_halt : ∃ w, BridgeHalt seatOff w := ⟨fun _ => .bot, fun _ => rfl, fun _ _ => rfl⟩

theorem halt_does_not_entail_RH : ¬ (∀ X : Seat, (∃ w, BridgeHalt X w) → RH X) :=

  fun h => off_notRH (h seatOff off_has_halt)

inductive Verdict | sealTrue | sealFalse | halt deriving DecidableEq, Repr

structure Record where

  witnessed  : Bool

  documented : Bool

  value      : Tri

deriving DecidableEq, Repr

def read (r : Record) : Verdict :=

  match r.witnessed, r.documented, r.value with

  | true, true, .tt => .sealTrue

  | true, true, .ff => .sealFalse

  | _, _, _         => .halt

def haltedBit : Record := ⟨true, true, .bot⟩

theorem direction_is_the_difference :

    read { haltedBit with value := .tt } = .sealTrue ∧

    read { haltedBit with value := .ff } = .sealFalse ∧ read haltedBit = .halt := ⟨rfl, rfl, rfl⟩

structure Mark (L : Type) where

  locus    : L

  examined : True

structure Elaborated (L : Type) where

  locus : L

  value : Tri

def rhLocus : String := "APEX-PSP-RH-MASTER-01"

theorem one_code_two_sides {L : Type} (x : L) (m₁ m₂ : Mark L)

    (h₁ : m₁.locus = x) (h₂ : m₂.locus = x) : m₁ = m₂ := by cases m₁; cases m₂; simp_all

theorem truth_silent {L : Type} (rd : Mark L → Verdict) (x : L) (m : Mark L)

    (hm : m.locus = x) : rd m = rd ⟨x, trivial⟩ := by cases m; simp_all

def enter {L : Type} (e : Elaborated L) : Verdict :=

  match e.value with | .tt => .sealTrue | .ff => .sealFalse | .bot => .halt

theorem elaboration_is_trap {L : Type} (e : Elaborated L) :

    enter e = .sealTrue ∨ enter e = .sealFalse ∨ enter e = .halt := by

  unfold enter; cases e.value <;> simp

/-! ## PART E · THE ARRIVAL, WHOLE -/

structure Arr (X : Seat) where

  Q          : Type

  bridgeOdd  : ∀ a : ExecFrame Q, ran (flip a) = !ran a

  anchor     : ExecFrame Q → X.S

  cont       : ∀ a, anchor (flip a) = X.τ (anchor a)

  cover      : ∀ s, X.Z s → ∃ a, anchor a = s

  w          : X.S → Tri

  wOdd       : ∀ s, w (X.τ s) = neg3 (w s)

  halt       : ∀ s, X.Z s → w s = .bot

  seat       : Mark String

  seatAt     : seat.locus = rhLocus

  witnessed  : True

  documented : True

def arrOn : Arr seatOn :=

  { Q := Unit, bridgeOdd := fun _ => rfl, anchor := fun _ => (), cont := fun _ => rfl,

    cover := fun _ _ => ⟨(true, ()), rfl⟩, w := fun _ => .bot, wOdd := fun _ => rfl,

    halt := fun _ _ => rfl, seat := ⟨_, trivial⟩, seatAt := rfl,

    witnessed := trivial, documented := trivial }

def arrOff : Arr seatOff :=

  { Q := Unit, bridgeOdd := fun _ => rfl, anchor := fun a => a.1, cont := fun _ => rfl,

    cover := fun s _ => ⟨(s, ()), rfl⟩, w := fun _ => .bot, wOdd := fun _ => rfl,

    halt := fun _ _ => rfl, seat := ⟨_, trivial⟩, seatAt := rfl,

    witnessed := trivial, documented := trivial }

theorem arrival_does_not_entail_RH : ¬ (∀ X : Seat, Arr X → RH X) :=

  fun h => off_notRH (h seatOff arrOff)

theorem arrival_consistent_with_RH : ∃ X : Seat, Nonempty (Arr X) ∧ RH X :=

  ⟨seatOn, ⟨arrOn⟩, on_RH⟩

/-! ## PART F · THE RECURSIONS AND THE MIRROR CHAIN -/

def Closes (P : Prop) : Prop := ¬P → P

/-- The RH → RH self-witness in RA's Omega shape. -/

def RecOmega (X : Seat) : Prop := Closes (RH X)

theorem omega_blocks_offseat : ¬ RecOmega seatOff := fun h => off_notRH (h off_notRH)

theorem omega_of_RH (X : Seat) (h : RH X) : RecOmega X := fun _ => h

theorem omega_gives_nn (X : Seat) (h : RecOmega X) : ¬¬ RH X := fun n => n (h n)

/-- The self-witness is RH restated: an equivalence, never a derivation. -/

theorem omega_iff_RH (X : Seat) : RecOmega X ↔ RH X :=

  ⟨fun h => Classical.byContradiction (fun n => n (h n)), omega_of_RH X⟩

/-- RA's reflex: physics supplies `utter`, the denial of actuation being an actuation. -/

theorem RA_reflex_shape (Act : Prop) (utter : ¬Act → Act) : Act :=

  Classical.byContradiction (fun n => n (utter n))

def Mirror (P Q : Prop) : Prop := Closes P → Closes Q

theorem mirror_of_iff (P Q : Prop) (h : P ↔ Q) : Mirror P Q :=

  fun c nq => h.mp (c (fun p => nq (h.mp p)))

def RAin (X : Seat) : Prop := Nonempty X.S

theorem RA_on  : RAin seatOn  := ⟨()⟩

theorem RA_off : RAin seatOff := ⟨true⟩

theorem RA_closes_both (X : Seat) (h : RAin X) : Closes (RAin X) := fun _ => h

theorem no_uniform_mirror : ¬ (∀ X : Seat, Mirror (RAin X) (RH X)) := by

  intro m

  exact off_notRH (m seatOff (RA_closes_both seatOff RA_off) off_notRH)

/-- RA → RAM → RH: no intermediate register rescues the chain. -/

theorem no_chain (RAM : Seat → Prop)

    (h1 : ∀ X, Mirror (RAin X) (RAM X)) (h2 : ∀ X, Mirror (RAM X) (RH X)) : False :=

  no_uniform_mirror (fun X c => h2 X (h1 X c))

/-! ## PART G · THE SHAPE, EXACT (half-units: h = 2·Re s, so h = 1 is the critical line) -/

abbrev Plane := Int × Int

def τ (p : Plane) : Plane := (2 - p.1, p.2)

def crit (p : Plane) : Prop := p.1 = 1

def δ (p : Plane) : Int := p.1 - 1

def ht (p : Plane) : Int := p.2

theorem pe {a b c d : Int} : ((a, b) : Plane) = (c, d) ↔ a = c ∧ b = d :=

  ⟨fun e => ⟨congrArg Prod.fst e, congrArg Prod.snd e⟩,

   fun ⟨e1, e2⟩ => by subst e1; subst e2; rfl⟩

theorem τ_involution (p : Plane) : τ (τ p) = p := by

  obtain ⟨h, t⟩ := p; show (2 - (2 - h), t) = (h, t); rw [pe]; omega

theorem fix_is_crit (p : Plane) : τ p = p ↔ crit p := by

  obtain ⟨h, t⟩ := p; show (2 - h, t) = (h, t) ↔ h = 1; rw [pe]; omega

theorem δ_odd (p : Plane) : δ (τ p) = - δ p := by

  obtain ⟨h, t⟩ := p; show (2 - h) - 1 = -(h - 1); omega

theorem ht_even (p : Plane) : ht (τ p) = ht p := rfl

theorem crit_iff_δ_zero (p : Plane) : crit p ↔ δ p = 0 := by show p.1 = 1 ↔ p.1 - 1 = 0; omega

def Symmetric (Z : Plane → Prop) : Prop := ∀ p, Z p → Z (τ p)

def RHp (Z : Plane → Prop) : Prop := ∀ p, Z p → crit p

/-- The plane with the functional-equation fold IS a seat; RH on it is RHp. -/

def planeSeat (Z : Plane → Prop) (hZ : Symmetric Z) : Seat := ⟨Plane, τ, τ_involution, Z, hZ⟩

theorem RH_planeSeat (Z : Plane → Prop) (hZ : Symmetric Z) : RH (planeSeat Z hZ) ↔ RHp Z := by

  constructor <;> intro h p hz

  · exact (fix_is_crit p).mp (h p hz)

  · exact (fix_is_crit p).mpr (h p hz)

/-- The Davenport–Heilbronn shape: symmetric, off the line. -/

def Zdh (p : Plane) : Prop := (p.1 = 0 ∨ p.1 = 2) ∧ p.2 = 171

theorem Zdh_symmetric : Symmetric Zdh := by

  intro p hp; obtain ⟨h, t⟩ := p; obtain ⟨hh, ht⟩ := hp

  show (2 - h = 0 ∨ 2 - h = 2) ∧ t = 171; omega

theorem Zdh_not_RH : ¬ RHp Zdh := fun h => by

  have := h (0, 171) ⟨Or.inl rfl, rfl⟩; exact absurd this (by simp [crit])

theorem symmetry_insufficient : ∃ Z, Symmetric Z ∧ ¬ RHp Z := ⟨Zdh, Zdh_symmetric, Zdh_not_RH⟩

def WhollyOdd (Z : Plane → Prop) (w : Plane → Bool) : Prop := ∀ p, Z p → w (τ p) = !w p

theorem no_odd_at_fixed (Z : Plane → Prop) (w : Plane → Bool) (hw : WhollyOdd Z w)

    (p : Plane) (hz : Z p) (hc : crit p) : False := by

  have h := hw p hz

  rw [(fix_is_crit p).mpr hc] at h

  cases w p <;> simp at h

theorem witness_space_empty_of_line_zero (Z : Plane → Prop) (p : Plane) (hz : Z p) (hc : crit p) :

    ¬ ∃ w, WhollyOdd Z w := fun ⟨w, hw⟩ => no_odd_at_fixed Z w hw p hz hc

def sgn (p : Plane) : Bool := decide (0 < δ p)

theorem sgn_odd_off (Z : Plane → Prop) (hoff : ∀ p, Z p → ¬ crit p) : WhollyOdd Z sgn := by

  intro p hz

  have hne : δ p ≠ 0 := fun h => hoff p hz ((crit_iff_δ_zero p).mpr h)

  unfold sgn; rw [δ_odd]

  by_cases hpos : 0 < δ p

  · have hn : ¬ (0 < -δ p) := by omega

    simp [hpos, hn]

  · have hn : 0 < -δ p := by omega

    simp [hpos, hn]

def calib (w : Plane → Bool) (p : Plane) : Bool := xor (w p) (sgn p)

theorem calib_even (Z : Plane → Prop) (w : Plane → Bool) (hw : WhollyOdd Z w)

    (hoff : ∀ p, Z p → ¬ crit p) (p : Plane) (hz : Z p) : calib w (τ p) = calib w p := by

  unfold calib; rw [hw p hz, sgn_odd_off Z hoff p hz]; cases w p <;> cases sgn p <;> rfl

theorem odd_from_calib (w : Plane → Bool) (p : Plane) : xor (sgn p) (calib w p) = w p := by

  unfold calib; cases w p <;> cases sgn p <;> rfl

theorem height_read_blind (g : Int → Bool) (p : Plane) : g (ht (τ p)) = g (ht p) := rfl

theorem no_height_readout_of_sgn (p : Plane) (hoff : ¬ crit p) :

    ¬ ∃ g : Int → Bool, ∀ q, (q = p ∨ q = τ p) → g (ht q) = sgn q := by

  intro ⟨g, hg⟩

  have h1 := hg p (Or.inl rfl)

  have h2 := hg (τ p) (Or.inr rfl)

  rw [height_read_blind g p, h1] at h2

  have hs := sgn_odd_off (fun q => q = p) (fun _ hq => hq ▸ hoff) p rfl

  rw [hs] at h2; cases sgn p <;> simp at h2

def τc (c : Int) (p : Plane) : Plane := (2*c - p.1, p.2)

theorem τ_is_τc_one : τ = τc 1 := by

  funext p; obtain ⟨h, t⟩ := p; show (2 - h, t) = (2*1 - h, t); rw [pe]; omega

theorem fix_τc (c : Int) (p : Plane) : τc c p = p ↔ p.1 = c := by

  obtain ⟨h, t⟩ := p; show (2*c - h, t) = (h, t) ↔ h = c; rw [pe]; omega

def shift (k : Int) (p : Plane) : Plane := (p.1 + k, p.2)

theorem mirrors_conjugate (c k : Int) (p : Plane) :

    shift k (τc c (shift (-k) p)) = τc (c + k) p := by

  obtain ⟨h, t⟩ := p; show (2*c - (h + -k) + k, t) = (2*(c + k) - h, t); rw [pe]; omega

theorem two_mirrors_translate (c c' : Int) (p : Plane) :

    τc c' (τc c p) = shift (2*(c' - c)) p := by

  obtain ⟨h, t⟩ := p; show (2*c' - (2*c - h), t) = (h + 2*(c' - c), t); rw [pe]; omega

def SymC (c : Int) (Z : Plane → Prop) : Prop := ∀ p, Z p → Z (τc c p)

def StripM (m : Nat) (p : Plane) : Prop := 0 < p.1 ∧ p.1 < 2 * (m : Int)

def Inv (d : Int) (Z : Plane → Prop) : Prop := ∀ p, Z p → Z (shift d p)

theorem climb (d : Int) (hd : 1 ≤ d) (Z : Plane → Prop) (hI : Inv d Z) (p : Plane) (hz : Z p) :

    ∀ n : Nat, ∃ q, Z q ∧ p.1 + (n : Int) ≤ q.1 := by

  intro n

  induction n with

  | zero => exact ⟨p, hz, by omega⟩

  | succ n ih =>

    obtain ⟨q, hq, hle⟩ := ih

    exact ⟨shift d q, hI q hq, by show p.1 + ((n + 1 : Nat) : Int) ≤ q.1 + d; omega⟩

theorem descend (d : Int) (hd : d ≤ -1) (Z : Plane → Prop) (hI : Inv d Z) (p : Plane) (hz : Z p) :

    ∀ n : Nat, ∃ q, Z q ∧ q.1 ≤ p.1 - (n : Int) := by

  intro n

  induction n with

  | zero => exact ⟨p, hz, by omega⟩

  | succ n ih =>

    obtain ⟨q, hq, hle⟩ := ih

    exact ⟨shift d q, hI q hq, by show q.1 + d ≤ p.1 - ((n + 1 : Nat) : Int); omega⟩

theorem no_translation (m : Nat) (d : Int) (hd : d ≠ 0) (Z : Plane → Prop)

    (hS : ∀ p, Z p → StripM m p) (p : Plane) (hz : Z p) (hI : Inv d Z) : False := by

  have hp := hS p hz

  by_cases hpos : 1 ≤ d

  · obtain ⟨q, hq, hle⟩ := climb d hpos Z hI p hz (2 * m)

    have hq' := hS q hq

    simp only [StripM] at hp hq'

    omega

  · have hneg : d ≤ -1 := by omega

    obtain ⟨q, hq, hle⟩ := descend d hneg Z hI p hz (2 * m)

    have hq' := hS q hq

    simp only [StripM] at hp hq'

    omega

/-- The election: a strip-confined symmetric set admits one mirror address. -/

theorem one_mirror_general (m : Nat) (Z : Plane → Prop) (hS : ∀ p, Z p → StripM m p)

    (p : Plane) (hz : Z p) (c c' : Int) (h1 : SymC c Z) (h2 : SymC c' Z) : c = c' := by

  refine Decidable.byContradiction fun hne => ?_

  refine no_translation m (2 * (c' - c)) (by omega) Z hS p hz ?_

  intro q hq

  rw [← two_mirrors_translate]

  exact h2 _ (h1 q hq)

/-- The functional equation supplies τ = τc 1; the address 1/2 is elected, uniquely. -/

theorem address_elected (m : Nat) (Z : Plane → Prop) (hS : ∀ p, Z p → StripM m p) (p : Plane)

    (hz : Z p) (hFE : Symmetric Z) (c : Int) (hc : SymC c Z) : c = 1 :=

  one_mirror_general m Z hS p hz c 1 hc (by unfold SymC; rw [← τ_is_τc_one]; exact hFE)

abbrev Q4 := Int × Int × Int × Int

def qconj (q : Q4) : Q4 := (q.1, -q.2.1, -q.2.2.1, -q.2.2.2)

def negI  (q : Q4) : Q4 := (-q.1, -q.2.1, -q.2.2.1, -q.2.2.2)

theorem fix_qconj (q : Q4) : qconj q = q ↔ q.2.1 = 0 ∧ q.2.2.1 = 0 ∧ q.2.2.2 = 0 := by

  obtain ⟨r, i, j, k⟩ := q

  show (r, -i, -j, -k) = (r, i, j, k) ↔ i = 0 ∧ j = 0 ∧ k = 0

  constructor

  · intro e

    have e1 := congrArg (fun q : Q4 => q.2.1) e

    have e2 := congrArg (fun q : Q4 => q.2.2.1) e

    have e3 := congrArg (fun q : Q4 => q.2.2.2) e

    simp at e1 e2 e3; omega

  · rintro ⟨rfl, rfl, rfl⟩; rfl

theorem fix_negI (q : Q4) : negI q = q ↔ q = (0, 0, 0, 0) := by

  obtain ⟨r, i, j, k⟩ := q

  show (-r, -i, -j, -k) = (r, i, j, k) ↔ (r, i, j, k) = (0, 0, 0, 0)

  constructor

  · intro e

    have e0 := congrArg (fun q : Q4 => q.1) e

    have e1 := congrArg (fun q : Q4 => q.2.1) e

    have e2 := congrArg (fun q : Q4 => q.2.2.1) e

    have e3 := congrArg (fun q : Q4 => q.2.2.2) e

    simp at e0 e1 e2 e3

    have : r = 0 := by omega

    have : i = 0 := by omega

    have : j = 0 := by omega

    have : k = 0 := by omega

    subst_vars; rfl

  · intro e; injection e with e0 e; injection e with e1 e; injection e with e2 e3

    subst e0 e1 e2 e3; rfl

def groundDim (e : List Int) : Nat := (e.filter (· = 1)).length

inductive Branch | xi | o deriving DecidableEq, Repr

def route : Nat → Option Branch | 1 => some .xi | 0 => some .o | _ => none

theorem router : groundDim [1, -1, -1, -1] = 1 ∧ groundDim [-1, -1, -1, -1] = 0 ∧

    route (groundDim [1, -1, -1, -1]) = some .xi ∧ route (groundDim [-1, -1, -1, -1]) = some .o := by

  decide

/-! ## PART H · FINITE CENSUSES BY `decide` (cross-receipted against the Fortran twins) -/

def gridP : List Plane := (List.range 9).flatMap fun (a : Nat) => (List.range 7).map fun (b : Nat) =>

  (Int.ofNat a - 3, Int.ofNat b - 3)

def gridQ : List Q4 := (List.range 5).flatMap fun (a : Nat) => (List.range 5).flatMap fun (b : Nat) =>

  (List.range 5).flatMap fun (c : Nat) => (List.range 5).map fun (d : Nat) =>

  (Int.ofNat a - 2, Int.ofNat b - 2, Int.ofNat c - 2, Int.ofNat d - 2)

theorem census_plane : (gridP.filter fun p => decide (τ p = p)).length = 7 := by decide

theorem census_mirror_sweep : ((List.range 9).map fun (c : Nat) =>

    (gridP.filter fun p => decide (τc (Int.ofNat c - 3) p = p)).length) = List.replicate 9 7 := by decide

theorem census_qconj : (gridQ.filter fun q => decide (qconj q = q)).length = 5 := by decide

theorem census_negI  : (gridQ.filter fun q => decide (negI q = q)).length = 1 := by decide

def orbitDH : List Plane := [(0, 171), (2, 171)]

def orbitPlusLine : List Plane := [(0, 171), (2, 171), (1, 14)]

def oddOn (pts : List Plane) (w : Plane → Bool) : Bool := pts.all fun p => w (τ p) == !w p

def witnessCount (pts : List Plane) : Nat :=

  ((List.range (2 ^ pts.length)).filter fun n =>

    oddOn pts fun p => match pts.idxOf? p with | some i => n.testBit i | none => false).length

theorem census_witness : witnessCount orbitDH = 2 ∧ witnessCount orbitPlusLine = 0 := by decide

/-! ## PART I · THE ARRIVAL ON ζ'S OWN STAGE, WHERE RH FAILS -/

/-- The whole arrival, built on the plane with the functional-equation fold and the DH-shaped zero set. -/

def arrPlaneDH : Arr (planeSeat Zdh Zdh_symmetric) :=

  { Q := Unit,

    bridgeOdd := fun _ => rfl,

    anchor := fun a => (if a.1 then 2 else 0, 171),

    cont := fun a => by obtain ⟨b, _⟩ := a; cases b <;> rfl,

    cover := fun s hs => by

      obtain ⟨h, t⟩ := s; obtain ⟨hh, ht⟩ := hs; subst ht

      rcases hh with h0 | h2

      · exact ⟨(false, ()), by subst h0; rfl⟩

      · exact ⟨(true, ()), by subst h2; rfl⟩,

    w := fun _ => .bot, wOdd := fun _ => rfl, halt := fun _ _ => rfl,

    seat := ⟨_, trivial⟩, seatAt := rfl, witnessed := trivial, documented := trivial }

theorem plane_arrival_does_not_entail_RH :

    ¬ (∀ (Z : Plane → Prop) (hZ : Symmetric Z), Arr (planeSeat Z hZ) → RHp Z) :=

  fun h => Zdh_not_RH (h Zdh Zdh_symmetric arrPlaneDH)

/-- The RH→RH self-witness on the plane is RHp restated. -/

theorem self_witness_is_RH_restated (Z : Plane → Prop) (hZ : Symmetric Z) :

    RecOmega (planeSeat Z hZ) ↔ RHp Z :=

  (omega_iff_RH _).trans (RH_planeSeat Z hZ)

/-! ## PART J · THE OBLIGATION, STATED AND NOT DISCHARGED

`RH_reflex Z` is the type a proof of RH on the zero set `Z` must inhabit (equivalently `RHp Z`).

For ζ's actual zero set it is not inhabited here. On the DH shape it is refuted. -/

def RH_reflex (Z : Plane → Prop) : Prop := ¬ RHp Z → RHp Z

theorem reflex_refuted_on_DH : ¬ RH_reflex Zdh := fun h => Zdh_not_RH (h Zdh_not_RH)

theorem reflex_iff_RH (Z : Plane → Prop) : RH_reflex Z ↔ RHp Z :=

  ⟨fun h => Classical.byContradiction (fun n => n (h n)), fun h _ => h⟩

/-! ## PART K · THE CONE -/

theorem cone : True :=

  let _ := @wall; let _ := @supply_refutes_RH; let _ := @self_on_seat_is_bot

  let _ := @halt_does_not_entail_RH; let _ := @direction_is_the_difference

  let _ := @one_code_two_sides; let _ := @truth_silent; let _ := @elaboration_is_trap

  let _ := @arrival_does_not_entail_RH; let _ := @arrival_consistent_with_RH

  let _ := @omega_blocks_offseat; let _ := @omega_iff_RH; let _ := @no_uniform_mirror

  let _ := @no_chain; let _ := @fix_is_crit; let _ := @δ_odd; let _ := @symmetry_insufficient

  let _ := @no_odd_at_fixed; let _ := @witness_space_empty_of_line_zero; let _ := @sgn_odd_off

  let _ := @calib_even; let _ := @no_height_readout_of_sgn; let _ := @mirrors_conjugate

  let _ := @two_mirrors_translate; let _ := @one_mirror_general; let _ := @address_elected

  let _ := @fix_qconj; let _ := @fix_negI; let _ := @router; let _ := @census_plane

  let _ := @census_mirror_sweep; let _ := @census_qconj; let _ := @census_negI

  let _ := @census_witness; let _ := @plane_arrival_does_not_entail_RH

  let _ := @self_witness_is_RH_restated; let _ := @reflex_refuted_on_DH; let _ := @reflex_iff_RH

  trivial

end RHBridge

/-! ## PART L · THE CONES, PINNED. A change to any cone below is a compile error. -/

/-- info: 'RHBridge.cone' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.cone

/-- info: 'RHBridge.arrival_does_not_entail_RH' does not depend on any axioms -/

#guard_msgs in #print axioms RHBridge.arrival_does_not_entail_RH

/-- info: 'RHBridge.plane_arrival_does_not_entail_RH' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.plane_arrival_does_not_entail_RH

/-- info: 'RHBridge.no_chain' does not depend on any axioms -/

#guard_msgs in #print axioms RHBridge.no_chain

/-- info: 'RHBridge.no_uniform_mirror' does not depend on any axioms -/

#guard_msgs in #print axioms RHBridge.no_uniform_mirror

/-- info: 'RHBridge.omega_blocks_offseat' does not depend on any axioms -/

#guard_msgs in #print axioms RHBridge.omega_blocks_offseat

/-- info: 'RHBridge.wall' depends on axioms: [propext] -/

#guard_msgs in #print axioms RHBridge.wall

/-- info: 'RHBridge.fix_is_crit' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.fix_is_crit

/-- info: 'RHBridge.one_mirror_general' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.one_mirror_general

/-- info: 'RHBridge.address_elected' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.address_elected

/-- info: 'RHBridge.witness_space_empty_of_line_zero' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.witness_space_empty_of_line_zero

/-- info: 'RHBridge.census_witness' depends on axioms: [propext] -/

#guard_msgs in #print axioms RHBridge.census_witness

/-- info: 'RHBridge.self_witness_is_RH_restated' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.self_witness_is_RH_restated

/-- info: 'RHBridge.reflex_iff_RH' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in #print axioms RHBridge.reflex_iff_RH

/-- info: 'RHBridge.reflex_refuted_on_DH' depends on axioms: [propext] -/

#guard_msgs in #print axioms RHBridge.reflex_refuted_on_DH