/-! TRISDUCTION · THE RH SHAPE, WITH THE BRIDGE · v1.0.0 · 2026-09-16

 /-! TRISDUCTION · THE RH SHAPE, WITH THE BRIDGE · v1.0.0 · 2026-09-16

    The geometric face of APEX-PSP-RH-MASTER-01, [⟀ T], built exact and kernel-checked,

    with the Bridge's torsor added on the fold. Core Lean 4.19.0, no Mathlib, no sorry.

    The stage is the deletion-tested one (codex line 4918): a plane with an involution,

    the even coordinate along the mirror, the odd coordinate across it. Half-units keep

    the address 1/2 exact: h = 2·Re(s), so h = 1 is the critical line. ΔM = 0. -/

set_option maxRecDepth 4000

namespace Shape

/-! ## 0 · THE STAGE -/

abbrev Plane := Int × Int

/-- The functional-equation fold τ(s) = 1 − s̄, in half-units: h ↦ 2 − h, t ↦ t. -/

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

/-- The critical line Re(s) = 1/2. -/

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

/-- The signed offset δ = Re(s) − 1/2 (half-units): the odd coordinate. -/

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

/-- The height: the even coordinate. -/

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

/-- Pair equality, componentwise (the kernel's own `Prod` ext). -/

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

/-- S1. Fix(τ) is exactly the critical line. -/

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

/-- S2. The offset is odd under the fold, the height is even. -/

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

/-! ## I · THE ZERO SET, THE FUNCTIONAL EQUATION, AND RH AS A SHAPE SENTENCE -/

/-- The functional equation donates one law: the zero set is τ-invariant. -/

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

/-- RH, deletion-tested: every zero on the fold. -/

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

theorem RH_iff_offset_zero (Z : Plane → Prop) : RH Z ↔ ∀ p, Z p → δ p = 0 :=

  ⟨fun h p hz => (crit_iff_δ_zero p).mp (h p hz), fun h p hz => (crit_iff_δ_zero p).mpr (h p hz)⟩

/-- S3. Symmetry alone does not force the line: a τ-symmetric set with an off-line orbit.

    (The Davenport–Heilbronn shape; the analytic witness is in the numeric receipt.) -/

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 : ¬ RH Zdh := fun h => by

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

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

/-! ## II · THE BRIDGE ON THE SHAPE: odd witnesses, the fold, and the torsor -/

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

/-- S4 (the wall on the fold). Where a zero is fixed, no wholly odd witness exists. -/

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

/-- Corollary: one zero on the line empties the Bridge's witness space on the whole set. -/

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

/-- S5 (the canonical odd witness). Off the line, the sign of the offset is wholly odd. -/

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]

/-- S6 (the price, on the fold). Every odd witness on an off-line set is sgn XOR an even calibration:

    exactly one bit per orbit, the calibration constant along each orbit. -/

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

/-- S7 (the even read is blind to the side). Any reading through the height alone

    cannot separate an off-line zero from its mirror image. -/

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

/-! ## III · THE ELECTED ADDRESS: the plane ranks every mirror alike, the strip elects one -/

/-- A mirror at address c (half-units): h ↦ 2c − h. -/

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)

/-- S8. Translation conjugates every mirror to every other: topologically one object. -/

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

/-- S9. Two mirrors compose to a translation. -/

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

/-- The critical strip 0 < Re(s) < 1, where every nontrivial zero lives (cited). -/

def Strip (p : Plane) : Prop := 0 < p.1 ∧ p.1 < 2

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

/-- S10 (the election). A nonempty zero set confined to the strip admits at most one mirror address.

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

theorem one_mirror (Z : Plane → Prop) (hS : ∀ p, Z p → Strip p) (p : Plane) (hz : Z p)

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

  have hq := hS _ (h2 _ (h1 p hz))

  rw [two_mirrors_translate] at hq

  have hp := hS p hz

  obtain ⟨hh, tt⟩ := p

  simp only [Strip, shift] at hq hp

  omega

/-- S10′ (the election, general). Any unit, any strip width m: a nonempty zero set confined to

    0 < h < 2m admits at most one mirror address. A second mirror would force invariance under a

    nonzero horizontal translation, which a bounded strip cannot carry. -/

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

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)

