Theme/Dirac.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Orbit3import FrcCore.Sum4import FrcCore.Instances5import FrcCore.Theme.Extension67/-!8# The Dirac theme — the square-class arithmetic, the coefficient field and the worked shells, no axioms910The finite content of *Schrödinger and Dirac Dynamics over Finite Substrate* (8-dirac, tree `8-dirac-20260709`;11the paper module `FrcCore/Dirac.lean` since the migration of 1 November 2026) from first principles, on every frame12`(τ; 0, 1, g)` of capacity `κ`, `p = 4κ + 1`: the square class is chronon parity — a residue `g^m` is a square13exactly when `m` is even (B5); the drive `g` and its inverse `g^{p−2}` are nonsquares, the quarter-turn14`i = −g^κ = g^{3κ}` is a square exactly when `κ` is even, and `2`, `2⁻¹`, `−2` are squares exactly when `κ` is15even — so on every κ-even shell the drive is the only nonsquare among the frame's named residues (B3); the16factorisation `ν = g = 2⁻¹·(2g)` on every shell, the cofactor `2g` a square exactly when `κ` is odd, the product17odd always (B4); the coefficient field `K = 𝔽_p[w]/(w² − ν)` on components with its conjugation and norm,18`z z̄ = N(z)`, `N(gz) = g² N(z)` (B6); the latitude identities `4κ ≡ −1`, `κ = −4⁻¹`, `1 + κ = 3·4⁻¹`, `2κ = −2⁻¹`,19`g^κ = −i` and the ladder `κ < κ + 1 ≤ 2κ` (F2); the drive's spectrum on the characters — the eigenvalue20`g^{(p−2)k}` inverse to `g^k`, the isotropy `Σ_j g^{2jk} = 0` unless `(p − 1) ∣ 2k`, and the two exceptional21lines `k = 0, 2κ` with eigenvalues `±1` (F3, F6); the sector separation — `g^{p−2}` primitive of order `p − 1`,22and `u² = 1 ⇒ u = ±1`, the meeting of the drive cycle and the norm-one cycle (F4, F6, X1). Decided by the kernel23on the laboratory Subjects `𝔽₁₃`, `𝔽₁₇₃` and `𝔽₁₅₄₉` (all with the drive `2`; the standard set of 5 November 2026, the24shell `𝔽₅` dropped): the Clifford relations, the spin conjugation with `A = 10`, `B = 2` on `𝔽₁₃`, `A = 170`, `B = 2` on25`𝔽₁₇₃` and `A = 1546`, `B = 2` on `𝔽₁₅₄₉`, the transported gammas (D2, D6, D7, D12); the spinor twist `X = γ⁰γ¹γ³` with `X² = ν`, its commutations, `(γ^μ)† X = −X γ^μ` and the failure of26the `γ⁰`-twist (D9, X4); the norm-one cycle `|N¹| = 14` on `𝔽₁₃` and `174` on `𝔽₁₇₃`, an order-three element on27`𝔽₁₇₃` and none on `𝔽₁₃` (D5, D12); the Cayley step of `H = −Δ` on `𝔽₁₃`, `U¹³ = I ≠ U` at `α = w` and `α = 6w`28(C6, E4); the potential propagators of order `14` on `𝔽₁₃` and `174` on `𝔽₁₇₃`, the least common multiple of the29phase orders (E4); the power-map image counts on `𝔽₁₃` (E2); the zero counts `2353`, `2041` on `𝔽₁₃` (B7); the unit-norm circle of `p − 1` points (F2); the named residues of the two Subjects (B3,30D12); the laboratory Carrier's `c = 171 106` with `c² = 2⁻¹` and `2⁻¹·12 = 6` (B4). Every declaration is checked31to depend on no axiom (`check_core_axioms.py`).3233Since the ledger migration (task LM17) the coefficient field is the extension theme's `FRC.Extension.Ext p ν`34(`Theme/Extension.lean`) and chronon parity is the frame theme's (`Orbit.lean`); every old name stays as an alias.35-/3637namespace FRC.Dirac3839open FRC.Shell4041section42open FRC.Extension43open FRC.Shell.Frame (two_mul_mod mod_two_of_mod_four_mul mod_n_mod_two parity_iff drive_nonsquare mod_two_cases succ_mod_two_eq_zero_iff inv_drive_odd inv_drive_nonsquare)4445/-! ## The square class is chronon parity (8:B5, B3, B4) -/46section parity47variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}4849/-- 8:B3 — the quarter-turn is `g^{3κ}` (`i = −g^κ`, `−1 = g^{2κ}`). -/50theorem quarterTurn_eq_pow (F : Frame p κ g) : Frame.quarterTurn g κ = g ^ (3 * κ) := by51  unfold Frame.quarterTurn52  rw [← Shell.neg_one_mul, ← F.half_period, ← Shell.pow_add]53  show g ^ (2 * κ + κ) = g ^ (3 * κ)54  rw [show 2 * κ + κ = 3 * κ from (Nat.succ_mul 2 κ).symm]5556/-- 8:B3 — `i` is a square exactly when the capacity is even (the eighth root of unity exists iff57`8 ∣ p − 1`). -/58theorem quarter_class (F : Frame p κ g) :59    (∃ y : Shell p, y * y = Frame.quarterTurn g κ) ↔ κ % 2 = 0 := by60  rw [quarterTurn_eq_pow F]61  refine (parity_iff F (3 * κ)).trans ?_62  have : 3 * κ = 2 * κ + κ := (Nat.succ_mul 2 κ)63  rw [this, FRC.Nat.add_mul_mod_self_left κ κ 2 (Nat.zero_lt_succ 1)]6465/-- 8:B3 — `2`, `2⁻¹` and `−2` are squares exactly when the capacity is even (the second supplementary66law at tier 0, 14-entropy's `two_is_square_iff`, and `−1 = (g^κ)²`). -/67theorem two_class (F : Frame p κ g) {h : Shell p} (hh : 2 * h = 1) :68    ((∃ r : Shell p, r * r = 2) ↔ κ % 2 = 0) ∧ ((∃ r : Shell p, r * r = h) ↔ κ % 2 = 0) ∧69    ((∃ r : Shell p, r * r = -2) ↔ κ % 2 = 0) := by70  have key : (∃ r : Shell p, r * r = 2) ↔ κ % 2 = 0 := by71    refine (FRC.Shell.Frame.two_is_square_iff F).trans ?_72    constructor73    · rintro ⟨m, hm⟩; rw [hm]; exact two_mul_mod m74    · intro h075      match FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) κ with76      | ⟨q, hq⟩ => exact ⟨q, by rw [h0, Nat.add_zero] at hq; exact hq⟩77  have hsq : (g ^ κ) * (g ^ κ) = -1 := by rw [← Shell.pow_two]; exact (F.quarter_turn_order).178  refine ⟨key, ?_, ?_⟩79  · refine Iff.trans ?_ key80    constructor81    · rintro ⟨r, hr⟩82      refine ⟨2 * r, ?_⟩83      rw [FRC.Shell.mul_mul_mul_comm, hr, Shell.mul_assoc, hh, Shell.mul_one]84    · rintro ⟨r, hr⟩85      refine ⟨r * h, ?_⟩86      rw [FRC.Shell.mul_mul_mul_comm, hr]87      calc (2 : Shell p) * (h * h) = 2 * h * h := (Shell.mul_assoc _ _ _).symm88        _ = h := by rw [hh, Shell.one_mul]89  · refine Iff.trans ?_ key90    constructor91    · rintro ⟨r, hr⟩92      refine ⟨g ^ κ * r, ?_⟩93      rw [FRC.Shell.mul_mul_mul_comm, hsq, hr, Shell.neg_mul_neg, Shell.one_mul]94    · rintro ⟨r, hr⟩95      refine ⟨g ^ κ * r, ?_⟩96      rw [FRC.Shell.mul_mul_mul_comm, hsq, hr, Shell.neg_one_mul]9798/-- 8:B4, 8:X2 — the factorisation of the temporal coefficient: `ν = g = 2⁻¹·(2g)` exactly on every shell99(`h = 2⁻¹`), and the cofactor `2g` is a square exactly when `κ` is odd — the product `g` odd always (Corollary100`coefficient-factors`); the one-way coefficient is the odd step `g`, the two-way constant the Carrier's. -/101theorem nu_factorisation (F : Frame p κ g) {h : Shell p} (hh : 2 * h = 1) :102    h * (2 * g) = g ∧ ((∃ y : Shell p, y * y = 2 * g) ↔ κ % 2 = 1) := by103  refine ⟨by rw [← Shell.mul_assoc, Shell.mul_comm h 2, hh, Shell.one_mul], ?_⟩104  obtain ⟨m, _, hm⟩ := F.eq_pow_of_ne_zero F.two_ne_zero105  have h2g : (2 : Shell p) * g = g ^ (m + 1) := by rw [Shell.pow_succ, hm]106  rw [h2g]107  refine (parity_iff F (m + 1)).trans ((succ_mod_two_eq_zero_iff m).trans ?_)108  have hm2 : (∃ r : Shell p, r * r = 2) ↔ m % 2 = 0 := by rw [← hm]; exact parity_iff F m109  replace hm2 : κ % 2 = 0 ↔ m % 2 = 0 := (two_class F hh).1.symm.trans hm2110  constructor111  · intro h1112    rcases mod_two_cases κ with hk | hk113    · exact absurd (hm2.1 hk) (by rw [h1]; exact fun e => Nat.noConfusion e)114    · exact hk115  · intro h1116    rcases mod_two_cases m with hm' | hm'117    · exact absurd (hm2.2 hm') (by rw [h1]; exact fun e => Nat.noConfusion e)118    · exact hm'119120end parity121122/-! ## The latitude identities (8:F2) -/123section latitude124variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}125126/-- 8:F2 — the ladder `1, …, 2κ`: `κ + 1`, the first rung past the midpoint `κ`, is still a rung. -/127theorem ladder (F : Frame p κ g) : κ + 1 ≤ 2 * κ := by128  rw [Nat.two_mul]; exact Nat.add_le_add_left F.cap_pos κ129130/-- 8:F2 — `4κ ≡ −1` on the shell (`4κ = p − 1`), so `κ = −4⁻¹` and the energy radius `1 + κ = 3·4⁻¹`. -/131theorem four_kappa (F : Frame p κ g) {q : Shell p} (hq : 4 * q = 1) :132    (4 : Shell p) * ofNat κ = -1 ∧ (ofNat κ : Shell p) = -q ∧ (1 : Shell p) + ofNat κ = 3 * q := by133  have h4 : (4 : Shell p) * ofNat κ = -1 := by134    have := F.two_pi135    unfold Frame.halfPeriod at this136    rw [← FRC.Nat.mul_assoc, ← Frame.ofNat_mul] at this137    exact this138  have hk : (ofNat κ : Shell p) = -q := by139    calc (ofNat κ : Shell p) = 1 * ofNat κ := (Shell.one_mul _).symm140      _ = 4 * q * ofNat κ := by rw [hq]141      _ = q * (4 * ofNat κ) := by rw [Shell.mul_comm 4 q, Shell.mul_assoc]142      _ = -q := by rw [h4, ← Shell.mul_neg, Shell.mul_one]143  refine ⟨h4, hk, ?_⟩144  have h3 : (4 : Shell p) = 3 + 1 :=145    Shell.ext (by rw [Shell.val_add, Shell.val_lit, Shell.val_lit, Shell.val_one,146      FRC.Nat.mod_add_mod _ _ _ Shell.hp, FRC.Nat.add_mod_mod _ _ _ Shell.hp])147  rw [hk, ← hq, h3, Shell.right_distrib, Shell.one_mul, Shell.add_assoc, Shell.add_neg, Shell.add_zero]148149/-- 8:F2 — the terminal latitude: `π = 2κ = −2⁻¹`; the quarter-cycle shift `m ↦ m + κ` on the150ladder is multiplication by `g^κ = −i` (`quarterTurn_eq_pow`, `i = −g^κ` by definition). -/151theorem terminal_latitude (F : Frame p κ g) {h : Shell p} (hh : 2 * h = 1) :152    (ofNat (2 * κ) : Shell p) = -h := by153  have h2 : (2 : Shell p) * ofNat (2 * κ) = -1 := by154    have := F.two_pi155    unfold Frame.halfPeriod at this156    rw [← Frame.ofNat_mul] at this157    exact this158  calc (ofNat (2 * κ) : Shell p) = 1 * ofNat (2 * κ) := (Shell.one_mul _).symm159    _ = 2 * h * ofNat (2 * κ) := by rw [hh]160    _ = h * (2 * ofNat (2 * κ)) := by rw [Shell.mul_comm 2 h, Shell.mul_assoc]161    _ = -h := by rw [h2, ← Shell.mul_neg, Shell.mul_one]162163end latitude164165/-! ## The free evolution is the drive (8:F3) and the two sectors (8:F4) -/166section drive167variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}168169/-- 8:F3, 8:F6 — the drive pullback on the characters: with `y = g⁻¹`, `χ_k(g^{j}) = y^k · χ_k(g^{j+1})` for every170`j, k` — the winding-`k` mode acquires the phase `g^{−k}` per chronon, so the drive is semisimple with the whole171drive cycle as its spectrum (Theorem `zonal` (2), Proposition `two-spectra`). -/172theorem drive_eigen {y : Shell p} (hy : g * y = 1) (j k : Nat) :173    y ^ k * g ^ ((j + 1) * k) = g ^ (j * k) := by174  rw [Nat.add_mul, Nat.one_mul, Shell.pow_add, Shell.mul_comm (g ^ (j * k)), ← Shell.mul_assoc,175    ← Shell.mul_pow, Shell.mul_comm y g, hy, Shell.one_pow, Shell.one_mul]176177/-- 8:F3 — the exceptional eigenvalue: `k = 2κ` gives `g^{−2κ} = −1` (and `k = 0` gives `1`) — the178intersection `N¹ ∩ μ_{p−1} = {±1}` of the norm-one torus with the phase cycle. -/179theorem exceptional_eigen (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) : y ^ (2 * κ) = -1 := by180  have h1 : y ^ (2 * κ) * g ^ (2 * κ) = 1 := by181    rw [← Shell.mul_pow, Shell.mul_comm y g, hy, Shell.one_pow]182  rw [F.half_period] at h1183  calc y ^ (2 * κ) = y ^ (2 * κ) * (-1 * -1) := by rw [Shell.neg_mul_neg, Shell.one_mul, Shell.mul_one]184    _ = y ^ (2 * κ) * -1 * -1 := (Shell.mul_assoc _ _ _).symm185    _ = -1 := by rw [h1, Shell.one_mul]186187/-- 8:F3 — isotropy: the character line `χ_k` is isotropic, `Σ_j χ_k(g^j)² = Σ_j g^{2jk} = 0`, unless188`(p − 1) ∣ 2k`; on the two exceptional lines the sum is `p − 1 = −1 ≠ 0` (Theorem `zonal` (3)). -/189theorem isotropy (F : Frame p κ g) (k : Nat) :190    ((2 * k) % (p - 1) ≠ 0 → sumRange (fun j => g ^ (j * k) * g ^ (j * k)) (p - 1) = 0) ∧191    ((2 * k) % (p - 1) = 0 → sumRange (fun j => g ^ (j * k) * g ^ (j * k)) (p - 1) = -1) := by192  have e : ∀ j, g ^ (j * k) * g ^ (j * k) = (g ^ (2 * k)) ^ j := fun j => by193    rw [← Shell.pow_add, ← Shell.pow_mul]194    show g ^ (j * k + j * k) = g ^ (2 * k * j)195    rw [← Nat.two_mul, Nat.mul_assoc 2 k j, Nat.mul_comm k j]196  rw [sum_congr (p - 1) (fun j _ => e j)]197  constructor198  · intro hk199    have hx : g ^ (2 * k) ≠ 1 := fun h1 => hk (F.mod_eq_zero_of_pow_eq_one h1)200    have hn : (g ^ (2 * k)) ^ (p - 1) = 1 := by rw [Shell.pow_mul_comm, F.pow_n, Shell.one_pow]201    exact Frame.geom_sum_eq_zero F (p - 1) hn hx202  · intro hk203    rw [sum_congr (p - 1) (fun j _ => by rw [F.pow_eq_one_of_mod hk, Shell.one_pow]),204      sum_const, Shell.mul_one]205    exact Frame.ofNat_n F206207/-- 8:F4, 8:F6, 8:X1, 8:E8 — sector separation: the inverse of the drive is primitive of order `p − 1` (`ord(g⁻¹) = p − 1`,208so the free evolution is no Cayley step, whose scalar phases have order dividing `p + 1`), and the norm-one209cycle meets the base field in `{±1}` alone (`u² = 1 ⇒ u = ±1`): the two spectra meet in the two signs. -/210theorem sector_separation (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :211    IsPrimitive y (p - 1) ∧ ∀ u : Shell p, u * u = 1 → u = 1 ∨ u = -1 := by212  refine ⟨⟨?_, fun l hl hl0 h1 => ?_⟩, fun u hu => F.sq_eq_one hu⟩213  · rw [← Shell.one_pow (p - 1), ← hy, Shell.mul_pow, F.pow_n, Shell.one_mul]214  · have h2 : g ^ l = 1 := by215      calc g ^ l = g ^ l * 1 := (Shell.mul_one _).symm216        _ = g ^ l * y ^ l := by rw [h1]217        _ = 1 := by rw [← Shell.mul_pow, hy, Shell.one_pow]218    exact F.prim.2 l hl hl0 h2219220end drive221222/-! ## The worked shells, decided by the kernel -/223section decided224variable {p : Nat} [Pos p]225226/-- `Σ_{a<p} Σ_{b<p} [f a b]`, the count of pairs of residues satisfying `f`. -/227def count2 (p : Nat) (f : Nat → Nat → Bool) : Nat :=228  (List.range p).foldl (fun acc a => (List.range p).foldl (fun acc b => if f a b then acc + 1 else acc) acc) 0229230/-- The count of quadruples of residues satisfying `f`. -/231def count4 (p : Nat) (f : Nat → Nat → Nat → Nat → Bool) : Nat :=232  (List.range p).foldl (fun acc a => (List.range p).foldl (fun acc b => (List.range p).foldl (fun acc c =>233    (List.range p).foldl (fun acc d => if f a b c d then acc + 1 else acc) acc) acc) acc) 0234235/-- 8:D5 — the number of points of the norm-one torus `N¹ = {a² − ν b² = 1}` on the shell. -/236def normOneCount (p : Nat) [Pos p] (ν : Shell p) : Nat :=237  count2 p fun a b => decide (Ext.norm (⟨ofNat a, ofNat b⟩ : Ext p ν) = 1)238239/-- 8:F2 — the number of points of the unit-norm circle `a² + b² = 1` of the framed-complex chart. -/240def unitCircleCount (p : Nat) [Pos p] : Nat :=241  count2 p fun a b => decide ((ofNat a : Shell p) * ofNat a + ofNat b * ofNat b = 1)242243/-- 8:B7 — the zero count of the Euclidean form `t² + x² + y² + z²`. -/244def euclidZeros (p : Nat) [Pos p] : Nat :=245  count4 p fun t x y z => decide ((ofNat t : Shell p) * ofNat t + ofNat x * ofNat x + ofNat y * ofNat y +246    ofNat z * ofNat z = 0)247248/-- 8:B7 — the zero count of the Lorentzian form `−ν t² + x² + y² + z²`. -/249def lorentzZeros (p : Nat) [Pos p] (ν : Shell p) : Nat :=250  count4 p fun t x y z => decide (-(ν * ((ofNat t : Shell p) * ofNat t)) + ofNat x * ofNat x +251    ofNat y * ofNat y + ofNat z * ofNat z = 0)252253/-- 8:B7 [value] — on `𝔽₁₃` the Euclidean form has `13³ + 13² − 13 = 2353` zeros and the Lorentzian form (`ν = g = 2`)254has `13³ − 13² + 13 = 2041`: the hyperbolic and the elliptic form part on the base shell. -/255theorem zeros13 : euclidZeros 13 = 2353 ∧ lorentzZeros 13 2 = 2041 := by decide +kernel256257/-- 8:D5, 8:D12, 8:D19, 8:C5, 8:F2, 8:F6 [value] — the norm-one cycle: `|N¹| = 14 = p + 1` on `𝔽₁₃` and `174` on `𝔽₁₇₃`258(both `ν = g = 2`); the unit-norm circle of the chart has `p − 1` points: `12` and `172` (8:F2). -/259theorem torus_counts :260    normOneCount 13 2 = 14 ∧ normOneCount 173 2 = 174 ∧ unitCircleCount 13 = 12 ∧ unitCircleCount 173 = 172 := by261  decide +kernel262263end decided264265/-! ## Matrices over the coefficient field, the gammas and the Cayley step, decided by the kernel -/266section matrices267variable {p : Nat} [Pos p] {ν : Shell p}268269/-- A matrix over `K` as a list of rows. -/270abbrev Mat (p : Nat) [Pos p] (ν : Shell p) := List (List (Ext p ν))271272namespace Mat273274/-- The `j`-th element of a list, `d` beyond its end (structural; Lean's `List.getD` carries `propext`). -/275def nth {α : Type} (d : α) : List α → Nat → α276  | [], _ => d277  | a :: _, 0 => a278  | _ :: l, n + 1 => nth d l n279def dot (r c : List (Ext p ν)) : Ext p ν := (List.zipWith (· * ·) r c).foldl (· + ·) 0280def col (A : Mat p ν) (j : Nat) : List (Ext p ν) := A.map fun r => nth 0 r j281def transpose (A : Mat p ν) : Mat p ν := (List.range (A.headD []).length).map (col A)282def mul (A B : Mat p ν) : Mat p ν :=283  let Bt := transpose B284  A.map fun r => Bt.map fun c => dot r c285def add (A B : Mat p ν) : Mat p ν := List.zipWith (fun r s => List.zipWith (· + ·) r s) A B286def neg (A : Mat p ν) : Mat p ν := A.map fun r => r.map (- ·)287def smul (c : Ext p ν) (A : Mat p ν) : Mat p ν := A.map fun r => r.map (c * ·)288def ident (n : Nat) : Mat p ν := (List.range n).map fun i => (List.range n).map fun j => if i = j then 1 else 0289/-- Powers by squaring. -/290def pow (A : Mat p ν) (n : Nat) : Nat → Mat p ν291  | 0 => ident n292  | e + 1 => mul (pow A n e) A293/-- The conjugate transpose (Frobenius on the entries). -/294def dagger (A : Mat p ν) : Mat p ν := (transpose A).map fun r => r.map Ext.conj295296instance : Mul (Mat p ν) := ⟨mul⟩297instance : Add (Mat p ν) := ⟨add⟩298instance : Neg (Mat p ν) := ⟨neg⟩299300end Mat301302open Mat303304/-- The gamma matrices of `(eq:gamma-definition)` over `K`, given the quarter-turn `i` of the shell:305`γ⁰ = i w β`, `γ^k = i ρ^k` (with `i² = −1`, so `γ²`'s entries are `∓i² = ±1`). -/306def gamma0 (i : Shell p) : Mat p ν :=307  let iw : Ext p ν := ⟨0, i⟩308  [[0, 0, iw, 0], [0, 0, 0, iw], [iw, 0, 0, 0], [0, iw, 0, 0]]309def gamma1 (i : Shell p) : Mat p ν :=310  let ii : Ext p ν := ⟨i, 0⟩311  [[0, 0, 0, ii], [0, 0, ii, 0], [0, -ii, 0, 0], [-ii, 0, 0, 0]]312def gamma2 (i : Shell p) : Mat p ν :=313  let ii : Ext p ν := ⟨i, 0⟩314  [[0, 0, 0, -(ii * ii)], [0, 0, ii * ii, 0], [0, ii * ii, 0, 0], [-(ii * ii), 0, 0, 0]]315def gamma3 (i : Shell p) : Mat p ν :=316  let ii : Ext p ν := ⟨i, 0⟩317  [[0, 0, ii, 0], [0, 0, 0, -ii], [-ii, 0, 0, 0], [0, ii, 0, 0]]318def gamma (i : Shell p) : Nat → Mat p ν319  | 0 => gamma0 i320  | 1 => gamma1 i321  | 2 => gamma2 i322  | _ => gamma3 i323/-- `η = diag(−ν, 1, 1, 1)`. -/324def eta (ν : Shell p) : Nat → Nat → Ext p ν325  | 0, 0 => -(⟨ν, 0⟩ : Ext p ν)326  | 1, 1 => 1327  | 2, 2 => 1328  | 3, 3 => 1329  | _, _ => 0330331/-- 8:D2 — the Clifford relations `γ^μ γ^ν + γ^ν γ^μ = 2 η_{μν} I₄`, all sixteen. -/332def clifford (ν : Shell p) (i : Shell p) : Bool :=333  (List.range 4).all fun μ => (List.range 4).all fun μ' =>334    decide (gamma i μ * gamma i μ' + gamma i μ' * gamma i μ = smul (2 * eta ν μ μ') (ident 4 : Mat p ν))335336/-- 8:D2, 8:D17 [value] — the Clifford relations hold on `𝔽₁₃` (`ν = 2`, `i = 5`), `𝔽₁₇₃` (`ν = 2`, `i = 93`) and337`𝔽₁₅₄₉` (`ν = 2`, `i = 1461`). -/338theorem clifford_values : clifford (2 : Shell 13) 5 = true ∧ clifford (2 : Shell 173) 93 = true ∧339    clifford (2 : Shell 1549) 1461 = true := by decide +kernel340341/-- The spin lift `S(x, y) = x I₄ + y γ⁰γ¹` and its inverse `δ⁻¹(x I₄ − y γ⁰γ¹)`, `δ = x² − ν y²`, with the342inverse of `δ` supplied. -/343def spinLift (i x y : Shell p) : Mat p ν :=344  smul ⟨x, 0⟩ (ident 4) + smul ⟨y, 0⟩ (gamma0 i * gamma1 i)345def spinLiftInv (i x y dinv : Shell p) : Mat p ν :=346  smul ⟨dinv, 0⟩ (smul ⟨x, 0⟩ (ident 4) + smul ⟨-y, 0⟩ (gamma0 i * gamma1 i))347348/-- 8:D6, 8:D16, 8:D12 — the spin conjugation `S⁻¹γ⁰S = Aγ⁰ + νBγ¹`, `S⁻¹γ¹S = Bγ⁰ + Aγ¹`, `γ², γ³` fixed, and349the transported gammas `Sγ⁰S⁻¹ = Aγ⁰ − νBγ¹`, `Sγ¹S⁻¹ = −Bγ⁰ + Aγ¹`, at the lift `(x, y)` with the entries350`A`, `B` given. -/351def spinConj (ν i x y dinv A B : Shell p) : Bool :=352  let S : Mat p ν := spinLift i x y353  let Si : Mat p ν := spinLiftInv i x y dinv354  let a : Ext p ν := ⟨A, 0⟩355  let b : Ext p ν := ⟨B, 0⟩356  let n : Ext p ν := ⟨ν, 0⟩357  decide (Si * S = ident 4) &&358  decide (Si * gamma0 i * S = smul a (gamma0 i) + smul (n * b) (gamma1 i)) &&359  decide (Si * gamma1 i * S = smul b (gamma0 i) + smul a (gamma1 i)) &&360  decide (Si * gamma2 i * S = gamma2 i) && decide (Si * gamma3 i * S = gamma3 i) &&361  decide (S * gamma0 i * Si = smul a (gamma0 i) + smul (-(n * b)) (gamma1 i)) &&362  decide (S * gamma1 i * Si = smul (-b) (gamma0 i) + smul a (gamma1 i))363364/-- 8:D6, 8:D16, 8:D12 [value] — on `𝔽₁₃` (`ν = g = 2`, `x = y = 1`, `δ = −1`): `A = 10`, `B = 2`,365`γ̂⁰ = 10γ⁰ − 4γ¹`, `γ̂¹ = −2γ⁰ + 10γ¹`; on `𝔽₁₇₃` (`ν = g = 2`, `i = 93`, `δ = −1`): `A = 170`, `B = 2`,366`γ̂⁰ = 170γ⁰ − 4γ¹`, `γ̂¹ = −2γ⁰ + 170γ¹`; on `𝔽₁₅₄₉` (`i = 1461`, `δ = −1`): `A = 1546`, `B = 2`. -/367theorem spin_conjugation_values :368    spinConj (2 : Shell 13) 5 1 1 12 10 2 = true ∧ spinConj (2 : Shell 173) 93 1 1 172 170 2 = true ∧369    spinConj (2 : Shell 1549) 1461 1 1 1548 1546 2 = true := by370  decide +kernel371372/-- 8:D9 — the spinor twist `X = γ⁰γ¹γ³`: Hermitian for the conjugate transpose, `X² = ν I₄`, commuting with373`γ⁰, γ¹, γ³`, anticommuting with `γ²`, and `(γ^μ)† X = −X γ^μ` for every `μ` (so `X⁻¹(γ^μ)†X = −γ^μ`); the374component signs `(γ⁰)† = −γ⁰`, `(γ¹)† = −γ¹`, `(γ²)† = +γ²` (the obstruction), `(γ³)† = −γ³`; and the failure375of the `γ⁰`-twist: `(γ¹)† γ⁰ ≠ −γ⁰ γ¹`. -/376def spinorForm (ν i : Shell p) : Bool :=377  let X : Mat p ν := gamma0 i * gamma1 i * gamma3 i378  let n : Ext p ν := ⟨ν, 0⟩379  decide (dagger X = X) && decide (X * X = smul n (ident 4)) &&380  decide (X * gamma0 i = gamma0 i * X) && decide (X * gamma1 i = gamma1 i * X) &&381  decide (X * gamma3 i = gamma3 i * X) && decide (X * gamma2 i = -(gamma2 i * X)) &&382  (List.range 4).all (fun μ => decide (dagger (gamma i μ) * X = -(X * gamma i μ))) &&383  decide ((dagger (gamma0 i) : Mat p ν) = -(gamma0 i)) && decide ((dagger (gamma1 i) : Mat p ν) = -(gamma1 i)) &&384  decide ((dagger (gamma2 i) : Mat p ν) = gamma2 i) && decide ((dagger (gamma3 i) : Mat p ν) = -(gamma3 i)) &&385  decide ((dagger (gamma1 i) : Mat p ν) * gamma0 i ≠ -(gamma0 i * gamma1 i))386387/-- 8:D9, 8:X4 [value] — the spinor form on `𝔽₁₃`, `𝔽₁₇₃` and `𝔽₁₅₄₉`: the `γ⁰`-twist fails and `X = γ⁰γ¹γ³` is the388form the arithmetic forces. -/389theorem spinor_form_values :390    spinorForm (2 : Shell 13) 5 = true ∧ spinorForm (2 : Shell 173) 93 = true ∧ spinorForm (2 : Shell 1549) 1461 = true := by391  decide +kernel392393/-- The inverse of a residue by bounded search (`0` when none). -/394def invS (a : Shell p) : Shell p :=395  match (List.range p).find? (fun b => decide (a * ofNat b = 1)) with396  | some b => ofNat b397  | none => 0398399/-- A circulant `p × p` matrix over `K` by its first row; the product of two circulants is the cyclic400convolution of their first rows. -/401def cyc (n : Nat) (a b : List (Ext p ν)) : List (Ext p ν) :=402  (List.range n).map fun k =>403    ((List.range n).map fun j => nth 0 a j * nth 0 b ((k + n - j) % n)).foldl (· + ·) 0404def cycId (n : Nat) : List (Ext p ν) := (List.range n).map fun k => if k = 0 then 1 else 0405def cycAdd (a b : List (Ext p ν)) : List (Ext p ν) := List.zipWith (· + ·) a b406def cycSmul (c : Ext p ν) (a : List (Ext p ν)) : List (Ext p ν) := a.map (c * ·)407def cycPow (n : Nat) (a : List (Ext p ν)) : Nat → List (Ext p ν)408  | 0 => cycId n409  | e + 1 => cyc n (cycPow n a e) a410411/-- `H = −Δ = 2I − T − T⁻¹` on `𝔽_p`, the kinetic Hamiltonian at unit stiffness, a circulant with first row412`(2, −1, 0, …, 0, −1)`. -/413def kineticRow (p : Nat) [Pos p] (ν : Shell p) : List (Ext p ν) :=414  (List.range p).map fun j => if j = 0 then 2 else if j = 1 ∨ j + 1 = p then -1 else 0415416/-- The Cayley step `U = (I − αH)⁻¹(I + αH)` of a nilpotent circulant `H`, the inverse as the series417`Σ_{j≤n} (αH)^j` (exact once `(αH)^n = 0`, which `cayley13` checks). -/418def cayleyRow (α : Ext p ν) (H : List (Ext p ν)) : List (Ext p ν) :=419  let N := cycSmul α H420  let inv := (List.range p).foldl (fun acc _ => cycAdd (cycId p) (cyc p N acc)) (cycId p)421  cyc p inv (cycAdd (cycId p) N)422423/-- 8:C6, 8:E4 — on `𝔽₁₃` with `ν = g = 2`: for `α = w` and `α = c = 6w` (`c² = 2⁻¹ = 7`, `(6w)² = 36·2 = 7`),424`(αH)^{13} = 0` (so the series inverse is exact), `U^{13} = I` and `U ≠ I`: the order is exactly `13`, the425translation torus `C_p` (Example `cayley-13`, Theorem `period-dichotomy` (1)). -/426def cayley13 (α : Ext 13 2) : Bool :=427  let H := kineticRow 13 2428  let U := cayleyRow α H429  decide (cycPow 13 (cycSmul α H) 13 = (List.range 13).map fun _ => (0 : Ext 13 2)) &&430  decide (cycPow 13 U 13 = cycId 13) && decide (U ≠ cycId 13)431432/-- 8:C6, 8:C15, 8:E4, 8:E7, 8:E8 [value] — the Cayley step of `H = −Δ` on `𝔽₁₃` has order exactly `13` at `α = w` and at433`α = c = 6w` (`c² = 7 = 2⁻¹`): every Cayley orbit on the shell is periodic, here with the period `13` (C15). -/434theorem cayley13_values : cayley13 ⟨0, 1⟩ = true ∧ cayley13 ⟨0, 6⟩ = true ∧435    ((⟨0, 6⟩ : Ext 13 2) * ⟨0, 6⟩ = 7 ∧ (2 : Shell 13) * 7 = 1) := by decide +kernel436437/-- The scalar Cayley map `φ(λ) = (1 + wλ)/(1 − wλ)` (`α = w`) on `K`, by the conjugate and the searched438inverse of the norm. -/439def phi (ν : Shell p) (lam : Shell p) : Ext p ν :=440  let num : Ext p ν := ⟨1, lam⟩441  let den : Ext p ν := ⟨1, -lam⟩442  num * Ext.conj den * Ext.ofShell (invS (Ext.norm den))443444/-- The order of `u` in the torus, by the running product up to `p + 1` steps (`0` if none). -/445def orderIn (u : Ext p ν) : Nat :=446  go u 1 (p + 1)447where448  go (x : Ext p ν) (e : Nat) : Nat → Nat449    | 0 => 0450    | fuel + 1 => if x = 1 then e else go (x * u) (e + 1) fuel451452/-- 8:E4 (2), 8:C5 — the potential propagator `U = diag(φ(V(x)))` for `V = id`: every phase `φ(λ)` has norm453one and `φ(λ)^{p+1} = 1`, and the order of the diagonal is the least common multiple of the phase orders —454`14 = p + 1` on `𝔽₁₃` and `174 = p + 1` on `𝔽₁₇₃`: the bound `p + 1` is attained. -/455def potentialOrder (p : Nat) [Pos p] (ν : Shell p) : Nat :=456  (List.range p).foldl (fun acc l => Nat.lcm acc (orderIn (phi ν (ofNat l)))) 1457458def potentialNormOne (p : Nat) [Pos p] (ν : Shell p) : Bool :=459  (List.range p).all fun l => decide (Ext.norm (phi ν (ofNat l)) = 1) && decide ((phi ν (ofNat l)) ^ (p + 1) = 1)460461/-- 8:E4, 8:E8 [value] — the potential propagator of `V = id` has order `14 = p + 1` on `𝔽₁₃` and `174` on `𝔽₁₇₃`, the462least common multiple of the phase orders, every phase of norm one. -/463theorem potential_orders : potentialNormOne 13 2 = true ∧ potentialOrder 13 2 = 14 ∧464    potentialNormOne 173 2 = true ∧ potentialOrder 173 2 = 174 := by decide +kernel465466/-- 8:D5 [value] — the triality clause: the norm-one cycle of `𝔽₁₇₃` (`174 = 3·58`) carries an element of order467three, and that of `𝔽₁₃` (`14`, `3 ∤ 14`) carries none: `u³ = 1`, `u ≠ 1` with `N(u) = 1`. -/468def hasOrderThree (p : Nat) [Pos p] (ν : Shell p) : Bool :=469  (List.range p).any fun a => (List.range p).any fun b =>470    let u : Ext p ν := ⟨ofNat a, ofNat b⟩471    decide (Ext.norm u = 1) && decide (u ^ 3 = 1) && decide (u ≠ 1)472473/-- 8:D5, 8:D12, 8:D19 [value] — an element of order three on the norm-one cycle of `𝔽₁₇₃`, none on that of `𝔽₁₃`. -/474theorem triality_values : hasOrderThree 173 2 = true ∧ hasOrderThree 13 2 = false := by decide +kernel475476/-- 8:E5 — the image count of the power map `x ↦ x^ε` on the nonzero residues. -/477def powerImage (p : Nat) [Pos p] (ε : Nat) : Nat :=478  ((List.range p).drop 1).foldl (fun acc y =>479    if ((List.range p).drop 1).any (fun x => decide ((ofNat x : Shell p) ^ ε = ofNat y)) then acc + 1 else acc) 0480481/-- 8:E5 [value] — on `𝔽₁₃`: the images of `x ↦ x^ε` have `(p − 1)/gcd(ε, 12)` elements — `12, 6, 4, 3, 2, 1`482for `ε = 1, 2, 3, 4, 6, 12` (loss factors `1, 2, 3, 4, 6, 12`). -/483theorem power_map13 : powerImage 13 1 = 12 ∧ powerImage 13 2 = 6 ∧ powerImage 13 3 = 4 ∧ powerImage 13 4 = 3 ∧484    powerImage 13 6 = 2 ∧ powerImage 13 12 = 1 := by decide +kernel485486/-- 8:D12, 8:D19, 8:B3 [value] — the worked shells: on `𝔽₁₃` (`g = 2`, `κ = 3`) the quarter-turn is `i = 5`, `2⁻¹ = 7`,487`e = g^i = 6` and `π = 2κ = 6`, and `2`, `7`, `5`, `6` are nonsquares; on `𝔽₁₇₃` (`g = 2`, `κ = 43`) `i = 93` with488`i² = −1`, `2⁻¹ = 87`, `e = 2^{93} = 45`, `π = 86`, and `2`, `87`, `93`, `45`, `86` are nonsquares; the lift at489`x = y = 1` has `δ = −1` on both, `A = (1 + ν)/δ = 10` and `170`, `B = −2/δ = 2`. -/490theorem shell173_values :491    ((2 : Shell 13) * 7 = 1 ∧ (5 : Shell 13) * 5 = -1 ∧ (2 : Shell 13) ^ 5 = 6 ∧492      ∀ r : Shell 13, r * r ≠ 2 ∧ r * r ≠ 7 ∧ r * r ≠ 5 ∧ r * r ≠ 6) ∧493    ((2 : Shell 173) * 87 = 1 ∧ (93 : Shell 173) * 93 = -1 ∧ (2 : Shell 173) ^ 93 = 45 ∧ (86 : Shell 173) = 2 * 43 ∧494      ∀ r : Shell 173, r * r ≠ 2 ∧ r * r ≠ 87 ∧ r * r ≠ 93 ∧ r * r ≠ 45 ∧ r * r ≠ 86) ∧495    ((-(1 : Shell 13)) * 10 = 1 + 2 ∧ (-(1 : Shell 13)) * 2 = -2 ∧ (-(1 : Shell 173)) * 170 = 1 + 2 ∧496      (-(1 : Shell 173)) * 2 = -2) := by decide +kernel497498/-- 8:B4 [value] — the laboratory Carrier `Ω = 2 408 561`: the two-way constant `c = 171 106` is a Carrier residue499with `c² = 2⁻¹ = 1 204 281`, and the two factors compose, `2⁻¹ · (2g) = 1 204 281 · 12 = 6 = g`. -/500theorem carrier_constants :501    (171106 : Shell 2408561) * 171106 = 1204281 ∧ (2 : Shell 2408561) * 1204281 = 1 ∧502    (1204281 : Shell 2408561) * 12 = 6 := by decide +kernel503504end matrices505506/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/507end508509section aliases510variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}511512theorem two_mul_mod (l : Nat) : (2 * l) % 2 = 0 :=513  FRC.Shell.Frame.two_mul_mod l514515theorem mod_two_of_mod_four_mul (m q : Nat) : (4 * q + m) % 2 = m % 2 :=516  FRC.Shell.Frame.mod_two_of_mod_four_mul m q517518theorem mod_n_mod_two (F : Frame p κ g) (m : Nat) : (m % (p - 1)) % 2 = m % 2 :=519  FRC.Shell.Frame.mod_n_mod_two F m520521/-- 8:B5, 8:X2 — the square class is chronon parity: on every frame, `g^m` is a square exactly when the drive-step522count `m` is even (Theorem `parity`); registered transport `g²` is even, the one-way step `g` odd. -/523theorem parity_iff (F : Frame p κ g) (m : Nat) : (∃ y : Shell p, y * y = g ^ m) ↔ m % 2 = 0 :=524  FRC.Shell.Frame.parity_iff F m525526/-- 8:B3 — the drive is a nonsquare on every frame (`m = 1`). -/527theorem drive_nonsquare (F : Frame p κ g) : ¬ ∃ y : Shell p, y * y = g :=528  FRC.Shell.Frame.drive_nonsquare F529530theorem mod_two_cases (m : Nat) : m % 2 = 0 ∨ m % 2 = 1 :=531  FRC.Shell.Frame.mod_two_cases m532533theorem succ_mod_two_eq_zero_iff (m : Nat) : (m + 1) % 2 = 0 ↔ m % 2 = 1 :=534  FRC.Shell.Frame.succ_mod_two_eq_zero_iff m535536/-- The inverse of the drive is `g^{p−2}`: every `y` with `g y = 1` is an odd power of `g`. -/537theorem inv_drive_odd (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :538    ∃ l, l < p - 1 ∧ g ^ l = y ∧ l % 2 = 1 :=539  FRC.Shell.Frame.inv_drive_odd F hy540541/-- 8:B3, 8:B6 — the reframing flip preserves the class: the inverse of the drive is a nonsquare (an odd542power of `g`), so `[g⁻¹] = [g]`. -/543theorem inv_drive_nonsquare (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :544    ¬ ∃ r : Shell p, r * r = y :=545  FRC.Shell.Frame.inv_drive_nonsquare F hy546547/-- 8:B1 — an element `a + b w` of the coefficient field, on components. -/548@[reducible] def Ext := @FRC.Extension.Ext549550namespace Ext551variable {ν : Shell p}552553theorem ext' {z z' : Ext p ν} (h1 : z.re = z'.re) (h2 : z.im = z'.im) : z = z' :=554  FRC.Extension.Ext.ext h1 h2555556/-- The base field inside `K`. -/557@[reducible] def ofShell (a : Shell p) : Ext p ν :=558  FRC.Extension.Ext.ofShell a559560/-- The adjoined root `w`, `w² = ν`. -/561@[reducible] def w : Ext p ν :=562  FRC.Extension.Ext.w563564/-- Frobenius conjugation `a + b w ↦ a − b w`. -/565@[reducible] def conj (z : Ext p ν) : Ext p ν :=566  FRC.Extension.Ext.conj z567568/-- The norm `N(z) = z z̄ = a² − ν b²`. -/569@[reducible] def norm (z : Ext p ν) : Shell p :=570  FRC.Extension.Ext.norm z571572/-- Powers by structural recursion. -/573@[reducible] def pow (z : Ext p ν) : Nat → Ext p ν :=574  FRC.Extension.Ext.pow z575576theorem mul_re (z z' : Ext p ν) : (z * z').re = z.re * z'.re + ν * (z.im * z'.im) :=577  FRC.Extension.Ext.mul_re z z'578579theorem mul_im (z z' : Ext p ν) : (z * z').im = z.re * z'.im + z.im * z'.re :=580  FRC.Extension.Ext.mul_im z z'581582theorem ofShell_re (a : Shell p) : (ofShell a : Ext p ν).re = a :=583  FRC.Extension.Ext.ofShell_re a584585theorem ofShell_im (a : Shell p) : (ofShell a : Ext p ν).im = 0 :=586  FRC.Extension.Ext.ofShell_im a587588theorem conj_re (z : Ext p ν) : (conj z).re = z.re :=589  FRC.Extension.Ext.conj_re z590591theorem conj_im (z : Ext p ν) : (conj z).im = -z.im :=592  FRC.Extension.Ext.conj_im z593594/-- `w² = ν`. -/595theorem w_sq : (w : Ext p ν) * w = ofShell ν :=596  FRC.Extension.Ext.w_sq597598/-- 8:B6 — the norm is the product with the conjugate: `z z̄ = N(z)`, a base-field element. -/599theorem mul_conj (z : Ext p ν) : z * conj z = ofShell (norm z) :=600  FRC.Extension.Ext.mul_conj z601602/-- Conjugation is multiplicative (the Frobenius involution is a ring map). -/603theorem conj_mul (z z' : Ext p ν) : conj (z * z') = conj z * conj z' :=604  FRC.Extension.Ext.conj_mul z z'605606/-- 8:B6 — norm growth: `N(c z) = c² N(z)` for every base residue `c`; one chronon of drive multiplies every607norm by `g²`, a square. -/608theorem norm_scale (c : Shell p) (z : Ext p ν) : norm (ofShell c * z) = c * c * norm z :=609  FRC.Extension.Ext.norm_scale c z610611end Ext612613end aliases614615616end FRC.Dirac617