Dirac.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Orbit3import FrcCore.Sum4import FrcCore.Instances5import FrcCore.Theme.Extension6import FrcCore.Keys.Extension7import FrcCore.Keys.Frame89/-!10# 8-dirac — the square-class arithmetic, the coefficient field and the worked shells, no axioms1112The finite content of *Schrödinger and Dirac Dynamics over Finite Substrate* (tree `8-dirac-20260709`) from13first principles, on every frame `(τ; 0, 1, g)` of capacity `κ`, `p = 4κ + 1`: the square class is chronon14parity — a residue `g^m` is a square exactly when `m` is even (B5); the drive `g` and its inverse `g^{p−2}`15are nonsquares, the quarter-turn `i = −g^κ = g^{3κ}` is a square exactly when `κ` is even, and `2`, `2⁻¹`,16`−2` are squares exactly when `κ` is even — so on every admissibility-class shell the drive is the only17nonsquare among the frame's named residues (B3); the factorisation `ν = g = c²·(2g)` with `c² = 2⁻¹`, the18cofactor `2g` a square exactly when `κ` is odd, the product odd always (B4); the coefficient field19`K = 𝔽_p[w]/(w² − ν)` on components with its conjugation and norm, `z z̄ = N(z)`, `N(gz) = g² N(z)` (B6, A2);20the latitude identities `4κ ≡ −1`, `κ = −4⁻¹`, `1 + κ = 3·4⁻¹`, `2κ = −2⁻¹`, `g^κ = −i` and the ladder21`κ < κ + 1 ≤ 2κ` (F2); the drive's spectrum on the characters — the eigenvalue `g^{(p−2)k}` inverse to `g^k`,22the isotropy `Σ_j g^{2jk} = 0` unless `(p − 1) ∣ 2k`, and the two exceptional lines `k = 0, 2κ` with23eigenvalues `±1` (F3); the sector separation — `g^{p−2}` primitive of order `p − 1`, and `u² = 1 ⇒ u = ±1`24(F4). Decided by the kernel on the worked shells: the Clifford relations, the spin conjugation with `A = 10`,25`B = 2` on `𝔽₁₃` and `A = 15`, `B = 1` on `𝔽₁₇`, the transported gammas (D2, D6, D7, D12); the spinor twist26`X = γ⁰γ¹γ³` with `X² = ν`, its commutations, `(γ^μ)† X = −X γ^μ` and the failure of the `γ⁰`-twist (D9); the27boost torus `|N¹| = 14` on `𝔽₁₃`, `18` on `𝔽₁₇`, an order-three element on `𝔽₁₇` and none on `𝔽₁₃` (D5, D12);28the Cayley step of `H = −Δ` on `𝔽₁₃`, `U¹³ = I ≠ U` at `α = w` and `α = c = 6w` (C6, E4); the potential29propagators of order `14` on `𝔽₁₃` and `18` on `𝔽₁₇`, the least common multiple of the phase orders (E4); the power-map image counts on `𝔽₁₃` (E2); the zero30counts `145`, `105` on `𝔽₅` and `2353`, `2041` on `𝔽₁₃` (B7); the unit-norm circle of `p − 1` points (F2); the31minimal admissible shell `𝔽₁₇` (D12); the laboratory Carrier's `c = 171 106`, `c² = 2⁻¹`, `2⁻¹·12 = 6` (B4).32Every declaration is checked to depend on no axiom (`check_core_axioms.py`).3334Since the ledger migration (task LM17) the coefficient field is the extension theme's `FRC.Extension.Ext p ν`35(`Theme/Extension.lean`) and chronon parity is the frame theme's (`Orbit.lean`); every old name stays as an alias.36-/3738namespace FRC.Dirac3940open FRC.Shell4142section43open FRC.Extension44open 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)4546/-! ## The square class is chronon parity (8:B5, B3, B4) -/47section parity48variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}4950/-- 8:B3 — the quarter-turn is `g^{3κ}` (`i = −g^κ`, `−1 = g^{2κ}`). -/51theorem quarterTurn_eq_pow (F : Frame p κ g) : Frame.quarterTurn g κ = g ^ (3 * κ) := by52  unfold Frame.quarterTurn53  rw [← Shell.neg_one_mul, ← F.half_period, ← Shell.pow_add]54  show g ^ (2 * κ + κ) = g ^ (3 * κ)55  rw [show 2 * κ + κ = 3 * κ from (Nat.succ_mul 2 κ).symm]5657/-- 8:B3 — `i` is a square exactly when the capacity is even (the eighth root of unity exists iff58`8 ∣ p − 1`). -/59theorem quarter_class (F : Frame p κ g) :60    (∃ y : Shell p, y * y = Frame.quarterTurn g κ) ↔ κ % 2 = 0 := by61  rw [quarterTurn_eq_pow F]62  refine (parity_iff F (3 * κ)).trans ?_63  have : 3 * κ = 2 * κ + κ := (Nat.succ_mul 2 κ)64  rw [this, FRC.Nat.add_mul_mod_self_left κ κ 2 (Nat.zero_lt_succ 1)]6566/-- 8:B3 — `2`, `2⁻¹` and `−2` are squares exactly when the capacity is even (the second supplementary67law at tier 0, 14-entropy's `two_is_square_iff`, and `−1 = (g^κ)²`). -/68theorem two_class (F : Frame p κ g) {h : Shell p} (hh : 2 * h = 1) :69    ((∃ r : Shell p, r * r = 2) ↔ κ % 2 = 0) ∧ ((∃ r : Shell p, r * r = h) ↔ κ % 2 = 0) ∧70    ((∃ r : Shell p, r * r = -2) ↔ κ % 2 = 0) := by71  have key : (∃ r : Shell p, r * r = 2) ↔ κ % 2 = 0 := by72    refine (FRC.Shell.Frame.two_is_square_iff F).trans ?_73    constructor74    · rintro ⟨m, hm⟩; rw [hm]; exact two_mul_mod m75    · intro h076      match FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) κ with77      | ⟨q, hq⟩ => exact ⟨q, by rw [h0, Nat.add_zero] at hq; exact hq⟩78  have hsq : (g ^ κ) * (g ^ κ) = -1 := by rw [← Shell.pow_two]; exact (F.quarter_turn_order).179  refine ⟨key, ?_, ?_⟩80  · refine Iff.trans ?_ key81    constructor82    · rintro ⟨r, hr⟩83      refine ⟨2 * r, ?_⟩84      rw [FRC.Shell.mul_mul_mul_comm, hr, Shell.mul_assoc, hh, Shell.mul_one]85    · rintro ⟨r, hr⟩86      refine ⟨r * h, ?_⟩87      rw [FRC.Shell.mul_mul_mul_comm, hr]88      calc (2 : Shell p) * (h * h) = 2 * h * h := (Shell.mul_assoc _ _ _).symm89        _ = h := by rw [hh, Shell.one_mul]90  · refine Iff.trans ?_ key91    constructor92    · rintro ⟨r, hr⟩93      refine ⟨g ^ κ * r, ?_⟩94      rw [FRC.Shell.mul_mul_mul_comm, hsq, hr, Shell.neg_mul_neg, Shell.one_mul]95    · rintro ⟨r, hr⟩96      refine ⟨g ^ κ * r, ?_⟩97      rw [FRC.Shell.mul_mul_mul_comm, hsq, hr, Shell.neg_one_mul]9899/-- 8:B4 — the factorisation of the coefficient: with `c² = 2⁻¹`, `ν = g = c²·(2g)` exactly on every shell,100and the cofactor `2g` is a square exactly when `κ` is odd — the product `g` odd always (Corollary101`two-seats`). -/102theorem nu_factorisation (F : Frame p κ g) {h : Shell p} (hh : 2 * h = 1) :103    h * (2 * g) = g ∧ ((∃ y : Shell p, y * y = 2 * g) ↔ κ % 2 = 1) := by104  refine ⟨by rw [← Shell.mul_assoc, Shell.mul_comm h 2, hh, Shell.one_mul], ?_⟩105  obtain ⟨m, _, hm⟩ := F.eq_pow_of_ne_zero F.two_ne_zero106  have h2g : (2 : Shell p) * g = g ^ (m + 1) := by rw [Shell.pow_succ, hm]107  rw [h2g]108  refine (parity_iff F (m + 1)).trans ((succ_mod_two_eq_zero_iff m).trans ?_)109  have hm2 : (∃ r : Shell p, r * r = 2) ↔ m % 2 = 0 := by rw [← hm]; exact parity_iff F m110  replace hm2 : κ % 2 = 0 ↔ m % 2 = 0 := (two_class F hh).1.symm.trans hm2111  constructor112  · intro h1113    rcases mod_two_cases κ with hk | hk114    · exact absurd (hm2.1 hk) (by rw [h1]; exact fun e => Nat.noConfusion e)115    · exact hk116  · intro h1117    rcases mod_two_cases m with hm' | hm'118    · exact absurd (hm2.2 hm') (by rw [h1]; exact fun e => Nat.noConfusion e)119    · exact hm'120121end parity122123/-! ## The latitude identities (8:F2) -/124section latitude125variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}126127/-- 8:F2 — the ladder `1, …, 2κ`: `κ + 1`, the first rung past the midpoint `κ`, is still a rung. -/128theorem ladder (F : Frame p κ g) : κ + 1 ≤ 2 * κ := by129  rw [Nat.two_mul]; exact Nat.add_le_add_left F.cap_pos κ130131/-- 8:F2 — `4κ ≡ −1` on the shell (`4κ = p − 1`), so `κ = −4⁻¹` and the energy radius `1 + κ = 3·4⁻¹`. -/132theorem four_kappa (F : Frame p κ g) {q : Shell p} (hq : 4 * q = 1) :133    (4 : Shell p) * ofNat κ = -1 ∧ (ofNat κ : Shell p) = -q ∧ (1 : Shell p) + ofNat κ = 3 * q := by134  have h4 : (4 : Shell p) * ofNat κ = -1 := by135    have := F.two_pi136    unfold Frame.halfPeriod at this137    rw [← FRC.Nat.mul_assoc, ← Frame.ofNat_mul] at this138    exact this139  have hk : (ofNat κ : Shell p) = -q := by140    calc (ofNat κ : Shell p) = 1 * ofNat κ := (Shell.one_mul _).symm141      _ = 4 * q * ofNat κ := by rw [hq]142      _ = q * (4 * ofNat κ) := by rw [Shell.mul_comm 4 q, Shell.mul_assoc]143      _ = -q := by rw [h4, ← Shell.mul_neg, Shell.mul_one]144  refine ⟨h4, hk, ?_⟩145  have h3 : (4 : Shell p) = 3 + 1 :=146    Shell.ext (by rw [Shell.val_add, Shell.val_lit, Shell.val_lit, Shell.val_one,147      FRC.Nat.mod_add_mod _ _ _ Shell.hp, FRC.Nat.add_mod_mod _ _ _ Shell.hp])148  rw [hk, ← hq, h3, Shell.right_distrib, Shell.one_mul, Shell.add_assoc, Shell.add_neg, Shell.add_zero]149150/-- 8:F2 — the terminal latitude: `π = 2κ = −2⁻¹` (`= −c²`); the quarter-cycle shift `m ↦ m + κ` on the151ladder is multiplication by `g^κ = −i` (`quarterTurn_eq_pow`, `i = −g^κ` by definition). -/152theorem terminal_latitude (F : Frame p κ g) {h : Shell p} (hh : 2 * h = 1) :153    (ofNat (2 * κ) : Shell p) = -h := by154  have h2 : (2 : Shell p) * ofNat (2 * κ) = -1 := by155    have := F.two_pi156    unfold Frame.halfPeriod at this157    rw [← Frame.ofNat_mul] at this158    exact this159  calc (ofNat (2 * κ) : Shell p) = 1 * ofNat (2 * κ) := (Shell.one_mul _).symm160    _ = 2 * h * ofNat (2 * κ) := by rw [hh]161    _ = h * (2 * ofNat (2 * κ)) := by rw [Shell.mul_comm 2 h, Shell.mul_assoc]162    _ = -h := by rw [h2, ← Shell.mul_neg, Shell.mul_one]163164end latitude165166/-! ## The free evolution is the drive (8:F3) and the two sectors (8:F4) -/167section drive168variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}169170/-- 8:F3 — the drive pullback on the characters: with `y = g⁻¹`, `χ_k(g^{j}) = y^k · χ_k(g^{j+1})` for every171`j, k` — the winding-`k` mode acquires the phase `g^{−k}` per chronon (Theorem `zonal` (2)). -/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 — 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-one209torus meets the base field in `{±1}` alone (`u² = 1 ⇒ u = ±1`). -/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 `5³ + 5² − 5 = 145` zeros and the Lorentzian form254(`ν = g = 2`) has `5³ − 5² + 5 = 105`: the hyperbolic and the elliptic form part on the base shell. -/255theorem zeros5 : euclidZeros 5 = 145 ∧ lorentzZeros 5 2 = 105 := by decide +kernel256257/-- 8:B7 [value] — on `𝔽₁₃`: `2353` and `2041` zeros (`13³ ± 13² ∓ 13`), `ν = g = 2`. -/258theorem zeros13 : euclidZeros 13 = 2353 ∧ lorentzZeros 13 2 = 2041 := by decide +kernel259260/-- 8:D5, 8:D12, 8:C5, 8:F2 [value] — the boost torus: `|N¹| = 14 = p + 1` on `𝔽₁₃` (`ν = 2`) and `18` on `𝔽₁₇`261(`ν = 3`); the unit-norm circle of the chart has `p − 1` points: `12` and `16` (8:F2). -/262theorem torus_counts :263    normOneCount 13 2 = 14 ∧ normOneCount 17 3 = 18 ∧ unitCircleCount 13 = 12 ∧ unitCircleCount 17 = 16 := by264  decide +kernel265266end decided267268/-! ## Matrices over the coefficient field, the gammas and the Cayley step, decided by the kernel -/269section matrices270variable {p : Nat} [Pos p] {ν : Shell p}271272/-- A matrix over `K` as a list of rows. -/273abbrev Mat (p : Nat) [Pos p] (ν : Shell p) := List (List (Ext p ν))274275namespace Mat276277/-- The `j`-th element of a list, `d` beyond its end (structural; Lean's `List.getD` carries `propext`). -/278def nth {α : Type} (d : α) : List α → Nat → α279  | [], _ => d280  | a :: _, 0 => a281  | _ :: l, n + 1 => nth d l n282def dot (r c : List (Ext p ν)) : Ext p ν := (List.zipWith (· * ·) r c).foldl (· + ·) 0283def col (A : Mat p ν) (j : Nat) : List (Ext p ν) := A.map fun r => nth 0 r j284def transpose (A : Mat p ν) : Mat p ν := (List.range (A.headD []).length).map (col A)285def mul (A B : Mat p ν) : Mat p ν :=286  let Bt := transpose B287  A.map fun r => Bt.map fun c => dot r c288def add (A B : Mat p ν) : Mat p ν := List.zipWith (fun r s => List.zipWith (· + ·) r s) A B289def neg (A : Mat p ν) : Mat p ν := A.map fun r => r.map (- ·)290def smul (c : Ext p ν) (A : Mat p ν) : Mat p ν := A.map fun r => r.map (c * ·)291def ident (n : Nat) : Mat p ν := (List.range n).map fun i => (List.range n).map fun j => if i = j then 1 else 0292/-- Powers by squaring. -/293def pow (A : Mat p ν) (n : Nat) : Nat → Mat p ν294  | 0 => ident n295  | e + 1 => mul (pow A n e) A296/-- The conjugate transpose (Frobenius on the entries). -/297def dagger (A : Mat p ν) : Mat p ν := (transpose A).map fun r => r.map Ext.conj298299instance : Mul (Mat p ν) := ⟨mul⟩300instance : Add (Mat p ν) := ⟨add⟩301instance : Neg (Mat p ν) := ⟨neg⟩302303end Mat304305open Mat306307/-- The gamma matrices of `(eq:gamma-definition)` over `K`, given the quarter-turn `i` of the shell:308`γ⁰ = i w β`, `γ^k = i ρ^k` (with `i² = −1`, so `γ²`'s entries are `∓i² = ±1`). -/309def gamma0 (i : Shell p) : Mat p ν :=310  let iw : Ext p ν := ⟨0, i⟩311  [[0, 0, iw, 0], [0, 0, 0, iw], [iw, 0, 0, 0], [0, iw, 0, 0]]312def gamma1 (i : Shell p) : Mat p ν :=313  let ii : Ext p ν := ⟨i, 0⟩314  [[0, 0, 0, ii], [0, 0, ii, 0], [0, -ii, 0, 0], [-ii, 0, 0, 0]]315def gamma2 (i : Shell p) : Mat p ν :=316  let ii : Ext p ν := ⟨i, 0⟩317  [[0, 0, 0, -(ii * ii)], [0, 0, ii * ii, 0], [0, ii * ii, 0, 0], [-(ii * ii), 0, 0, 0]]318def gamma3 (i : Shell p) : Mat p ν :=319  let ii : Ext p ν := ⟨i, 0⟩320  [[0, 0, ii, 0], [0, 0, 0, -ii], [-ii, 0, 0, 0], [0, ii, 0, 0]]321def gamma (i : Shell p) : Nat → Mat p ν322  | 0 => gamma0 i323  | 1 => gamma1 i324  | 2 => gamma2 i325  | _ => gamma3 i326/-- `η = diag(−ν, 1, 1, 1)`. -/327def eta (ν : Shell p) : Nat → Nat → Ext p ν328  | 0, 0 => -(⟨ν, 0⟩ : Ext p ν)329  | 1, 1 => 1330  | 2, 2 => 1331  | 3, 3 => 1332  | _, _ => 0333334/-- 8:D2 — the Clifford relations `γ^μ γ^ν + γ^ν γ^μ = 2 η_{μν} I₄`, all sixteen. -/335def clifford (ν : Shell p) (i : Shell p) : Bool :=336  (List.range 4).all fun μ => (List.range 4).all fun μ' =>337    decide (gamma i μ * gamma i μ' + gamma i μ' * gamma i μ = smul (2 * eta ν μ μ') (ident 4 : Mat p ν))338339/-- 8:D2 [value] — the Clifford relations hold on `𝔽₁₃` (`ν = 2`, `i = 5`), `𝔽₁₇` (`ν = 3`, `i = 4`) and340`𝔽₅` (`ν = 2`, `i = 2`). -/341theorem clifford_values : clifford (2 : Shell 13) 5 = true ∧ clifford (3 : Shell 17) 4 = true ∧342    clifford (2 : Shell 5) 2 = true := by decide +kernel343344/-- The spin lift `S(x, y) = x I₄ + y γ⁰γ¹` and its inverse `δ⁻¹(x I₄ − y γ⁰γ¹)`, `δ = x² − ν y²`, with the345inverse of `δ` supplied. -/346def spinLift (i x y : Shell p) : Mat p ν :=347  smul ⟨x, 0⟩ (ident 4) + smul ⟨y, 0⟩ (gamma0 i * gamma1 i)348def spinLiftInv (i x y dinv : Shell p) : Mat p ν :=349  smul ⟨dinv, 0⟩ (smul ⟨x, 0⟩ (ident 4) + smul ⟨-y, 0⟩ (gamma0 i * gamma1 i))350351/-- 8:D6, 8:D7, 8:D12 — the spin conjugation `S⁻¹γ⁰S = Aγ⁰ + νBγ¹`, `S⁻¹γ¹S = Bγ⁰ + Aγ¹`, `γ², γ³` fixed, and352the transported gammas `Sγ⁰S⁻¹ = Aγ⁰ − νBγ¹`, `Sγ¹S⁻¹ = −Bγ⁰ + Aγ¹`, at the lift `(x, y)` with the entries353`A`, `B` given. -/354def spinConj (ν i x y dinv A B : Shell p) : Bool :=355  let S : Mat p ν := spinLift i x y356  let Si : Mat p ν := spinLiftInv i x y dinv357  let a : Ext p ν := ⟨A, 0⟩358  let b : Ext p ν := ⟨B, 0⟩359  let n : Ext p ν := ⟨ν, 0⟩360  decide (Si * S = ident 4) &&361  decide (Si * gamma0 i * S = smul a (gamma0 i) + smul (n * b) (gamma1 i)) &&362  decide (Si * gamma1 i * S = smul b (gamma0 i) + smul a (gamma1 i)) &&363  decide (Si * gamma2 i * S = gamma2 i) && decide (Si * gamma3 i * S = gamma3 i) &&364  decide (S * gamma0 i * Si = smul a (gamma0 i) + smul (-(n * b)) (gamma1 i)) &&365  decide (S * gamma1 i * Si = smul (-b) (gamma0 i) + smul a (gamma1 i))366367/-- 8:D6, 8:D7, 8:D12 [value] — on `𝔽₁₃` (`ν = g = 2`, `x = y = 1`, `δ = −1`): `A = 10`, `B = 2`,368`γ̂⁰ = 10γ⁰ − 4γ¹`, `γ̂¹ = −2γ⁰ + 10γ¹`; on `𝔽₁₇` (`ν = g = 3`, `δ = −2`, `δ⁻¹ = 8`): `A = 15`, `B = 1`,369`γ̂⁰ = 15γ⁰ − 3γ¹`, `γ̂¹ = −γ⁰ + 15γ¹`. -/370theorem spin_conjugation_values :371    spinConj (2 : Shell 13) 5 1 1 12 10 2 = true ∧ spinConj (3 : Shell 17) 4 1 1 8 15 1 = true := by372  decide +kernel373374/-- 8:D9 — the spinor twist `X = γ⁰γ¹γ³`: Hermitian for the conjugate transpose, `X² = ν I₄`, commuting with375`γ⁰, γ¹, γ³`, anticommuting with `γ²`, and `(γ^μ)† X = −X γ^μ` for every `μ` (so `X⁻¹(γ^μ)†X = −γ^μ`); the376component signs `(γ⁰)† = −γ⁰`, `(γ¹)† = −γ¹`, `(γ²)† = +γ²` (the obstruction), `(γ³)† = −γ³`; and the failure377of the `γ⁰`-twist: `(γ¹)† γ⁰ ≠ −γ⁰ γ¹`. -/378def spinorForm (ν i : Shell p) : Bool :=379  let X : Mat p ν := gamma0 i * gamma1 i * gamma3 i380  let n : Ext p ν := ⟨ν, 0⟩381  decide (dagger X = X) && decide (X * X = smul n (ident 4)) &&382  decide (X * gamma0 i = gamma0 i * X) && decide (X * gamma1 i = gamma1 i * X) &&383  decide (X * gamma3 i = gamma3 i * X) && decide (X * gamma2 i = -(gamma2 i * X)) &&384  (List.range 4).all (fun μ => decide (dagger (gamma i μ) * X = -(X * gamma i μ))) &&385  decide ((dagger (gamma0 i) : Mat p ν) = -(gamma0 i)) && decide ((dagger (gamma1 i) : Mat p ν) = -(gamma1 i)) &&386  decide ((dagger (gamma2 i) : Mat p ν) = gamma2 i) && decide ((dagger (gamma3 i) : Mat p ν) = -(gamma3 i)) &&387  decide ((dagger (gamma1 i) : Mat p ν) * gamma0 i ≠ -(gamma0 i * gamma1 i))388389/-- 8:D9 [value] — the spinor form on `𝔽₅`, `𝔽₁₃` and `𝔽₁₇`. -/390theorem spinor_form_values :391    spinorForm (2 : Shell 5) 2 = true ∧ spinorForm (2 : Shell 13) 5 = true ∧ spinorForm (3 : Shell 17) 4 = true := by392  decide +kernel393394/-- The inverse of a residue by bounded search (`0` when none). -/395def invS (a : Shell p) : Shell p :=396  match (List.range p).find? (fun b => decide (a * ofNat b = 1)) with397  | some b => ofNat b398  | none => 0399400/-- A circulant `p × p` matrix over `K` by its first row; the product of two circulants is the cyclic401convolution of their first rows. -/402def cyc (n : Nat) (a b : List (Ext p ν)) : List (Ext p ν) :=403  (List.range n).map fun k =>404    ((List.range n).map fun j => nth 0 a j * nth 0 b ((k + n - j) % n)).foldl (· + ·) 0405def cycId (n : Nat) : List (Ext p ν) := (List.range n).map fun k => if k = 0 then 1 else 0406def cycAdd (a b : List (Ext p ν)) : List (Ext p ν) := List.zipWith (· + ·) a b407def cycSmul (c : Ext p ν) (a : List (Ext p ν)) : List (Ext p ν) := a.map (c * ·)408def cycPow (n : Nat) (a : List (Ext p ν)) : Nat → List (Ext p ν)409  | 0 => cycId n410  | e + 1 => cyc n (cycPow n a e) a411412/-- `H = −Δ = 2I − T − T⁻¹` on `𝔽_p`, the kinetic Hamiltonian at unit stiffness, a circulant with first row413`(2, −1, 0, …, 0, −1)`. -/414def kineticRow (p : Nat) [Pos p] (ν : Shell p) : List (Ext p ν) :=415  (List.range p).map fun j => if j = 0 then 2 else if j = 1 ∨ j + 1 = p then -1 else 0416417/-- The Cayley step `U = (I − αH)⁻¹(I + αH)` of a nilpotent circulant `H`, the inverse as the series418`Σ_{j≤n} (αH)^j` (exact once `(αH)^n = 0`, which `cayley13` checks). -/419def cayleyRow (α : Ext p ν) (H : List (Ext p ν)) : List (Ext p ν) :=420  let N := cycSmul α H421  let inv := (List.range p).foldl (fun acc _ => cycAdd (cycId p) (cyc p N acc)) (cycId p)422  cyc p inv (cycAdd (cycId p) N)423424/-- 8:C6, 8:E4 — on `𝔽₁₃` with `ν = g = 2`: for `α = w` and `α = c = 6w` (`c² = 2⁻¹ = 7`, `(6w)² = 36·2 = 7`),425`(αH)^{13} = 0` (so the series inverse is exact), `U^{13} = I` and `U ≠ I`: the order is exactly `13`, the426translation torus `C_p` (Example `cayley-13`, Theorem `period-dichotomy` (1)). -/427def cayley13 (α : Ext 13 2) : Bool :=428  let H := kineticRow 13 2429  let U := cayleyRow α H430  decide (cycPow 13 (cycSmul α H) 13 = (List.range 13).map fun _ => (0 : Ext 13 2)) &&431  decide (cycPow 13 U 13 = cycId 13) && decide (U ≠ cycId 13)432433/-- 8:C6, 8:E4 [value] — the Cayley step of `H = −Δ` on `𝔽₁₃` has order exactly `13` at `α = w` and at `α = c = 6w`434(`c² = 7 = 2⁻¹`). -/435theorem cayley13_values : cayley13 ⟨0, 1⟩ = true ∧ cayley13 ⟨0, 6⟩ = true ∧436    ((⟨0, 6⟩ : Ext 13 2) * ⟨0, 6⟩ = 7 ∧ (2 : Shell 13) * 7 = 1) := by decide +kernel437438/-- The scalar Cayley map `φ(λ) = (1 + wλ)/(1 − wλ)` (`α = w`) on `K`, by the conjugate and the searched439inverse of the norm. -/440def phi (ν : Shell p) (lam : Shell p) : Ext p ν :=441  let num : Ext p ν := ⟨1, lam⟩442  let den : Ext p ν := ⟨1, -lam⟩443  num * Ext.conj den * Ext.ofShell (invS (Ext.norm den))444445/-- The order of `u` in the torus, by search up to `p + 1` (`0` if none). -/446def orderIn (u : Ext p ν) : Nat :=447  match (List.range (p + 2)).find? (fun e => decide (0 < e ∧ u ^ e = 1)) with448  | some e => e449  | none => 0450451/-- 8:E4 (2), 8:C5 — the potential propagator `U = diag(φ(V(x)))` for `V = id`: every phase `φ(λ)` has norm452one and `φ(λ)^{p+1} = 1`, and the order of the diagonal is the least common multiple of the phase orders —453`14 = p + 1` on `𝔽₁₃` and `18 = p + 1` on `𝔽₁₇`: the bound `p + 1` is attained. -/454def potentialOrder (p : Nat) [Pos p] (ν : Shell p) : Nat :=455  (List.range p).foldl (fun acc l => Nat.lcm acc (orderIn (phi ν (ofNat l)))) 1456457def potentialNormOne (p : Nat) [Pos p] (ν : Shell p) : Bool :=458  (List.range p).all fun l => decide (Ext.norm (phi ν (ofNat l)) = 1) && decide ((phi ν (ofNat l)) ^ (p + 1) = 1)459460/-- 8:E4 [value] — the potential propagator of `V = id` has order `14 = p + 1` on `𝔽₁₃` and `18` on `𝔽₁₇`, the461least common multiple of the phase orders, every phase of norm one. -/462theorem potential_orders : potentialNormOne 13 2 = true ∧ potentialOrder 13 2 = 14 ∧463    potentialNormOne 17 3 = true ∧ potentialOrder 17 3 = 18 := by decide +kernel464465/-- 8:D5 [value] — the triality clause: the torus of `𝔽₁₇` (`18 = 3·6`) carries an element of order three,466and the torus of `𝔽₁₃` (`14`, `3 ∤ 14`) carries none: `u³ = 1`, `u ≠ 1` with `N(u) = 1`. -/467def hasOrderThree (p : Nat) [Pos p] (ν : Shell p) : Bool :=468  (List.range p).any fun a => (List.range p).any fun b =>469    let u : Ext p ν := ⟨ofNat a, ofNat b⟩470    decide (Ext.norm u = 1) && decide (u ^ 3 = 1) && decide (u ≠ 1)471472/-- 8:D5 [value] — an element of order three on the torus of `𝔽₁₇`, none on the torus of `𝔽₁₃`. -/473theorem triality_values : hasOrderThree 17 3 = true ∧ hasOrderThree 13 2 = false := by decide +kernel474475/-- 8:E2 — the image count of the power map `x ↦ x^ε` on the nonzero residues. -/476def powerImage (p : Nat) [Pos p] (ε : Nat) : Nat :=477  ((List.range p).drop 1).foldl (fun acc y =>478    if ((List.range p).drop 1).any (fun x => decide ((ofNat x : Shell p) ^ ε = ofNat y)) then acc + 1 else acc) 0479480/-- 8:E2 [value] — on `𝔽₁₃`: the images of `x ↦ x^ε` have `(p − 1)/gcd(ε, 12)` elements — `12, 6, 4, 3, 2, 1`481for `ε = 1, 2, 3, 4, 6, 12` (loss factors `1, 2, 3, 4, 6, 12`). -/482theorem power_map13 : powerImage 13 1 = 12 ∧ powerImage 13 2 = 6 ∧ powerImage 13 3 = 4 ∧ powerImage 13 4 = 3 ∧483    powerImage 13 6 = 2 ∧ powerImage 13 12 = 1 := by decide +kernel484485/-- 8:B4, 8:B3, 8:D12 [value] — the anchors: on `𝔽₁₃` (`g = 2`, `i = 5`) `2⁻¹ = 7` is a nonsquare and486`e = g^i = 6` is a nonsquare; on `𝔽₁₇` (`g = 3`, `i = 4`) `2 = 6²`, `i = 2²` and `e = 3⁴ = 13 = 8²` are487squares, and `ν = g = 3` is the only nonsquare among the named residues — so the class of `e` is not488stable across shells (B3). -/489theorem anchors :490    ((2 : Shell 13) * 7 = 1 ∧ ∀ r : Shell 13, r * r ≠ 7) ∧ ((2 : Shell 13) ^ 5 = 6 ∧ ∀ r : Shell 13, r * r ≠ 6) ∧491    ((6 : Shell 17) * 6 = 2 ∧ (2 : Shell 17) * 2 = 4 ∧ (3 : Shell 17) ^ 4 = 13 ∧ (8 : Shell 17) * 8 = 13 ∧492      ∀ r : Shell 17, r * r ≠ 3) := by decide +kernel493494/-- 8:D12 — the shell admissibility congruences of the programme: `κ` even, `κ ≡ 1 (mod 3)`, `4κ + 1` prime. -/495def shellAdmissible (κ : Nat) : Prop := κ % 2 = 0 ∧ κ % 3 = 1 ∧ FRC.Nat.isPrime (4 * κ + 1)496instance (κ : Nat) : Decidable (shellAdmissible κ) := by unfold shellAdmissible; exact inferInstance497498/-- 8:D12, 8:A5 [value] — `𝔽₁₇` (`κ = 4`) is the minimal admissible shell: `17 ≡ 5 (mod 12)`, and no capacity below499`4` is admissible (`κ = 1, 3` odd, `κ = 2` gives `9`). -/500theorem minimal_admissible : shellAdmissible 4 ∧ (∀ κ, κ < 4 → ¬ shellAdmissible κ) ∧ 17 % 12 = 5 := by501  decide +kernel502503/-- 8:B4, 8:A5 [value] — the laboratory Carrier `Ω = 2 408 561`: `c = 171 106` is base-rational with504`c² = 2⁻¹ = 1 204 281`, and the two factors compose, `2⁻¹ · (2g) = 1 204 281 · 12 = 6 = g`. -/505theorem carrier_constants :506    (171106 : Shell 2408561) * 171106 = 1204281 ∧ (2 : Shell 2408561) * 1204281 = 1 ∧507    (1204281 : Shell 2408561) * 12 = 6 := by decide +kernel508509end matrices510511/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/512end513514section aliases515variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}516517theorem two_mul_mod (l : Nat) : (2 * l) % 2 = 0 :=518  FRC.Shell.Frame.two_mul_mod l519520theorem mod_two_of_mod_four_mul (m q : Nat) : (4 * q + m) % 2 = m % 2 :=521  FRC.Shell.Frame.mod_two_of_mod_four_mul m q522523theorem mod_n_mod_two (F : Frame p κ g) (m : Nat) : (m % (p - 1)) % 2 = m % 2 :=524  FRC.Shell.Frame.mod_n_mod_two F m525526/-- 8:B5 — the square class is chronon parity: on every frame, `g^m` is a square exactly when the drive-step527count `m` is even (Theorem `parity`). -/528theorem parity_iff (F : Frame p κ g) (m : Nat) : (∃ y : Shell p, y * y = g ^ m) ↔ m % 2 = 0 :=529  FRC.Shell.Frame.parity_iff F m530531/-- 8:B3 — the drive is a nonsquare on every frame (`m = 1`). -/532theorem drive_nonsquare (F : Frame p κ g) : ¬ ∃ y : Shell p, y * y = g :=533  FRC.Shell.Frame.drive_nonsquare F534535theorem mod_two_cases (m : Nat) : m % 2 = 0 ∨ m % 2 = 1 :=536  FRC.Shell.Frame.mod_two_cases m537538theorem succ_mod_two_eq_zero_iff (m : Nat) : (m + 1) % 2 = 0 ↔ m % 2 = 1 :=539  FRC.Shell.Frame.succ_mod_two_eq_zero_iff m540541/-- The inverse of the drive is `g^{p−2}`: every `y` with `g y = 1` is an odd power of `g`. -/542theorem inv_drive_odd (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :543    ∃ l, l < p - 1 ∧ g ^ l = y ∧ l % 2 = 1 :=544  FRC.Shell.Frame.inv_drive_odd F hy545546/-- 8:B3, 8:B6 — the reframing flip preserves the class: the inverse of the drive is a nonsquare (an odd547power of `g`), so `[g⁻¹] = [g]`. -/548theorem inv_drive_nonsquare (F : Frame p κ g) {y : Shell p} (hy : g * y = 1) :549    ¬ ∃ r : Shell p, r * r = y :=550  FRC.Shell.Frame.inv_drive_nonsquare F hy551552/-- 8:B1 — an element `a + b w` of the coefficient field, on components. -/553@[reducible] def Ext := @FRC.Extension.Ext554555namespace Ext556variable {ν : Shell p}557558theorem ext' {z z' : Ext p ν} (h1 : z.re = z'.re) (h2 : z.im = z'.im) : z = z' :=559  FRC.Extension.Ext.ext h1 h2560561/-- The base field inside `K`. -/562@[reducible] def ofShell (a : Shell p) : Ext p ν :=563  FRC.Extension.Ext.ofShell a564565/-- The adjoined root `w`, `w² = ν`. -/566@[reducible] def w : Ext p ν :=567  FRC.Extension.Ext.w568569/-- Frobenius conjugation `a + b w ↦ a − b w`. -/570@[reducible] def conj (z : Ext p ν) : Ext p ν :=571  FRC.Extension.Ext.conj z572573/-- The norm `N(z) = z z̄ = a² − ν b²`. -/574@[reducible] def norm (z : Ext p ν) : Shell p :=575  FRC.Extension.Ext.norm z576577/-- Powers by structural recursion. -/578@[reducible] def pow (z : Ext p ν) : Nat → Ext p ν :=579  FRC.Extension.Ext.pow z580581theorem mul_re (z z' : Ext p ν) : (z * z').re = z.re * z'.re + ν * (z.im * z'.im) :=582  FRC.Extension.Ext.mul_re z z'583584theorem mul_im (z z' : Ext p ν) : (z * z').im = z.re * z'.im + z.im * z'.re :=585  FRC.Extension.Ext.mul_im z z'586587theorem ofShell_re (a : Shell p) : (ofShell a : Ext p ν).re = a :=588  FRC.Extension.Ext.ofShell_re a589590theorem ofShell_im (a : Shell p) : (ofShell a : Ext p ν).im = 0 :=591  FRC.Extension.Ext.ofShell_im a592593theorem conj_re (z : Ext p ν) : (conj z).re = z.re :=594  FRC.Extension.Ext.conj_re z595596theorem conj_im (z : Ext p ν) : (conj z).im = -z.im :=597  FRC.Extension.Ext.conj_im z598599/-- 8:A2 — `w² = ν`. -/600theorem w_sq : (w : Ext p ν) * w = ofShell ν :=601  FRC.Extension.Ext.w_sq602603/-- 8:A2 — the norm is the product with the conjugate: `z z̄ = N(z)`, a base-field element. -/604theorem mul_conj (z : Ext p ν) : z * conj z = ofShell (norm z) :=605  FRC.Extension.Ext.mul_conj z606607/-- 8:A2 — conjugation is multiplicative (the Frobenius involution is a ring map). -/608theorem conj_mul (z z' : Ext p ν) : conj (z * z') = conj z * conj z' :=609  FRC.Extension.Ext.conj_mul z z'610611/-- 8:B6 — norm growth: `N(c z) = c² N(z)` for every base residue `c`; one chronon of drive multiplies every612norm by `g²`, a square. -/613theorem norm_scale (c : Shell p) (z : Ext p ν) : norm (ofShell c * z) = c * c * norm z :=614  FRC.Extension.Ext.norm_scale c z615616end Ext617618end aliases619620-- Ledger predicates of 8-dirac (generated by make_predicates.py from docs/8-dirac/8-dirac-ledger.json; edit the ledger, not this section)621/-- 8:A2 (p08002) — Finite-field algebra: the quadratic extension $K=\Fp[\w]/(\w^{2}-\nu)$ with Frobenius conjugation and norm, Hilbert's Theorem~90, the square classes by Euler's criterion, the unitary group of a nondegenerate Hermitian form over a finite field. -/622theorem p08002 : ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Dirac.Ext p ν), z * z.conj = FRC.Dirac.Ext.ofShell z.norm :=623  @FRC.Ledger.p08002624/-- 8:A5 (p08005) — The programme's admissibility congruences ($\kap$ even, $\kap\equiv1\pmod3$, $\p\equiv5\pmod{12}$), the laboratory Carrier $\Omega=2\,408\,561$ with $S=602\,140$, and the constants web ($c^{2}=2^{-1}$, $\hbar=\It$). -/625theorem p08005 : (FRC.Dirac.shellAdmissible (4 : Nat) ∧ (∀ (κ : Nat), κ < (4 : Nat) → ¬FRC.Dirac.shellAdmissible κ) ∧ (17 : Nat) % (12 : Nat) = (5 : Nat)) ∧ (171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (1204281 : FRC.Shell (2408561 : Nat)) ∧ (2 : FRC.Shell (2408561 : Nat)) * (1204281 : FRC.Shell (2408561 : Nat)) = (1 : FRC.Shell (2408561 : Nat)) ∧ (1204281 : FRC.Shell (2408561 : Nat)) * (12 : FRC.Shell (2408561 : Nat)) = (6 : FRC.Shell (2408561 : Nat)) :=626  And.intro @FRC.Dirac.minimal_admissible (@FRC.Dirac.carrier_constants)627/-- 8:B3 (p08009) — The drive is canonical: $g$ is a nonsquare on every shell and the only named residue whose class is nonsquare on every symmetry-complete shell; $\It$, $2$, $2^{-1}$, $-2$ are squares exactly when $\kap$ is even; $e=g^{\It}$ has no stable class; $[g^{-1}]=[g]$. Exhaustive on $\p<2000$. -/628theorem p08009 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ¬∃ y, y * y = g) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ¬∃ r, r * r = y) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ((∃ y, y * y = FRC.Shell.Frame.quarterTurn g κ) ↔ κ % (2 : Nat) = (0 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → ((∃ r, r * r = (2 : FRC.Shell p)) ↔ κ % (2 : Nat) = (0 : Nat)) ∧ ((∃ r, r * r = h) ↔ κ % (2 : Nat) = (0 : Nat)) ∧ ((∃ r, r * r = (-2 : FRC.Shell p)) ↔ κ % (2 : Nat) = (0 : Nat))) ∧ ((2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ ∀ (r : FRC.Shell (13 : Nat)), r * r ≠ (7 : FRC.Shell (13 : Nat))) ∧ ((2 : FRC.Shell (13 : Nat)) ^ (5 : Nat) = (6 : FRC.Shell (13 : Nat)) ∧ ∀ (r : FRC.Shell (13 : Nat)), r * r ≠ (6 : FRC.Shell (13 : Nat))) ∧ (6 : FRC.Shell (17 : Nat)) * (6 : FRC.Shell (17 : Nat)) = (2 : FRC.Shell (17 : Nat)) ∧ (2 : FRC.Shell (17 : Nat)) * (2 : FRC.Shell (17 : Nat)) = (4 : FRC.Shell (17 : Nat)) ∧ (3 : FRC.Shell (17 : Nat)) ^ (4 : Nat) = (13 : FRC.Shell (17 : Nat)) ∧ (8 : FRC.Shell (17 : Nat)) * (8 : FRC.Shell (17 : Nat)) = (13 : FRC.Shell (17 : Nat)) ∧ ∀ (r : FRC.Shell (17 : Nat)), r * r ≠ (3 : FRC.Shell (17 : Nat)) :=629  And.intro @FRC.Dirac.drive_nonsquare (And.intro @FRC.Dirac.inv_drive_nonsquare (And.intro @FRC.Dirac.quarter_class (And.intro @FRC.Dirac.two_class (@FRC.Dirac.anchors))))630/-- 8:B4 (p08010) — The two speed-of-light seats: $\nu=g=c^{2}\cdot(2g)$ exactly on every shell; $[c^{2}]$ is even iff $\kap$ is even, $[2g]$ odd iff $\kap$ is even, the product odd always; the temporal coefficient is not $c^{2}$; anchors $\F_{13}$ ($2^{-1}=7$ nonsquare), $\F_{17}$ ($2,\It,e$ squares), and the laboratory Carrier ($c=171\,106$ base-rational, $1\,204\,281\cdot12=6=g$). -/631theorem p08010 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → h * ((2 : FRC.Shell p) * g) = g ∧ ((∃ y, y * y = (2 : FRC.Shell p) * g) ↔ κ % (2 : Nat) = (1 : Nat))) ∧ (171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (1204281 : FRC.Shell (2408561 : Nat)) ∧ (2 : FRC.Shell (2408561 : Nat)) * (1204281 : FRC.Shell (2408561 : Nat)) = (1 : FRC.Shell (2408561 : Nat)) ∧ (1204281 : FRC.Shell (2408561 : Nat)) * (12 : FRC.Shell (2408561 : Nat)) = (6 : FRC.Shell (2408561 : Nat)) :=632  And.intro @FRC.Dirac.nu_factorisation (@FRC.Dirac.carrier_constants)633/-- 8:B5 (p08011) — The square class is chronon parity: the squares are $\langle g^{2}\rangle$, a residue's class is the parity of its drive-step count; on $\kap$-even shells every element of $Q_4=\{1,\It,-1,-\It\}$ is a square, so the order-four chart grading carries no signature. Exhaustive over every primitive root of $\F_{13}$, $\F_{17}$; Euler form on $\p<2000$. -/634theorem p08011 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m : Nat), (∃ y, y * y = g ^ m) ↔ m % (2 : Nat) = (0 : Nat) :=635  @FRC.Ledger.p08011636/-- 8:B6 (p08012) — Norm growth and parity: $N(gz)=g^{2}N(z)$ with $g^{2}$ a square, the single-chronon multiplier $g$ odd, $x^{2}=\nu$ unsolvable in $\Fp$; the flip $g\mapsto g^{-1}$ preserves the parity class. -/637theorem p08012 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (c : FRC.Shell p) (z : FRC.Dirac.Ext p ν), (FRC.Dirac.Ext.ofShell c * z).norm = c * c * z.norm) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ¬∃ r, r * r = y :=638  @FRC.Ledger.p08012639/-- 8:B7 (p08013) — Signature lives on $\Fp$: the Euclidean form has $\p^{3}+\p^{2}-\p$ zeros (hyperbolic, Witt index two), $Q_\nu$ has $\p^{3}-\p^{2}+\p$ (elliptic, Witt index one) on every symmetry-complete $\p<60$; $2353$ and $2041$ at $\p=13$; over $K$ every element of $\Fp$ is a square and the dichotomy collapses. -/640theorem p08013 : (FRC.Dirac.euclidZeros (5 : Nat) = (145 : Nat) ∧ FRC.Dirac.lorentzZeros (5 : Nat) (2 : FRC.Shell (5 : Nat)) = (105 : Nat)) ∧ FRC.Dirac.euclidZeros (13 : Nat) = (2353 : Nat) ∧ FRC.Dirac.lorentzZeros (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (2041 : Nat) :=641  And.intro @FRC.Dirac.zeros5 (@FRC.Dirac.zeros13)642/-- 8:C5 (p08019) — The finite Cayley transform: $\varphi(\lambda)=(1+\alpha\lambda)/(1-\alpha\lambda)$ is defined on all of $\Fp$, takes values in the norm-one torus $N^{1}$, and with $\varphi(\infty)=-1$ bijects $\mathbb P^{1}(\Fp)$ onto $N^{1}$, $|N^{1}|=\p+1$; the unitary group of one channel is $N^{1}$; the orientation gauge $\alpha\mapsto-\alpha$ inverts every $\varphi(\lambda)$ and imports the derived orientation of the shell. -/643theorem p08019 : FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (17 : Nat) (3 : FRC.Shell (17 : Nat)) = (18 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (17 : Nat) = (16 : Nat) :=644  @FRC.Dirac.torus_counts645/-- 8:C6 (p08020) — The $\F_{13}$ Schr\"odinger example: $H=-\Delta_E$ on $\F_{13}$ is nilpotent, so $\calA(H)=K^{-}$; at $\alpha=c$, $U^{13}=I$; every $\alpha=kc$, $k\ne0$, gives order $13$, and $U$ is unitary for the form. -/646theorem p08020 : FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) :=647  @FRC.Dirac.cayley13_values648/-- 8:D2 (p08022) — The Clifford relations $\gamma^{\mu}\gamma^{\nu}+\gamma^{\nu}\gamma^{\mu}=2\eta_{\mu\nu}I_4$. -/649theorem p08022 : FRC.Dirac.clifford (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.clifford (3 : FRC.Shell (17 : Nat)) (4 : FRC.Shell (17 : Nat)) = true ∧ FRC.Dirac.clifford (2 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) = true :=650  @FRC.Dirac.clifford_values651/-- 8:D5 (p08025) — The boost group is the non-split torus: $\Lambda(x,y)\in O(Q_\nu,\Fp)$, $G_\nu$ a subgroup, $z\mapsto\Lambda$ a surjection $K^{\times}\to G_\nu$ with kernel $\Fpx$ and $A-B\w=z/\bar z$; $G_\nu\simeq N^{1}\simeq C_{\p+1}$, cyclic; an order-three boost exists iff $3\mid\p+1$ ($|G_3|=18$ at $17$, $|G_2|=14$ at $13$). -/652theorem p08025 : (FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (17 : Nat) (3 : FRC.Shell (17 : Nat)) = (18 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (17 : Nat) = (16 : Nat)) ∧ FRC.Dirac.hasOrderThree (17 : Nat) (3 : FRC.Shell (17 : Nat)) = true ∧ FRC.Dirac.hasOrderThree (13 : Nat) (2 : FRC.Shell (13 : Nat)) = false :=653  And.intro @FRC.Dirac.torus_counts (@FRC.Dirac.triality_values)654/-- 8:D6 (p08026) — Spin conjugation: $S^{-1}\gamma^{0}S=A\gamma^{0}+\nu B\gamma^{1}$, $S^{-1}\gamma^{1}S=B\gamma^{0}+A\gamma^{1}$, $\gamma^{2},\gamma^{3}$ fixed. -/655theorem p08026 : FRC.Dirac.spinConj (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (12 : FRC.Shell (13 : Nat)) (10 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinConj (3 : FRC.Shell (17 : Nat)) (4 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) (8 : FRC.Shell (17 : Nat)) (15 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) = true :=656  @FRC.Dirac.spin_conjugation_values657/-- 8:D7 (p08027) — The transported family: $\nabla^{E_\Lambda}_\mu\Lambda_*=\Lambda_*\nabla^{E_0}_\mu$; $\mathcal D_{\Lambda,S}=\sum\widehat\gamma^{\mu}\nabla^{E_\Lambda}_\mu$ with $\widehat\gamma^{0}=A\gamma^{0}-\nu B\gamma^{1}$, $\widehat\gamma^{1}=-B\gamma^{0}+A\gamma^{1}$; the transported Clifford relations and factorization. -/658theorem p08027 : FRC.Dirac.spinConj (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (12 : FRC.Shell (13 : Nat)) (10 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinConj (3 : FRC.Shell (17 : Nat)) (4 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) (8 : FRC.Shell (17 : Nat)) (15 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) = true :=659  @FRC.Dirac.spin_conjugation_values660/-- 8:D9 (p08029) — The spinor form: under the plain conjugate transpose the gammas carry mixed signs ($\gamma^{2}$ the obstruction) and the $\gamma^{0}$-twist fails; $X=\gamma^{0}\gamma^{1}\gamma^{3}$ is Hermitian with $X^{2}=\nu$, commutes with $\gamma^{0},\gamma^{1},\gamma^{3}$, anticommutes with $\gamma^{2}$, and $X^{-1}(\gamma^{\mu})^{\dagger}X=-\gamma^{\mu}$ for all $\mu$; $\langle\cdot,\cdot\rangle_X$ is nondegenerate Hermitian, $T-T^{-1}$ nilpotent and anti-self-adjoint, $\mathcal D^{s}$ $X$-self-adjoint and nilpotent ($\p=5,13,17$). -/661theorem p08029 : FRC.Dirac.spinorForm (2 : FRC.Shell (5 : Nat)) (2 : FRC.Shell (5 : Nat)) = true ∧ FRC.Dirac.spinorForm (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinorForm (3 : FRC.Shell (17 : Nat)) (4 : FRC.Shell (17 : Nat)) = true :=662  @FRC.Dirac.spinor_form_values663/-- 8:D12 (p08032) — The worked shells: $\F_{13}$ with $\nu=g=2$, $x=y=1$: $A=10$, $B=2$, $S=I+\gamma^{0}\gamma^{1}$, $\widehat\gamma^{0}=10\gamma^{0}-4\gamma^{1}$, $\widehat\gamma^{1}=-2\gamma^{0}+10\gamma^{1}$; $\F_{17}$ the minimal admissible shell ($17\equiv5\bmod12$, no smaller symmetry-complete prime), $\It=4$, $2,\It,e$ squares, $\nu=3$, $A=15$, $B=1$, $|G_3|=18$, triality present. -/664theorem p08032 : (FRC.Dirac.spinConj (2 : FRC.Shell (13 : Nat)) (5 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) (12 : FRC.Shell (13 : Nat)) (10 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.spinConj (3 : FRC.Shell (17 : Nat)) (4 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) (8 : FRC.Shell (17 : Nat)) (15 : FRC.Shell (17 : Nat)) (1 : FRC.Shell (17 : Nat)) = true) ∧ (FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (17 : Nat) (3 : FRC.Shell (17 : Nat)) = (18 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (17 : Nat) = (16 : Nat)) ∧ (((2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ ∀ (r : FRC.Shell (13 : Nat)), r * r ≠ (7 : FRC.Shell (13 : Nat))) ∧ ((2 : FRC.Shell (13 : Nat)) ^ (5 : Nat) = (6 : FRC.Shell (13 : Nat)) ∧ ∀ (r : FRC.Shell (13 : Nat)), r * r ≠ (6 : FRC.Shell (13 : Nat))) ∧ (6 : FRC.Shell (17 : Nat)) * (6 : FRC.Shell (17 : Nat)) = (2 : FRC.Shell (17 : Nat)) ∧ (2 : FRC.Shell (17 : Nat)) * (2 : FRC.Shell (17 : Nat)) = (4 : FRC.Shell (17 : Nat)) ∧ (3 : FRC.Shell (17 : Nat)) ^ (4 : Nat) = (13 : FRC.Shell (17 : Nat)) ∧ (8 : FRC.Shell (17 : Nat)) * (8 : FRC.Shell (17 : Nat)) = (13 : FRC.Shell (17 : Nat)) ∧ ∀ (r : FRC.Shell (17 : Nat)), r * r ≠ (3 : FRC.Shell (17 : Nat))) ∧ FRC.Dirac.shellAdmissible (4 : Nat) ∧ (∀ (κ : Nat), κ < (4 : Nat) → ¬FRC.Dirac.shellAdmissible κ) ∧ (17 : Nat) % (12 : Nat) = (5 : Nat) :=665  And.intro @FRC.Dirac.spin_conjugation_values (And.intro @FRC.Dirac.torus_counts (And.intro @FRC.Dirac.anchors (@FRC.Dirac.minimal_admissible)))666/-- 8:E2 (p08035) — A self-map is bijective iff $L_X(f)=1$; the power map $x\mapsto x^{\varepsilon}$ on $\Fpx$ has image $(\p-1)/d$ and loss factor $d=\gcd(\varepsilon,\p-1)$, every nonempty fibre of size $d$ ($\varepsilon=1,2,3,4,6,12$ on $\F_{13}$). -/667theorem p08035 : FRC.Dirac.powerImage (13 : Nat) (1 : Nat) = (12 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (2 : Nat) = (6 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (3 : Nat) = (4 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (4 : Nat) = (3 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (6 : Nat) = (2 : Nat) ∧ FRC.Dirac.powerImage (13 : Nat) (12 : Nat) = (1 : Nat) :=668  @FRC.Dirac.power_map13669/-- 8:E4 (p08037) — Period dichotomy: kinetic Hamiltonians are nilpotent, fully admissible, with unipotent propagators of order $\p$; potential Hamiltonians give diagonal propagators with phases in $N^{1}$ and order dividing $\p+1$ ($14$ at $13$, $18$ at $17$); the mixed datum $\operatorname{ord}(U)=1563$ at $\p=5$; composites take the lcm ($13,14\mapsto182$); the three tori $C_{\p-1}$, $C_\p$, $C_{\p+1}$ each govern one dynamical role. -/670theorem p08037 : (FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (1 : FRC.Shell (13 : Nat)) } = true ∧ FRC.Dirac.cayley13 { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = true ∧ { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } * { re := (0 : FRC.Shell (13 : Nat)), im := (6 : FRC.Shell (13 : Nat)) } = (7 : FRC.Dirac.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ FRC.Dirac.potentialNormOne (13 : Nat) (2 : FRC.Shell (13 : Nat)) = true ∧ FRC.Dirac.potentialOrder (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.potentialNormOne (17 : Nat) (3 : FRC.Shell (17 : Nat)) = true ∧ FRC.Dirac.potentialOrder (17 : Nat) (3 : FRC.Shell (17 : Nat)) = (18 : Nat) :=671  And.intro @FRC.Dirac.cayley13_values (@FRC.Dirac.potential_orders)672/-- 8:F2 (p08039) — The latitude identities: $\kap+1$ is the first rung past the midpoint of the ladder $1,\dots,2\kap$; $m\mapsto m+\kap$ is multiplication by $g^{\kap}=\pm\It$ and $a\mapsto a+\kap$ sends $1$ to $\kap+1$; $\kap=-4^{-1}$ so the energy radius is $3\cdot4^{-1}$; $\pi=2\kap=-2^{-1}=-c^{2}$, on the Carrier $\pi_\Omega=2S$; the unit-norm circle has $\p-1$ points. On $\F_{13}$, $\F_{17}$ and the laboratory Carrier. -/673theorem p08039 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → κ + (1 : Nat) ≤ (2 : Nat) * κ) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {q : FRC.Shell p}, (4 : FRC.Shell p) * q = (1 : FRC.Shell p) → (4 : FRC.Shell p) * FRC.Shell.ofNat κ = (-1 : FRC.Shell p) ∧ FRC.Shell.ofNat κ = -q ∧ (1 : FRC.Shell p) + FRC.Shell.ofNat κ = (3 : FRC.Shell p) * q) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {h : FRC.Shell p}, (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → FRC.Shell.ofNat ((2 : Nat) * κ) = -h) ∧ FRC.Dirac.normOneCount (13 : Nat) (2 : FRC.Shell (13 : Nat)) = (14 : Nat) ∧ FRC.Dirac.normOneCount (17 : Nat) (3 : FRC.Shell (17 : Nat)) = (18 : Nat) ∧ FRC.Dirac.unitCircleCount (13 : Nat) = (12 : Nat) ∧ FRC.Dirac.unitCircleCount (17 : Nat) = (16 : Nat) :=674  And.intro @FRC.Dirac.ladder (And.intro @FRC.Dirac.four_kappa (And.intro @FRC.Dirac.terminal_latitude (@FRC.Dirac.torus_counts)))675/-- 8:F3 (p08040) — The free evolution is the drive: the pullback $D\psi(x)=\psi(g^{-1}x)$ is unitary, the characters $\chi_k$ are its eigenvectors with $D\chi_k=g^{-k}\chi_k$, and every character line is isotropic except $k=0,(\p-1)/2$ with eigenvalues $\pm1=N^{1}\cap\mu_{\p-1}$. Exhaustive on $\F_{13}$, $\F_{17}$. -/676theorem p08040 : (∀ {p : Nat} [FRC.Pos p] {g y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → ∀ (j k : Nat), y ^ k * g ^ ((j + (1 : Nat)) * k) = g ^ (j * k)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → y ^ ((2 : Nat) * κ) = (-1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k : Nat), ((2 : Nat) * k % (p - (1 : Nat)) ≠ (0 : Nat) → FRC.Shell.sumRange (fun j => g ^ (j * k) * g ^ (j * k)) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ ((2 : Nat) * k % (p - (1 : Nat)) = (0 : Nat) → FRC.Shell.sumRange (fun j => g ^ (j * k) * g ^ (j * k)) (p - (1 : Nat)) = (-1 : FRC.Shell p)) :=677  And.intro @FRC.Dirac.drive_eigen (And.intro @FRC.Dirac.exceptional_eigen (@FRC.Dirac.isotropy))678/-- 8:F4 (p08041) — Two evolution sectors, one space: the split-phase sector of the drive and the norm-one sector of the Cayley propagators meet in $\{\pm1\}$ alone ($\operatorname{ord}(g^{-1})=\p-1$); the cycle Laplacian $\Delta_\Phi=D+D^{-1}-2I$ is self-adjoint, its Cayley steps commute with $D$ and the composite is unitary ($\p=13$); the dispersion relation $-\Delta_\Phi\chi_k=(2-g^{k}-g^{-k})\chi_k$; no meridional plane waves ($\gcd(\p,|K^{\times}|)=1$); $\mathcal D^{s}-m$ invertible for $m\ne0$, so mass is an evolution phase, not a kernel condition. -/679theorem p08041 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {y : FRC.Shell p}, g * y = (1 : FRC.Shell p) → y.IsPrimitive (p - (1 : Nat)) ∧ ∀ (u : FRC.Shell p), u * u = (1 : FRC.Shell p) → u = (1 : FRC.Shell p) ∨ u = (-1 : FRC.Shell p) :=680  @FRC.Dirac.sector_separation681-- end ledger predicates682683end FRC.Dirac684