theorem address_elected (Z : Plane → Prop) (hS : ∀ p, Z p → Strip p) (p : Plane) (hz : Z p)

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

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

/-! ## IV · THE GROUND DIMENSION: quaternionic conjugation against the diagonal -/

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)

/-- S11. Fix(σ) is the scalar line ℝ: a Ground of dimension one. -/

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

/-- S12. Fix(−I) is the origin alone: Ground dimension zero, the sibling's terrain. -/

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 sigmaEig : List Int := [1, -1, -1, -1]

def diagEig  : List Int := [-1, -1, -1, -1]

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

/-- S13. The router bit, computed: σ routes to Ξ, the diagonal to Ø. -/

theorem router : groundDim sigmaEig = 1 ∧ groundDim diagEig = 0 ∧

    route (groundDim sigmaEig) = some .xi ∧ route (groundDim diagEig) = some .o := by decide

/-! ## V · FINITE CENSUSES BY `decide`, cross-receipted against the Fortran twin -/

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)                                       -- h ∈ [−3,5], t ∈ [−3,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)         -- coords ∈ [−2,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

/-- The Bridge's witness space, counted on a two-point orbit and on the orbit plus one line point. -/

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

/-! ## VI · THE CONE -/

theorem shapeCone : True :=

  let _ := @τ_involution; let _ := @fix_is_crit; let _ := @δ_odd; let _ := @ht_even

  let _ := @crit_iff_δ_zero; let _ := @RH_iff_offset_zero; let _ := @symmetry_insufficient

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

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

  let _ := @τ_is_τc_one; let _ := @fix_τc; let _ := @mirrors_conjugate

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

  let _ := @no_translation; 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

  trivial

end Shape

#print axioms Shape.shapeCone

#print axioms Shape.fix_is_crit

#print axioms Shape.one_mirror

#print axioms Shape.no_odd_at_fixed

#print axioms Shape.address_elected

#print axioms Shape.one_mirror_general

! TRISDUCTION · THE RH SHAPE, WITH THE BRIDGE · FORTRAN TWIN v1.0.0 · 2026-09-16

! Kinetic twin of the Lean shape file. Every integer here is cross-receipted against a Lean `decide`.

! BUILD (sealed): gfortran -std=f2018 -O2 -fno-fast-math -ffp-contract=off

program rh_shape_twin

  implicit none

  integer, parameter :: dp = selected_real_kind(15, 307)

  integer :: checks = 0, fails = 0

  integer :: h, t, c, k, cp, nfix, ninv, nodd, ncons, ntr, nel, a, b, cc, d, nq, nd, npos, nn, bits, i

  integer :: gdim_s, gdim_d, ev_s(4), ev_d(4), sweep(9)

  logical :: okw

  real(dp) :: r1, r2, m(3,3), mr(3,3), gm(3,3), gr(3,3), lam, lamr

  write(*,'(A)') repeat('=',72)

  write(*,'(A)') ' RH SHAPE / BRIDGE · FORTRAN TWIN · executed'

  write(*,'(A)') repeat('=',72)

  ! S1 · the fold on the grid h in [-3,5], t in [-3,3] (half-units; h = 1 is Re = 1/2)

  nfix = 0; ninv = 0; nodd = 0

  do h = -3, 5

     do t = -3, 3

        if (2 - h == h) nfix = nfix + 1                              ! fixed points

        if (2 - (2 - h) == h) ninv = ninv + 1                        ! involution

        if ((2 - h) - 1 == -(h - 1) .and. t == t) nodd = nodd + 1    ! offset odd, height even

     end do

  end do

  write(*,'(A,I0,A,I0,A,I0,A)') ' S1 fold: fixed points ', nfix, ' | involutive ', ninv, &

       '/63 | offset-odd height-even ', nodd, '/63'

  call check('S1 Fix(tau) = the critical line, 7 grid points (Lean census_plane = 7)', nfix == 7)

  call check('S1 tau is an involution on all 63 points', ninv == 63)

  call check('S1 the offset is odd and the height even on all 63 points', nodd == 63)

  ! S2 · the mirror sweep c in [-3,5]: the plane ranks every mirror alike; conjugacy; two mirrors = translation

  ncons = 0; ntr = 0

  do c = -3, 5

     sweep(c+4) = 0

     do h = -3, 5

        do t = -3, 3

           if (2*c - h == h) sweep(c+4) = sweep(c+4) + 1

           do k = -2, 2

              if (2*c - (h + (-k)) + k == 2*(c + k) - h) ncons = ncons + 1     ! shift∘tau_c∘shift^-1 = tau_{c+k}

           end do

           do cp = -3, 5

              if (2*cp - (2*c - h) == h + 2*(cp - c)) ntr = ntr + 1           ! tau_c' ∘ tau_c = translation 2(c'-c)

           end do

        end do

     end do

  end do

  write(*,'(A,9I2,A,I0,A,I0,A)') ' S2 mirror sweep fixed counts', sweep, ' | conjugacy ids ', ncons, &

       '/2835 | translation ids ', ntr, '/5103'

  call check('S2 every mirror fixes 7 grid points (Lean census_mirror_sweep = replicate 9 7)', all(sweep == 7))

  call check('S2 translation conjugates every mirror to every other, exactly', ncons == 9*63*5)

  call check('S2 two mirrors compose to a translation, exactly', ntr == 9*63*9)

  ! S3 · the election, in tenth-units (h = 10 Re s, strip 0 < h < 10): an off-line symmetric pair admits ONE mirror

  nel = 0

  do cp = -30, 30

     if (2*cp - 3 == 7 .and. 2*cp - 7 == 3) nel = nel + 1              ! Z = {Re = 0.3, Re = 0.7} at one height

  end do

  write(*,'(A,I0,A)') ' S3 election: mirrors leaving {0.3, 0.7} invariant = ', nel, ' (address 0.5 alone)'

  call check('S3 exactly one mirror address, 1/2, for a strip-confined symmetric set', nel == 1)

  ! S4 · the Ground dimension: sigma = quaternionic conjugation against the diagonal -I

  nq = 0; nd = 0

  do a = -2, 2; do b = -2, 2; do cc = -2, 2; do d = -2, 2

     if (a == a .and. -b == b .and. -cc == cc .and. -d == d) nq = nq + 1

     if (-a == a .and. -b == b .and. -cc == cc .and. -d == d) nd = nd + 1

  end do; end do; end do; end do

  ev_s = [1, -1, -1, -1]; ev_d = [-1, -1, -1, -1]

  gdim_s = count(ev_s == 1); gdim_d = count(ev_d == 1)

  write(*,'(A,I0,A,I0,A,I0,A,I0)') ' S4 Fix(sigma) grid points ', nq, ' (scalar line) | Fix(-I) ', nd, &

       ' (origin) | Ground dim ', gdim_s, ' vs ', gdim_d

  call check('S4 Fix(sigma) = R on the grid: 5 points (Lean census_qconj = 5)', nq == 5)

  call check('S4 Fix(-I) = origin: 1 point (Lean census_negI = 1)', nd == 1)

  call check('S4 router bit: sigma Ground dim 1 -> Xi, diagonal Ground dim 0 -> O', gdim_s == 1 .and. gdim_d == 0)

  ! S5 · the Bridge's witness space, enumerated: the DH orbit {0,2}x{171} and the orbit plus one line point

  npos = 0

  do bits = 0, 3                        ! two points, w(p0)=bit0, w(p1)=bit1, tau swaps them

     if (ibits(bits,1,1) == 1 - ibits(bits,0,1) .and. ibits(bits,0,1) == 1 - ibits(bits,1,1)) npos = npos + 1

  end do

  nn = 0

  do bits = 0, 7                        ! plus the fixed point (1,14): needs w = 1 - w, impossible

     okw = ibits(bits,1,1) == 1 - ibits(bits,0,1) .and. ibits(bits,0,1) == 1 - ibits(bits,1,1) &

           .and. ibits(bits,2,1) == 1 - ibits(bits,2,1)

     if (okw) nn = nn + 1

  end do

  write(*,'(A,I0,A,I0)') ' S5 |D_tau| on the off-line orbit ', npos, ' | with one line zero added ', nn

  call check('S5 one free orbit carries exactly one bit: two witnesses (Lean census_witness)', npos == 2)

  call check('S5 one fixed zero empties the witness space (Lean witness_space_empty)', nn == 0)

  ! S6 · the Return lands on Fix(sigma): i*j*k = -1 is a scalar

  call check('S6 the Return i*j*k = -1 lies on the scalar line Fix(sigma)', &

       all(qmul(qmul([0._dp,1._dp,0._dp,0._dp],[0._dp,0._dp,1._dp,0._dp]),[0._dp,0._dp,0._dp,1._dp]) &

           == [-1._dp,0._dp,0._dp,0._dp]))

  ! S7 · the DH pair: an off-line zero and its mirror image, reflected exactly about 1/2 (constants from the mpmath receipt)

  r1 = 0.8085171824566374_dp; r2 = 0.1914828175433626_dp

  write(*,'(A,ES9.2,A,ES9.2)') ' S7 DH pair: |1 - r1 - r2| = ', abs(1._dp - r1 - r2), &

       ' | offsets sum ', (r1-0.5_dp)+(r2-0.5_dp)

  call check('S7 the DH pair is a free tau-orbit about 1/2 to double precision', &

       abs(1._dp - r1 - r2) <= 4.e-16_dp)

  ! S8 · the Number is blind to the side: the lock scalar det(R) is bit-identical under the fold, lambda flips

  m = reshape([0.3_dp,0.5_dp,-0.6_dp, 0.7_dp,-0.4_dp,0.1_dp, -0.2_dp,0.8_dp,0.9_dp],[3,3])

  mr = m; mr(:,3) = -mr(:,3)

  gm = matmul(m, transpose(m)); gr = matmul(mr, transpose(mr))

  lam = det3(m); lamr = det3(mr)

  write(*,'(A,ES9.2,A,F10.6,A,F10.6)') ' S8 max|R - R(reflected)| = ', maxval(abs(gm-gr)), &

       ' | lambda ', lam, ' -> ', lamr

  call check('S8 the even read is bit-identical under the fold, the odd bit flips exactly', &

       maxval(abs(gm-gr)) == 0._dp .and. lamr == -lam)

  write(*,'(A)') repeat('=',72)

  write(*,'(A,I0,A,I0,A)') ' BATTERY: ', checks, ' checks, ', fails, ' failures'

  write(*,'(A,I0,A,I0,A)') ' BATTERY-JSON: {"checks":', checks, ',"failures":', fails, ',"mode":"sealed"}'

  if (fails > 0) error stop 1

  write(*,'(A)') ' SHAPE [seal T]: the line is Fix(tau), the address 1/2 is elected,'

  write(*,'(A)') '   one bit per free orbit, none on the line.'

  write(*,'(A)') ' The load is proven. Delta-M = 0.'

