Theme/Gravity.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Series3import FrcCore.Ring45/-!6# FrcCore.Theme.Gravity — the gravity theme: the horizon's count (ledger migration, task LM27)78The master's block E where its rows are exact. On a frame `(τ; 0, 1, g)` of capacity `κ` (`p = 4κ + 1`):910* the registration sphere `x² + y² + z² = κ²` of `𝔽_p³` has exactly `A = p(p + 1)` points, and so has the sphere at every11  nonzero square rung (`sphere_area`, `sphere_area_rung`): the plane conic `x² + y² = c` has `p − 1` points for `c ≠ 0`12  and `2p − 1` for `c = 0` (`pair_count`), since `−1 = i²` turns it into `uv = c`;13* the record `S = κ(p + 1)` against the area: `4S + 1 = p²` (the record law, the `Q₄` quotient of `𝔽_{p²}^×`, and14  `(Ω − 1)/4` at `p² = Ω`), `S p = κ A` (`S/A = κ/p`), `4 S p = A (p − 1)` (`S = (A/4)(1 − 1/p)`) (`count_identity`, moved15  from 21-gravity's `Gravity.lean`, which keeps the name), and `S = M(M − 1)` on the rate face `M = (p + 1)/2`16  (`record_mass`);17* the response: `S(M + h) = S(M) + p h + h²` (`dS/dM = p`, `T_resp = 1/p`; `record_response`); the registration rate18  `T = A/p³ = (p + 1)/p²` (`temperature_rate`); the two Smarr relations `2 T_resp S = M(1 − 1/p)` and19  `2 T S = M(1 − 1/p²)` (`smarr`);20* the merger law on the count face `A = M(M + 1)`: `ΔA = 2 M₁ M₂` (`merger_area`).2122The counts are natural numbers: `count P` counts the residues satisfying `P`, and `nsum` adds natural numbers; both are23invariant under a bijection of the residues (`count_bij`, `nsum_perm`). The identities between natural numbers are24decided by the ring normaliser, read in the natural numbers (`nat_sound`): no shell is built for them. No axioms.25-/2627namespace FRC.Grav2829open FRC.Shell FRC.Shell.Frame3031/-! ## Identities between natural numbers, by the ring normaliser -/3233/-- An expression read in the natural numbers (a negation reads `0`; the identities below have none). -/34def natEval (env : Nat → Nat) : RE → Nat35  | .var i => env i36  | .zero => 037  | .one => 138  | .add a b => natEval env a + natEval env b39  | .mul a b => natEval env a * natEval env b40  | .neg _ => 04142/-- The expression has no negation. -/43def negFree : RE → Bool44  | .var _ => true45  | .zero => true46  | .one => true47  | .add a b => negFree a && negFree b48  | .mul a b => negFree a && negFree b49  | .neg _ => false5051/-- The assignment of natural numbers to the variables `0, 1, 2, …`. -/52def nlook : List Nat → Nat → Nat53  | [], _ => 054  | x :: _, 0 => x55  | _ :: l, n + 1 => nlook l n5657/-- A monomial and a polynomial read in the natural numbers. -/58def mEvalN (env : Nat → Nat) : List Nat → Nat59  | [] => 160  | i :: m => env i * mEvalN env m6162def pEvalN (env : Nat → Nat) : List (List Nat) → Nat63  | [] => 064  | m :: P => mEvalN env m + pEvalN env P6566theorem mEvalN_append (env : Nat → Nat) (m n : List Nat) : mEvalN env (m ++ n) = mEvalN env m * mEvalN env n := by67  induction m with68  | nil => exact (Nat.one_mul _).symm69  | cons i m ih => show env i * mEvalN env (m ++ n) = env i * mEvalN env m * mEvalN env n; rw [ih, FRC.Nat.mul_assoc]7071theorem pEvalN_append (env : Nat → Nat) (P Q : List (List Nat)) : pEvalN env (P ++ Q) = pEvalN env P + pEvalN env Q := by72  induction P with73  | nil => exact (Nat.zero_add _).symm74  | cons m P ih => show mEvalN env m + pEvalN env (P ++ Q) = mEvalN env m + pEvalN env P + pEvalN env Q; rw [ih, Nat.add_assoc]7576theorem pEvalN_row (env : Nat → Nat) (m : List Nat) (Q : List (List Nat)) : pEvalN env (pRow m Q) = mEvalN env m * pEvalN env Q := by77  induction Q with78  | nil => exact (Nat.mul_zero _).symm79  | cons n Q ih =>80    show mEvalN env (m ++ n) + pEvalN env (pRow m Q) = mEvalN env m * (mEvalN env n + pEvalN env Q)81    rw [ih, mEvalN_append, Nat.left_distrib]8283theorem pEvalN_mul (env : Nat → Nat) (P Q : List (List Nat)) : pEvalN env (pMul P Q) = pEvalN env P * pEvalN env Q := by84  induction P with85  | nil => exact (Nat.zero_mul _).symm86  | cons m P ih =>87    show pEvalN env (pRow m Q ++ pMul P Q) = (mEvalN env m + pEvalN env P) * pEvalN env Q88    rw [pEvalN_append, pEvalN_row, ih, FRC.Nat.add_mul]8990theorem pMul_nil : ∀ P : List (List Nat), pMul P [] = []91  | [] => rfl92  | _ :: P => by show [] ++ pMul P [] = []; rw [pMul_nil P]; rfl9394theorem toP_neg_nil : ∀ e : RE, negFree e = true → e.toP.2 = []95  | .var _, _ => rfl96  | .zero, _ => rfl97  | .one, _ => rfl98  | .add a b, h => by99    show a.toP.2 ++ b.toP.2 = []100    rw [toP_neg_nil a (and_true_left h), toP_neg_nil b (and_true_right h)]; rfl101  | .mul a b, h => by102    show pMul a.toP.1 b.toP.2 ++ pMul a.toP.2 b.toP.1 = []103    rw [toP_neg_nil a (and_true_left h), toP_neg_nil b (and_true_right h), pMul_nil]; rfl104  | .neg _, h => Bool.noConfusion h105106theorem natEval_toP (env : Nat → Nat) : ∀ e : RE, negFree e = true → natEval env e = pEvalN env e.toP.1107  | .var i, _ => by show env i = env i * 1 + 0; rw [Nat.mul_one, Nat.add_zero]108  | .zero, _ => rfl109  | .one, _ => rfl110  | .add a b, h => by111    show natEval env a + natEval env b = pEvalN env (a.toP.1 ++ b.toP.1)112    rw [pEvalN_append, ← natEval_toP env a (and_true_left h), ← natEval_toP env b (and_true_right h)]113  | .mul a b, h => by114    show natEval env a * natEval env b = pEvalN env (pMul a.toP.1 b.toP.1 ++ pMul a.toP.2 b.toP.2)115    rw [toP_neg_nil a (and_true_left h), pEvalN_append, pEvalN_mul, ← natEval_toP env a (and_true_left h),116      ← natEval_toP env b (and_true_right h)]117    show _ = _ + pEvalN env (pMul [] b.toP.2)118    rfl119120theorem mEvalN_insM (env : Nat → Nat) (i : Nat) (m : List Nat) : mEvalN env (insM i m) = env i * mEvalN env m := by121  induction m with122  | nil => rfl123  | cons j m ih =>124    show mEvalN env (if Nat.ble i j then i :: j :: m else j :: insM i m) = env i * (env j * mEvalN env m)125    cases Nat.ble i j with126    | true => rfl127    | false => show env j * mEvalN env (insM i m) = _; rw [ih, FRC.Nat.mul_left_comm]128129theorem mEvalN_sortM (env : Nat → Nat) (m : List Nat) : mEvalN env (sortM m) = mEvalN env m := by130  induction m with131  | nil => rfl132  | cons i m ih => show mEvalN env (insM i (sortM m)) = env i * mEvalN env m; rw [mEvalN_insM, ih]133134theorem add_left_comm' (a b c : Nat) : a + (b + c) = b + (a + c) := by135  rw [← Nat.add_assoc, Nat.add_comm a b, Nat.add_assoc]136137theorem pEvalN_insP (env : Nat → Nat) (m : List Nat) (P : List (List Nat)) : pEvalN env (insP m P) = mEvalN env m + pEvalN env P := by138  induction P with139  | nil => rfl140  | cons n P ih =>141    show pEvalN env (if lexLe m n then m :: n :: P else n :: insP m P) = mEvalN env m + (mEvalN env n + pEvalN env P)142    cases lexLe m n with143    | true => rfl144    | false => show mEvalN env n + pEvalN env (insP m P) = _; rw [ih, add_left_comm']145146theorem pEvalN_nfP (env : Nat → Nat) (P : List (List Nat)) : pEvalN env (nfP P) = pEvalN env P := by147  induction P with148  | nil => rfl149  | cons m P ih => show pEvalN env (insP (sortM m) (nfP P)) = mEvalN env m + pEvalN env P; rw [pEvalN_insP, ih, mEvalN_sortM]150151/-- The normaliser's soundness on the natural numbers, read in the naturals themselves. No shell is built, and the152kernel's decision runs over the expressions' monomials, never over the values of their variables (Q20). -/153theorem nat_sound (env : Nat → Nat) (l r : RE) (hl : negFree l = true) (hr : negFree r = true)154    (hb : RE.check l r = true) : natEval env l = natEval env r := by155  have h := pbeq_eq hb156  have e := congrArg (pEvalN env) h157  rw [pEvalN_nfP, pEvalN_nfP, pEvalN_append, pEvalN_append] at e158  have zl : pEvalN env l.toP.2 = 0 := congrArg (pEvalN env) (toP_neg_nil l hl)159  have zr : pEvalN env r.toP.2 = 0 := congrArg (pEvalN env) (toP_neg_nil r hr)160  rw [zl, zr, Nat.add_zero, Nat.add_zero] at e161  rw [natEval_toP env l hl, natEval_toP env r hr]162  exact e163164/-! ## Sums of natural numbers -/165166/-- `Σ_{l<n} f l` in the natural numbers. -/167def nsum (f : Nat → Nat) : Nat → Nat168  | 0 => 0169  | n + 1 => nsum f n + f n170171theorem nsum_congr {f h : Nat → Nat} : ∀ n, (∀ l, l < n → f l = h l) → nsum f n = nsum h n172  | 0, _ => rfl173  | n + 1, e => by174    show nsum f n + f n = nsum h n + h n175    rw [nsum_congr n (fun l hl => e l (Nat.lt_succ_of_lt hl)), e n (Nat.lt_succ_self n)]176177theorem nsum_add (f h : Nat → Nat) : ∀ n, nsum (fun l => f l + h l) n = nsum f n + nsum h n178  | 0 => rfl179  | n + 1 => by180    show nsum (fun l => f l + h l) n + (f n + h n) = (nsum f n + f n) + (nsum h n + h n)181    rw [nsum_add f h n, FRC.Nat.add_add_add_comm]182183theorem nsum_zero : ∀ n, nsum (fun _ => 0) n = 0184  | 0 => rfl185  | n + 1 => by show nsum (fun _ => 0) n + 0 = 0; rw [nsum_zero n]186187theorem nsum_const (c : Nat) : ∀ n, nsum (fun _ => c) n = n * c188  | 0 => (Nat.zero_mul c).symm189  | n + 1 => by show nsum (fun _ => c) n + c = (n + 1) * c; rw [nsum_const c n, Nat.succ_mul]190191theorem nsum_mul_left (c : Nat) (f : Nat → Nat) : ∀ n, nsum (fun l => c * f l) n = c * nsum f n192  | 0 => (Nat.mul_zero c).symm193  | n + 1 => by show nsum (fun l => c * f l) n + c * f n = c * (nsum f n + f n); rw [nsum_mul_left c f n, Nat.mul_add]194195/-- Double sums commute. -/196theorem nsum_comm (f : Nat → Nat → Nat) (m : Nat) : ∀ n,197    nsum (fun i => nsum (fun j => f i j) m) n = nsum (fun j => nsum (fun i => f i j) n) m198  | 0 => (nsum_zero m).symm199  | n + 1 => by200    show nsum (fun i => nsum (fun j => f i j) m) n + nsum (fun j => f n j) m = _201    rw [nsum_comm f m n, ← nsum_add]202    rfl203204/-- Splitting off the first term. -/205theorem nsum_succ' (f : Nat → Nat) : ∀ n, nsum f (n + 1) = f 0 + nsum (fun l => f (l + 1)) n206  | 0 => (Nat.add_comm _ _).trans rfl207  | n + 1 => by208    show nsum f (n + 1) + f (n + 1) = f 0 + (nsum (fun l => f (l + 1)) n + f (n + 1))209    rw [nsum_succ' f n, Nat.add_assoc]210211/-- The sum of `F` over a list of indices. -/212def nsumList (F : Nat → Nat) : List Nat → Nat213  | [] => 0214  | a :: l => F a + nsumList F l215216theorem nsumList_imageList (F : Nat → Nat) (σ : Nat → Nat) : ∀ n,217    nsumList F (imageList σ n) = nsum (fun j => F (σ j)) n218  | 0 => rfl219  | n + 1 => by220    show F (σ n) + nsumList F (imageList σ n) = nsum (fun j => F (σ j)) n + F (σ n)221    rw [nsumList_imageList F σ n, Nat.add_comm]222223theorem nsumList_erase (F : Nat → Nat) {v : Nat} : ∀ {l : List Nat}, Pigeonhole.mem v l →224    nsumList F l = F v + nsumList F (Pigeonhole.erase v l)225  | [], h => absurd h id226  | a :: l, h => by227    exact match Nat.decEq a v with228      | isTrue e => by rw [show Pigeonhole.erase v (a :: l) = l from ite_eq_left e, e]; rfl229      | isFalse e => by230          rw [show Pigeonhole.erase v (a :: l) = a :: Pigeonhole.erase v l from ite_eq_right e]231          have hm : Pigeonhole.mem v l := match h with232            | Or.inl h' => absurd h'.symm e233            | Or.inr h' => h'234          show F a + nsumList F l = F v + (F a + nsumList F (Pigeonhole.erase v l))235          rw [nsumList_erase F hm, Nat.add_left_comm]236237theorem nsumList_eq_nsum (F : Nat → Nat) : ∀ (n : Nat) (l : List Nat), Pigeonhole.NoDup l →238    (∀ e, Pigeonhole.mem e l → e < n) → l.length = n → nsumList F l = nsum F n239  | 0, [], _, _, _ => rfl240  | 0, a :: l, _, hb, _ => absurd (hb a (Or.inl rfl)) (Nat.not_lt_zero a)241  | n + 1, l, hnd, hb, hlen => by242    have hm : Pigeonhole.mem n l := Pigeonhole.mem_of_nodup_of_length_lt (n + 1) l hnd hb hlen n (Nat.lt_succ_self n)243    rw [nsumList_erase F hm]244    show F n + nsumList F (Pigeonhole.erase n l) = nsum F n + F n245    rw [Nat.add_comm]246    have hb' : ∀ e, Pigeonhole.mem e (Pigeonhole.erase n l) → e < n := fun e he =>247      match Nat.lt_or_ge e n with248      | Or.inl hlt => hlt249      | Or.inr hge =>250        have : e = n := Nat.le_antisymm (Nat.le_of_lt_succ (hb e (Pigeonhole.mem_of_mem_erase he))) hge251        absurd (this ▸ he) (Pigeonhole.not_mem_erase_self n hnd)252    have hlen' : (Pigeonhole.erase n l).length = n := by253      have := Pigeonhole.length_erase_of_mem hm; rw [hlen] at this; exact Nat.succ.inj this254    rw [nsumList_eq_nsum F n (Pigeonhole.erase n l) (Pigeonhole.nodup_erase n hnd) hb' hlen']255256/-- Permutation invariance: for `σ` injective on `[0, n)` with values below `n`, `Σ_{j<n} F (σ j) = Σ_{l<n} F l`. -/257theorem nsum_perm (F : Nat → Nat) (σ : Nat → Nat) (n : Nat) (hlt : ∀ j, j < n → σ j < n)258    (hinj : ∀ i j, i < n → j < n → σ i = σ j → i = j) :259    nsum (fun j => F (σ j)) n = nsum F n := by260  rw [← nsumList_imageList]261  exact nsumList_eq_nsum F n (imageList σ n) (imageList_nodup hinj (Nat.le_refl n))262    (fun e he => match mem_imageList he with | ⟨j, hj, e'⟩ => e' ▸ hlt j hj) (imageList_length σ n)263264/-! ## Counting residues -/265266theorem natCount_eq_nsum (P : Nat → Prop) [DecidablePred P] : ∀ n, natCount P n = nsum (fun x => if P x then 1 else 0) n267  | 0 => rfl268  | n + 1 => by269    show natCount P n + (if P n then 1 else 0) = nsum (fun x => if P x then 1 else 0) n + (if P n then 1 else 0)270    rw [natCount_eq_nsum P n]271272/-- A predicate holding at exactly one point below `n` counts `1`. -/273theorem natCount_single (P : Nat → Prop) [DecidablePred P] {x₀ : Nat} (h₀ : P x₀) :274    ∀ n, x₀ < n → (∀ x, x < n → P x → x = x₀) → natCount P n = 1275  | 0, h, _ => absurd h (Nat.not_lt_zero _)276  | n + 1, h, hu => by277    show natCount P n + (if P n then 1 else 0) = 1278    exact match Nat.decEq x₀ n with279      | isTrue e => by280        have h0 : natCount P n = 0 := natCount_eq_zero P n (fun x hx hP => by281          have h1 := hu x (Nat.lt_succ_of_lt hx) hP282          rw [h1, e] at hx283          exact Nat.lt_irrefl n hx)284        rw [ite_eq_left (e ▸ h₀), h0]285      | isFalse e => by286        rw [natCount_single P h₀ n (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ h) e)287            (fun x hx hP => hu x (Nat.lt_succ_of_lt hx) hP),288          ite_eq_right (fun hn => e (hu n (Nat.lt_succ_self n) hn).symm)]289290/-- Disjoint predicates count additively. -/291theorem natCount_or (P Q : Nat → Prop) [DecidablePred P] [DecidablePred Q] (hd : ∀ x, P x → ¬ Q x) :292    ∀ n, natCount (fun x => P x ∨ Q x) n = natCount P n + natCount Q n293  | 0 => rfl294  | n + 1 => by295    show natCount (fun x => P x ∨ Q x) n + (if P n ∨ Q n then 1 else 0)296      = (natCount P n + (if P n then 1 else 0)) + (natCount Q n + (if Q n then 1 else 0))297    rw [natCount_or P Q hd n, FRC.Nat.add_add_add_comm]298    congr 1299    exact match (inferInstance : Decidable (P n)), (inferInstance : Decidable (Q n)) with300      | isTrue hp, _ => by rw [ite_eq_left (Or.inl hp), ite_eq_left hp, ite_eq_right (hd n hp)]301      | isFalse hp, isTrue hq => by rw [ite_eq_left (Or.inr hq), ite_eq_right hp, ite_eq_left hq]302      | isFalse hp, isFalse hq => by303        rw [ite_eq_right (fun h => h.elim hp hq), ite_eq_right hp, ite_eq_right hq]304305theorem natCount_true : ∀ n, natCount (fun _ => True) n = n306  | 0 => rfl307  | n + 1 => by show natCount (fun _ => True) n + (if True then 1 else 0) = n + 1; rw [natCount_true n, ite_eq_left trivial]308309variable {p : Nat} [Pos p]310311/-- The residues of the shell satisfying `P`, counted. -/312def count (P : Shell p → Prop) [DecidablePred P] : Nat := natCount (fun x => P (ofNat x)) p313314theorem count_congr {P Q : Shell p → Prop} [DecidablePred P] [DecidablePred Q] (h : ∀ x, P x ↔ Q x) :315    count P = count Q :=316  natCount_congr _ _ p (fun x _ => h (ofNat x))317318theorem ofNat_inj {i j : Nat} (hi : i < p) (hj : j < p) (h : (ofNat i : Shell p) = ofNat j) : i = j := by319  have := val_injective h320  rw [val_ofNat, val_ofNat, FRC.Nat.mod_eq_of_lt hi, FRC.Nat.mod_eq_of_lt hj] at this321  exact this322323/-- A bijection of the residues preserves counts. -/324theorem count_bij (f g : Shell p → Shell p) (hgf : ∀ x, g (f x) = x) (P : Shell p → Prop) [DecidablePred P] :325    count (fun x => P (f x)) = count P := by326  unfold count327  rw [natCount_eq_nsum, natCount_eq_nsum]328  have e : ∀ x, x < p → (fun x => if P (f (ofNat x)) then 1 else 0) x329      = (fun y => if P (ofNat y) then 1 else 0) ((f (ofNat x)).val) := fun x _ => by330    show (if P (f (ofNat x)) then 1 else 0) = (if P (ofNat (f (ofNat x)).val) then 1 else 0)331    rw [ofNat_val]332  rw [nsum_congr p e]333  exact nsum_perm (fun y => if P (ofNat y) then 1 else 0) (fun x => (f (ofNat x)).val) p (fun x _ => (f (ofNat x)).lt)334    (fun i j hi hj h => ofNat_inj hi hj (by rw [← hgf (ofNat i), ← hgf (ofNat j), ext h]))335336/-- Exactly one residue equals `c`. -/337theorem count_eq (c : Shell p) : count (fun x => x = c) = 1 :=338  natCount_single (fun x => (ofNat x : Shell p) = c) (ofNat_val c) p c.lt339    (fun _ hx h => ofNat_inj hx c.lt (h.trans (ofNat_val c).symm))340341theorem count_true : count (fun _ : Shell p => True) = p := natCount_true p342343theorem count_false : count (fun _ : Shell p => False) = 0 := natCount_eq_zero _ p (fun _ _ h => h)344345346/-- Equivalent conditions select the same branch. -/347theorem ite_iff {α : Type} {P Q : Prop} [Decidable P] [Decidable Q] (h : P ↔ Q) (x y : α) :348    (if P then x else y) = (if Q then x else y) :=349  match (inferInstance : Decidable P) with350  | isTrue hp => by rw [ite_eq_left hp, ite_eq_left (h.1 hp)]351  | isFalse hp => by rw [ite_eq_right hp, ite_eq_right (fun hq => hp (h.2 hq))]352353theorem red1 {L T a X : Shell p} (h : L = T + a * X) (ha : a = 0) : L = T := by354  rw [h, ha, zero_mul, add_zero]355356/-! ## The registration sphere (00:E6) -/357358section frame359variable {κ : Nat} {g : Shell p}360361/-- Through `u = a + i y` (`i² = −1`) the conic row `a² + y² = c` becomes `u (2a − u) = c`: the same count. -/362theorem conic_row (F : Frame p κ g) (a c : Shell p) :363    count (fun y => a * a + y * y = c) = count (fun u => u * (a + a + -u) = c) := by364  have hi : quarterTurn g κ * quarterTurn g κ + 1 = 0 := by rw [F.quarter_turn_sq, neg_add]365  have e : ∀ i y : Shell p, i * i + 1 = 0 → (a + i * y) * (a + a + -(a + i * y)) = a * a + y * y := fun i y h =>366    red1 (Shell.Frame.RE.sound (Shell.Frame.look [a, i, y]) (.mul (.add (.var 0) (.mul (.var 1) (.var 2))) (.add (.add (.var 0) (.var 0)) (.neg (.add (.var 0) (.mul (.var 1) (.var 2)))))) (.add (.add (.mul (.var 0) (.var 0)) (.mul (.var 2) (.var 2))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.neg (.mul (.var 2) (.var 2))))) (by decide +kernel)) h367  have hP : ∀ y, a * a + y * y = c ↔ (fun u => u * (a + a + -u) = c) (a + quarterTurn g κ * y) := fun y => by368    show a * a + y * y = c ↔ (a + quarterTurn g κ * y) * (a + a + -(a + quarterTurn g κ * y)) = c369    rw [e _ y hi]370  rw [count_congr hP]371  exact count_bij (fun y => a + quarterTurn g κ * y) (fun u => (u + -a) * -(quarterTurn g κ))372    (fun y => red1 ((fun i => Shell.Frame.RE.sound (Shell.Frame.look [a, i, y]) (.mul (.add (.add (.var 0) (.mul (.var 1) (.var 2))) (.neg (.var 0))) (.neg (.var 1))) (.add (.var 2) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.neg (.var 2)))) (by decide +kernel)) (quarterTurn g κ)) hi) (fun u => u * (a + a + -u) = c)373374/-- 00:E6, 38:B6, 38:A9 — the plane conic `x² + y² = c` on every frame: `p − 1` points for `c ≠ 0`, `2p − 1` for375`c = 0`; the circle `x² + y² = 1` is the drive torus of the split fibration (38-s13). -/376theorem conic_count (F : Frame p κ g) (c : Shell p) :377    nsum (fun x => count (fun y => ofNat x * ofNat x + y * y = c)) p = (p - 1) + (if c = 0 then p else 0) := by378  rw [nsum_congr p (fun x _ => conic_row F (ofNat x) c)]379  have hswap : nsum (fun x => count (fun u => u * ((ofNat x : Shell p) + ofNat x + -u) = c)) p380      = nsum (fun u => count (fun a => (ofNat u : Shell p) * (a + a + -(ofNat u)) = c)) p := by381    unfold count382    rw [nsum_congr p (fun x _ => natCount_eq_nsum _ p), nsum_congr p (fun u _ => natCount_eq_nsum _ p)]383    exact nsum_comm (fun x u => if (ofNat u : Shell p) * (ofNat x + ofNat x + -(ofNat u)) = c then 1 else 0) p p384  rw [hswap]385  have hcol : ∀ u, u < p → count (fun a => (ofNat u : Shell p) * (a + a + -(ofNat u)) = c)386      = (fun u => if u = 0 then (if c = 0 then p else 0) else 1) u := fun u hu => by387    show _ = if u = 0 then (if c = 0 then p else 0) else 1388    match Nat.decEq u 0 with389    | isTrue e0 =>390      rw [ite_eq_left e0, e0]391      have h0 : ∀ a : Shell p, (ofNat 0 : Shell p) * (a + a + -(ofNat 0)) = c ↔ c = 0 := fun a =>392        ⟨fun h => h ▸ zero_mul _, fun h => by rw [h]; exact zero_mul _⟩393      rw [count_congr h0]394      match (inferInstance : Decidable (c = 0)) with395      | isTrue hc => rw [ite_eq_left hc, count_congr (fun _ => ⟨fun _ => trivial, fun _ => hc⟩), count_true]396      | isFalse hc => rw [ite_eq_right hc, count_congr (fun _ => ⟨fun h => hc h, fun h => h.elim⟩), count_false]397    | isFalse e0 =>398      rw [ite_eq_right e0]399      have hw : (ofNat u : Shell p) ≠ 0 := fun h => e0 (ofNat_inj hu Pos.pos h)400      have hs : (ofNat u : Shell p) + ofNat u ≠ 0 := by401        rw [← two_mul']; exact F.mul_ne_zero F.two_ne_zero hw402      obtain ⟨t, ht⟩ := F.exists_inv hs403      have h1 : ∀ a : Shell p, (ofNat u : Shell p) * (a + a + -(ofNat u)) = c ↔404          a = (c + ofNat u * ofNat u) * t := fun a => by405        constructor406        · intro h407          calc a = a * ((ofNat u + ofNat u) * t) := by rw [ht, mul_one]408            _ = (ofNat u * (a + a + -(ofNat u)) + ofNat u * ofNat u) * t :=409                (fun a w t => Shell.Frame.RE.sound (Shell.Frame.look [a, w, t]) (.mul (.var 0) (.mul (.add (.var 1) (.var 1)) (.var 2))) (.mul (.add (.mul (.var 1) (.add (.add (.var 0) (.var 0)) (.neg (.var 1)))) (.mul (.var 1) (.var 1))) (.var 2)) (by decide +kernel)) a (ofNat u) t410            _ = (c + ofNat u * ofNat u) * t := by rw [h]411        · intro h412          rw [h]413          calc (ofNat u : Shell p) * ((c + ofNat u * ofNat u) * t + (c + ofNat u * ofNat u) * t + -(ofNat u))414              = (ofNat u + ofNat u) * t * (c + ofNat u * ofNat u) + -(ofNat u * ofNat u) :=415                (fun w t X => Shell.Frame.RE.sound (Shell.Frame.look [w, t, X]) (.mul (.var 0) (.add (.add (.mul (.var 2) (.var 1)) (.mul (.var 2) (.var 1))) (.neg (.var 0)))) (.add (.mul (.mul (.add (.var 0) (.var 0)) (.var 1)) (.var 2)) (.neg (.mul (.var 0) (.var 0)))) (by decide +kernel)) (ofNat u) t (c + ofNat u * ofNat u)416            _ = c := by rw [ht, one_mul, add_assoc, add_neg, add_zero]417      rw [count_congr h1, count_eq]418  rw [nsum_congr p hcol]419  have hp : (p - 1) + 1 = p := FRC.Nat.sub_add_cancel Pos.pos420  calc nsum (fun u => if u = 0 then (if c = 0 then p else 0) else 1) p421      = nsum (fun u => if u = 0 then (if c = 0 then p else 0) else 1) ((p - 1) + 1) := by rw [hp]422    _ = (if c = 0 then p else 0) + nsum (fun _ => 1) (p - 1) := by423        rw [nsum_succ']424        exact congrArg _ (nsum_congr (p - 1) (fun l _ => ite_eq_right (Nat.succ_ne_zero l)))425    _ = (p - 1) + (if c = 0 then p else 0) := by rw [nsum_const, Nat.mul_one, Nat.add_comm]426427/-- 00:E6 — the sphere `x² + y² + z² = a` of `𝔽_p³`: `p(p − 1) + p · #{z : z² = a}` points. -/428theorem sphere_count (F : Frame p κ g) (a : Shell p) :429    nsum (fun z => nsum (fun x => count (fun y => ofNat x * ofNat x + y * y + ofNat z * ofNat z = a)) p) p430      = p * (p - 1) + p * count (fun z => z * z = a) := by431  have hz : ∀ z, z < p → nsum (fun x => count (fun y => ofNat x * ofNat x + y * y + ofNat z * ofNat z = a)) p432      = (p - 1) + (if (ofNat z : Shell p) * ofNat z = a then p else 0) := fun z _ => by433    have hc : ∀ x, count (fun y => (ofNat x : Shell p) * ofNat x + y * y + ofNat z * ofNat z = a)434        = count (fun y => (ofNat x : Shell p) * ofNat x + y * y = a + -(ofNat z * ofNat z)) := fun x =>435      count_congr (fun y => ⟨fun h => by rw [← h, add_assoc, add_neg, add_zero],436        fun h => by rw [h, add_assoc, neg_add, add_zero]⟩)437    rw [nsum_congr p (fun x _ => hc x), conic_count F]438    congr 1439    exact ite_iff ⟨fun h => by440        calc (ofNat z : Shell p) * ofNat z = ofNat z * ofNat z + (a + -(ofNat z * ofNat z)) := by rw [h, add_zero]441          _ = a := by rw [add_left_comm, add_neg, add_zero],442      fun h => by rw [h, add_neg]⟩ p 0443  rw [nsum_congr p hz, nsum_add, nsum_const]444  congr 1445  unfold count446  rw [natCount_eq_nsum, ← nsum_mul_left]447  exact nsum_congr p (fun z _ => match (inferInstance : Decidable ((ofNat z : Shell p) * ofNat z = a)) with448    | isTrue h => by rw [ite_eq_left h, ite_eq_left h, Nat.mul_one]449    | isFalse h => by rw [ite_eq_right h, ite_eq_right h, Nat.mul_zero])450451/-- A nonzero square has exactly two square roots, `±b`. -/452theorem count_sq (F : Frame p κ g) {b : Shell p} (hb : b ≠ 0) : count (fun z => z * z = b * b) = 2 := by453  have hne : b ≠ -b := fun e => by454    have h2 : b + b = 0 := by455      calc b + b = b + -b := by rw [← e]456        _ = 0 := add_neg b457    rw [← two_mul'] at h2458    exact F.mul_ne_zero F.two_ne_zero hb h2459  have h : ∀ z, z * z = b * b ↔ (z = b ∨ z = -b) := fun z => by460    constructor461    · intro hz462      have e : (z + -b) * (z + b) = 0 := by463        have e1 : (z + -b) * (z + b) = z * z + -(b * b) := (fun z b => Shell.Frame.RE.sound (Shell.Frame.look [z, b]) (.mul (.add (.var 0) (.neg (.var 1))) (.add (.var 0) (.var 1))) (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 1) (.var 1)))) (by decide +kernel)) z b464        rw [e1, hz, add_neg]465      match F.mul_eq_zero e with466      | .inl h1 => exact .inl (by467          calc z = z + -b + b := by rw [add_assoc, neg_add, add_zero]468            _ = b := by rw [h1, zero_add])469      | .inr h1 => exact .inr (eq_neg_of_add_eq_zero h1)470    · intro hz471      match hz with472      | .inl e => rw [e]473      | .inr e => rw [e, neg_mul_neg]474  rw [count_congr h]475  unfold count476  rw [natCount_or (fun x => (ofNat x : Shell p) = b) (fun x => (ofNat x : Shell p) = -b)477    (fun x h1 h2 => hne (h1.symm.trans h2))]478  show count (fun x => x = b) + count (fun x => x = -b) = 2479  rw [count_eq, count_eq]480481/-- The quadratic form `x² + y² + z²` of `𝔽_p³`. -/482def quad (x y z : Shell p) : Shell p := x * x + y * y + z * z483484/-- The points of the sphere `x² + y² + z² = a` in `𝔽_p³`, counted. -/485def sphereCount (p : Nat) [Pos p] (a : Shell p) : Nat :=486  nsum (fun z => nsum (fun x => count (fun y => quad (ofNat x) y (ofNat z) = a)) p) p487488/-- 00:E6, 38:A9 — the area of the sphere at every nonzero square rung `a = b²`: `p(p + 1)`; the unit sphere's489`p(p + 1)` points are the base of the split fibration (38-s13). -/490theorem sphere_area_rung (F : Frame p κ g) {b : Shell p} (hb : b ≠ 0) : sphereCount p (b * b) = p * (p + 1) := by491  show nsum (fun z => nsum (fun x => count (fun y => ofNat x * ofNat x + y * y + ofNat z * ofNat z = b * b)) p) p = _492  rw [sphere_count F, count_sq F hb, ← Nat.mul_add]493  have hp : (p - 1) + 1 = p := FRC.Nat.sub_add_cancel Pos.pos494  congr 1495  calc p - 1 + 2 = (p - 1 + 1) + 1 := rfl496    _ = p + 1 := by rw [hp]497498/-- 00:E6, 37:C6 — the registration sphere `x² + y² + z² = κ²` at the capacity has area `A = p(p + 1)`. -/499theorem sphere_area (F : Frame p κ g) : sphereCount p (ofNat κ * ofNat κ) = p * (p + 1) := by500  have hκ : κ < p := by501    rw [F.cap]; exact Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left κ (Nat.zero_lt_succ 3)) (Nat.lt_succ_self _)502  exact sphere_area_rung F (fun h => Nat.ne_of_gt F.cap_pos (ofNat_inj hκ Pos.pos h))503504end frame505506/-! ## The record, the response and the merger law (00:E6, 00:E7) -/507508/-- 00:E6, 00:E7, 21:C13 — the record `S = κ(p + 1) = κ(4κ + 2)` on `p = 4κ + 1`, against the area `A = p(p + 1)`:509`4S + 1 = p²` (the record law: `S = (p² − 1)/4`, the `Q₄` quotient of `𝔽_{p²}^×`, and `S = (Ω − 1)/4` at `p² = Ω`);510`S p = κ A` (`S/A = κ/p`); `4 S p = A (p − 1)` (`S = (A/4)(1 − 1/p)`). Moved here from 21-gravity's `Gravity.lean` (task511LM27), which keeps the name. -/512theorem count_identity (κ : Nat) :513    4 * (κ * (4 * κ + 2)) + 1 = (4 * κ + 1) * (4 * κ + 1) ∧514    κ * (4 * κ + 2) * (4 * κ + 1) = κ * ((4 * κ + 1) * (4 * κ + 2)) ∧515    4 * (κ * (4 * κ + 2)) * (4 * κ + 1) = ((4 * κ + 1) * (4 * κ + 2)) * (4 * κ) :=516  ⟨nat_sound (nlook [κ]) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.mul (.var 0) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)))) .one) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one)) rfl rfl (by decide +kernel),517   nat_sound (nlook [κ]) (.mul (.mul (.var 0) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one))) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one)) (.mul (.var 0) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)))) rfl rfl (by decide +kernel),518   nat_sound (nlook [κ]) (.mul (.mul (.add (.add (.add .one .one) .one) .one) (.mul (.var 0) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)))) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one)) (.mul (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one))) (.mul (.add (.add (.add .one .one) .one) .one) (.var 0))) rfl rfl (by decide +kernel)⟩519520/-- 00:E7, 37:B5 — the record on the rate face `M = (p + 1)/2 = 2κ + 1`: `S = M (M − 1)`. -/521theorem record_mass (κ : Nat) : κ * (4 * κ + 2) = (2 * κ + 1) * (2 * κ) :=522  nat_sound (nlook [κ]) (.mul (.var 0) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one))) (.mul (.add (.mul (.add .one .one) (.var 0)) .one) (.mul (.add .one .one) (.var 0))) rfl rfl (by decide +kernel)523524/-- 00:E7 — the response: `S(M) = M (M − 1)` grows as `S(M + h) = S(M) + (2M − 1) h + h²`, here with `M = m + 1`; on the525rate face `M = 2κ + 1` the coefficient `2M − 1` is `p`: `dS/dM = p` exactly, `T_resp = 1/p`. -/526theorem record_response (m h : Nat) : (m + 1 + h) * (m + h) = (m + 1) * m + (2 * m + 1) * h + h * h :=527  nat_sound (nlook [m, h]) (.mul (.add (.add (.var 0) .one) (.var 1)) (.add (.var 0) (.var 1))) (.add (.add (.mul (.add (.var 0) .one) (.var 0)) (.mul (.add (.mul (.add .one .one) (.var 0)) .one) (.var 1))) (.mul (.var 1) (.var 1))) rfl rfl (by decide +kernel)528529/-- 00:E7 — the response on the rate face `M = 2κ + 1` (`m = 2κ`): the coefficient of `h` is `p = 4κ + 1`, so530`dS/dM = p` exactly and `T_resp = 1/p`. -/531theorem record_response_rate (κ h : Nat) :532    (2 * κ + 1 + h) * (2 * κ + h) = (2 * κ + 1) * (2 * κ) + (4 * κ + 1) * h + h * h := by533  have e := record_response (2 * κ) h534  have c : 2 * (2 * κ) + 1 = 4 * κ + 1 := by rw [← FRC.Nat.mul_assoc]535  rw [c] at e536  exact e537538/-- 00:E7 — the registration rate `T = A/p³` is `(p + 1)/p²`: `A p² = (p + 1) p³`. -/539theorem temperature_rate (κ : Nat) :540    ((4 * κ + 1) * (4 * κ + 2)) * ((4 * κ + 1) * (4 * κ + 1)) = (4 * κ + 2) * ((4 * κ + 1) * (4 * κ + 1) * (4 * κ + 1)) :=541  nat_sound (nlook [κ]) (.mul (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)) (.mul (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one)) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) .one))) rfl rfl (by decide +kernel)542543/-- 00:E7 — the two Smarr relations on the rate face `M = 2κ + 1`: `2 T_resp S = M (1 − 1/p)` with `T_resp = 1/p`, that is544`2S = M (p − 1)`; and `2 T S = M (1 − 1/p²)` with `T = (p + 1)/p²`, that is `2 (p + 1) S = M (p − 1)(p + 1)`. -/545theorem smarr (κ : Nat) :546    2 * (κ * (4 * κ + 2)) = (2 * κ + 1) * (4 * κ) ∧547    2 * (4 * κ + 2) * (κ * (4 * κ + 2)) = (2 * κ + 1) * ((4 * κ) * (4 * κ + 2)) :=548  ⟨nat_sound (nlook [κ]) (.mul (.add .one .one) (.mul (.var 0) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)))) (.mul (.add (.mul (.add .one .one) (.var 0)) .one) (.mul (.add (.add (.add .one .one) .one) .one) (.var 0))) rfl rfl (by decide +kernel),549   nat_sound (nlook [κ]) (.mul (.mul (.add .one .one) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one))) (.mul (.var 0) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)))) (.mul (.add (.mul (.add .one .one) (.var 0)) .one) (.mul (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.add .one .one)))) rfl rfl (by decide +kernel)⟩550551/-- 00:E6, 37:C20 — the merger law on the count face `A = M (M + 1)`: `ΔA = 2 M₁ M₂`. -/552theorem merger_area (M₁ M₂ : Nat) :553    (M₁ + M₂) * (M₁ + M₂ + 1) = M₁ * (M₁ + 1) + M₂ * (M₂ + 1) + 2 * (M₁ * M₂) :=554  nat_sound (nlook [M₁, M₂]) (.mul (.add (.var 0) (.var 1)) (.add (.add (.var 0) (.var 1)) .one)) (.add (.add (.mul (.var 0) (.add (.var 0) .one)) (.mul (.var 1) (.add (.var 1) .one))) (.mul (.add .one .one) (.mul (.var 0) (.var 1)))) rfl rfl (by decide +kernel)555556/-! ## The register on every frame (21:A1, C2, C5, C16; 00:C1): moved from 21-gravity's `Gravity.lean`, 10 October 2026 -/557section register558variable {κ : Nat} {g : Shell p}559560/-- 21:C16, 21:A1, 38:D3 — the calibration congruence on every frame: the full cycle `2π ↦ 4κ = p − 1` is `−1`,561and `(4κ)² = 1`. -/562theorem calibration (F : Frame p κ g) :563    (ofNat (4 * κ) : Shell p) = -1 ∧ (ofNat (4 * κ) : Shell p) * ofNat (4 * κ) = 1 := by564  have h : (ofNat (4 * κ) : Shell p) = -1 := by565    have h2 := F.two_pi566    have e : 2 * Frame.halfPeriod κ = 4 * κ := (FRC.Nat.mul_assoc 2 2 κ).symm567    rw [e] at h2568    exact h2569  exact ⟨h, by rw [h, Shell.neg_mul_neg, Shell.one_mul]⟩570571/-- 21:C2, 21:C5, 21:C16 — the register value of the Newton constant on every frame, `G = 2κ`, the half-cycle:572`2G = −1`; `(−2) G = 1` (the face convention `4π ↦ −2`, `G = (−2)⁻¹`); the Gauss count `(2 · 4κ) G = 1`;573`c² = 2⁻¹ = 2κ + 1` with `2c² = 1`; and `G = −c²`. -/574theorem newton_residue (F : Frame p κ g) :575    (2 : Shell p) * ofNat (2 * κ) = -1 ∧ (-2 : Shell p) * ofNat (2 * κ) = 1 ∧576    (2 * ofNat (4 * κ) : Shell p) * ofNat (2 * κ) = 1 ∧577    (2 : Shell p) * ofNat (2 * κ + 1) = 1 ∧ (ofNat (2 * κ) : Shell p) = -ofNat (2 * κ + 1) := by578  obtain ⟨h4, _⟩ := calibration F579  have hG : (2 : Shell p) * ofNat (2 * κ) = -1 := by580    show ofNat 2 * ofNat (2 * κ) = -1581    rw [Frame.ofNat_mul, ← FRC.Nat.mul_assoc]582    exact h4583  have hG' : (-2 : Shell p) * ofNat (2 * κ) = 1 := by584    rw [← Shell.neg_mul, hG, Shell.neg_neg]585  have hc : (2 : Shell p) * ofNat (2 * κ + 1) = 1 := by586    show ofNat 2 * ofNat (2 * κ + 1) = 1587    rw [Frame.ofNat_mul, Nat.mul_add, ← FRC.Nat.mul_assoc, Nat.mul_one, ← Frame.ofNat_add, h4]588    show -1 + ofNat 2 = 1589    rw [show (ofNat 2 : Shell p) = 1 + 1 from Frame.two_eq_one_add_one, ← Shell.add_assoc, Shell.neg_add,590      Shell.zero_add]591  refine ⟨hG, hG', ?_, hc, ?_⟩592  · rw [h4, ← Shell.mul_neg, Shell.mul_one, hG']593  · apply Shell.eq_neg_of_add_eq_zero594    rw [Frame.ofNat_add, ← Nat.add_assoc, F.four_kappa, F.n_eq, ← F.cap]595    exact Frame.ofNat_self596597/-- 21:C5 — the action quantum on every frame: `ħ = g^κ` is a member of the quarter-turn pair (`−i`, the598frame's `quarterTurn` being `−g^κ`), `ħ² = −1`; with `c² = 2κ + 1` the residue `r = ħ c²` is a square root of599the capacity, `r² = κ`, and `ħ = 2r` — the paper's `ħ = 2√S` read on the shell. -/600theorem hbar_root (F : Frame p κ g) :601    (g ^ κ) ^ 2 = -1 ∧ (g ^ κ * ofNat (2 * κ + 1)) * (g ^ κ * ofNat (2 * κ + 1)) = ofNat κ ∧602    (2 : Shell p) * (g ^ κ * ofNat (2 * κ + 1)) = g ^ κ := by603  obtain ⟨hq, _⟩ := F.quarter_turn_order604  obtain ⟨_, _, _, hc, _⟩ := newton_residue F605  obtain ⟨h4, _⟩ := calibration F606  have h2r : (2 : Shell p) * (g ^ κ * ofNat (2 * κ + 1)) = g ^ κ := by607    rw [Shell.mul_left_comm, hc, Shell.mul_one]608  refine ⟨hq, ?_, h2r⟩609  -- `4 (r² − κ) = (2r)² − 4κ = ħ² + 1 = 0`, and `4 ≠ 0` on the shell610  have h4ne : (4 : Shell p) ≠ 0 := by611    rw [show (4 : Shell p) = 2 * 2 from (Frame.ofNat_mul 2 2).symm]612    exact F.mul_ne_zero F.two_ne_zero F.two_ne_zero613  have h4κ : (4 : Shell p) * ofNat κ = -1 := by614    show ofNat 4 * ofNat κ = -1615    rw [Frame.ofNat_mul]; exact h4616  have h4r : (4 : Shell p) * ((g ^ κ * ofNat (2 * κ + 1)) * (g ^ κ * ofNat (2 * κ + 1))) = -1 := by617    rw [show (4 : Shell p) = 2 * 2 from (Frame.ofNat_mul 2 2).symm, FRC.Shell.mul_mul_mul_comm, h2r,618      ← Shell.pow_two, hq]619  have key : (4 : Shell p) * ((g ^ κ * ofNat (2 * κ + 1)) * (g ^ κ * ofNat (2 * κ + 1)) + -ofNat κ) = 0 := by620    rw [Shell.left_distrib, h4r, ← Shell.mul_neg, h4κ, Shell.neg_neg]621    exact Shell.neg_add 1622  rcases F.mul_eq_zero key with h | h623  · exact absurd h h4ne624  · have := Shell.eq_neg_of_add_eq_zero h625    rw [Shell.neg_neg] at this626    exact this627628/-- 21:X1 — the closed chart on every frame: the drive's full cycle is `p − 1 = 4κ` chronons. Every nonzero residue629returns after it (`x = g^m` by the frame's generation, so `x^{4κ} = (g^{4κ})^m = 1`), the generator after no shorter630run, and the half cycle is the half-turn `g^{2κ} = −1`. The chart closes at the totality datum: its circumference, the631horizon's `2π r_H` in light time, is the full cycle (the primer). The curvature is the chart's reading of the same datum,632`Λ = 3/r_H² = 12π/(Ω − 1)` in Planck units with `S = π r_H²` and `Ω = 4S + 1` (the ledger file's check A7, over ℚ with `π` a633symbol); the register carries no value for it. -/634theorem closed_chart (F : Frame p κ g) :635    (∀ x : Shell p, x ≠ 0 → x ^ (4 * κ) = 1) ∧ g ^ (4 * κ) = 1 ∧ (∀ k, 0 < k → k < 4 * κ → g ^ k ≠ 1) ∧636    g ^ (2 * κ) = -1 := by637  have e : 4 * κ = p - 1 := F.n_eq.symm638  refine ⟨fun x hx => ?_, ?_, fun k hk hk' => ?_, F.half_period⟩639  · have hv : 0 < x.val := Nat.pos_of_ne_zero (fun h0 => hx (Shell.ext h0))640    obtain ⟨m, _, hm⟩ := F.generates x.val x.lt hv641    rw [← Shell.ext hm, Shell.pow_mul_comm, e, F.pow_n, Shell.one_pow]642  · rw [e]; exact F.pow_n643  · rw [e] at hk'; exact F.prim.2 k hk' hk644645end register646647/-- 21:A9, 38:C7 — the two-face count: the angular face `κ/S` against the temporal face `κ/(2S)` has ratio `2`648(`κ · 2S = 2 · κS`), and the registration fibre product has `(p − 1)(Ω − 1) = 4 · 4κS` for `p = 4κ + 1`,649`Ω = 4S + 1`. -/650theorem two_face_count (κ S : Nat) :651    κ * (2 * S) = 2 * (κ * S) ∧ (4 * κ) * (4 * S) = 4 * (4 * (κ * S)) := by652  refine ⟨Nat.mul_left_comm κ 2 S, ?_⟩653  rw [Nat.mul_assoc 4 κ, Nat.mul_left_comm κ 4]654655/-! ## The values decided by the kernel (21:C2, C5, C13, C16): moved from 21-gravity's `Gravity.lean`, 10 October 2026 -/656section values657658/-- 21:C2, 21:C5, 21:C16 — the register on `𝔽₁₃` (`κ = 3`, drive `2`): `4κ = 12 = −1`, `G = 6` with659`2G = −1`, `c² = 7` with `2c² = 1`, `ħ = 2³ = 8 = −i` with `ħ² = −1` (the frame's `quarterTurn` is `5`), the root `r = 8 · 7 = 4` with `r² = 3 = κ` and660`2r = ħ`; and on `𝔽₁₇` (`κ = 4`, drive `3`): `4κ = 16 = −1`, `G = 8`, `c² = 9`, `ħ = 3⁴ = 13 = −i` (`quarterTurn`661`4`), `r = 15` with `r² = 4 = κ`, `2r = 13`. -/662theorem register13_17 :663    (12 : Shell 13) = -1 ∧ 2 * (6 : Shell 13) = -1 ∧ 2 * (7 : Shell 13) = 1 ∧ (6 : Shell 13) = -7 ∧664    (2 : Shell 13) ^ 3 = 8 ∧ (8 : Shell 13) * 8 = -1 ∧ (4 : Shell 13) * 4 = 3 ∧ 2 * (4 : Shell 13) = 8 ∧665    (16 : Shell 17) = -1 ∧ 2 * (8 : Shell 17) = -1 ∧ 2 * (9 : Shell 17) = 1 ∧ (8 : Shell 17) = -9 ∧666    (3 : Shell 17) ^ 4 = 13 ∧ (13 : Shell 17) * 13 = -1 ∧ (15 : Shell 17) * 15 = 4 ∧667    2 * (15 : Shell 17) = 13 := by decide +kernel668669/-- 21:C13 — the merger law's instance on the count face `A = M(M + 1)`: `27 811 + 1 596 → 29 407` gives670`ΔA = 2 · 27 811 · 1 596 = 88 772 712`. -/671theorem merger_instance :672    29407 * (29407 + 1) = 27811 * (27811 + 1) + 1596 * (1596 + 1) + 88772712 ∧673    2 * (27811 * 1596) = 88772712 ∧ 27811 + 1596 = 29407 := by decide674675/-- 21:C2, 21:C5, 21:C16 — the laboratory Carrier `Ω = 2 408 561` (`S = 602 140`), host-decided: `4S = 2 408 560 = −1`676and `(4S)² = 1` (the calibration congruence); `G = 1 204 280 = 2S` with `2G = −1`, `(−2) G = 1` and the Gauss677count `(2 · 4S) G = 1`; `ħ = 18 688` with `ħ² = −1`, `ħ = 2 · 9 344` and `9 344² = S`. -/678theorem lab_register :679    4 * 602140 = 2408560 ∧ (2408560 : Shell 2408561) = -1 ∧680    (2408560 : Shell 2408561) * 2408560 = 1 ∧681    2 * (1204280 : Shell 2408561) = -1 ∧ (-2 : Shell 2408561) * 1204280 = 1 ∧682    (2 * (2408560 : Shell 2408561)) * 1204280 = 1 ∧683    (18688 : Shell 2408561) * 18688 = -1 ∧ 2 * (9344 : Shell 2408561) = 18688 ∧684    (9344 : Shell 2408561) * 9344 = 602140 := by decide +kernel685686end values687688/-! ## The registered adjacency chart: the counting obstruction (00:E11; master T1 obstructed, 15 October 2026) -/689section chart690691/-- 00:E11 — the planar count: a homogeneous chart on `Ω` cells that is `Z²`-flat to radius `R` holds the `ℓ¹` ball692`2R² + 2R + 1`; with `Ω < (R+1)²` (the horizon radius `R = ⌊√Ω⌋`) the ball overflows the totality:693`(R+1)² ≤ 2R² + 2R + 1`. -/694theorem chart_plane_overflows (R Ω : Nat) (h : Ω < (R + 1) * (R + 1)) : Ω < 2 * (R * R) + 2 * R + 1 := by695  have e : (R + 1) * (R + 1) = R * R + 2 * R + 1 := by696    rw [Nat.add_mul, Nat.mul_add, Nat.mul_add, Nat.one_mul, Nat.mul_one, Nat.one_mul, Nat.two_mul, Nat.add_assoc,697      Nat.add_assoc, ← Nat.add_assoc R R 1]698  have hle : R * R + 2 * R + 1 ≤ 2 * (R * R) + 2 * R + 1 := by699    rw [Nat.two_mul (R * R)]700    exact Nat.add_le_add_right (Nat.add_le_add_right (Nat.le_add_left (R * R) (R * R)) (2 * R)) 1701  exact Nat.lt_of_lt_of_le (e ▸ h) hle702703/-- 00:E11 — the spatial count: three times the `ℓ¹` ball of `Z³` at radius `R` is the integer `4R³ + 6R² + 8R + 3`;704with `Ω < (R+1)²` it exceeds `3Ω`: `3(R+1)² = 3R² + 6R + 3 ≤ 4R³ + 6R² + 8R + 3`. So no homogeneous chart on the705`Ω` residues is `Z³`-flat to the horizon radius. -/706theorem chart_space_overflows (R Ω : Nat) (h : Ω < (R + 1) * (R + 1)) :707    3 * Ω < 4 * (R * R * R) + 6 * (R * R) + 8 * R + 3 := by708  have e : 3 * ((R + 1) * (R + 1)) = 3 * (R * R) + 6 * R + 3 := by709    have e1 : (R + 1) * (R + 1) = R * R + 2 * R + 1 := by710      rw [Nat.add_mul, Nat.mul_add, Nat.mul_add, Nat.one_mul, Nat.mul_one, Nat.one_mul, Nat.two_mul, Nat.add_assoc,711        Nat.add_assoc, ← Nat.add_assoc R R 1]712    rw [e1, Nat.mul_add, Nat.mul_add, ← Nat.mul_assoc 3 2 R]713  have h3 : 3 * Ω < 3 * ((R + 1) * (R + 1)) := Nat.mul_lt_mul_of_pos_left h (Nat.zero_lt_succ 2)714  have hle : 3 * (R * R) + 6 * R + 3 ≤ 4 * (R * R * R) + 6 * (R * R) + 8 * R + 3 := by715    have a1 : 3 * (R * R) ≤ 6 * (R * R) := Nat.mul_le_mul_right (R * R) (by decide : 3 ≤ 6)716    have a2 : 6 * R ≤ 8 * R := Nat.mul_le_mul_right R (by decide : 6 ≤ 8)717    have a3 : 3 * (R * R) + 6 * R + 3 ≤ 6 * (R * R) + 8 * R + 3 :=718      Nat.add_le_add_right (Nat.add_le_add a1 a2) 3719    have a4 : 6 * (R * R) + 8 * R + 3 ≤ 4 * (R * R * R) + 6 * (R * R) + 8 * R + 3 := by720      rw [Nat.add_assoc (4 * (R * R * R)), Nat.add_assoc (4 * (R * R * R))]721      exact Nat.le_add_left _ _722    exact Nat.le_trans a3 a4723  exact Nat.lt_of_lt_of_le (e ▸ h3) hle724725/-- 00:E11 — the linear count fits: the `ℓ¹` ball of `Z¹` at radius `R`, `2R + 1`, is at most `Ω` when `R² ≤ Ω`,726`5 ≤ Ω` and `2 ≤ R` — the scale-time direction the drive induces is the one direction flat to the horizon radius. -/727theorem chart_line_fits (R Ω : Nat) (hR : R * R ≤ Ω) (h5 : 5 ≤ Ω) (h2 : 2 ≤ R) : 2 * R + 1 ≤ Ω := by728  cases R with729  | zero => exact absurd h2 (by decide)730  | succ r =>731    cases r with732    | zero => exact absurd h2 (by decide)733    | succ r' =>734      cases r' with735      | zero => exact h5736      | succ r'' =>737        have : 2 * (r'' + 3) + 1 ≤ (r'' + 3) * (r'' + 3) := by738          have e : (r'' + 3) * (r'' + 3) = r'' * r'' + 6 * r'' + 9 := by739            rw [Nat.add_mul, Nat.mul_add, Nat.mul_add, Nat.mul_comm r'' 3, ← Nat.add_assoc, Nat.add_assoc (r'' * r''),740              ← Nat.two_mul, ← Nat.mul_assoc]741          rw [e]742          have b1 : 2 * (r'' + 3) + 1 = 2 * r'' + 7 := by rw [Nat.mul_add]743          rw [b1]744          have c1 : 2 * r'' ≤ r'' * r'' + 6 * r'' :=745            Nat.le_trans (Nat.mul_le_mul_right r'' (by decide : 2 ≤ 6)) (Nat.le_add_left _ _)746          exact Nat.add_le_add c1 (by decide : 7 ≤ 9)747        exact Nat.le_trans this hR748749/-- 00:E11 — the laboratory Carrier `Ω = 2 408 561`, `R = 1551` (`1551² ≤ Ω < 1552²`): the spatial ball fits at750`R = 121` and overflows at `122` (`2 391 687 ≤ Ω < 2 451 225`), the planar ball fits at `1096` and overflows at `1097`,751the linear ball fits at the horizon radius (`3103 ≤ Ω`). -/752theorem chart_lab_instance :753    1551 * 1551 ≤ 2408561 ∧ 2408561 < 1552 * 1552 ∧754    (4 * (121 * 121 * 121) + 6 * (121 * 121) + 8 * 121 + 3) / 3 = 2391687 ∧ 2391687 ≤ 2408561 ∧755    (4 * (122 * 122 * 122) + 6 * (122 * 122) + 8 * 122 + 3) / 3 = 2451225 ∧ 2408561 < 2451225 ∧756    2 * (1096 * 1096) + 2 * 1096 + 1 ≤ 2408561 ∧ 2408561 < 2 * (1097 * 1097) + 2 * 1097 + 1 ∧757    2 * 1551 + 1 ≤ 2408561 := by decide758759end chart760761end FRC.Grav762