Theme/Extension.lean — FrcCore

1import FrcCore.Ring2import FrcCore.Frame3import FrcCore.Theme.Quadratic45/-!6# FrcCore.Theme.Extension — the quaternion norm and the Lorentzian plane (the extension theme, task LM17)78The quadratic extension `FRC.Extension.Ext p ν` itself is `Theme/Quadratic.lean`, frame-free, and the normaliser that9decides ring identities on the shell is the base's `Ring.lean` (both split off by task LM24, every name unchanged).10This file keeps what needs the frame or the quaternions: conjugation fixes exactly the prime meridian (`fixed_conj`);11the quaternions over the shell, the Hamilton product, conjugation and the norm, and the multiplicativity of the norm12`N(qr) = N(q) N(r)` (1-algebra's Quaternion.lean, names unchanged); and the Lorentzian plane of the shell: the square13classes, the diagonal form `Q_ν = −ν t² + x² + y² + z²`, the boosts `Λ(γ, b)` with `γ² − νb² = 1` (the norm-one elements14of `𝔽_p(√ν)`), their velocities and the counts of the null cone and of the boosts (3-causality's Causality.lean, task15LM20, names unchanged); and the two strata of probability (00:C10, 8 October 2026): the tally line, the conjugate-pair16trace tally and the dial-ensemble Parseval tally in the extension, the engineered-core weights and the framed readout.17No axioms.18-/1920namespace FRC.Extension2122open FRC.Shell2324namespace Ext25variable {p : Nat} [Pos p] {ν : Shell p}2627section frame28variable {κ : Nat} {g : Shell p}2930/-- 20:B9 — the fixed locus of conjugation is the prime meridian: `z̄ = z ⟺ b = 0`. -/31theorem fixed_conj (F : Frame p κ g) (z : Ext p ν) : conj z = z ↔ z.im = 0 := by32  constructor33  · intro h34    exact F.eq_zero_of_eq_neg (im_congr h).symm35  · intro h36    exact ext rfl (show -z.im = z.im by rw [h, Shell.neg_zero])3738end frame3940end Ext4142end FRC.Extension434445namespace FRC46namespace Shell47namespace Frame4849variable {p : Nat} [Pos p]5051/-- A quaternion over the shell. -/52structure Quat (p : Nat) [Pos p] where53  a : Shell p54  b : Shell p55  c : Shell p56  d : Shell p5758/-- The Hamilton product on the shell. -/59def Quat.mul (q r : Quat p) : Quat p :=60  ⟨(q.a * r.a + -(q.b * r.b)) + (-(q.c * r.c) + -(q.d * r.d)),61   (q.a * r.b + q.b * r.a) + (q.c * r.d + -(q.d * r.c)),62   (q.a * r.c + -(q.b * r.d)) + (q.c * r.a + q.d * r.b),63   (q.a * r.d + q.b * r.c) + (-(q.c * r.b) + q.d * r.a)⟩64656667/-! ## Quaternions over the shell: conjugation, norm, cross and dot products, and their expression twins -/6869def Quat.conj (q : Quat p) : Quat p := ⟨q.a, -q.b, -q.c, -q.d⟩70def Quat.nrm (q : Quat p) : Shell p := q.a * q.a + q.b * q.b + (q.c * q.c + q.d * q.d)71def Quat.vec (q : Quat p) : Quat p := ⟨0, q.b, q.c, q.d⟩72def Quat.sc (s : Shell p) : Quat p := ⟨s, 0, 0, 0⟩73def Quat.smul (s : Shell p) (q : Quat p) : Quat p := ⟨s * q.a, s * q.b, s * q.c, s * q.d⟩74def Quat.add (q r : Quat p) : Quat p := ⟨q.a + r.a, q.b + r.b, q.c + r.c, q.d + r.d⟩75def Quat.neg (q : Quat p) : Quat p := ⟨-q.a, -q.b, -q.c, -q.d⟩76def Quat.cross (v x : Quat p) : Quat p := ⟨0, v.c * x.d + -(v.d * x.c), v.d * x.b + -(v.b * x.d), v.b * x.c + -(v.c * x.b)⟩77def Quat.dot (v x : Quat p) : Shell p := v.b * x.b + v.c * x.c + v.d * x.d78/-- Conjugation by `q`, not yet divided by the norm: `x ↦ q x q̄`. -/79def Quat.conjBy (q x : Quat p) : Quat p := Quat.mul (Quat.mul q x) (Quat.conj q)8081theorem Quat.ext4 {q r : Quat p} (ha : q.a = r.a) (hb : q.b = r.b) (hc : q.c = r.c) (hd : q.d = r.d) : q = r :=82  match q, r, ha, hb, hc, hd with83  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl, rfl, rfl, rfl => rfl8485theorem Quat.pure_eq {x : Quat p} (hx : x.a = 0) : x = ⟨0, x.b, x.c, x.d⟩ :=86  match x, hx with87  | ⟨_, _, _, _⟩, rfl => rfl8889structure QR where90  a : RE91  b : RE92  c : RE93  d : RE9495def QR.eval (env : Nat → Shell p) (q : QR) : Quat p := ⟨q.a.eval env, q.b.eval env, q.c.eval env, q.d.eval env⟩96def QR.mul (q r : QR) : QR :=97  ⟨.add (.add (.mul q.a r.a) (.neg (.mul q.b r.b))) (.add (.neg (.mul q.c r.c)) (.neg (.mul q.d r.d))),98   .add (.add (.mul q.a r.b) (.mul q.b r.a)) (.add (.mul q.c r.d) (.neg (.mul q.d r.c))),99   .add (.add (.mul q.a r.c) (.neg (.mul q.b r.d))) (.add (.mul q.c r.a) (.mul q.d r.b)),100   .add (.add (.mul q.a r.d) (.mul q.b r.c)) (.add (.neg (.mul q.c r.b)) (.mul q.d r.a))⟩101def QR.conj (q : QR) : QR := ⟨q.a, .neg q.b, .neg q.c, .neg q.d⟩102def QR.nrm (q : QR) : RE := .add (.add (.mul q.a q.a) (.mul q.b q.b)) (.add (.mul q.c q.c) (.mul q.d q.d))103def QR.vec (q : QR) : QR := ⟨.zero, q.b, q.c, q.d⟩104def QR.sc (s : RE) : QR := ⟨s, .zero, .zero, .zero⟩105def QR.smul (s : RE) (q : QR) : QR := ⟨.mul s q.a, .mul s q.b, .mul s q.c, .mul s q.d⟩106def QR.add (q r : QR) : QR := ⟨.add q.a r.a, .add q.b r.b, .add q.c r.c, .add q.d r.d⟩107def QR.neg (q : QR) : QR := ⟨.neg q.a, .neg q.b, .neg q.c, .neg q.d⟩108def QR.cross (v x : QR) : QR :=109  ⟨.zero, .add (.mul v.c x.d) (.neg (.mul v.d x.c)), .add (.mul v.d x.b) (.neg (.mul v.b x.d)), .add (.mul v.b x.c) (.neg (.mul v.c x.b))⟩110def QR.dot (v x : QR) : RE := .add (.add (.mul v.b x.b) (.mul v.c x.c)) (.mul v.d x.d)111def QR.conjBy (q x : QR) : QR := QR.mul (QR.mul q x) (QR.conj q)112/-- A quaternion of variables `i, i+1, i+2, i+3`; a pure one of variables `i, i+1, i+2`. -/113def QR.v (i : Nat) : QR := ⟨.var i, .var (i + 1), .var (i + 2), .var (i + 3)⟩114def QR.pv (i : Nat) : QR := ⟨.zero, .var i, .var (i + 1), .var (i + 2)⟩115116def QR.check (l r : QR) : Bool := RE.check l.a r.a && RE.check l.b r.b && (RE.check l.c r.c && RE.check l.d r.d)117118theorem QR.sound (env : Nat → Shell p) (l r : QR) (h : QR.check l r = true) : l.eval env = r.eval env :=119  Quat.ext4 (RE.sound env _ _ (and_true_left (and_true_left h))) (RE.sound env _ _ (and_true_right (and_true_left h)))120    (RE.sound env _ _ (and_true_left (and_true_right h))) (RE.sound env _ _ (and_true_right (and_true_right h)))121122123/-- 1:E8, the norm is multiplicative: `N(qr) = N(q) N(r)`. -/124theorem nrm_mul (q r : Quat p) : Quat.nrm (Quat.mul q r) = Quat.nrm q * Quat.nrm r :=125  RE.sound (look [q.a, q.b, q.c, q.d, r.a, r.b, r.c, r.d]) (QR.nrm (QR.mul (QR.v 0) (QR.v 4))) (.mul (QR.nrm (QR.v 0)) (QR.nrm (QR.v 4))) (by decide +kernel)126127end Frame128end Shell129end FRC130131/-! ## The Lorentzian plane of the shell: the square classes, the diagonal form and the boosts (3-causality's132`Causality.lean`, moved by the ledger migration, task LM20, names unchanged) -/133134namespace FRC135namespace Shell136namespace Frame137138variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}139140/-- `x` is a square: `x = y·y` for some residue `y`. -/141def IsSquare (x : Shell p) : Prop := ∃ y : Shell p, y * y = x142143/-- 3:B2 (Thm. nonexistence, first clause) — `c² = ν` makes `ν` a square, so a nonsquare `ν` has no root `c`. -/144theorem no_causal_root {ν : Shell p} (h : ¬IsSquare ν) (c : Shell p) : c * c ≠ ν := fun e => h ⟨c, e⟩145146theorem sq_mul (a b : Shell p) : (a * b) * (a * b) = (a * a) * (b * b) := mul_mul_mul_comm a b a b147148/-- 3:B2 (Thm. nonexistence, the consequence) — `−c²` is a square on every shell: `−c² = (i·c)²` with `i² = −1`;149so with `c ≠ 0` every coefficient of `−c² t² + x² + y² + z²` is a square and the form is Euclidean. -/150theorem neg_sq_is_square (F : Frame p κ g) (c : Shell p) : IsSquare (-(c * c)) :=151  ⟨quarterTurn g κ * c, by rw [sq_mul, F.quarter_turn_sq, neg_one_mul]⟩152153/-- 3:B2 — `−1` itself is a square (`i²`): the paper's hypothesis `p ≡ 1 (mod 4)` in the shell's own terms. -/154theorem neg_one_is_square (F : Frame p κ g) : IsSquare (-1 : Shell p) := ⟨quarterTurn g κ, F.quarter_turn_sq⟩155156/-- 3:B3 (Lemma absorption) — if `a_i = w_i² a_0` for `i = 1, 2, 3` then157`a_0 x_0² + a_1 x_1² + a_2 x_2² + a_3 x_3² = a_0 (x_0² + (w_1 x_1)² + (w_2 x_2)² + (w_3 x_3)²)`: a common square158class is absorbed by the rescaling `x_i ↦ w_i x_i`, with no square root of `a_0` itself required. -/159theorem absorb (a0 a1 a2 a3 w1 w2 w3 x0 x1 x2 x3 : Shell p) (h1 : w1 * w1 * a0 = a1) (h2 : w2 * w2 * a0 = a2)160    (h3 : w3 * w3 * a0 = a3) :161    a0 * (x0 * x0) + a1 * (x1 * x1) + a2 * (x2 * x2) + a3 * (x3 * x3) =162    a0 * (x0 * x0 + (w1 * x1) * (w1 * x1) + (w2 * x2) * (w2 * x2) + (w3 * x3) * (w3 * x3)) := by163  rw [← h1, ← h2, ← h3, sq_mul w1 x1, sq_mul w2 x2, sq_mul w3 x3, left_distrib, left_distrib, left_distrib,164    mul_left_comm a0 (w1 * w1), mul_left_comm a0 (w2 * w2), mul_left_comm a0 (w3 * w3),165    mul_assoc (w1 * w1), mul_assoc (w2 * w2), mul_assoc (w3 * w3)]166167/-! ### The binary form `x² − ν t²`, the norm of `K = F_p(√ν)` -/168169/-- The `(t, x)`-plane form `Q₂(t, x) = x² − ν t²`, the norm `N(x + t√ν)`. -/170def Q2 (ν t x : Shell p) : Shell p := x * x + -(ν * (t * t))171172/-- 3:B5 — the plane `x² − ν t²` is anisotropic when `ν` is a nonsquare: `x² = ν t²` forces `t = x = 0`173(else `ν = (x/t)²`).  This is the Witt kernel of the Lorentzian form, its index one. -/174theorem aniso_tx (F : Frame p κ g) {ν : Shell p} (h : ¬IsSquare ν) {t x : Shell p} (e : x * x = ν * (t * t)) :175    t = 0 ∧ x = 0 := by176  match Shell.instDecidableEq t 0 with177  | .isTrue ht =>178    refine ⟨ht, ?_⟩179    rw [ht, mul_zero, mul_zero] at e180    match F.mul_eq_zero e with181    | .inl hx => exact hx182    | .inr hx => exact hx183  | .isFalse ht =>184    match F.exists_inv ht with185    | ⟨s, hs⟩ =>186      exact absurd ⟨x * s, by187        calc (x * s) * (x * s) = (x * x) * (s * s) := sq_mul x s188          _ = ν * ((t * t) * (s * s)) := by rw [e, mul_assoc]189          _ = ν * ((t * s) * (t * s)) := by rw [sq_mul t s]190          _ = ν := by rw [hs, one_mul, mul_one]⟩ h191192/-- 3:B5 — the `(y, z)`-plane `y² + z²` is hyperbolic on every shell: `(1, i)` is null. -/193theorem null_yz (F : Frame p κ g) : (1 : Shell p) * 1 + quarterTurn g κ * quarterTurn g κ = 0 := by194  rw [F.quarter_turn_sq, one_mul, add_neg]195196/-- 3:B5 — for a square `ν = w²` the `(t, x)`-plane is hyperbolic too: `(1, w)` is null; the form is then197`H ⊥ H`, Witt index two — the Euclidean type. -/198theorem null_tx_of_square (w : Shell p) : Q2 (w * w) 1 w = 0 := by199  unfold Q2; rw [mul_one, mul_one, add_neg]200201/-! ### The boosts -/202203theorem sq_add (u v : Shell p) : (u + v) * (u + v) = u * u + (u * v + u * v) + v * v := by204  rw [right_distrib, left_distrib, left_distrib, mul_comm v u, ← add_assoc, add_assoc (u * u)]205206theorem regroup (P R S T X : Shell p) : P + (X + X) + R + (S + -(X + X) + T) = P + S + T + R := by207  rw [add_add_add_comm, add_assoc P, add_left_comm (X + X), add_neg, add_zero, add_comm R T, ← add_assoc]208209/-- The norm is multiplicative: `N((a + b√ν)(c + d√ν)) = N(a + b√ν) N(c + d√ν)`, i.e.210`(ac + νbd)² − ν(ad + bc)² = (a² − νb²)(c² − νd²)` — the identity behind every boost. -/211theorem norm_mul (ν a b c d : Shell p) :212    Q2 ν (a * d + b * c) (a * c + ν * (b * d)) = (a * a + -(ν * (b * b))) * (c * c + -(ν * (d * d))) := by213  unfold Q2214  have cross : (a * c) * (b * d) = (a * d) * (b * c) := by215    rw [mul_assoc, mul_left_comm c, ← mul_assoc, mul_assoc a d, mul_left_comm d, ← mul_assoc a b (d * c), mul_comm d c]216  have e1 : (a * c + ν * (b * d)) * (a * c + ν * (b * d)) =217      (a * c) * (a * c) + (ν * ((a * c) * (b * d)) + ν * ((a * c) * (b * d))) + (ν * ν) * ((b * d) * (b * d)) := by218    rw [sq_add, mul_left_comm (a * c) ν (b * d), sq_mul ν (b * d)]219  have e2 : -(ν * ((a * d + b * c) * (a * d + b * c))) =220      -(ν * ((a * d) * (a * d))) + -(ν * ((a * d) * (b * c)) + ν * ((a * d) * (b * c))) + -(ν * ((b * c) * (b * c))) := by221    rw [sq_add, left_distrib, left_distrib, left_distrib, neg_add_rev, neg_add_rev]222  rw [e1, e2, cross, regroup]223  rw [right_distrib, left_distrib, left_distrib, ← mul_neg, ← neg_mul, neg_mul_neg, ← add_assoc,224    ← sq_mul a c, mul_left_comm (a * a) ν (d * d), ← sq_mul a d, mul_assoc ν (b * b) (c * c), ← sq_mul b c,225    mul_assoc ν (b * b) (ν * (d * d)), mul_left_comm (b * b) ν (d * d), ← mul_assoc ν ν, ← sq_mul b d]226227/-- The boost `Λ(γ, b)` of `(t, x)`: `t ↦ γ t + b x`, `x ↦ γ x + ν b t` (multiplication by `γ + b√ν` in `K`). -/228def boostT (_ν γ b t x : Shell p) : Shell p := γ * t + b * x229def boostX (ν γ b t x : Shell p) : Shell p := γ * x + ν * (b * t)230231/-- 3:C2 (the finite Lorentz boost) — with `γ² − νb² = 1`, `Λ(γ, b)` preserves `x² − ν t²` exactly, on every shell. -/232theorem boost_preserves {ν γ b : Shell p} (h : γ * γ + -(ν * (b * b)) = 1) (t x : Shell p) :233    Q2 ν (boostT ν γ b t x) (boostX ν γ b t x) = Q2 ν t x := by234  unfold boostT boostX235  have := norm_mul ν γ b x t236  unfold Q2 at this ⊢237  rw [this, h, one_mul]238239/-- 3:C2 — boosts compose as their parameters multiply in `K`:240`Λ(γ₁, b₁) Λ(γ₂, b₂) = Λ(γ₁γ₂ + νb₁b₂, γ₁b₂ + b₁γ₂)`, the `t`-row. -/241theorem boost_comp_t (ν γ1 b1 γ2 b2 t x : Shell p) :242    boostT ν γ1 b1 (boostT ν γ2 b2 t x) (boostX ν γ2 b2 t x) =243    boostT ν (γ1 * γ2 + ν * (b1 * b2)) (γ1 * b2 + b1 * γ2) t x := by244  unfold boostT boostX245  rw [left_distrib, left_distrib, right_distrib, right_distrib, ← mul_assoc γ1 γ2 t, ← mul_assoc γ1 b2 x,246    ← mul_assoc b1 γ2 x, mul_left_comm b1 ν (b2 * t), ← mul_assoc b1 b2 t, ← mul_assoc ν (b1 * b2) t,247    add_comm (b1 * γ2 * x) (ν * (b1 * b2) * t), add_add_add_comm]248249/-- 3:C2 — the composition, the `x`-row. -/250theorem boost_comp_x (ν γ1 b1 γ2 b2 t x : Shell p) :251    boostX ν γ1 b1 (boostT ν γ2 b2 t x) (boostX ν γ2 b2 t x) =252    boostX ν (γ1 * γ2 + ν * (b1 * b2)) (γ1 * b2 + b1 * γ2) t x := by253  unfold boostT boostX254  rw [left_distrib, left_distrib, left_distrib, right_distrib, right_distrib, left_distrib,255    ← mul_assoc γ1 γ2 x, mul_left_comm γ1 ν (b2 * t), ← mul_assoc γ1 b2 t, ← mul_assoc b1 γ2 t,256    ← mul_assoc b1 b2 x, ← mul_assoc ν (b1 * b2) x,257    add_comm (ν * (b1 * γ2 * t)) (ν * (b1 * b2) * x), add_add_add_comm]258259/-- 3:C2 — the norm-one elements form a group: `N(z₁z₂) = N(z₁)N(z₂) = 1`. -/260theorem norm_one_mul {ν γ1 b1 γ2 b2 : Shell p} (h1 : γ1 * γ1 + -(ν * (b1 * b1)) = 1)261    (h2 : γ2 * γ2 + -(ν * (b2 * b2)) = 1) :262    (γ1 * γ2 + ν * (b1 * b2)) * (γ1 * γ2 + ν * (b1 * b2)) +263      -(ν * ((γ1 * b2 + b1 * γ2) * (γ1 * b2 + b1 * γ2))) = 1 := by264  have := norm_mul ν γ1 b1 γ2 b2265  unfold Q2 at this266  rw [this, h1, h2, one_mul]267268/-- 3:C3 — `γ ≠ 0` on every boost of the Lorentzian plane: `γ = 0` would give `ν b² = −1`, i.e.269`ν = (i/b)²`, a square. -/270theorem gamma_ne_zero (F : Frame p κ g) {ν γ b : Shell p} (hν : ¬IsSquare ν) (h : γ * γ + -(ν * (b * b)) = 1) :271    γ ≠ 0 := fun hγ => by272  rw [hγ, mul_zero, zero_add] at h273  have hb : b ≠ 0 := fun hb => by274    rw [hb, mul_zero, mul_zero, neg_zero] at h275    exact F.one_ne_zero h.symm276  have hνb : ν * (b * b) = -1 := by rw [← neg_neg (ν * (b * b)), h]277  match F.exists_inv hb with278  | ⟨s, hs⟩ =>279    exact hν ⟨quarterTurn g κ * s, by280      calc quarterTurn g κ * s * (quarterTurn g κ * s) = (quarterTurn g κ * quarterTurn g κ) * (s * s) := sq_mul _ _281        _ = -1 * (s * s) := by rw [F.quarter_turn_sq]282        _ = (ν * (b * b)) * (s * s) := by rw [hνb]283        _ = ν * ((b * s) * (b * s)) := by rw [mul_assoc, sq_mul b s]284        _ = ν := by rw [hs, one_mul, mul_one]⟩285286/-- 3:C3 — the velocity of the boost, `v = −νb/γ` (`vγ = −νb`), satisfies `γ² (ν − v²) = ν`: the finite form of287`γ = 1/√(1 − β²)` with `β² = v²/ν`. -/288theorem gamma_velocity {ν γ b v : Shell p} (hz : γ * γ + -(ν * (b * b)) = 1) (hv : v * γ = -(ν * b)) :289    γ * γ * (ν + -(v * v)) = ν := by290  calc γ * γ * (ν + -(v * v)) = γ * γ * ν + -((v * γ) * (v * γ)) := by291        rw [left_distrib, ← mul_neg, sq_mul v γ, mul_comm (v * v)]292    _ = ν * (γ * γ) + -(ν * (ν * (b * b))) := by293        rw [hv, neg_mul_neg, sq_mul ν b, mul_assoc ν ν (b * b), mul_comm (γ * γ) ν]294    _ = ν * (γ * γ + -(ν * (b * b))) := by rw [left_distrib, ← mul_neg]295    _ = ν := by rw [hz, mul_one]296297/-- 3:C3 (the velocity addition law) — for boosts with velocities `v₁, v₂` (`v_i γ_i = −ν b_i`) and the composed298boost's velocity `v₁₂`, `v₁₂ (ν + v₁v₂) = ν (v₁ + v₂)`: Einstein's law `v₁₂ = (v₁ + v₂)/(1 + v₁v₂/ν)`, exact. -/299theorem velocity_addition (F : Frame p κ g) {ν γ1 b1 γ2 b2 v1 v2 v12 : Shell p} (hν : ¬IsSquare ν)300    (hz1 : γ1 * γ1 + -(ν * (b1 * b1)) = 1) (hz2 : γ2 * γ2 + -(ν * (b2 * b2)) = 1)301    (hv1 : v1 * γ1 = -(ν * b1)) (hv2 : v2 * γ2 = -(ν * b2))302    (hv12 : v12 * (γ1 * γ2 + ν * (b1 * b2)) = -(ν * (γ1 * b2 + b1 * γ2))) :303    v12 * (ν + v1 * v2) = ν * (v1 + v2) := by304  have hγ : γ1 * γ2 ≠ 0 := F.mul_ne_zero (gamma_ne_zero F hν hz1) (gamma_ne_zero F hν hz2)305  apply F.mul_left_cancel hγ306  calc γ1 * γ2 * (v12 * (ν + v1 * v2)) = v12 * (γ1 * γ2 * ν + (v1 * γ1) * (v2 * γ2)) := by307        rw [mul_left_comm (γ1 * γ2) v12, left_distrib, mul_mul_mul_comm γ1 γ2 v1 v2, mul_comm γ1 v1, mul_comm γ2 v2]308    _ = v12 * (ν * (γ1 * γ2 + ν * (b1 * b2))) := by309        rw [hv1, hv2, neg_mul_neg, mul_mul_mul_comm ν b1 ν b2, mul_assoc ν ν (b1 * b2), mul_comm (γ1 * γ2) ν,310          ← left_distrib]311    _ = ν * (v12 * (γ1 * γ2 + ν * (b1 * b2))) := mul_left_comm _ _ _312    _ = -(ν * (ν * (γ1 * b2 + b1 * γ2))) := by rw [hv12, ← mul_neg]313    _ = ν * (-(γ2 * (ν * b1)) + -(γ1 * (ν * b2))) := by314        rw [mul_left_comm γ2 ν b1, mul_left_comm γ1 ν b2, ← neg_add_rev, ← left_distrib, mul_comm γ2 b1, ← mul_neg,315          add_comm (b1 * γ2) (γ1 * b2)]316    _ = ν * (γ2 * (v1 * γ1) + γ1 * (v2 * γ2)) := by rw [hv1, hv2, ← mul_neg, ← mul_neg]317    _ = γ1 * γ2 * (ν * (v1 + v2)) := by318        rw [mul_left_comm (γ1 * γ2) ν]319        refine congrArg (ν * ·) ?_320        rw [left_distrib, mul_comm v1 γ1, mul_comm v2 γ2, ← mul_assoc γ2 γ1 v1, mul_comm γ2 γ1, ← mul_assoc γ1 γ2 v2]321322/-! ### The counts, decided by the kernel -/323324/-- `Σ_{i<n} f i` on naturals. -/325def sumTo (f : Nat → Nat) : Nat → Nat326  | 0 => 0327  | n + 1 => sumTo f n + f n328329/-- The number of `(t, x, y, z) ∈ [0, p)⁴` with `−ν t² + x² + y² + z² ≡ 0 (mod p)`. -/330def nullCount (p ν : Nat) : Nat :=331  sumTo (fun t => sumTo (fun x => sumTo (fun y => sumTo (fun z =>332    if (x * x + y * y + z * z + (p - ν) * (t * t)) % p = 0 then 1 else 0) p) p) p) p333334/-- The number of `(γ, b) ∈ [0, p)²` with `γ² − ν b² ≡ 1 (mod p)`: the boosts. -/335def normOneCount (p ν : Nat) : Nat :=336  sumTo (fun γ => sumTo (fun b => if (γ * γ + (p - ν) * (b * b)) % p = 1 then 1 else 0) p) p337338/-- 3:B4, 3:D1 [value] — the null cone of `Q_2` on `𝔽₁₃` has `2041 = 13³ − 13² + 13` points: the elliptic type. -/339theorem null13 : nullCount 13 2 = 2041 := by decide +kernel340/-- 3:B4 [value] — the Euclidean form (`ν = 1`) on `𝔽₁₃` has `2353 = 13³ + 13² − 13` zeros: the hyperbolic type. -/341theorem euclid13 : nullCount 13 1 = 2353 := by decide +kernel342/-- 3:B4 [value] — `𝔽₅`, `ν = 2`: `105 = 5³ − 5² + 5` null points; `ν = 1`: `145`. -/343theorem null5 : nullCount 5 2 = 105 ∧ nullCount 5 1 = 145 := by decide +kernel344/-- 3:B4 [value] — `𝔽₁₇`, `ν = 3`: `4641 = 17³ − 17² + 17` null points. -/345theorem null17 : nullCount 17 3 = 4641 := by decide +kernel346/-- 3:C2, 3:D1 [value] — the boosts number `p + 1`: `6`, `14`, `18`, `30` on `𝔽₅`, `𝔽₁₃`, `𝔽₁₇`, `𝔽₂₉`. -/347theorem normOne_values : normOneCount 5 2 = 6 ∧ normOneCount 13 2 = 14 ∧ normOneCount 17 3 = 18 ∧348    normOneCount 29 2 = 30 := by decide +kernel349350end Frame351end Shell352end FRC353354/-! ## The two strata of probability (00:C10; the push of 8 October 2026)355356A structural weight is an element of the quadratic extension `𝔽_p[w]/(w² − ν)` (`Ext`); a registered value lies on the357tally line, the elements `a + 0 w`, the part fixed by the extension's conjugation. The paper's two-way subring is the358part of the cyclotomic ring fixed by `ζ ↦ ζ⁻¹`: for `ℤ[i]` it is the tally line (`ν = −1`), and for `ν = 2` it holds359`w = √2 = ζ₈ + ζ₈⁻¹` itself (`root_two_two_way`), so the engineered-core weights `2 ± w` are two-way, and `w ↦ −w` is360the conjugate-pair involution `W₊ ↔ W₋`. The two reductions that join the strata on the stationary core-valued sector361(22-quantum, Rem. strata; the witness `22:stratum.py`, S9 and S10): the conjugate-pair trace tally,362`z^k z̄^(k+m) + z̄^k z^(k+m) = N(z)^k · tr(z^m)`, core-valued for every weight `z`, with the trace sequence's363recurrence `t_{m+2} + N(z) t_m = tr(z) t_{m+1}` and the dial-shift conjugation `w₊(M − θ) = w₋(θ)`; and the364dial-ensemble Parseval tally, `Σ_θ w±(θ) = Σ_θ w₊ w₋ = 2N` over a dial of `N` settings closed under `ζ`, the cross365terms cancelling by the character sums. The engineered-core weights `W± = 2 ± w`, `w² = 2`, have `W₊ + W₋ = 4` and366`W₊ W₋ = 2`, on `Ω = 641` as residues (S2, S4); the framed readout's instances are decided by the kernel (S5–S7): a367readout computation over the naturals of the laboratory host in which the paper's Carrier `Ω = 641` is observed, as368decision Q20 allows, not a count of the totality. The frame supplies the odd prime where one is needed. -/369370namespace FRC.Extension371372open FRC.Shell373374section strata375variable {p : Nat} [Pos p] {ν : Shell p} {κ : Nat} {g : Shell p}376377theorem lit_add (a b : Nat) : (ofNat a : Shell p) + ofNat b = ofNat (a + b) :=378  Shell.ext (show (a % p + b % p) % p = (a + b) % p from (FRC.Nat.add_mod a b p Pos.pos).symm)379380theorem two_eq : (2 : Shell p) = 1 + 1 := (lit_add 1 1).symm381382theorem ext_add_comm (z z' : Ext p ν) : z + z' = z' + z :=383  Ext.ext (Shell.add_comm z.re z'.re) (Shell.add_comm z.im z'.im)384385theorem ext_mul_add (u a b : Ext p ν) : u * (a + b) = u * a + u * b :=386  Ext.ext (Shell.Frame.RE.sound (Shell.Frame.look [ν, u.re, u.im, a.re, a.im, b.re, b.im])387      (.add (.mul (.var 1) (.add (.var 3) (.var 5))) (.mul (.var 0) (.mul (.var 2) (.add (.var 4) (.var 6)))))388      (.add (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4)))) (.add (.mul (.var 1) (.var 5)) (.mul (.var 0) (.mul (.var 2) (.var 6)))))389      (by decide +kernel))390    (Shell.Frame.RE.sound (Shell.Frame.look [ν, u.re, u.im, a.re, a.im, b.re, b.im])391      (.add (.mul (.var 1) (.add (.var 4) (.var 6))) (.mul (.var 2) (.add (.var 3) (.var 5))))392      (.add (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3))) (.add (.mul (.var 1) (.var 6)) (.mul (.var 2) (.var 5))))393      (by decide +kernel))394395theorem ext_conj_one : Ext.conj (1 : Ext p ν) = 1 := Ext.ext rfl Shell.neg_zero396397/-- The symmetrised weight is core-valued: `z + z̄ = tr(z)` on the tally line. -/398theorem ext_tally_line (u : Ext p ν) : u + Ext.conj u = Ext.ofShell (Ext.trace u) := Ext.ext rfl (Shell.add_neg u.im)399400theorem ext_conj_pow (z : Ext p ν) : ∀ n : Nat, Ext.conj (z ^ n) = Ext.conj z ^ n401  | 0 => ext_conj_one402  | n + 1 => by show Ext.conj (z ^ n * z) = Ext.conj z ^ n * Ext.conj z; rw [Ext.conj_mul, ext_conj_pow z n]403404theorem ext_mul_pow (z z' : Ext p ν) : ∀ n : Nat, (z * z') ^ n = z ^ n * z' ^ n405  | 0 => (Ext.mul_one 1).symm406  | n + 1 => by407    show (z * z') ^ n * (z * z') = z ^ n * z * (z' ^ n * z')408    rw [ext_mul_pow z z' n, Ext.mul_assoc, ← Ext.mul_assoc (z' ^ n), Ext.mul_comm (z' ^ n) z, Ext.mul_assoc (z ^ n),409      Ext.mul_assoc z]410411theorem ext_ofShell_pow (c : Shell p) : ∀ n : Nat, (Ext.ofShell c : Ext p ν) ^ n = Ext.ofShell (c ^ n)412  | 0 => rfl413  | n + 1 => by414    show (Ext.ofShell c : Ext p ν) ^ n * Ext.ofShell c = Ext.ofShell (c ^ n * c)415    rw [ext_ofShell_pow c n, Ext.ofShell_mul]416417theorem ext_trace_add (u v : Ext p ν) : Ext.trace (u + v) = Ext.trace u + Ext.trace v :=418  Shell.add_add_add_comm u.re v.re u.re v.re419420theorem ext_trace_smul (c : Shell p) (u : Ext p ν) : Ext.trace (Ext.ofShell c * u) = c * Ext.trace u :=421  Shell.Frame.RE.sound (Shell.Frame.look [ν, c, u.re, u.im])422    (.add (.add (.mul (.var 1) (.var 2)) (.mul (.var 0) (.mul .zero (.var 3)))) (.add (.mul (.var 1) (.var 2)) (.mul (.var 0) (.mul .zero (.var 3)))))423    (.mul (.var 1) (.add (.var 2) (.var 2)))424    (by decide +kernel)425426/-- Cayley–Hamilton in the extension: `z² + N(z) = tr(z) z`. -/427theorem ext_cayley_hamilton (z : Ext p ν) : z * z + Ext.ofShell (Ext.norm z) = Ext.ofShell (Ext.trace z) * z :=428  Ext.ext (Shell.Frame.RE.sound (Shell.Frame.look [ν, z.re, z.im])429      (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))))430      (.add (.mul (.add (.var 1) (.var 1)) (.var 1)) (.mul (.var 0) (.mul .zero (.var 2))))431      (by decide +kernel))432    (Shell.Frame.RE.sound (Shell.Frame.look [ν, z.re, z.im])433      (.add (.add (.mul (.var 1) (.var 2)) (.mul (.var 2) (.var 1))) .zero)434      (.add (.mul (.add (.var 1) (.var 1)) (.var 2)) (.mul .zero (.var 1)))435      (by decide +kernel))436437/-- 00:C10 (S1), 22:C10, 22:X1 — the part of the extension fixed by its conjugation is the tally line: a weight `z` is its own438conjugate exactly when its `w`-component vanishes (the frame's odd prime), and the symmetrised weight `z + z̄` is the439tally-line element `tr(z)`. For `ℤ[i]`, `ν = −1`, this is the paper's two-way subring. -/440theorem two_way_tally (F : Frame p κ g) (z : Ext p ν) :441    (Ext.conj z = z ↔ z.im = 0) ∧ z + Ext.conj z = Ext.ofShell (Ext.trace z) :=442  ⟨⟨fun h => F.eq_zero_of_eq_neg (Ext.im_congr h).symm, fun h => Ext.ext rfl (by show -z.im = z.im; rw [h, Shell.neg_zero])⟩,443    ext_tally_line z⟩444445/-- The engineered-core weight `W₊ = 2 + w` in `𝔽_p[w]/(w² − 2)`; `W₋ = W̄₊ = 2 − w`. -/446def Wp : Ext p 2 := ⟨2, 1⟩447448/-- 00:C10 (S2, S4), 22:C10 — the engineered-core weights reduce to the core: `W₊ + W₋ = 4` and `W₊ W₋ = 2` in every449`𝔽_p[w]/(w² − 2)`, and on `Ω = 641` (`641 ≡ 1 (mod 8)`) as residues, `r = 67`, `r² = 2`, `W± = 2 ± r`, with `r` a450grid point of the Subject chart of generator `3`, `r = 3⁵⁵⁵` (S4). -/451theorem core_weights :452    ((Wp : Ext p 2) + Ext.conj Wp = Ext.ofShell 4 ∧ (Wp : Ext p 2) * Ext.conj Wp = Ext.ofShell 2 ∧453      Ext.trace (Wp : Ext p 2) = 4 ∧ Ext.norm (Wp : Ext p 2) = 2) ∧454    (641 % 8 = 1 ∧ (67 : Shell 641) * 67 = 2 ∧ (2 + 67 : Shell 641) + (2 + -67) = 4 ∧455      (2 + 67 : Shell 641) * (2 + -67) = 2 ∧ (3 : Shell 641) ^ 555 = 67) := by456  have hn : Ext.norm (Wp : Ext p 2) = 2 := by457    show (2 : Shell p) * 2 + -(2 * (1 * 1)) = 2458    have h4 : (2 : Shell p) * 2 = 2 + 2 := by rw [two_eq, Shell.right_distrib, Shell.one_mul]459    rw [Shell.one_mul, Shell.mul_one, h4, Shell.add_assoc, Shell.add_neg, Shell.add_zero]460  refine ⟨⟨Ext.ext (lit_add 2 2) (Shell.add_neg 1), by rw [Ext.mul_conj, hn], lit_add 2 2, hn⟩, by decide,461    by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel⟩462463/-- 00:C10 (S2), 22:C10 — the two-way root of two: on a frame, for `ζ` of order `8` (`ζ⁸ = 1`, `ζ⁴ ≠ 1`) and `η = ζ⁻¹`,464`(ζ + η)² = 2`. So `w = ζ₈ + ζ₈⁻¹` lies in the paper's two-way subring, the part of the cyclotomic ring fixed by465`ζ ↦ ζ⁻¹`, and the engineered-core weights `2 ± w` are two-way (on `641`: `ζ₈ = 318`, `ζ₈ + ζ₈⁻¹ = 574 = −67`). -/466theorem root_two_two_way (F : Frame p κ g) {ζ η : Shell p} (h8 : ζ ^ 8 = 1) (h4 : ζ ^ 4 ≠ 1) (hζη : ζ * η = 1) :467    (ζ + η) * (ζ + η) = 2 := by468  have hsq : ζ ^ 4 * ζ ^ 4 = 1 := by rw [← pow_add]; exact h8469  have hm1 : ζ ^ 4 = -1 := match F.sq_eq_one hsq with470    | .inl h => absurd h h4471    | .inr h => h472  have h22 : ζ ^ 2 * ζ ^ 2 = -1 := by rw [← pow_add]; exact hm1473  have hη2 : ζ ^ 2 * η ^ 2 = 1 := by rw [← mul_pow, hζη, one_pow]474  have hzero : ζ ^ 2 + η ^ 2 = 0 := by475    calc ζ ^ 2 + η ^ 2 = η ^ 2 * (ζ ^ 2 * ζ ^ 2) + η ^ 2 := by476          rw [← mul_assoc, mul_comm (η ^ 2) (ζ ^ 2), hη2, one_mul]477      _ = η ^ 2 * -1 + η ^ 2 := by rw [h22]478      _ = 0 := by rw [← mul_neg, mul_one, neg_add]479  rw [right_distrib, left_distrib, left_distrib, hζη, mul_comm η ζ, hζη, add_comm 1 (η * η), add_add_add_comm,480    ← pow_two ζ, ← pow_two η, hzero, zero_add]481  exact two_eq.symm482483/-- 00:C10 (S9), 22:C11 — the conjugate-pair trace tally: a flip-summed pair of conjugate string weights is core-valued,484`z^k z̄^(k+m) + z̄^k z^(k+m) = N(z)^k · tr(z^m)` on the tally line, for every weight `z` of every quadratic extension. -/485theorem conjugate_pair_tally (z : Ext p ν) (k m : Nat) :486    z ^ k * Ext.conj z ^ (k + m) + Ext.conj z ^ k * z ^ (k + m) = Ext.ofShell (Ext.norm z ^ k * Ext.trace (z ^ m)) := by487  rw [Ext.pow_add, Ext.pow_add, ← Ext.mul_assoc, ← Ext.mul_assoc, ← ext_mul_pow, ← ext_mul_pow, Ext.mul_conj,488    Ext.mul_comm (Ext.conj z) z, Ext.mul_conj, ext_ofShell_pow, ← ext_mul_add, ← ext_conj_pow, ext_add_comm,489    ext_tally_line (z ^ m), Ext.ofShell_mul]490491/-- 00:C10 (S9), 22:C11 — the trace sequence `t_m = tr(z^m)` obeys `t_{m+2} + N(z) t_m = tr(z) t_{m+1}`; for `W₊` (`tr = 4`,492`N = 2`): `t_0 = 2`, `t_1 = 4`, `t_{m+2} = 4 t_{m+1} − 2 t_m`, so `t_2 = 12`, `t_3 = 40` (on `Ω = 641`). -/493theorem trace_recurrence :494    (∀ (z : Ext p ν) (m : Nat), Ext.trace (z ^ (m + 2)) + Ext.norm z * Ext.trace (z ^ m) = Ext.trace z * Ext.trace (z ^ (m + 1))) ∧495    (Ext.trace ((Wp : Ext p 2) ^ 0) = 2 ∧ Ext.trace ((Wp : Ext p 2) ^ 1) = 4) ∧496    (Ext.trace ((Wp : Ext 641 2) ^ 2) = 12 ∧ Ext.trace ((Wp : Ext 641 2) ^ 3) = 40) := by497  refine ⟨fun z m => ?_, ⟨lit_add 1 1, by show Ext.trace (1 * Wp) = 4; rw [Ext.one_mul]; exact lit_add 2 2⟩,498    by decide +kernel, by decide +kernel⟩499  have h : z ^ (m + 2) + Ext.ofShell (Ext.norm z) * z ^ m = Ext.ofShell (Ext.trace z) * z ^ (m + 1) := by500    calc z ^ (m + 2) + Ext.ofShell (Ext.norm z) * z ^ m501        = z ^ m * (z * z) + z ^ m * Ext.ofShell (Ext.norm z) := by502          rw [Ext.mul_comm (Ext.ofShell _)]; show z ^ m * z * z + _ = _; rw [Ext.mul_assoc]503      _ = z ^ m * (z * z + Ext.ofShell (Ext.norm z)) := (ext_mul_add _ _ _).symm504      _ = z ^ m * (Ext.ofShell (Ext.trace z) * z) := by rw [ext_cayley_hamilton]505      _ = Ext.ofShell (Ext.trace z) * z ^ (m + 1) := by506          show z ^ m * (Ext.ofShell (Ext.trace z) * z) = Ext.ofShell (Ext.trace z) * (z ^ m * z)507          rw [← Ext.mul_assoc, Ext.mul_comm (z ^ m), Ext.mul_assoc]508  have := congrArg Ext.trace h509  rw [ext_trace_add, ext_trace_smul, ext_trace_smul] at this510  exact this511512theorem geom_sum_zero (F : Frame p κ g) {x : Shell p} (n : Nat) (hn : x ^ n = 1) (hx : x ≠ 1) :513    sumRange (fun l => x ^ l) n = 0 := by514  have hg := geom_sum_mul x n515  rw [hn, add_neg] at hg516  match F.mul_eq_zero hg with517  | .inl h => exact h518  | .inr h => exact absurd (by519      calc x = x + 0 := (add_zero x).symm520        _ = x + (-1 + 1) := by rw [neg_add]521        _ = (x + -1) + 1 := (add_assoc _ _ _).symm522        _ = 1 := by rw [h, zero_add]) hx523524/-- 00:C10 (S9), 22:C11 — the dial-shift conjugation: on a dial of `2M` settings (`ζ^(2M) = 1`, `ζ^M ≠ 1`, `η = ζ⁻¹`), the525weight at the shifted setting is the conjugate weight, `w₊(M − θ) = w₋(θ)` for `θ ≤ M` (the witness: `M = 40` in526`ℤ[x]/(x⁴⁰ + 1)`, `w₊(40 − D) = w₋(D)`). -/527theorem dial_shift (F : Frame p κ g) {ζ η : Shell p} (M : Nat) (h2M : ζ ^ (2 * M) = 1) (hM : ζ ^ M ≠ 1)528    (hζη : ζ * η = 1) (θ : Nat) (hθ : θ ≤ M) :529    2 + (ζ ^ (M - θ) + η ^ (M - θ)) = 2 + -(ζ ^ θ + η ^ θ) := by530  have hsq : ζ ^ M * ζ ^ M = 1 := by rw [← pow_add, ← Nat.two_mul]; exact h2M531  have hζM : ζ ^ M = -1 := match F.sq_eq_one hsq with532    | .inl h => absurd h hM533    | .inr h => h534  have hηM : η ^ M = -1 := by535    have h1 : ζ ^ M * η ^ M = 1 := by rw [← mul_pow, hζη, one_pow]536    rw [hζM] at h1537    calc η ^ M = -(-1 * η ^ M) := by rw [neg_mul, neg_neg, one_mul]538      _ = -1 := by rw [h1]539  have hθη : ζ ^ θ * η ^ θ = 1 := by rw [← mul_pow, hζη, one_pow]540  have e1 : ζ ^ (M - θ) = -(η ^ θ) := by541    calc ζ ^ (M - θ) = ζ ^ (M - θ) * (ζ ^ θ * η ^ θ) := by rw [hθη, mul_one]542      _ = ζ ^ M * η ^ θ := by rw [← mul_assoc, ← pow_add, FRC.Nat.sub_add_cancel hθ]543      _ = -(η ^ θ) := by rw [hζM, neg_one_mul]544  have e2 : η ^ (M - θ) = -(ζ ^ θ) := by545    calc η ^ (M - θ) = η ^ (M - θ) * (η ^ θ * ζ ^ θ) := by rw [mul_comm (η ^ θ), hθη, mul_one]546      _ = η ^ M * ζ ^ θ := by rw [← mul_assoc, ← pow_add, FRC.Nat.sub_add_cancel hθ]547      _ = -(ζ ^ θ) := by rw [hηM, neg_one_mul]548  rw [e1, e2, neg_add_rev, add_comm (-(ζ ^ θ))]549550/-- 00:C10 (S10), 22:C11 — the dial-ensemble Parseval tally: over a dial of `N` settings closed under `ζ` (`ζ^N = 1`,551`ζ² ≠ 1`, `η = ζ⁻¹`) on a frame, the weights `w±(θ) = 2 ± (ζ^θ + η^θ)` sum to `2N`, and so do the products552`w₊(θ) w₋(θ)`: the cross terms cancel by the character sums (the frame: no zero divisors). -/553theorem dial_tally (F : Frame p κ g) {ζ η : Shell p} (N : Nat) (hN : ζ ^ N = 1) (hζη : ζ * η = 1) (h2 : ζ * ζ ≠ 1) :554    sumRange (fun θ => 2 + (ζ ^ θ + η ^ θ)) N = ofNat N * 2 ∧555    sumRange (fun θ => 2 + -(ζ ^ θ + η ^ θ)) N = ofNat N * 2 ∧556    sumRange (fun θ => (2 + (ζ ^ θ + η ^ θ)) * (2 + -(ζ ^ θ + η ^ θ))) N = ofNat N * 2 := by557  have hζ1 : ζ ≠ 1 := fun h => h2 (by rw [h, Shell.one_mul])558  have hηN : η ^ N = 1 := by559    have : (ζ * η) ^ N = 1 := by rw [hζη, one_pow]560    rw [mul_pow, hN, Shell.one_mul] at this; exact this561  have hη1 : η ≠ 1 := fun h => hζ1 (calc ζ = ζ * 1 := (Shell.mul_one ζ).symm562    _ = ζ * η := by rw [h]563    _ = 1 := hζη)564  have hζ2N : (ζ * ζ) ^ N = 1 := by rw [mul_pow, hN, Shell.one_mul]565  have hη2N : (η * η) ^ N = 1 := by rw [mul_pow, hηN, Shell.one_mul]566  have hη2 : η * η ≠ 1 := fun h => h2 (by567    calc ζ * ζ = ζ * ζ * (η * η) := by rw [h, Shell.mul_one]568      _ = (ζ * η) * (ζ * η) := Shell.Frame.RE.sound (Shell.Frame.look [ζ, η])569            (.mul (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1)))570            (by decide +kernel)571      _ = 1 := by rw [hζη, Shell.mul_one])572  have gζ := geom_sum_zero F N hN hζ1573  have gη := geom_sum_zero F N hηN hη1574  have gζ2 := geom_sum_zero F N hζ2N h2575  have gη2 := geom_sum_zero F N hη2N hη2576  have term : ∀ θ, θ < N → (2 + (ζ ^ θ + η ^ θ)) * (2 + -(ζ ^ θ + η ^ θ)) = 2 + -((ζ * ζ) ^ θ + (η * η) ^ θ) := by577    intro θ _578    have hab : ζ ^ θ * η ^ θ = 1 := by rw [← mul_pow, hζη, one_pow]579    rw [mul_pow, mul_pow, two_eq]580    calc (1 + 1 + (ζ ^ θ + η ^ θ)) * (1 + 1 + -(ζ ^ θ + η ^ θ))581        = (1 + 1 + -(ζ ^ θ * ζ ^ θ + η ^ θ * η ^ θ)) + (1 + 1 + -(ζ ^ θ * η ^ θ + ζ ^ θ * η ^ θ)) :=582          Shell.Frame.RE.sound (Shell.Frame.look [ζ ^ θ, η ^ θ])583            (.mul (.add (.add .one .one) (.add (.var 0) (.var 1))) (.add (.add .one .one) (.neg (.add (.var 0) (.var 1)))))584            (.add (.add (.add .one .one) (.neg (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1)))))585              (.add (.add .one .one) (.neg (.add (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))))))586            (by decide +kernel)587      _ = 1 + 1 + -(ζ ^ θ * ζ ^ θ + η ^ θ * η ^ θ) := by rw [hab, add_neg, add_zero]588  refine ⟨?_, ?_, ?_⟩589  · rw [sum_add (fun _ => (2 : Shell p)) (fun θ => ζ ^ θ + η ^ θ) N, sum_const, sum_add (fun θ => ζ ^ θ) (fun θ => η ^ θ) N,590      gζ, gη, add_zero, add_zero]591  · rw [sum_add (fun _ => (2 : Shell p)) (fun θ => -(ζ ^ θ + η ^ θ)) N, sum_const, sum_neg (fun θ => ζ ^ θ + η ^ θ) N,592      sum_add (fun θ => ζ ^ θ) (fun θ => η ^ θ) N, gζ, gη, add_zero, neg_zero, add_zero]593  · rw [sum_congr N term, sum_add (fun _ => (2 : Shell p)) (fun θ => -((ζ * ζ) ^ θ + (η * η) ^ θ)) N, sum_const,594      sum_neg (fun θ => (ζ * ζ) ^ θ + (η * η) ^ θ) N, sum_add (fun θ => (ζ * ζ) ^ θ) (fun θ => (η * η) ^ θ) N,595      gζ2, gη2, add_zero, neg_zero, add_zero]596597/-- The framed grid points `s_n = ⌊√(2 · 9ⁿ)⌋`, `n ≤ 8`, of the Subject chart with generator `g = 3`. -/598def gridPoint : Nat → Nat599  | 0 => 1 | 1 => 4 | 2 => 12 | 3 => 38 | 4 => 114 | 5 => 343 | 6 => 1030 | 7 => 3092 | 8 => 9278 | _ => 0600601/-- The `i`-th entry of a list of naturals, `0` past its end (the core's `getD` carries `propext`). -/602def nth : List Nat → Nat → Nat603  | [], _ => 0604  | x :: _, 0 => x605  | _ :: xs, i + 1 => nth xs i606607/-- The rank of the `i`-th remainder among `rems`: the number of remainders that precede it, the larger first and, at a608tie, the earlier index. -/609def remainderRank (rems : List Nat) (i : Nat) : Nat := go 0 rems610where611  go : Nat → List Nat → Nat612    | _, [] => 0613    | j, r :: rs => (if r > nth rems i ∨ (r = nth rems i ∧ j < i) then 1 else 0) + go (j + 1) rs614615/-- The largest-remainder allocation of `B` counts to the probabilities `nums / den`: each takes its floor, and the616seats left go one each to the largest remainders, ties by index. -/617def largestRemainder (B den : Nat) (nums : List Nat) : List Nat :=618  let floors := nums.map (fun n => B * n / den)619  let rems := nums.map (fun n => B * n % den)620  let seats := B - floors.foldl (· + ·) 0621  (List.range nums.length).map (fun i => nth floors i + if remainderRank rems i < seats then 1 else 0)622623/-- 00:C10 (S5–S7), 22:C10, 22:C11, 22:X6 — a registered probability is a framed rational, decided by the kernel: the grid bound624`s_n² ≤ 2 · 9ⁿ < (s_n + 1)²` at every scale `n ≤ 8` and the readouts nest, `3 s_n ≤ s_{n+1} ≤ 3 s_n + 2`; the readout625`R_4((2 + √2)/8) = (2 · 3⁴ + 114)/(8 · 3⁴) = 23/54`; the `√3` instance `s_3 = 46`; the largest-remainder allocation at626`B = 81` of `(23/54, 23/54, 4/54, 4/54)` is `35 + 34 + 6 + 6` (the floors `34 + 34 + 6 + 6`, the one seat left to the627first of the two remainders `27/54`). A readout computation over the naturals of the laboratory host (decision Q20). -/628theorem framed_readout :629    (∀ n, n < 9 → gridPoint n * gridPoint n ≤ 2 * 9 ^ n ∧ 2 * 9 ^ n < (gridPoint n + 1) * (gridPoint n + 1)) ∧630    (∀ n, n < 8 → 3 * gridPoint n ≤ gridPoint (n + 1) ∧ gridPoint (n + 1) ≤ 3 * gridPoint n + 2) ∧631    (2 * 3 ^ 4 + gridPoint 4) * 54 = 23 * (8 * 3 ^ 4) ∧ (46 * 46 ≤ 3 * 3 ^ 6 ∧ 3 * 3 ^ 6 < 47 * 47) ∧632    (23 + 23 + 4 + 4 = 54 ∧ largestRemainder 81 54 [23, 23, 4, 4] = [35, 34, 6, 6]) := by633  refine ⟨by decide, by decide, by decide, by decide, by decide⟩634635end strata636637end FRC.Extension638