contains

  pure function qmul(a, b) result(c)

    real(dp), intent(in) :: a(4), b(4)

    real(dp) :: c(4)

    c(1) = a(1)*b(1) - a(2)*b(2) - a(3)*b(3) - a(4)*b(4)

    c(2) = a(1)*b(2) + a(2)*b(1) + a(3)*b(4) - a(4)*b(3)

    c(3) = a(1)*b(3) - a(2)*b(4) + a(3)*b(1) + a(4)*b(2)

    c(4) = a(1)*b(4) + a(2)*b(3) - a(3)*b(2) + a(4)*b(1)

  end function qmul

  pure function det3(x) result(dt)

    real(dp), intent(in) :: x(3,3)

    real(dp) :: dt

    dt = x(1,1)*(x(2,2)*x(3,3) - x(2,3)*x(3,2)) - x(1,2)*(x(2,1)*x(3,3) - x(2,3)*x(3,1)) &

       + x(1,3)*(x(2,1)*x(3,2) - x(2,2)*x(3,1))

  end function det3

  subroutine check(name, cond)

    character(*), intent(in) :: name

    logical, intent(in) :: cond

    checks = checks + 1

    if (.not. cond) then

       fails = fails + 1

       write(*,'(A,A)') ' CHECK FAILED: ', name

    end if

  end subroutine check

end program rh_shape_twin

APEX-PSP-RH-SHAPE-BRIDGE-01 · The RH Shape, With the Bridge · v1.0.0 · 

M register · 2026-09-16 · Lean 4.19.0 (core, no Mathlib, no sorry) + gfortran f2018 sealed flags + mpmath 30 dp · ΔM = 0 · W_social = 0 · every figure read from the receipts in this folder.

SCOPE

The geometric face of APEX-PSP-RH-MASTER-01, already [⟀ T] in the master, rebuilt exact on the deletion-tested stage (codex line 4918) and extended by the Bridge's torsor. The string face is not touched: it stays where the master and the Zenodo termination paper (10.5281/zenodo.21900518) leave it.

THE STAGE

A plane in half-units (h = 2·Re s, so h = 1 is the critical line), the fold τ(h, t) = (2 − h, t), the offset δ = h − 1 across the mirror, the height t along it. Mirror addresses in the unit; the general election theorem is proved for any unit and any strip width.

FACES, ALL [⟀ T], KERNEL-CHECKED

#	Statement	Machine form	Twin / receipt
S1	Fix(τ) is exactly the critical line	fix_is_crit	Fortran S1: 7/63 fixed; Lean census_plane = 7
S2	The offset is odd, the height even	δ_odd, ht_even	Fortran S1: 63/63
S3	Symmetry alone does not force the line	symmetry_insufficient (Zdh)	mpmath A2: DH zero 0.8085171824566373855534 + 85.699…i, completed F(s) = F(1−s) to 10⁻³⁰
S4	The wall on the fold: no odd witness where a zero is fixed; one line zero empties the witness space	no_odd_at_fixed, witness_space_empty_of_line_zero	A3: D_τ on 12 ζ-zeros = 0, DH pair = 2, mixed = 0; Fortran S5
S5	Off the line, sign(δ) is the canonical odd witness	sgn_odd_off	mutant SM2 fails without the off-line hypothesis
S6	The price on the fold: every odd witness = sgn ⊕ even calibration, one bit per orbit	calib_even, odd_from_calib	Fortran S5 = 2
S7	The even read is blind to the side	height_read_blind, no_height_readout_of_sgn	Fortran S8: max
S8	Every mirror is conjugate to every other; two mirrors compose to a translation	mirrors_conjugate, two_mirrors_translate	Fortran S2: 2835/2835, 5103/5103; A4 sweep residual 0.0
S9	The election: a strip-confined symmetric set admits one mirror address; the functional equation supplies τ = τc 1, so 1/2 is elected uniquely	one_mirror, one_mirror_general, address_elected	Fortran S3 = 1; A1: ξ(s) = ξ(1−s) to 10⁻³⁰; mutant SM4 fails on an unbounded strip
S10	Ground dimension: Fix(σ) = ℝ (dim 1), Fix(−I) = {0} (dim 0); router Ξ vs Ø	fix_qconj, fix_negI, router	Fortran S4: 5, 1, dims 1 vs 0

External facts consumed, cited and not re-derived: τ is ζ's functional-equation reflection (A1 executes it); every nontrivial zero lies in the strip; at least one zero lies on the line (Hardy 1914; A3 executes the first). Nothing else enters.

WHAT THE BRIDGE ADDS TO THE SHAPE

Before: the line is Fix(σ), the offset is the odd coordinate. Now, kernel-checked: the Bridge's witness space on any zero set is nonempty exactly when the set is entirely off the line, and empty as soon as one zero is on it. Applied to ζ with its first zero, D_τ(Z_ζ) = ∅ by theorem. The one free bit per orbit exists only on a hypothetical off-line orbit, and no even reading (height, |ζ|, N(T)) could ever locate it there (S7). The address 1/2 is not geometric: the plane ranks every mirror alike, and the arithmetic elects one.

FENCES · [X]

• The shape seal read as line-localization: fenced twice in the master already, re-fenced here by symmetry_insufficient.
• D_τ(Z_ζ) = ∅ read as RH: it is implied by one line zero and holds in the mixed world too (A3, third count). It is orientation-blindness made exact, not a verdict on the string.
• Anything here read as touching [Ξ₀]: nothing in this folder decides whether Z_ζ has a free orbit.

RECEIPTS

lean_receipt.log (cone: propext, Classical.choice, Quot.sound; no sorry) · mutant_receipt.log (5/5 match) · fortran_receipt.log (15/15) · analytic_receipt.log · MANIFEST.sha256.