Dirac.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Extension3import FrcLedger.Theme.Frame4import FrcLedger.Keys.Frame56/-!7# 8-dirac — Schrödinger and Dirac dynamics over the finite substrate: the ledger predicates in Lean (2026-09-20)89Rows of the predicate ledger of *Schrödinger and Dirac Dynamics over Finite Substrate* (tree10`8-dirac-20260709`). The coefficient field `K = F[w]/(w² − ν)` on components with its Frobenius conjugation11and norm, a field when `ν` is a nonsquare, `|K| = |F|²` (A2, B1); the square-class arithmetic on12`ZMod p`: two nonsquares differ by a square and the Lorentzian form depends on `ν` through its class alone13(B2); chronon parity — `g^k` is a square exactly when `k` is even, so the drive and its inverse are14nonsquares and `2`, `2⁻¹`, `−2` and the quarter-turn `i = g^{3κ}` are squares exactly when `κ` is even (B3,15B5); the two seats `ν = g = c²·(2g)` (B4); the norm growth `N(gz) = g² N(z)` (B6); over `K` every base element16is a square, the dichotomy collapsing (B7). The Hermitian form on functions of a finite set — symmetric,17nondegenerate, the translations unitary with `T_u† = T_{−u}`, the Laplacian and the Hamiltonians18self-adjoint (C2); the Cayley step unitary for any anti-involution, hence for the form and for the `X`-form19(C4, D10); the Cayley transform norm-one valued, injective, inverted by the orientation gauge, and the torus20of `|F| + 1` points (C5); kinetic Hamiltonians nilpotent with `𝒜(H) = K⁻`, the Cayley step of period exactly21`p` (C6, E4). The Clifford relations from `i² = −1`, `w² = ν` alone, by the block computation of the paper's22proof (D2); the boost torus — `A² − νB² = 1`, the group law of the entries, the boost `z ↦ z/z̄` a23homomorphism onto `N¹` with kernel the scalar line (Hilbert 90), `N¹ ≅ C_{p+1}` cyclic, an element of order24three exactly when `3 ∣ p + 1` (D5); spin conjugation and the transported gammas (D6, D7); the spinor twist25`X = γ⁰γ¹γ³` with `X² = ν`, its commutations, the dagger signs with `γ²` the obstruction, `(γ^μ)†X = −Xγ^μ`26and the failure of the `γ⁰`-twist (D9); the transport of the form `S†XS = δX` (D11); the worked shells27`𝔽₁₃`, `𝔽₁₇` and the laboratory Carrier (D12, B4). The loss factor and the power-map counts on the cyclic28group `(ZMod p)ˣ` (E2, E3), the potential period `p + 1` attained (E4); the latitude identities (F2); the29drive on the characters — the eigenvalues `g^{−k}`, the isotropy `Σ_x x^{2k}` by the character sum, the30exceptional lines `±1` (F3); the sector separation, no meridional plane waves, the dispersion relation (F4).31Classical (tier 2) on Mathlib's hierarchy; the finite content — parity, latitude and spectral rows on every32frame, the worked shells decided by the kernel — is proved with no axioms in `FrcCore/Dirac.lean`. Outside33both modules: the factorization `(𝒟 − m)(𝒟 + m) = KG − m²` (D3), the pullback identity and the transported34factorization (D7), the covariance of the transported family (D8), the operator clauses of D9 (`T − T⁻¹`35nilpotent and anti-self-adjoint, `𝒟^s` `X`-self-adjoint and nilpotent — the package's instances), the massless36clause and the numerals `5`, `75`, `150` of D10 (the Cayley step's `X`-unitarity is `cayley_unitary` given that37self-adjointness), the pullback and transport clauses of D11, the frame covariance of C2, the surjectivity38of the Cayley transform onto `N¹ ∖ {−1}` (C5 — injectivity and the count are proved), the mixed datum `1563`39of E4, the general count of the unit-norm circle (F2 — instances in the core), and the realisation rows B8,40D13, F5.41-/4243namespace FRC.Dirac4445section46open FRC.Extension (Ext)47open FRC.Extension.Ext48open FRC.Frame (parity_iff drive_nonsquare)4950/-! ## The norm-one torus and the Cayley transform -/51namespace Ext52variable {F : Type*} [Field F] {ν : F}5354/-- The finite Cayley transform `φ_α(t) = (1 + αt)/(1 − αt)` for `α = k w`, computed by the conjugate:55`(1 + αt) · conj(1 − αt) / N(1 − αt)`. -/56noncomputable def cayley (k t : F) : Ext F ν :=57  (1 + ofBase (k * t) * w) * (1 - ofBase (k * t) * w)⁻¹5859theorem norm_ofBase_mul (a : F) (z : Ext F ν) : Ext.norm (ofBase a * z) = a ^ 2 * Ext.norm z := by60  simp only [Ext.norm, mul_re, mul_im, ofBase_re, ofBase_im]; ring6162theorem norm_one_add_kw (k t : F) : Ext.norm ((1 : Ext F ν) + ofBase (k * t) * w) = 1 - ν * (k * t) ^ 2 := by63  simp only [Ext.norm, add_re, add_im, one_re, one_im, mul_re, mul_im, ofBase_re, ofBase_im, w_re, w_im]; ring6465theorem norm_one_sub_kw (k t : F) : Ext.norm ((1 : Ext F ν) - ofBase (k * t) * w) = 1 - ν * (k * t) ^ 2 := by66  simp only [Ext.norm, sub_re, sub_im, one_re, one_im, mul_re, mul_im, ofBase_re, ofBase_im, w_re, w_im]; ring6768theorem norm_conj (z : Ext F ν) : Ext.norm (conj z) = Ext.norm z := by simp [Ext.norm]6970/-- `N(z⁻¹) = N(z)⁻¹`. -/71theorem norm_inv (hν : ¬ IsSquare ν) (z : Ext F ν) : Ext.norm z⁻¹ = (Ext.norm z)⁻¹ := by72  by_cases hz : z = 073  · subst hz74    rw [inv_def]75    simp [Ext.norm]76  · rw [inv_def, norm_ofBase_mul, norm_conj]77    have := (norm_eq_zero_iff hν z).not.2 hz78    field_simp7980theorem one_sub_nu_sq_ne_zero (hν : ¬ IsSquare ν) (t : F) : 1 - ν * t ^ 2 ≠ 0 := by81  intro h82  by_cases ht : t = 083  · simp [ht] at h84  · apply hν85    refine ⟨t⁻¹, ?_⟩86    field_simp87    linear_combination -h8889/-- 8:C5 — the Cayley transform takes values in the norm-one torus: `N(φ_α(λ)) = 1` for every `λ ∈ F`, the90denominator never vanishing (Theorem `cayley-transform`). -/91theorem cayley_norm (hν : ¬ IsSquare ν) (k t : F) : Ext.norm (cayley k t : Ext F ν) = 1 := by92  unfold cayley93  rw [Ext.norm_mul, norm_inv hν, norm_one_add_kw, norm_one_sub_kw]94  exact mul_inv_cancel₀ (one_sub_nu_sq_ne_zero hν _)9596end Ext9798/-! ## The norm-one torus as a group, the boost homomorphism and Hilbert 90 (8:D5, C5) -/99namespace Ext100variable {F : Type*} [Field F] {ν : F}101102/-- Conjugation as a ring homomorphism. -/103def conjHom : Ext F ν →+* Ext F ν where104  toFun := conj105  map_one' := conj_one106  map_mul' := Ext.conj_mul107  map_zero' := by ext <;> simp108  map_add' := conj_add109110@[simp] theorem conjHom_apply (z : Ext F ν) : conjHom z = conj z := rfl111112instance : Nontrivial (Ext F ν) := ⟨⟨0, 1, fun h => by simpa using congrArg re h⟩⟩113114/-- The base field as a ring homomorphism into `K`. -/115def ofBaseHom : F →+* Ext F ν where116  toFun := ofBase117  map_one' := rfl118  map_mul' := ofBase_mul119  map_zero' := rfl120  map_add' := ofBase_add121122@[simp] theorem ofBaseHom_apply (a : F) : ofBaseHom a = (ofBase a : Ext F ν) := rfl123124theorem norm_one : Ext.norm (1 : Ext F ν) = 1 := by simp [Ext.norm]125126/-- `N¹`, the norm-one torus, as a subgroup of the units of `K` (no field structure needed). -/127def normOneGroup (F : Type*) [Field F] (ν : F) : Subgroup (Ext F ν)ˣ where128  carrier := {u | Ext.norm (u : Ext F ν) = 1}129  mul_mem' {a b} ha hb := by130    simp only [Set.mem_setOf_eq, Units.val_mul] at *131    rw [Ext.norm_mul, ha, hb, one_mul]132  one_mem' := by simp [norm_one]133  inv_mem' {a} ha := by134    simp only [Set.mem_setOf_eq] at *135    have h := Ext.norm_mul (a : Ext F ν) (↑a⁻¹ : Ext F ν)136    rw [Units.mul_inv, norm_one, ha, one_mul] at h137    exact h.symm138139theorem mem_normOneGroup {u : (Ext F ν)ˣ} : u ∈ normOneGroup F ν ↔ Ext.norm (u : Ext F ν) = 1 := Iff.rfl140141/-- Conjugation on the units. -/142def conjUnits : (Ext F ν)ˣ →* (Ext F ν)ˣ where143  toFun z := ⟨conj z, conj (↑z⁻¹ : Ext F ν), by rw [← Ext.conj_mul, Units.mul_inv, conj_one],144    by rw [← Ext.conj_mul, Units.inv_mul, conj_one]⟩145  map_one' := Units.ext (by simp [conj_one])146  map_mul' z z' := Units.ext (by simp [Ext.conj_mul])147148@[simp] theorem conjUnits_val (z : (Ext F ν)ˣ) : ((conjUnits z : (Ext F ν)ˣ) : Ext F ν) = conj z := rfl149150/-- The boost map `z ↦ z / z̄` on the units, a homomorphism (Lemma `boost-torus`). -/151def boost : (Ext F ν)ˣ →* (Ext F ν)ˣ where152  toFun z := z * (conjUnits z)⁻¹153  map_one' := by simp154  map_mul' z z' := by155    simp only [map_mul, mul_inv]156    exact mul_mul_mul_comm _ _ _ _157158theorem boost_def (z : (Ext F ν)ˣ) : boost z = z * (conjUnits z)⁻¹ := rfl159160theorem boost_val (z : (Ext F ν)ˣ) : (boost z : Ext F ν) * conj (z : Ext F ν) = (z : Ext F ν) := by161  rw [boost_def, Units.val_mul, mul_assoc, ← conjUnits_val, ← Units.val_mul, inv_mul_cancel, Units.val_one,162    mul_one]163164/-- 8:D5 — the boost of every unit lies in `N¹`: `N(z/z̄) = 1`. -/165theorem boost_mem (z : (Ext F ν)ˣ) : boost z ∈ normOneGroup F ν := by166  rw [mem_normOneGroup]167  have h := congrArg Ext.norm (boost_val z)168  rw [Ext.norm_mul, norm_conj] at h169  have hz : Ext.norm (z : Ext F ν) ≠ 0 := by170    intro h0171    have := Ext.norm_mul (z : Ext F ν) (↑z⁻¹ : Ext F ν)172    rw [Units.mul_inv, norm_one, h0, zero_mul] at this173    exact one_ne_zero this174  exact mul_right_cancel₀ hz (by rw [h, one_mul])175176/-- 8:D5 — the kernel of the boost is the scalar line: `z/z̄ = 1 ⟺ z̄ = z ⟺ z ∈ F`. -/177theorem boost_eq_one_iff (h2 : (2 : F) ≠ 0) [NoZeroDivisors F] (z : (Ext F ν)ˣ) :178    boost z = 1 ↔ (z : Ext F ν).im = 0 := by179  rw [← conj_eq_self_iff (z : Ext F ν) h2, boost_def, mul_inv_eq_one]180  constructor181  · intro h; exact (congrArg Units.val h).symm182  · intro h; exact Units.ext h.symm183184/-- 8:D5, 8:A2 — Hilbert 90 on the torus: every `u ∈ N¹` is a boost — `u = (1 + u)/(1 + ū)` for `u ≠ −1`, and185`−1 = w/w̄`. -/186theorem exists_boost_eq (hν : ¬ IsSquare ν) {u : (Ext F ν)ˣ} (hu : u ∈ normOneGroup F ν) :187    ∃ z : (Ext F ν)ˣ, boost z = u := by188  letI := field hν189  rw [mem_normOneGroup] at hu190  have hconj : conj (u : Ext F ν) = ((u⁻¹ : (Ext F ν)ˣ) : Ext F ν) := by191    have := mul_conj (u : Ext F ν)192    rw [hu, ofBase_one] at this193    exact (Units.inv_eq_of_mul_eq_one_right this).symm194  by_cases hm : (u : Ext F ν) = -1195  · -- `u = −1 = w / w̄`196    have hw : (w : Ext F ν) ≠ 0 := fun h => by simpa using congrArg im h197    refine ⟨Units.mk0 w hw, Units.ext ?_⟩198    apply mul_right_cancel₀ (show conj (w : Ext F ν) ≠ 0 by rw [conj_w]; exact neg_ne_zero.2 hw)199    have hb := boost_val (Units.mk0 w hw)200    rw [Units.val_mk0] at hb201    rw [hb, hm, conj_w, neg_one_mul, neg_neg]202  · have h1 : (1 : Ext F ν) + (u : Ext F ν) ≠ 0 := fun h => hm (by linear_combination h)203    refine ⟨Units.mk0 ((1 : Ext F ν) + (u : Ext F ν)) h1, Units.ext ?_⟩204    apply mul_right_cancel₀ (show conj ((1 : Ext F ν) + (u : Ext F ν)) ≠ 0 by205      intro h206      have := congrArg conj h207      rw [conj_conj] at this208      exact h1 (this.trans (by ext <;> simp)))209    have hb := boost_val (Units.mk0 ((1 : Ext F ν) + (u : Ext F ν)) h1)210    rw [Units.val_mk0] at hb211    rw [hb, conj_add, conj_one, hconj]212    have : (u : Ext F ν) * ((u⁻¹ : (Ext F ν)ˣ) : Ext F ν) = 1 := Units.mul_inv u213    linear_combination -this214215end Ext216217/-! ## The cardinalities: `|K| = |F|²`, `|N¹| = |F| + 1` (8:C5, D5) -/218namespace Ext219variable {F : Type*} [Field F] {ν : F}220221/-- `K ≃ F × F` on components. -/222def equivProd : Ext F ν ≃ F × F where223  toFun z := (z.re, z.im)224  invFun x := ⟨x.1, x.2⟩225  left_inv z := by cases z; rfl226  right_inv x := by cases x; rfl227228instance [Finite F] : Finite (Ext F ν) := Finite.of_equiv _ (equivProd (ν := ν)).symm229230omit [Field F] in231theorem card_ext [CommRing F] [Finite F] : Nat.card (Ext F ν) = Nat.card F ^ 2 := by232  rw [Nat.card_congr (equivProd (ν := ν)), Nat.card_prod, sq]233234/-- The kernel of the boost is the image of `Fˣ`: its cardinality is `|F| − 1`. -/235def baseUnits (h2 : (2 : F) ≠ 0) : Fˣ ≃ (boost (F := F) (ν := ν)).ker where236  toFun a := ⟨Units.map (ofBaseHom (ν := ν)).toMonoidHom a, by237      rw [MonoidHom.mem_ker, boost_eq_one_iff h2]; rfl⟩238  invFun z := Units.mk0 ((z : (Ext F ν)ˣ) : Ext F ν).re (by239      intro h240      have hz := (z : (Ext F ν)ˣ).ne_zero241      have him : ((z : (Ext F ν)ˣ) : Ext F ν).im = 0 := (boost_eq_one_iff h2 _).1 (MonoidHom.mem_ker.1 z.2)242      exact hz (by ext <;> simp [h, him]))243  left_inv a := by ext; rfl244  right_inv z := by245    have him : ((z : (Ext F ν)ˣ) : Ext F ν).im = 0 := (boost_eq_one_iff h2 _).1 (MonoidHom.mem_ker.1 z.2)246    apply Subtype.ext; apply Units.ext247    ext248    · rfl249    · exact him.symm250251/-- 8:D5, 8:C5 — the torus has `|F| + 1` elements: `|Kˣ| = |ker| · |N¹|`, `(q² − 1) = (q − 1)(q + 1)`. -/252theorem card_normOneGroup [Finite F] (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) :253    Nat.card (normOneGroup F ν) = Nat.card F + 1 := by254  letI := field hν255  have hrange : (boost (F := F) (ν := ν)).range = normOneGroup F ν := by256    ext u257    constructor258    · rintro ⟨z, rfl⟩; exact boost_mem z259    · intro hu; exact exists_boost_eq hν hu260  have h1 : Nat.card (Ext F ν)ˣ = Nat.card (Ext F ν) - 1 := Nat.card_units _261  have h2' : Nat.card (Ext F ν)ˣ = Nat.card ((Ext F ν)ˣ ⧸ (boost (F := F) (ν := ν)).ker) * Nat.card (boost (F := F) (ν := ν)).ker :=262    Subgroup.card_eq_card_quotient_mul_card_subgroup _263  have h3 : Nat.card ((Ext F ν)ˣ ⧸ (boost (F := F) (ν := ν)).ker) = Nat.card (normOneGroup F ν) := by264    rw [Nat.card_congr (QuotientGroup.quotientKerEquivRange (boost (F := F) (ν := ν))).toEquiv, hrange]265  have h4 : Nat.card (boost (F := F) (ν := ν)).ker = Nat.card F - 1 := by266    rw [← Nat.card_congr (baseUnits h2), Nat.card_units]267  have hq : 2 ≤ Nat.card F := by268    have := Nat.card_pos (α := F)269    by_contra hlt270    have h1' : Nat.card F = 1 := by omega271    have := Nat.card_eq_one_iff_unique.1 h1'272    obtain ⟨hsub, _⟩ := this273    exact one_ne_zero (hsub.elim 1 0)274  rw [h3, h4] at h2'275  rw [card_ext] at h1276  -- (q² − 1) = N · (q − 1)  ⇒  N = q + 1277  have key : Nat.card F ^ 2 - 1 = Nat.card (normOneGroup F ν) * (Nat.card F - 1) := by rw [← h1]; exact h2'278  have hsq : Nat.card F ^ 2 - 1 = (Nat.card F + 1) * (Nat.card F - 1) := by279    have := sq_tsub_sq (Nat.card F) 1280    rw [one_pow] at this281    exact this282  rw [hsq] at key283  exact (Nat.eq_of_mul_eq_mul_right (by omega) key).symm284285end Ext286287/-! ## Field-generic lemmas (the `ZMod p` instances under `Fact p.Prime` are not `ring`-friendly) -/288section generic289variable {K : Type*} [Field K]290291theorem inv_square_iff (a : K) : IsSquare a⁻¹ ↔ IsSquare a := by292  constructor293  · rintro ⟨r, hr⟩; exact ⟨r⁻¹, by rw [← mul_inv, ← hr, inv_inv]⟩294  · rintro ⟨r, hr⟩; exact ⟨r⁻¹, by rw [← mul_inv, ← hr]⟩295296theorem neg_two_square_iff {i : K} (hi : -1 = i * i) : IsSquare (-2 : K) ↔ IsSquare (2 : K) := by297  constructor298  · rintro ⟨r, hr⟩; exact ⟨i * r, by linear_combination (r * r) * hi - hr⟩299  · rintro ⟨r, hr⟩; exact ⟨i * r, by linear_combination (r * r) * hi - hr⟩300301theorem three_kappa_pow (g : K) (κ : ℕ) (h : g ^ (2 * κ) = -1) : g ^ (3 * κ) = -g ^ κ := by302  rw [show 3 * κ = 2 * κ + κ by ring, pow_add, h, neg_one_mul]303304theorem sq_eq_one_cases {x : K} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by305  rw [sq] at h; exact mul_self_eq_one_iff.1 h306307theorem neg_inv_of_mul {a c : K} (hc : c ≠ 0) (h : c * a = -1) : a = -c⁻¹ := by308  field_simp; linear_combination h309310theorem three_quarters {a : K} (h4 : (4 : K) ≠ 0) (h : a = -4⁻¹) : 1 + a = 3 * 4⁻¹ := by311  rw [h]; field_simp; ring312313theorem half_neg {a : K} (h2 : (2 : K) ≠ 0) (h : 4 * a = -1) : 2 * a = -2⁻¹ := by314  field_simp; linear_combination h315316theorem four_ne_zero_of_two {K : Type*} [Ring K] (h : (2 : K) ≠ 0) [NoZeroDivisors K] : (4 : K) ≠ 0 := by317  intro h4; apply h318  have : (4 : K) = 2 * 2 := by norm_num319  rw [this] at h4320  rcases mul_eq_zero.1 h4 with h0 | h0 <;> exact h0321322end generic323324/-! ## Chronon parity (8:B5, B3, B4) on `ZMod p` -/325section parity326variable {p : ℕ} [hp : Fact (Nat.Prime p)]327328/-- 8:B3, 8:B4 — on the shell `p = 4κ + 1`: `2` is a square ⟺ `κ` even (the second supplementary law), and329so `2⁻¹ = c²` and `−2` (`−1` a square); the quarter-turn `i = g^{−κ} = g^{3κ}` is a square ⟺ `κ` even. -/330theorem named_residues (κ : ℕ) [hp' : Fact (Nat.Prime (4 * κ + 1))] {g : ZMod (4 * κ + 1)}331    (hg : orderOf g = 4 * κ) :332    (IsSquare (2 : ZMod (4 * κ + 1)) ↔ Even κ) ∧ (IsSquare (2⁻¹ : ZMod (4 * κ + 1)) ↔ Even κ) ∧333    (IsSquare (-2 : ZMod (4 * κ + 1)) ↔ Even κ) ∧ (IsSquare (g ^ (3 * κ)) ↔ Even κ) ∧334    g ^ (3 * κ) = -g ^ κ ∧ IsSquare (-1 : ZMod (4 * κ + 1)) := by335  have hne : 4 * κ + 1 ≠ 2 := by omega336  have h2 : IsSquare (2 : ZMod (4 * κ + 1)) ↔ Even κ := by337    rw [ZMod.exists_sq_eq_two_iff hne, Nat.even_iff]; omega338  have hm1 : IsSquare (-1 : ZMod (4 * κ + 1)) := (ZMod.exists_sq_eq_neg_one_iff (p := 4 * κ + 1)).2 (by omega)339  have h2z : (2 : ZMod (4 * κ + 1)) ≠ 0 := by340    intro h341    have := (ZMod.natCast_eq_zero_iff 2 (4 * κ + 1)).1 (by exact_mod_cast h)342    have := Nat.le_of_dvd (by norm_num) this343    have := hp'.out.two_le344    omega345  have hodd : (4 * κ + 1) % 2 = 1 := by omega346  have hg' : orderOf g = 4 * κ + 1 - 1 := by rw [hg]; rfl347  have hhalf : g ^ (2 * κ) = -1 := by348    have h1 := pow_orderOf_eq_one g349    rw [hg] at h1350    have h2' : (g ^ (2 * κ)) ^ 2 = 1 := by rw [← pow_mul, show 2 * κ * 2 = 4 * κ by ring]; exact h1351    rcases sq_eq_one_cases h2' with h | h352    · exfalso353      have := orderOf_dvd_iff_pow_eq_one.2 h354      rw [hg] at this355      have hκ : 0 < κ := by356        by_contra hk; push_neg at hk357        have : κ = 0 := by omega358        subst this; exact absurd hp'.out (by decide)359      have := Nat.le_of_dvd (by omega) this360      omega361    · exact h362  refine ⟨h2, ?_, ?_, ?_, ?_, hm1⟩363  · exact (inv_square_iff (2 : ZMod (4 * κ + 1))).trans h2364  · obtain ⟨i, hi⟩ := hm1365    exact (neg_two_square_iff hi).trans h2366  · rw [parity_iff hg' hodd, Nat.even_mul]367    constructor368    · rintro (h | h)369      · exact absurd h (by decide)370      · exact h371    · intro h; exact Or.inr h372  · exact three_kappa_pow g κ hhalf373374end parity375376/-! ## The Cayley step preserves any Hermitian pairing (8:C4, D10) -/377section cayley378variable {R : Type*} [Ring R]379380/-- 8:C4, 8:D10 — the exact Hermitian preservation, for any anti-involution `σ` of the operator ring (the381adjoint of a nondegenerate Hermitian form, or the `X`-adjoint of the spinor form): if `σ h = h`, the scalar382`a` is central with `σ a = −a`, and `1 − a h` is a unit, then `u = (1 − a h)⁻¹ (1 + a h)` satisfies383`σ u · u = 1` — the Cayley step is unitary (Theorem `cayley-preservation`). For D10 the premise384`σ h = h` is the `X`-self-adjointness of `𝒟^s − m` (D9's operator clause, decided by the package at385`p = 5, 13, 17` and not proved here). -/386theorem cayley_unitary (σ : R → R) (hmul : ∀ x y, σ (x * y) = σ y * σ x) (hadd : ∀ x y, σ (x + y) = σ x + σ y)387    (hone : σ 1 = 1) (hneg : ∀ x, σ (-x) = -σ x)388    {h a : R} (hh : σ h = h) (ha : σ a = -a) (hc : ∀ x, Commute a x)389    (hu : IsUnit (1 - a * h)) :390    let u := (hu.unit⁻¹ : Rˣ) * (1 + a * h)391    σ (u : R) * u = 1 := by392  intro u393  -- σ(1 − a h) = 1 + a h and σ(1 + a h) = 1 − a h394  have hsub : σ (1 - a * h) = 1 + a * h := by395    rw [sub_eq_add_neg, hadd, hone, hneg, hmul, hh, ha, mul_neg, neg_neg, (hc h).eq]396  have hadd' : σ (1 + a * h) = 1 - a * h := by397    rw [hadd, hone, hmul, hh, ha, mul_neg, (hc h).eq, sub_eq_add_neg]398  -- the inverse commutes with 1 + a h399  have hcomm : Commute (1 - a * h) (1 + a * h) :=400    (Commute.one_left _).sub_left ((Commute.one_right (a * h)).add_right (Commute.refl (a * h)))401  have hinv_comm : Commute ((hu.unit⁻¹ : Rˣ) : R) (1 + a * h) := by402    have hcu : Commute (hu.unit : R) (1 + a * h) := by rw [IsUnit.unit_spec]; exact hcomm403    exact (Commute.units_inv_left_iff).2 hcu404  -- σ of the inverse is the inverse of σ405  have hσinv : σ ((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h) = 1 := by406    have e : (1 - a * h) * ((hu.unit⁻¹ : Rˣ) : R) = 1 := by407      have := hu.unit.mul_inv408      rw [IsUnit.unit_spec] at this409      exact this410    have := congrArg σ e411    rw [hmul, hsub, hone] at this412    exact this413  show σ (((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h)) * (((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h)) = 1414  rw [hmul, hadd']415  -- (1 − a h) · σ(inv) · inv · (1 + a h): use σ(inv)(1 + a h) = 1 and commutation416  calc (1 - a * h) * σ ((hu.unit⁻¹ : Rˣ) : R) * (((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h))417      = (1 - a * h) * σ ((hu.unit⁻¹ : Rˣ) : R) * ((1 + a * h) * ((hu.unit⁻¹ : Rˣ) : R)) := by418        rw [hinv_comm.eq]419    _ = (1 - a * h) * (σ ((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h)) * ((hu.unit⁻¹ : Rˣ) : R) := by420        simp only [mul_assoc]421    _ = (1 - a * h) * ((hu.unit⁻¹ : Rˣ) : R) := by rw [hσinv, mul_one]422    _ = 1 := by423        have := hu.unit.mul_inv424        rw [IsUnit.unit_spec] at this425        exact this426427/-- 8:C4 — every orbit is periodic: a unit of a finite ring has finite order (Corollary428`finite-periodicity`). -/429theorem cayley_periodic {R : Type*} [Ring R] [Finite R] (u : Rˣ) : IsOfFinOrder u := isOfFinOrder_of_finite u430431end cayley432433/-! ## Kinetic Hamiltonians: nilpotent, fully admissible, of period `p` (8:C6, E4) -/434section kinetic435variable {R : Type*} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p]436437/-- 8:E4 (1), 8:C6, 8:D10 — the translation `t` of order `p` (`t^p = 1`) has `(t − 1)^p = 0` in438characteristic `p`: the kinetic Hamiltonians and the symmetric differences are nilpotent (Theorem439`period-dichotomy` (1), Corollary `kinetic-admissible`). -/440theorem translation_nilpotent {t : R} (ht : t ^ p = 1) : (t - 1) ^ p = 0 := by441  rw [sub_pow_char_of_commute p (Commute.one_right t), ht, one_pow, sub_self]442443/-- 8:E4 (1), 8:C6 — `h = c (t + t^{p−1} − 2) = c t^{p−1} (t − 1)²` and with it `a h` for any `a` commuting with444`t` and `c` is nilpotent, `(a h)^p = 0`, so `1 − a h` is a unit: the Cayley step is defined for every `a` —445`𝒜(H) = K⁻` (Corollary `kinetic-admissible`; `H = −Δ` at `c = −1`). -/446theorem kinetic_nilpotent {t c a : R} (ht : t ^ p = 1) (hct : Commute c t) (hat : Commute a t)447    (hac : Commute a c) :448    let h := c * (t + t ^ (p - 1) - 2)449    (a * h) ^ p = 0 ∧ IsNilpotent (a * h) ∧ IsUnit (1 - a * h) := by450  intro h451  have hp1 : (p - 1) + 1 = p := Nat.sub_add_cancel hp.out.one_le452  -- h = c t^{p−1} (t − 1)²453  have hfac : h = c * t ^ (p - 1) * (t - 1) ^ 2 := by454    show c * (t + t ^ (p - 1) - 2) = c * t ^ (p - 1) * (t - 1) ^ 2455    have e : t ^ (p - 1) * (t - 1) ^ 2 = t + t ^ (p - 1) - 2 := by456      have : t ^ (p - 1) * t = 1 := by rw [← pow_succ, hp1, ht]457      have h2 : t ^ (p - 1) * t ^ 2 = t := by rw [pow_two, ← mul_assoc, this, one_mul]458      calc t ^ (p - 1) * (t - 1) ^ 2 = t ^ (p - 1) * t ^ 2 - 2 * (t ^ (p - 1) * t) + t ^ (p - 1) := by459            noncomm_ring460        _ = t + t ^ (p - 1) - 2 := by rw [h2, this, mul_one]; noncomm_ring461    rw [mul_assoc, e]462  have hcomm : Commute a (c * t ^ (p - 1) * (t - 1) ^ 2) :=463    (hac.mul_right (hat.pow_right _)).mul_right ((hat.sub_right (Commute.one_right a)).pow_right 2)464  have hcomm2 : Commute (a * (c * t ^ (p - 1))) ((t - 1) ^ 2) := by465    have h1 : Commute a ((t - 1) ^ 2) := (hat.sub_right (Commute.one_right a)).pow_right 2466    have h2 : Commute (c * t ^ (p - 1)) ((t - 1) ^ 2) :=467      ((hct.sub_right (Commute.one_right c)).pow_right 2).mul_left ((Commute.refl t).pow_left _ |>.sub_right (Commute.one_right _) |>.pow_right 2)468    exact h1.mul_left h2469  have key : (a * h) ^ p = 0 := by470    rw [hfac, ← mul_assoc, hcomm2.mul_pow, ← pow_mul, show 2 * p = p + p by ring, pow_add,471      translation_nilpotent ht, mul_zero, mul_zero]472  refine ⟨key, ⟨p, key⟩, IsNilpotent.isUnit_one_sub ⟨p, key⟩⟩473474/-- 8:E4 (1), 8:C6 — the period: for a nilpotent `n` with `n^p = 0` and `2` a unit, the Cayley step475`u = (1 − n)⁻¹(1 + n)` is unipotent — `u − 1 = 2(1 − n)⁻¹ n`, `(u − 1)^p = 0`, `u^p = 1` — and `u ≠ 1` when476`n ≠ 0`, so in the prime characteristic `ord(U) = p` exactly (Theorem `period-dichotomy` (1); on `𝔽₁₃`,477`ord(U_{kw, −Δ}) = 13` for every `k ≠ 0`, Example `cayley-13`). -/478theorem cayley_period {n : R} (hn : n ^ p = 0) (h2 : IsUnit (2 : R)) (hn0 : n ≠ 0) :479    let hu : IsUnit (1 - n) := IsNilpotent.isUnit_one_sub ⟨p, hn⟩480    let hu' : IsUnit (1 + n) := by481      rw [← sub_neg_eq_add]; exact IsNilpotent.isUnit_one_sub ⟨p, by rw [neg_pow, hn, mul_zero]⟩482    let u : Rˣ := hu.unit⁻¹ * hu'.unit483    (u : R) = ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) ∧ u ^ p = 1 ∧ u ≠ 1 ∧ orderOf u = p := by484  intro hu hu' u485  have hval : (u : R) = ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) := by486    show ((hu.unit⁻¹ : Rˣ) : R) * (hu'.unit : R) = _487    rw [IsUnit.unit_spec]488  have hv : ((hu.unit⁻¹ : Rˣ) : R) * (1 - n) = 1 := by489    have := hu.unit.inv_mul; rwa [IsUnit.unit_spec] at this490  have hvn : Commute ((hu.unit⁻¹ : Rˣ) : R) n := by491    have : Commute (hu.unit : R) n := by492      rw [IsUnit.unit_spec]; exact (Commute.one_left n).sub_left (Commute.refl n)493    exact (Commute.units_inv_left_iff).2 this494  have hu1 : (u : R) - 1 = 2 * (((hu.unit⁻¹ : Rˣ) : R) * n) := by495    rw [hval]496    calc ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) - 1497        = ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) - ((hu.unit⁻¹ : Rˣ) : R) * (1 - n) := by rw [hv]498      _ = 2 * (((hu.unit⁻¹ : Rˣ) : R) * n) := by noncomm_ring499  have hpow : ((u : R) - 1) ^ p = 0 := by500    rw [hu1, (Commute.ofNat_left 2 _).mul_pow, hvn.mul_pow, hn, mul_zero, mul_zero]501  have hup : u ^ p = 1 := by502    apply Units.ext503    rw [Units.val_pow_eq_pow_val, Units.val_one]504    have : (u : R) = ((u : R) - 1) + 1 := (sub_add_cancel _ _).symm505    rw [this, add_pow_char_of_commute p (Commute.one_right _), hpow, one_pow, zero_add]506  have hne : u ≠ 1 := by507    intro h508    have : (u : R) - 1 = 0 := by rw [h, Units.val_one, sub_self]509    rw [hu1] at this510    have := (h2.mul_right_eq_zero).1 this511    have := ((Units.isUnit (hu.unit⁻¹)).mul_right_eq_zero).1 this512    exact hn0 this513  exact ⟨hval, hup, hne, orderOf_eq_prime hup hne⟩514515end kinetic516517/-! ## The Hermitian form on a finite configuration space (8:C2) -/518section hermitian519variable {K : Type*} [CommRing K] [StarRing K] {X : Type*} [Fintype X]520521/-- `⟨ψ, φ⟩_X = Σ_x ψ(x)* φ(x)` (Definition `hermitian-form`). -/522def herm (ψ φ : X → K) : K := ∑ x, star (ψ x) * φ x523524/-- 8:C2 — Hermitian symmetry `⟨ψ, φ⟩* = ⟨φ, ψ⟩`; linearity in the second slot, conjugate-linearity in the first. -/525theorem herm_star (ψ φ : X → K) : star (herm ψ φ) = herm φ ψ := by526  simp [herm, star_sum, star_mul, mul_comm]527528theorem herm_add_right (ψ φ φ' : X → K) : herm ψ (φ + φ') = herm ψ φ + herm ψ φ' := by529  simp [herm, mul_add, Finset.sum_add_distrib]530531theorem herm_sub_right (ψ φ φ' : X → K) : herm ψ (φ - φ') = herm ψ φ - herm ψ φ' := by532  simp [herm, mul_sub, Finset.sum_sub_distrib]533534theorem herm_smul_right (ψ φ : X → K) (c : K) : herm ψ (c • φ) = c * herm ψ φ := by535  simp [herm, Finset.mul_sum, mul_left_comm]536537theorem herm_add_left (ψ ψ' φ : X → K) : herm (ψ + ψ') φ = herm ψ φ + herm ψ' φ := by538  simp [herm, add_mul, Finset.sum_add_distrib]539540theorem herm_sub_left (ψ ψ' φ : X → K) : herm (ψ - ψ') φ = herm ψ φ - herm ψ' φ := by541  simp [herm, sub_mul, Finset.sum_sub_distrib]542543theorem herm_smul_left (ψ φ : X → K) (c : K) : herm (c • ψ) φ = star c * herm ψ φ := by544  simp [herm, Finset.mul_sum, mul_assoc]545546/-- 8:C2 — nondegeneracy: `⟨ψ, φ⟩ = 0` for every `φ` forces `ψ = 0` (Lemma `hermitian-nondeg`; the test547function is the point mass at `x₀`). -/548theorem herm_nondegenerate [DecidableEq X] (ψ : X → K) (h : ∀ φ, herm ψ φ = 0) : ψ = 0 := by549  funext x₀550  have := h (Pi.single x₀ 1)551  simp [herm, Pi.single_apply] at this552  have h2 := congrArg star this553  simpa using h2554555/-- The translation `(T_u ψ)(x) = ψ(x + u)` on an additive group. -/556def translate {G : Type*} [AddGroup G] (u : G) (ψ : G → K) : G → K := fun x => ψ (x + u)557558/-- 8:C2 — every translation is unitary for the form, and `T_u† = T_{−u}` (Proposition559`translation-unitary`). -/560theorem herm_translate {G : Type*} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K) :561    herm (translate u ψ) (translate u φ) = herm ψ φ := by562  unfold herm translate563  exact Fintype.sum_equiv (Equiv.addRight u) _ _ (fun x => rfl)564565/-- 8:C2 — the adjoint of a translation is the opposite translation, `T_u† = T_{−u}` (Proposition566`translation-unitary`). -/567theorem herm_translate_adjoint {G : Type*} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K) :568    herm (translate u ψ) φ = herm ψ (translate (-u) φ) := by569  unfold herm translate570  refine (Fintype.sum_equiv (Equiv.addRight u) _ _ (fun x => ?_))571  simp572573/-- The finite Laplacian along one direction, `Δ = T_e + T_{−e} − 2`, and the Hamiltonian574`H = −ϰ Δ + M_V` (`(M_V ψ)(x) = V(x) ψ(x)`). -/575def laplacian {G : Type*} [AddGroup G] (e : G) (ψ : G → K) : G → K :=576  translate e ψ + translate (-e) ψ - (2 : K) • ψ577578def hamiltonian {G : Type*} [AddGroup G] (e : G) (ϰ : K) (V : G → K) (ψ : G → K) : G → K :=579  (-ϰ) • laplacian e ψ + fun x => V x * ψ x580581/-- 8:C2 — the Laplacian along one direction is self-adjoint, `⟨Δψ, φ⟩ = ⟨ψ, Δφ⟩` (Proposition582`laplacian-sa`; the `d`-dimensional Laplacian is the sum over the directions), and with it every Hamiltonian583`−ϰΔ + M_V` with `ϰ` and `V` Frobenius-fixed (Corollary `hamiltonian-sa`). -/584theorem herm_laplacian {G : Type*} [AddGroup G] [Fintype G] (e : G) (ψ φ : G → K) :585    herm (laplacian e ψ) φ = herm ψ (laplacian e φ) := by586  unfold laplacian587  rw [herm_sub_left, herm_add_left, herm_smul_left, herm_sub_right, herm_add_right, herm_smul_right,588    herm_translate_adjoint, herm_translate_adjoint (-e), neg_neg, star_ofNat, add_comm (herm ψ (translate (-e) φ))]589590/-- 8:C2 — every Hamiltonian `−ϰΔ + M_V` with `ϰ` and `V` Frobenius-fixed is self-adjoint (Corollary591`hamiltonian-sa`). -/592theorem herm_hamiltonian {G : Type*} [AddGroup G] [Fintype G] (e : G) (ϰ : K) (hϰ : star ϰ = ϰ)593    (V : G → K) (hV : ∀ x, star (V x) = V x) (ψ φ : G → K) :594    herm (hamiltonian e ϰ V ψ) φ = herm ψ (hamiltonian e ϰ V φ) := by595  unfold hamiltonian596  rw [herm_add_left, herm_smul_left, herm_laplacian, herm_add_right, herm_smul_right, star_neg, hϰ]597  congr 1598  unfold herm599  refine Finset.sum_congr rfl (fun x _ => ?_)600  rw [star_mul, hV]; ring601602end hermitian603604605/-! ## The free evolution is the drive: the characters, the spectrum and the isotropy (8:F3, F4) -/606section drive607variable {p : ℕ} [hp : Fact (Nat.Prime p)]608609/-- The drive pullback on functions of the phase cycle `Φ = (ZMod p)ˣ`: `(Dψ)(x) = ψ(g⁻¹ x)`. -/610def drive (g : (ZMod p)ˣ) (ψ : (ZMod p)ˣ → ZMod p) : (ZMod p)ˣ → ZMod p := fun x => ψ (g⁻¹ * x)611612/-- The multiplicative characters `χ_k(x) = x^k` (the winding-`k` modes). -/613def chi (k : ℕ) : (ZMod p)ˣ → ZMod p := fun x => (x : ZMod p) ^ k614615/-- 8:F3 (2) — the characters are eigenvectors of the drive with eigenvalue `g^{−k}`: the winding-`k` mode616acquires the phase `g^{−k}` per chronon (Theorem `zonal`). -/617theorem drive_chi (g : (ZMod p)ˣ) (k : ℕ) : drive g (chi k) = fun x => ((g⁻¹ : (ZMod p)ˣ) : ZMod p) ^ k * chi k x := by618  funext x619  simp only [drive, chi, Units.val_mul, mul_pow]620621/-- 8:F3 (1) — the drive is a permutation of the cycle: it preserves the sum defining the form (unitary). -/622theorem drive_sum (g : (ZMod p)ˣ) (f : (ZMod p)ˣ → ZMod p) : ∑ x, f (g⁻¹ * x) = ∑ x, f x :=623  Fintype.sum_equiv (Equiv.mulLeft g⁻¹) _ _ (fun _ => rfl)624625/-- 8:F3 (3) — isotropy: the character values are Frobenius-fixed, so `⟨χ_k, χ_k⟩ = Σ_x x^{2k}`, which is626`0` unless `(p − 1) ∣ 2k` and `−1` otherwise (Mathlib's `FiniteField.sum_pow_units`): every character line is627isotropic except `k = 0` and `k = (p − 1)/2`. -/628theorem chi_isotropy (k : ℕ) :629    (∑ x : (ZMod p)ˣ, chi k x * chi k x) = if p - 1 ∣ 2 * k then -1 else 0 := by630  rw [show (∑ x : (ZMod p)ˣ, chi k x * chi k x) = ∑ x : (ZMod p)ˣ, (x : ZMod p) ^ (2 * k) from631    Finset.sum_congr rfl (fun x _ => by rw [chi, ← mul_pow, ← sq, ← pow_mul])]632  have := FiniteField.sum_pow_units (K := ZMod p) (2 * k)633  rwa [ZMod.card] at this634635/-- 8:F3 (3), 8:F4 — the exceptional eigenvalues are `±1`: on the shell `p = 4κ + 1` with `g` of order `4κ`,636`k = 2κ` gives `g^{−2κ} = −1` (and `k = 0` gives `1`); and these are all of `N¹ ∩ 𝔽_p`: a base-field element637of norm one (`u ū = u² = 1`) is `±1` (Corollary `sectors`). -/638theorem exceptional_eigen (κ : ℕ) [Fact (Nat.Prime (4 * κ + 1))] (g : (ZMod (4 * κ + 1))ˣ)639    (hg : orderOf g = 4 * κ) :640    ((g⁻¹ : (ZMod (4 * κ + 1))ˣ) : ZMod (4 * κ + 1)) ^ (2 * κ) = -1 ∧641    ∀ u : ZMod (4 * κ + 1), u * u = 1 → u = 1 ∨ u = -1 := by642  refine ⟨?_, fun u hu => mul_self_eq_one_iff.1 hu⟩643  have h4 : g ^ (4 * κ) = 1 := by have := pow_orderOf_eq_one g; rwa [hg] at this644  have h2 : (g ^ (2 * κ)) ^ 2 = 1 := by rw [← pow_mul, show 2 * κ * 2 = 4 * κ by ring, h4]645  have hne : g ^ (2 * κ) ≠ 1 := by646    intro h647    have := orderOf_dvd_iff_pow_eq_one.2 h648    rw [hg] at this649    have hκ : 0 < κ := by650      rcases Nat.eq_zero_or_pos κ with h0 | h0651      · subst h0; exact absurd (Fact.out : Nat.Prime (4 * 0 + 1)) (by decide)652      · exact h0653    have := Nat.le_of_dvd (by omega) this654    omega655  have hval : ((g ^ (2 * κ) : (ZMod (4 * κ + 1))ˣ) : ZMod (4 * κ + 1)) = -1 := by656    have h2' : (((g ^ (2 * κ) : (ZMod (4 * κ + 1))ˣ) : ZMod (4 * κ + 1))) ^ 2 = 1 := by657      rw [← Units.val_pow_eq_pow_val, h2, Units.val_one]658    rw [sq] at h2'659    rcases mul_self_eq_one_iff.1 h2' with h | h660    · exact absurd (Units.ext h) hne661    · exact h662  rw [← Units.val_pow_eq_pow_val, inv_pow, ← hval]663  have : (g ^ (2 * κ))⁻¹ = g ^ (2 * κ) := by664    rw [inv_eq_iff_mul_eq_one, ← sq, h2]665  rw [this]666667/-- 8:F4 — the sector separation: `ord(g⁻¹) = ord(g) = p − 1`, the drive's phases run on the split cycle668`μ_{p−1}`, while the norm-one torus has order `p + 1`; and there are no meridional plane waves: no669`K`-valued character of the translation cycle `C_p`, since `p ∤ p² − 1` — no unit of `K` has order `p`670(`gcd(p, |Kˣ|) = 1`). -/671theorem sector_separation {K : Type*} [Field K] [Finite K] (hK : Nat.card K = p ^ 2)672    (g : (ZMod p)ˣ) (hg : orderOf g = p - 1) :673    orderOf g⁻¹ = p - 1 ∧ ∀ x : Kˣ, orderOf x ≠ p := by674  refine ⟨by rw [orderOf_inv, hg], fun x hx => ?_⟩675  have hd := orderOf_dvd_natCard x676  rw [Nat.card_units, hK, hx] at hd677  have hp2 : p ∣ p ^ 2 := dvd_pow_self p two_ne_zero678  have h1 : p ∣ 1 := by679    have := Nat.dvd_sub hp2 hd680    have hle : 1 ≤ p ^ 2 := Nat.one_le_pow _ _ hp.out.pos681    rwa [Nat.sub_sub_self hle] at this682  exact hp.out.one_lt.ne' (Nat.dvd_one.1 h1)683684/-- The dispersion identity in any commutative ring. -/685theorem dispersion_generic {R : Type*} [CommRing R] (a b c : R) (k : ℕ) :686    -((a * c) ^ k + (b * c) ^ k - 2 * c ^ k) = (2 - b ^ k - a ^ k) * c ^ k := by ring687688/-- 8:F4 — the dispersion relation on the cycle: `−Δ_Φ χ_k = (2 − g^k − g^{−k}) χ_k` with689`Δ_Φ = D + D⁻¹ − 2` (the finite band curve). -/690theorem dispersion (g : (ZMod p)ˣ) (k : ℕ) :691    (fun x => -(drive g (chi k) x + drive g⁻¹ (chi k) x - 2 * chi k x)) =692      fun x => (2 - ((g : ZMod p)) ^ k - ((g⁻¹ : (ZMod p)ˣ) : ZMod p) ^ k) * chi k x := by693  funext x694  simp only [drive, chi, inv_inv, Units.val_mul]695  exact dispersion_generic _ _ _ k696697end drive698699/-! ## Reversibility and the information counts (8:E2, E3) -/700section counts701variable {X : Type*} [Fintype X] [DecidableEq X]702703/-- 8:E2 — a self-map of a finite set is bijective exactly when its image count is the whole count (loss704factor `1`): `|f(X)| = |X| ⟺ f bijective` (Proposition `loss-factor-one`). -/705theorem loss_factor_one (f : X → X) : (Finset.univ.image f).card = Fintype.card X ↔ Function.Bijective f := by706  rw [← Finset.card_univ, Finset.card_image_iff, Finset.coe_univ, Set.injOn_univ]707  exact Finite.injective_iff_bijective708709/-- 8:E3 — an invertible map has loss factor one: left multiplication by a unit is a bijection (the Cayley710propagators and the boost transports). -/711theorem unit_loss_factor_one {R : Type*} [Monoid R] (u : Rˣ) : Function.Bijective (fun x : R => (u : R) * x) :=712  (Units.mulLeft u).bijective713714variable {p : ℕ} [hp : Fact (Nat.Prime p)]715716/-- 8:E2 — the power-map count on the phase cycle: `x ↦ x^ε` on `(ZMod p)ˣ` has image of size717`(p − 1)/gcd(ε, p − 1)`, and its kernel — the fibre over `1`, of which every nonempty fibre is a coset —718has `gcd(ε, p − 1)` elements (Proposition `power-map-count`, on the cyclic group of order `p − 1`). -/719theorem power_map_count (ε : ℕ) :720    Nat.card ((powMonoidHom ε : (ZMod p)ˣ →* (ZMod p)ˣ).ker) = Nat.gcd (p - 1) ε ∧721    Nat.card ((powMonoidHom ε : (ZMod p)ˣ →* (ZMod p)ˣ).range) = (p - 1) / Nat.gcd (p - 1) ε := by722  have hc : Nat.card (ZMod p)ˣ = p - 1 := by rw [Nat.card_eq_fintype_card, ZMod.card_units]723  refine ⟨?_, ?_⟩724  · rw [IsCyclic.card_powMonoidHom_ker, hc]725  · rw [IsCyclic.card_powMonoidHom_range, hc]726727end counts728729730/-! ## The torus as a cyclic group of order `p + 1`: the potential periods and the triality clause (8:D5, E4) -/731namespace Ext732variable {F : Type*} [Field F] {ν : F}733734/-- 8:D5 — the range of the boost is exactly `N¹` (Lemma `boost-torus`: `G_ν ≅ K^×/F^× ≅ N¹`). -/735theorem boost_range (hν : ¬ IsSquare ν) :736    (boost (F := F) (ν := ν)).range = normOneGroup F ν := by737  ext u738  constructor739  · rintro ⟨z, rfl⟩; exact boost_mem z740  · intro hu; exact exists_boost_eq hν hu741742/-- 8:D5, 8:C5 — `N¹` is cyclic (a finite subgroup of the units of a field), of order `p + 1` on `F = 𝔽_p`:743`N¹ ≅ C_{p+1}`. -/744theorem normOne_cyclic [Finite F] (hν : ¬ IsSquare ν) :745    letI := field hν; IsCyclic (normOneGroup F ν) := by746  letI := field hν747  infer_instance748749/-- 8:E4 (2) — every phase on the torus has `u^{p+1} = 1`: a potential propagator, diagonal with entries in750`N¹`, has order dividing `p + 1`; and some phase has order exactly `p + 1` (the torus is cyclic), so the bound751is attained (Theorem `period-dichotomy` (2)). -/752theorem torus_period [Finite F] (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) :753    (∀ u : normOneGroup F ν, u ^ (Nat.card F + 1) = 1) ∧ ∃ u : normOneGroup F ν, orderOf u = Nat.card F + 1 := by754  letI := field hν755  have hc := card_normOneGroup hν h2756  refine ⟨fun u => by rw [← hc]; exact pow_card_eq_one', ?_⟩757  obtain ⟨u, hu⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := normOneGroup F ν)758  exact ⟨u, by rw [hu, hc]⟩759760/-- 8:D5 — the triality clause: the torus carries an element of order three exactly when `3 ∣ p + 1`761(Cauchy in the cyclic group `C_{p+1}`; `|G_3| = 18` at `17`, `|G_2| = 14` at `13`). -/762theorem order_three_iff [Finite F] (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) :763    (∃ u : normOneGroup F ν, orderOf u = 3) ↔ 3 ∣ Nat.card F + 1 := by764  have hc := card_normOneGroup hν h2765  constructor766  · rintro ⟨u, hu⟩767    rw [← hc, ← hu]; exact orderOf_dvd_natCard u768  · intro h769    rw [← hc] at h770    exact exists_prime_orderOf_dvd_card' 3 h771772end Ext773774/-! ## The Cayley transform: injective, norm-one valued, inverted by the orientation gauge (8:C5) -/775namespace Ext776variable {F : Type*} [Field F] {ν : F}777778/-- 8:C5 — `φ_α(λ) = (1 + αλ)/(1 − αλ)`, `α = kw ≠ 0`, is injective on `F` (a nonconstant Möbius map): the779self-adjoint line embeds in the torus (Theorem `cayley-transform`). -/780theorem cayley_injective (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) {k : F} (hk : k ≠ 0) :781    Function.Injective (cayley (ν := ν) k) := by782  letI := field hν783  intro s t hst784  unfold cayley at hst785  have hs := one_sub_nu_sq_ne_zero hν (k * s)786  have ht := one_sub_nu_sq_ne_zero hν (k * t)787  have hs' : (1 : Ext F ν) - ofBase (k * s) * w ≠ 0 := fun h => hs (by rw [← norm_one_sub_kw, h]; simp [Ext.norm])788  have ht' : (1 : Ext F ν) - ofBase (k * t) * w ≠ 0 := fun h => ht (by rw [← norm_one_sub_kw, h]; simp [Ext.norm])789  rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff hs' ht'] at hst790  -- (1 + αs)(1 − αt) = (1 + αt)(1 − αs) ⇒ 2α(s − t) = 0791  have him := congrArg im hst792  simp at him793  have : (2 : F) * (k * (s - t)) = 0 := by linear_combination him794  rcases mul_eq_zero.1 this with h | h795  · exact absurd h h2796  · rcases mul_eq_zero.1 h with h | h797    · exact absurd h hk798    · exact sub_eq_zero.1 h799800/-- 8:C5 — the orientation gauge `α ↦ −α` inverts every value: `φ_{−α}(λ) · φ_α(λ) = 1` (Remark801`forward-step`: the forward step imports the derived orientation of the shell). -/802theorem cayley_gauge (hν : ¬ IsSquare ν) (k t : F) :803    (cayley (ν := ν) (-k) t) * cayley k t = 1 := by804  letI := field hν805  unfold cayley806  have h1 := one_sub_nu_sq_ne_zero hν (k * t)807  have hs' : (1 : Ext F ν) - ofBase (k * t) * w ≠ 0 := fun h => h1 (by rw [← norm_one_sub_kw, h]; simp [Ext.norm])808  have ha' : (1 : Ext F ν) + ofBase (k * t) * w ≠ 0 := fun h => h1 (by rw [← norm_one_add_kw, h]; simp [Ext.norm])809  have e1 : (1 : Ext F ν) + ofBase (-k * t) * w = 1 - ofBase (k * t) * w := by ext <;> simp810  have e2 : (1 : Ext F ν) - ofBase (-k * t) * w = 1 + ofBase (k * t) * w := by ext <;> simp811  rw [e1, e2, ← div_eq_mul_inv, ← div_eq_mul_inv, div_mul_div_comm,812    mul_comm ((1 : Ext F ν) - ofBase (k * t) * w) (1 + ofBase (k * t) * w), div_self (mul_ne_zero ha' hs')]813814end Ext815816/-! ## The class is the datum, and the extension erases it (8:B2, B7) -/817section classes818variable {p : ℕ} [hp : Fact (Nat.Prime p)]819820/-- 8:B2 — two nonsquares differ by a square factor: `F^×/(F^×)²` has order two (Lemma `class-datum`); the821Lorentzian form then depends on `ν` only through its class, `−(m²ν) x₀² = −ν (m x₀)²`. -/822theorem class_datum {a b : ZMod p} (ha0 : a ≠ 0) (hb0 : b ≠ 0) (ha : ¬ IsSquare a) (hb : ¬ IsSquare b) :823    IsSquare (a * b) := by824  have h := quadraticChar_one_iff_isSquare (F := ZMod p) (mul_ne_zero ha0 hb0)825  rw [← h, map_mul, (quadraticChar_neg_one_iff_not_isSquare (F := ZMod p)).2 ha,826    (quadraticChar_neg_one_iff_not_isSquare (F := ZMod p)).2 hb]827  norm_num828829/-- 8:B2 — the rescaling `x₀ ↦ m x₀` identifies the forms of `ν` and `m²ν`: a ring identity, the content of830the clause "the form depends on `ν` only through its class". -/831theorem form_class {K : Type*} [CommRing K] (ν m x₀ x₁ x₂ x₃ : K) :832    -(m ^ 2 * ν) * x₀ ^ 2 + x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 = -ν * (m * x₀) ^ 2 + x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 := by ring833834/-- 8:B7 — over the quadratic extension every element of `F_p` is a square: a nonsquare `a = m² ν` becomes835`(m w)²`, so the Euclidean–Lorentzian dichotomy collapses in `K` (Remark `signature-record`). -/836theorem ext_square (hν : ¬ IsSquare (ν : ZMod p)) (a : ZMod p) : IsSquare (Ext.ofBase a : Ext (ZMod p) ν) := by837  by_cases ha : IsSquare a838  · obtain ⟨r, hr⟩ := ha839    exact ⟨Ext.ofBase r, by rw [hr, Ext.ofBase_mul]⟩840  · by_cases ha0 : a = 0841    · exact ⟨0, by rw [ha0, mul_zero]; exact Ext.ofBase_zero⟩842    · have hν0 : ν ≠ 0 := fun h => hν ⟨0, by rw [h]; ring⟩843      obtain ⟨m, hm⟩ := class_datum ha0 hν0 ha hν844      -- a ν = m², so a = (m/ν)² ν = (m/ν · w)²845      refine ⟨Ext.ofBase (m / ν) * Ext.w, ?_⟩846      ext847      · simp; field_simp; linear_combination hm848      · simp849850end classes851852/-! ## The factorisation of the coefficient and the norm growth (8:B4, B6) -/853section factorisation854variable {K : Type*} [Field K]855856/-- 8:B4 — with `c² = 2⁻¹`, the temporal coefficient factors identically, `ν = g = c² · (2g)`, on every857shell (Corollary `two-seats`; the classes of the two factors: `named_residues`, `two_g_class`). -/858theorem nu_factorisation (g : K) (h2 : (2 : K) ≠ 0) : (2 : K)⁻¹ * (2 * g) = g := by859  field_simp860861/-- 8:B6 — norm growth: `N(gz) = g² N(z)` (Theorem `even-transport`; `g²` is even by `parity_iff`). -/862theorem norm_growth {ν : K} (g : K) (z : FRC.Extension.Ext K ν) :863    Ext.norm (Ext.ofBase g * z) = g ^ 2 * Ext.norm z :=864  Ext.norm_ofBase_mul g z865866end factorisation867868section twog869variable {p : ℕ} [hp : Fact (Nat.Prime p)]870871/-- 8:B4 — the cofactor's class: for a primitive root `g` (a nonsquare), `2g` is a square exactly when `2` is872not, i.e. exactly when `κ` is odd on the shell `p = 4κ + 1` (`named_residues`): the product `ν = g` is odd873always, `c² = 2⁻¹` even exactly on the admissibility class. -/874theorem two_g_class {g : ZMod p} (hg0 : g ≠ 0) (hg : ¬ IsSquare g) (h2 : (2 : ZMod p) ≠ 0) :875    IsSquare (2 * g) ↔ ¬ IsSquare (2 : ZMod p) := by876  have h := quadraticChar_one_iff_isSquare (F := ZMod p) (mul_ne_zero h2 hg0)877  rw [← h, map_mul, (quadraticChar_neg_one_iff_not_isSquare (F := ZMod p)).2 hg, mul_neg_one, neg_eq_iff_eq_neg,878    quadraticChar_neg_one_iff_not_isSquare]879880end twog881882/-! ## The latitude identities (8:F2) -/883section latitude884885/-- 8:F2 — on the shell `p = 4κ + 1`: `4κ = −1`, so `κ = −4⁻¹`, the energy radius `1 + κ = 3·4⁻¹`,886`π = 2κ = −2⁻¹`; `g^κ = −i` for `i = g^{−κ} = g^{3κ}` (`−1 = g^{2κ}`); and `κ + 1`, the first rung past the887midpoint of the ladder `1, …, 2κ`, is still a rung. -/888theorem latitude_identities (κ : ℕ) [hp : Fact (Nat.Prime (4 * κ + 1))] {g : ZMod (4 * κ + 1)}889    (hg : orderOf g = 4 * κ) :890    (4 * κ : ZMod (4 * κ + 1)) = -1 ∧ (κ : ZMod (4 * κ + 1)) = -4⁻¹ ∧891    (1 + κ : ZMod (4 * κ + 1)) = 3 * 4⁻¹ ∧ (2 * κ : ZMod (4 * κ + 1)) = -2⁻¹ ∧892    g ^ κ = -g ^ (3 * κ) ∧ κ + 1 ≤ 2 * κ := by893  have h4 : (4 * κ : ZMod (4 * κ + 1)) = -1 := by894    have := ZMod.natCast_self (4 * κ + 1)895    push_cast at this896    exact eq_neg_of_add_eq_zero_left this897  have hκ0 : 0 < κ := by898    rcases Nat.eq_zero_or_pos κ with h0 | h0899    · subst h0; exact absurd hp.out (by decide)900    · exact h0901  have h2z : (2 : ZMod (4 * κ + 1)) ≠ 0 := by902    intro h903    have := (ZMod.natCast_eq_zero_iff 2 (4 * κ + 1)).1 (by exact_mod_cast h)904    have := Nat.le_of_dvd (by norm_num) this905    omega906  have h4z : (4 : ZMod (4 * κ + 1)) ≠ 0 := four_ne_zero_of_two h2z907  have hκ : (κ : ZMod (4 * κ + 1)) = -4⁻¹ := neg_inv_of_mul h4z h4908  refine ⟨h4, hκ, three_quarters h4z hκ, half_neg h2z h4, ?_, by omega⟩909  have hh : g ^ (2 * κ) = -1 := by910    have h1 := pow_orderOf_eq_one g911    rw [hg] at h1912    have h2' : (g ^ (2 * κ)) ^ 2 = 1 := by rw [← pow_mul, show 2 * κ * 2 = 4 * κ by ring]; exact h1913    rcases sq_eq_one_cases h2' with h | h914    · exfalso915      have := orderOf_dvd_iff_pow_eq_one.2 h916      rw [hg] at this917      have := Nat.le_of_dvd (by omega) this918      omega919    · exact h920  rw [three_kappa_pow g κ hh]921  exact (neg_neg _).symm922923end latitude924925926/-! ## The gamma matrices in blocks, and the Clifford relations (8:D2) -/927section clifford928variable {K : Type*} [CommRing K]929open Matrix930931/-- The Pauli matrices over `K`, with the shell's quarter-turn `i` (`i² = −1`) in `σ²`. -/932def σ1 : Matrix (Fin 2) (Fin 2) K := !![0, 1; 1, 0]933def σ2 (i : K) : Matrix (Fin 2) (Fin 2) K := !![0, -i; i, 0]934def σ3 : Matrix (Fin 2) (Fin 2) K := !![1, 0; 0, -1]935/-- `J = σ¹σ³ = (0 −1; 1 0)`, the block of the spinor twist. -/936def J : Matrix (Fin 2) (Fin 2) K := !![0, -1; 1, 0]937938/-- `β = (0 I; I 0)` and `ρ(σ) = (0 σ; −σ 0)` on `K² ⊕ K²`. -/939def β : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := fromBlocks 0 1 1 0940def ρ (s : Matrix (Fin 2) (Fin 2) K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := fromBlocks 0 s (-s) 0941942/-- The gamma matrices of `(eq:gamma-definition)`: `γ⁰ = i w β`, `γ^k = i ρ(σ^k)`. -/943def γ0 (i w : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := (i * w) • β944def γ1 (i : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := i • ρ σ1945def γ2 (i : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := i • ρ (σ2 i)946def γ3 (i : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := i • ρ σ3947948/-- 8:D2 — the Pauli identities `σ^j σ^k + σ^k σ^j = 2 δ_{jk} I₂` over `K`, from `i² = −1`. -/949theorem pauli {i : K} (hi : i * i = -1) :950    σ1 * σ1 = (1 : Matrix (Fin 2) (Fin 2) K) ∧ σ2 i * σ2 i = 1 ∧ σ3 * σ3 = (1 : Matrix (Fin 2) (Fin 2) K) ∧951    σ1 * σ2 i + σ2 i * σ1 = 0 ∧ σ1 * σ3 + σ3 * σ1 = (0 : Matrix (Fin 2) (Fin 2) K) ∧ σ2 i * σ3 + σ3 * σ2 i = 0 := by952  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;>953  · ext a b954    fin_cases a <;> fin_cases b <;>955    simp [σ1, σ2, σ3, Matrix.mul_apply, Fin.sum_univ_two, Matrix.one_apply] <;>956    linear_combination (-1 : K) * hi957958theorem β_sq : (β : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) * β = 1 := by959  simp [β, fromBlocks_multiply, fromBlocks_one]960961theorem ρ_mul (s t : Matrix (Fin 2) (Fin 2) K) : ρ s * ρ t = fromBlocks (-(s * t)) 0 0 (-(s * t)) := by962  simp [ρ, fromBlocks_multiply]963964theorem β_ρ_anticomm (s : Matrix (Fin 2) (Fin 2) K) : β * ρ s + ρ s * β = 0 := by965  simp [β, ρ, fromBlocks_multiply, fromBlocks_add]966967/-- 8:D2 — the Clifford relations `γ^μ γ^ν + γ^ν γ^μ = 2 η_{μν} I₄`, `η = diag(−ν, 1, 1, 1)`, from `i² = −1` and968`w² = ν` alone (Proposition `clifford`), by the block computation of its proof: `β² = I`, `(ρ^k)² = −I`,969`ρ^jρ^k + ρ^kρ^j = 0`, `βρ^k + ρ^kβ = 0`. -/970theorem clifford {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :971    γ0 i w * γ0 i w = (-ν) • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) ∧972    γ1 i * γ1 i = 1 ∧ γ2 i * γ2 i = 1 ∧ γ3 i * γ3 i = 1 ∧973    γ0 i w * γ1 i + γ1 i * γ0 i w = 0 ∧ γ0 i w * γ2 i + γ2 i * γ0 i w = 0 ∧974    γ0 i w * γ3 i + γ3 i * γ0 i w = 0 ∧ γ1 i * γ2 i + γ2 i * γ1 i = 0 ∧975    γ1 i * γ3 i + γ3 i * γ1 i = 0 ∧ γ2 i * γ3 i + γ3 i * γ2 i = 0 := by976  obtain ⟨h11, h22, h33, h12, h13, h23⟩ := pauli hi977  have hsq : ∀ s : Matrix (Fin 2) (Fin 2) K, s * s = 1 → (i • ρ s) * (i • ρ s) = 1 := fun s hs => by978    rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, ρ_mul, hs, hi]979    simp [fromBlocks_one, fromBlocks_neg]980  have hanti : ∀ s t : Matrix (Fin 2) (Fin 2) K, s * t + t * s = 0 →981      (i • ρ s) * (i • ρ t) + (i • ρ t) * (i • ρ s) = 0 := fun s t hst => by982    rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, Matrix.smul_mul, Matrix.mul_smul, smul_smul, ← smul_add,983      ρ_mul, ρ_mul, fromBlocks_add]984    have : -(s * t) + -(t * s) = 0 := by rw [← neg_add, hst, neg_zero]985    simp [this]986  have h0k : ∀ s : Matrix (Fin 2) (Fin 2) K, γ0 i w * (i • ρ s) + (i • ρ s) * γ0 i w = 0 := fun s => by987    unfold γ0988    rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, Matrix.smul_mul, Matrix.mul_smul, smul_smul,989      mul_comm i (i * w), ← smul_add, β_ρ_anticomm, smul_zero]990  refine ⟨?_, hsq _ h11, hsq _ h22, hsq _ h33, h0k _, h0k _, h0k _, hanti _ _ h12, hanti _ _ h13, hanti _ _ h23⟩991  unfold γ0992  rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, β_sq]993  congr 1994  linear_combination (w * w) * hi - hw995996/-- `M = γ⁰γ¹` and the spinor twist `X = γ⁰γ¹γ³`. -/997def Mγ (i w : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := γ0 i w * γ1 i998def Xγ (i w : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := γ0 i w * γ1 i * γ3 i9991000/-- Push a block identity down to its four `2 × 2` blocks and close each entrywise, reducing the powers of1001`i` and `w`. -/1002macro "block_entries" hs:term : tactic =>1003  `(tactic| (rw [fromBlocks_inj]; refine ⟨?_, ?_, ?_, ?_⟩ <;>1004      (ext a b; fin_cases a <;> fin_cases b <;>1005        (try simp [σ1, σ2, σ3, J, Matrix.mul_apply, Fin.sum_univ_two, Matrix.one_apply, Matrix.conjTranspose_apply,1006          $hs:term]) <;>1007        (try ring_nf) <;> (try simp only [$hs:term]) <;> (try ring_nf))))10081009theorem powers {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1010    i ^ 2 = -1 ∧ i ^ 3 = -i ∧ i ^ 4 = 1 ∧ i ^ 5 = i ∧ i ^ 6 = -1 ∧ i ^ 7 = -i ∧ i ^ 8 = 1 ∧1011    w ^ 2 = ν ∧ w ^ 3 = ν * w ∧ w ^ 4 = ν ^ 2 ∧ w ^ 5 = ν ^ 2 * w := by1012  have hi2 : i ^ 2 = -1 := by rw [sq]; exact hi1013  have hw2 : w ^ 2 = ν := by rw [sq]; exact hw1014  refine ⟨hi2, ?_, ?_, ?_, ?_, ?_, ?_, hw2, ?_, ?_, ?_⟩1015  · rw [pow_succ, hi2]; ring1016  · rw [show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hi2]; ring1017  · rw [pow_succ, show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hi2]; ring1018  · rw [show (6 : ℕ) = 2 * 3 by rfl, pow_mul, hi2]; ring1019  · rw [pow_succ, show (6 : ℕ) = 2 * 3 by rfl, pow_mul, hi2]; ring1020  · rw [show (8 : ℕ) = 2 * 4 by rfl, pow_mul, hi2]; ring1021  · rw [pow_succ, hw2]1022  · rw [show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hw2]1023  · rw [pow_succ, show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hw2]10241025/-- `M = γ⁰γ¹ = diag(w σ¹, −w σ¹)` in blocks. -/1026theorem Mγ_eq {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1027    Mγ i w = fromBlocks (w • σ1) 0 0 (-(w • σ1)) := by1028  have hs := powers hi hw1029  simp only [Mγ, γ0, γ1, β, ρ, Matrix.smul_mul, Matrix.mul_smul, smul_smul, fromBlocks_multiply, fromBlocks_smul]1030  block_entries hs10311032/-- `X = γ⁰γ¹γ³ = (0, i w J; i w J, 0)` in blocks, `J = σ¹σ³`. -/1033theorem Xγ_eq {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1034    Xγ i w = fromBlocks 0 ((i * w) • J) ((i * w) • J) 0 := by1035  have hs := powers hi hw1036  have : Xγ i w = Mγ i w * γ3 i := rfl1037  rw [this, Mγ_eq hi hw]1038  simp only [γ3, ρ, Matrix.smul_mul, Matrix.mul_smul, smul_smul, fromBlocks_multiply, fromBlocks_smul]1039  block_entries hs10401041/-- 8:D6, 8:D7 (the transported gammas) — spin conjugation up to the scalar `δ`: `M² = ν`,1042`(x − yM) γ⁰ (x + yM) = (x² + νy²) γ⁰ − 2xyν γ¹`, `(x − yM) γ¹ (x + yM) = −2xy γ⁰ + (x² + νy²) γ¹`, and `M`1043commutes with `γ²` and `γ³` (Proposition `spin-conjugation`; the division by `δ = x² − νy²` onto1044`A = (x² + νy²)/δ`, `B = −2xy/δ` is `spin_conjugation_AB`); `y ↦ −y` gives the transported gammas1045`γ̂⁰ = Aγ⁰ − νBγ¹`, `γ̂¹ = −Bγ⁰ + Aγ¹` (Proposition `transported-dirac-form`, the pullback identity and the1046transported factorization not formalised). -/1047theorem spin_conjugation {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (x y : K) :1048    Mγ i w * Mγ i w = ν • 1 ∧1049    (x • 1 + (-y) • Mγ i w) * γ0 i w * (x • 1 + y • Mγ i w) = (x ^ 2 + ν * y ^ 2) • γ0 i w + (-(2 * x * y * ν)) • γ1 i ∧1050    (x • 1 + (-y) • Mγ i w) * γ1 i * (x • 1 + y • Mγ i w) = (-(2 * x * y)) • γ0 i w + (x ^ 2 + ν * y ^ 2) • γ1 i ∧1051    Mγ i w * γ2 i = γ2 i * Mγ i w ∧ Mγ i w * γ3 i = γ3 i * Mγ i w := by1052  have hs := powers hi hw1053  rw [Mγ_eq hi hw]1054  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>1055  · simp only [γ0, γ1, γ2, γ3, β, ρ, ← fromBlocks_one, Matrix.smul_mul, Matrix.mul_smul, smul_smul,1056      fromBlocks_multiply, fromBlocks_smul, fromBlocks_add, fromBlocks_neg]1057    block_entries hs10581059/-- 8:D9 — the spinor twist: `X² = ν`, `X` commutes with `γ⁰, γ¹, γ³` and anticommutes with `γ²` (Lemma1060`spinor-form`, the algebraic part). -/1061theorem spinor_twist {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1062    Xγ i w * Xγ i w = ν • 1 ∧ Xγ i w * γ0 i w = γ0 i w * Xγ i w ∧ Xγ i w * γ1 i = γ1 i * Xγ i w ∧1063    Xγ i w * γ3 i = γ3 i * Xγ i w ∧ Xγ i w * γ2 i = -(γ2 i * Xγ i w) := by1064  have hs := powers hi hw1065  rw [Xγ_eq hi hw]1066  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>1067  · simp only [γ0, γ1, γ2, γ3, β, ρ, ← fromBlocks_one, Matrix.smul_mul, Matrix.mul_smul, smul_smul,1068      fromBlocks_multiply, fromBlocks_smul, fromBlocks_add, fromBlocks_neg]1069    block_entries hs10701071end clifford107210731074section spinorform1075variable {K : Type*} [CommRing K] [StarRing K]1076open Matrix10771078theorem σ1_dagger : (σ1 : Matrix (Fin 2) (Fin 2) K)ᴴ = σ1 := by1079  ext a b; fin_cases a <;> fin_cases b <;> simp [σ1, Matrix.conjTranspose_apply]1080theorem σ3_dagger : (σ3 : Matrix (Fin 2) (Fin 2) K)ᴴ = σ3 := by1081  ext a b; fin_cases a <;> fin_cases b <;> simp [σ3, Matrix.conjTranspose_apply]1082theorem J_dagger : (J : Matrix (Fin 2) (Fin 2) K)ᴴ = -J := by1083  ext a b; fin_cases a <;> fin_cases b <;> simp [J, Matrix.conjTranspose_apply]1084theorem σ2_dagger {i : K} (hsi : star i = i) : (σ2 i)ᴴ = -σ2 i := by1085  ext a b; fin_cases a <;> fin_cases b <;> simp [σ2, Matrix.conjTranspose_apply, hsi]10861087/-- 8:D9 — under the conjugate transpose (Frobenius fixing `i`, negating `w`): `(γ⁰)† = −γ⁰`, `(γ¹)† = −γ¹`,1088`(γ²)† = +γ²` (the obstruction: `σ²` is antisymmetric with `i` Frobenius-fixed), `(γ³)† = −γ³`, and1089`X† = X` for the twist `X = γ⁰γ¹γ³` (Lemma `spinor-form`). -/1090theorem gamma_dagger {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (hsi : star i = i) (hsw : star w = -w) :1091    (γ0 i w)ᴴ = -γ0 i w ∧ (γ1 i)ᴴ = -γ1 i ∧ (γ2 i)ᴴ = γ2 i ∧ (γ3 i)ᴴ = -γ3 i ∧ (Xγ i w)ᴴ = Xγ i w := by1092  refine ⟨?_, ?_, ?_, ?_, ?_⟩1093  · simp only [γ0, β, Matrix.conjTranspose_smul, star_mul', hsi, hsw, fromBlocks_conjTranspose,1094      Matrix.conjTranspose_zero, Matrix.conjTranspose_one, ← neg_smul]1095    congr 1; ring1096  · simp only [γ1, ρ, Matrix.conjTranspose_smul, hsi, fromBlocks_conjTranspose, Matrix.conjTranspose_zero,1097      Matrix.conjTranspose_neg, σ1_dagger, ← smul_neg, fromBlocks_neg, neg_neg, neg_zero]1098  · simp only [γ2, ρ, Matrix.conjTranspose_smul, hsi, fromBlocks_conjTranspose, Matrix.conjTranspose_zero,1099      Matrix.conjTranspose_neg, σ2_dagger hsi, neg_neg]1100  · simp only [γ3, ρ, Matrix.conjTranspose_smul, hsi, fromBlocks_conjTranspose, Matrix.conjTranspose_zero,1101      Matrix.conjTranspose_neg, σ3_dagger, ← smul_neg, fromBlocks_neg, neg_neg, neg_zero]1102  · rw [Xγ_eq hi hw]1103    simp only [fromBlocks_conjTranspose, Matrix.conjTranspose_zero, Matrix.conjTranspose_smul, star_mul', hsi, hsw,1104      J_dagger, smul_neg, neg_smul, neg_neg, mul_neg]11051106/-- 8:D9 — the twist conjugates every gamma to its negative, `(γ^μ)† X = −X γ^μ` (so `X⁻¹(γ^μ)†X = −γ^μ`),1107while the `γ⁰`-twist leaves mixed signs: `(γ⁰)† γ⁰ = −γ⁰γ⁰` but `(γ¹)† γ⁰ = +γ⁰γ¹` (Lemma `spinor-form`). -/1108theorem twist_adjoint {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (hsi : star i = i) (hsw : star w = -w) :1109    (γ0 i w)ᴴ * Xγ i w = -(Xγ i w * γ0 i w) ∧ (γ1 i)ᴴ * Xγ i w = -(Xγ i w * γ1 i) ∧1110    (γ2 i)ᴴ * Xγ i w = -(Xγ i w * γ2 i) ∧ (γ3 i)ᴴ * Xγ i w = -(Xγ i w * γ3 i) ∧1111    (γ0 i w)ᴴ * γ0 i w = -(γ0 i w * γ0 i w) ∧ (γ1 i)ᴴ * γ0 i w = γ0 i w * γ1 i := by1112  obtain ⟨d0, d1, d2, d3, _⟩ := gamma_dagger hi hw hsi hsw1113  obtain ⟨_, c0, c1, c3, a2⟩ := spinor_twist hi hw1114  have hs := powers hi hw1115  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩1116  · rw [d0, neg_mul, c0]1117  · rw [d1, neg_mul, c1]1118  · rw [d2, a2, neg_neg]1119  · rw [d3, neg_mul, c3]1120  · rw [d0, neg_mul]1121  · rw [d1, neg_mul, neg_eq_iff_eq_neg]1122    simp only [γ0, γ1, β, ρ, Matrix.smul_mul, Matrix.mul_smul, smul_smul, fromBlocks_multiply, fromBlocks_smul,1123      fromBlocks_neg]1124    block_entries hs11251126/-- `M† = −M`. -/1127theorem Mγ_dagger {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (hsw : star w = -w) :1128    (Mγ i w)ᴴ = -(Mγ i w) := by1129  rw [Mγ_eq hi hw]1130  simp only [fromBlocks_conjTranspose, Matrix.conjTranspose_smul, Matrix.conjTranspose_neg,1131    Matrix.conjTranspose_zero, fromBlocks_neg, hsw, σ1_dagger, neg_smul, neg_neg, neg_zero]11321133/-- 8:D11 — the lift's adjoint: `S† = S(x, −y)` for Frobenius-fixed `x, y` (so, `X` commuting with `M`,1134`S^# = X⁻¹S†X = S(x, −y)`), and `S(x, −y) S(x, y) = (x² − νy²) I = δ I` (Proposition `two-diracs`). -/1135theorem lift_adjoint {i w ν x y : K} (hi : i * i = -1) (hw : w * w = ν) (hsw : star w = -w)1136    (hx : star x = x) (hy : star y = y) :1137    (x • 1 + y • Mγ i w)ᴴ = x • 1 + (-y) • Mγ i w ∧1138    (x • 1 + (-y) • Mγ i w) * (x • 1 + y • Mγ i w) = (x ^ 2 - ν * y ^ 2) • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) := by1139  obtain ⟨hM2, _, _, _, _⟩ := spin_conjugation hi hw x y1140  refine ⟨?_, ?_⟩1141  · rw [Matrix.conjTranspose_add, Matrix.conjTranspose_smul, Matrix.conjTranspose_smul, Matrix.conjTranspose_one,1142      Mγ_dagger hi hw hsw, hx, hy, smul_neg, neg_smul]1143  · simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, neg_mul, mul_neg, smul_smul,1144      smul_neg, smul_add, neg_smul, hM2]1145    module11461147/-- 8:D11 — the transport of the spinor form: for a lift `S = x + yM` with Frobenius-fixed `x, y`,1148`S† X S = (x² − νy²) X = δ X` — norm-one lifts preserve the form exactly, and the odd coset scales it by1149the lift norm `δ` (Proposition `two-diracs`). -/1150theorem lift_transport {i w ν x y : K} (hi : i * i = -1) (hw : w * w = ν) (hsi : star i = i) (hsw : star w = -w)1151    (hx : star x = x) (hy : star y = y) :1152    (x • 1 + y • Mγ i w)ᴴ * Xγ i w * (x • 1 + y • Mγ i w) = (x ^ 2 - ν * y ^ 2) • Xγ i w := by1153  obtain ⟨hM2, _, _, _, _⟩ := spin_conjugation hi hw x y1154  obtain ⟨_, c0, c1, _, _⟩ := spinor_twist hi hw1155  have hXM : Xγ i w * Mγ i w = Mγ i w * Xγ i w := by1156    show Xγ i w * (γ0 i w * γ1 i) = γ0 i w * γ1 i * Xγ i w1157    rw [← mul_assoc, c0, mul_assoc, c1, ← mul_assoc]1158  rw [Matrix.conjTranspose_add, Matrix.conjTranspose_smul, Matrix.conjTranspose_smul, Matrix.conjTranspose_one,1159    Mγ_dagger hi hw hsw, hx, hy]1160  have e1 : (x • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) + y • -Mγ i w) * Xγ i w =1161      Xγ i w * (x • 1 + y • -Mγ i w) := by1162    simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, neg_mul, mul_neg, hXM]1163  rw [e1, mul_assoc]1164  have e2 : (x • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) + y • -Mγ i w) * (x • 1 + y • Mγ i w) =1165      (x ^ 2 - ν * y ^ 2) • 1 := by1166    simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, neg_mul, mul_neg, smul_smul,1167      smul_neg, smul_add, hM2]1168    module1169  rw [e2, mul_smul_comm, mul_one]11701171end spinorform11721173/-! ## The coordinate boost (8:D5) -/1174section boostmatrix1175variable {F : Type*} [Field F]11761177/-- The boost entries `A = (x² + νy²)/δ`, `B = −2xy/δ`, `δ = x² − νy²`. -/1178noncomputable def Aent (ν x y : F) : F := (x ^ 2 + ν * y ^ 2) / (x ^ 2 - ν * y ^ 2)1179noncomputable def Bent (ν x y : F) : F := -(2 * x * y) / (x ^ 2 - ν * y ^ 2)11801181/-- 8:D5, 8:D7 — `Λ(x, y) ∈ O(Q_ν)`: `A² − νB² = 1` (Proposition `boost-orthogonal`); and the group law1182`Λ(x, y)Λ(u, v) = Λ(xu + νyv, xv + yu)` on the entries, with `Λ(1, 0) = I` and `Λ(x, −y) = Λ(x, y)⁻¹`1183(Proposition `boost-subgroup`). -/1184theorem boost_entries (ν x y u v : F) (hd : x ^ 2 - ν * y ^ 2 ≠ 0) (hd' : u ^ 2 - ν * v ^ 2 ≠ 0) :1185    Aent ν x y ^ 2 - ν * Bent ν x y ^ 2 = 1 ∧1186    Aent ν x y * Aent ν u v + ν * (Bent ν x y * Bent ν u v) = Aent ν (x * u + ν * y * v) (x * v + y * u) ∧1187    Aent ν x y * Bent ν u v + Bent ν x y * Aent ν u v = Bent ν (x * u + ν * y * v) (x * v + y * u) ∧1188    Aent ν 1 0 = 1 ∧ Bent ν 1 0 = 0 ∧ Aent ν x (-y) = Aent ν x y ∧ Bent ν x (-y) = -Bent ν x y := by1189  have hdd : (x * u + ν * y * v) ^ 2 - ν * (x * v + y * u) ^ 2 = (x ^ 2 - ν * y ^ 2) * (u ^ 2 - ν * v ^ 2) := by1190    ring1191  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> simp only [Aent, Bent]1192  · field_simp; ring1193  · rw [hdd]; field_simp; ring1194  · rw [hdd]; field_simp; ring1195  · norm_num1196  · norm_num1197  · ring1198  · ring11991200/-- 8:D6 — the spin conjugation with the inverse: for `δ = x² − νy² ≠ 0`, `S⁻¹ = δ⁻¹(x − yM)` and1201`S⁻¹γ⁰S = Aγ⁰ + νBγ¹`, `S⁻¹γ¹S = Bγ⁰ + Aγ¹` with `A = (x² + νy²)/δ`, `B = −2xy/δ` (Proposition1202`spin-conjugation`). -/1203theorem spin_conjugation_AB {i w ν x y : F} (hi : i * i = -1) (hw : w * w = ν) (hd : x ^ 2 - ν * y ^ 2 ≠ 0) :1204    ((x ^ 2 - ν * y ^ 2)⁻¹ • (x • 1 + (-y) • Mγ i w)) * γ0 i w * (x • 1 + y • Mγ i w) =1205      Aent ν x y • γ0 i w + (ν * Bent ν x y) • γ1 i ∧1206    ((x ^ 2 - ν * y ^ 2)⁻¹ • (x • 1 + (-y) • Mγ i w)) * γ1 i * (x • 1 + y • Mγ i w) =1207      Bent ν x y • γ0 i w + Aent ν x y • γ1 i := by1208  obtain ⟨_, h0, h1, _, _⟩ := spin_conjugation hi hw x y1209  refine ⟨?_, ?_⟩1210  · rw [Matrix.smul_mul, Matrix.smul_mul, h0, smul_add, smul_smul, smul_smul]1211    simp only [Aent, Bent]1212    congr 2 <;> field_simp1213  · rw [Matrix.smul_mul, Matrix.smul_mul, h1, smul_add, smul_smul, smul_smul]1214    simp only [Aent, Bent]1215    congr 2 <;> field_simp12161217end boostmatrix12181219/-! ## The worked shells (8:D12, B4, B3) -/1220section shells12211222instance : Fact (Nat.Prime 13) := ⟨by norm_num⟩1223instance : Fact (Nat.Prime 17) := ⟨by norm_num⟩12241225/-- 8:D12, 8:B4, 8:B3 [value] — `𝔽₁₃` with `ν = g = 2`, `x = y = 1`: `A = 10`, `B = 2`, `A² − νB² = 1`;1226`2⁻¹ = 7` is a nonsquare and `e = 2^5 = 6` a nonsquare; `2` is primitive (`orderOf 2 = 12`). -/1227theorem shell13 :1228    Aent (2 : ZMod 13) 1 1 = 10 ∧ Bent (2 : ZMod 13) 1 1 = 2 ∧ (10 : ZMod 13) ^ 2 - 2 * 2 ^ 2 = 1 ∧1229    (2 : ZMod 13) * 7 = 1 ∧ ¬ IsSquare (7 : ZMod 13) ∧ (2 : ZMod 13) ^ 5 = 6 ∧ ¬ IsSquare (6 : ZMod 13) ∧1230    orderOf (2 : ZMod 13) = 12 := by1231  refine ⟨?_, ?_, by decide, by decide, by decide, by decide, by decide, ?_⟩1232  · simp only [Aent]; rw [div_eq_iff (by decide)]; decide1233  · simp only [Bent]; rw [div_eq_iff (by decide)]; decide1234  · rw [orderOf_eq_iff (by norm_num)]1235    exact ⟨by decide, fun m hm hm0 => by interval_cases m <;> decide⟩12361237/-- 8:D12, 8:B3 [value] — `𝔽₁₇` (`κ = 4`) with `ν = g = 3`, `i = 4`: `A = 15`, `B = 1`, `A² − νB² = 1`;1238`2 = 6²`, `i = 2²`, `e = 3⁴ = 13 = 8²` are squares (so the class of `e` is not stable across shells), `3` a1239nonsquare, `3` primitive; `17 ≡ 5 (mod 12)`, and no capacity below `4` is even and `≡ 1 (mod 3)`: the1240minimal admissible shell. -/1241theorem shell17 :1242    Aent (3 : ZMod 17) 1 1 = 15 ∧ Bent (3 : ZMod 17) 1 1 = 1 ∧ (15 : ZMod 17) ^ 2 - 3 * 1 ^ 2 = 1 ∧1243    (3 : ZMod 17) ^ 4 = 13 ∧ (4 : ZMod 17) ^ 2 = -1 ∧ IsSquare (2 : ZMod 17) ∧ IsSquare (4 : ZMod 17) ∧1244    IsSquare (13 : ZMod 17) ∧ ¬ IsSquare (3 : ZMod 17) ∧ orderOf (3 : ZMod 17) = 16 ∧ 17 % 12 = 5 ∧1245    (Even 4 ∧ 4 % 3 = 1 ∧ Nat.Prime 17) ∧1246    ∀ κ < 4, ¬ (Even κ ∧ κ % 3 = 1 ∧ Nat.Prime (4 * κ + 1)) := by1247  refine ⟨?_, ?_, by decide, by decide, by decide, by decide, by decide, by decide, by decide, ?_, by decide,1248    ⟨by decide, by decide, by norm_num⟩, ?_⟩1249  · simp only [Aent]; rw [div_eq_iff (by decide)]; decide1250  · simp only [Bent]; rw [div_eq_iff (by decide)]; decide1251  · rw [orderOf_eq_iff (by norm_num)]1252    exact ⟨by decide, fun m hm hm0 => by interval_cases m <;> decide⟩1253  · intro κ hκ1254    interval_cases κ <;> simp [Nat.even_iff]12551256/-- 8:B4, 8:A5 [value] — the laboratory Carrier `Ω = 2 408 561`: `c = 171 106` is base-rational with `c² = 2⁻¹`1257(`171106² · 2 ≡ 1`), `2⁻¹ = 1 204 281`, and the two seats compose: `2⁻¹ · 12 ≡ 6 = g`. -/1258theorem carrier_constants :1259    (171106 * 171106 * 2) % 2408561 = 1 ∧ (2 * 1204281) % 2408561 = 1 ∧ (1204281 * 12) % 2408561 = 6 ∧1260    Nat.Prime 2408561 := by1261  refine ⟨by norm_num, by norm_num, by norm_num, by norm_num⟩12621263end shells12641265end12661267/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/12681269section parity_aliases1270variable {p : ℕ} [hp : Fact (Nat.Prime p)]12711272/-- 8:B5 — the square class is chronon parity: for a primitive root `g` (`orderOf g = p − 1`), `g^k` is a1273square exactly when `k` is even (Theorem `parity`). -/1274theorem parity_iff {g : ZMod p} (hg : orderOf g = p - 1) (hodd : p % 2 = 1) (k : ℕ) :1275    IsSquare (g ^ k) ↔ Even k :=1276  FRC.Frame.parity_iff hg hodd k12771278/-- 8:B3 — the drive is a nonsquare (`g^{(p−1)/2} = −1`), and so is its inverse `g^{p−2}`: `[g⁻¹] = [g]`. -/1279theorem drive_nonsquare {g : ZMod p} (hg : orderOf g = p - 1) (hodd : p % 2 = 1) :1280    ¬ IsSquare g ∧ ¬ IsSquare g⁻¹ :=1281  FRC.Frame.drive_nonsquare hg hodd12821283end parity_aliases12841285@[reducible] def Ext := @FRC.Extension.Ext12861287namespace Ext1288variable {F : Type*} [CommRing F] {ν : F}12891290theorem zero_re : (0 : Ext F ν).re = 0 :=1291  FRC.Extension.Ext.zero_re12921293theorem zero_im : (0 : Ext F ν).im = 0 :=1294  FRC.Extension.Ext.zero_im12951296theorem one_re : (1 : Ext F ν).re = 1 :=1297  FRC.Extension.Ext.one_re12981299theorem one_im : (1 : Ext F ν).im = 0 :=1300  FRC.Extension.Ext.one_im13011302theorem add_re (z z' : Ext F ν) : (z + z').re = z.re + z'.re :=1303  FRC.Extension.Ext.add_re z z'13041305theorem add_im (z z' : Ext F ν) : (z + z').im = z.im + z'.im :=1306  FRC.Extension.Ext.add_im z z'13071308theorem neg_re (z : Ext F ν) : (-z).re = -z.re :=1309  FRC.Extension.Ext.neg_re z13101311theorem neg_im (z : Ext F ν) : (-z).im = -z.im :=1312  FRC.Extension.Ext.neg_im z13131314theorem sub_re (z z' : Ext F ν) : (z - z').re = z.re - z'.re :=1315  FRC.Extension.Ext.sub_re z z'13161317theorem sub_im (z z' : Ext F ν) : (z - z').im = z.im - z'.im :=1318  FRC.Extension.Ext.sub_im z z'13191320theorem mul_re (z z' : Ext F ν) : (z * z').re = z.re * z'.re + ν * (z.im * z'.im) :=1321  FRC.Extension.Ext.mul_re z z'13221323theorem mul_im (z z' : Ext F ν) : (z * z').im = z.re * z'.im + z.im * z'.re :=1324  FRC.Extension.Ext.mul_im z z'13251326theorem nsmul_re (n : ℕ) (z : Ext F ν) : (n • z).re = n • z.re :=1327  FRC.Extension.Ext.nsmul_re n z13281329theorem nsmul_im (n : ℕ) (z : Ext F ν) : (n • z).im = n • z.im :=1330  FRC.Extension.Ext.nsmul_im n z13311332theorem zsmul_re (n : ℤ) (z : Ext F ν) : (n • z).re = n • z.re :=1333  FRC.Extension.Ext.zsmul_re n z13341335theorem zsmul_im (n : ℤ) (z : Ext F ν) : (n • z).im = n • z.im :=1336  FRC.Extension.Ext.zsmul_im n z13371338@[reducible] def ofBase (a : F) : Ext F ν :=1339  FRC.Extension.Ext.ofBase a13401341@[reducible] def w : Ext F ν :=1342  FRC.Extension.Ext.w13431344@[reducible] def conj (z : Ext F ν) : Ext F ν :=1345  FRC.Extension.Ext.conj z13461347@[reducible] def norm (z : Ext F ν) : F :=1348  FRC.Extension.Ext.norm z13491350theorem ofBase_re (a : F) : (ofBase a : Ext F ν).re = a :=1351  FRC.Extension.Ext.ofBase_re a13521353theorem ofBase_im (a : F) : (ofBase a : Ext F ν).im = 0 :=1354  FRC.Extension.Ext.ofBase_im a13551356theorem w_re : (w : Ext F ν).re = 0 :=1357  FRC.Extension.Ext.w_re13581359theorem w_im : (w : Ext F ν).im = 1 :=1360  FRC.Extension.Ext.w_im13611362theorem conj_re (z : Ext F ν) : (conj z).re = z.re :=1363  FRC.Extension.Ext.conj_re z13641365theorem conj_im (z : Ext F ν) : (conj z).im = -z.im :=1366  FRC.Extension.Ext.conj_im z13671368theorem w_sq : (w : Ext F ν) ^ 2 = ofBase ν :=1369  FRC.Extension.Ext.w_sq13701371theorem conj_mul (z z' : Ext F ν) : conj (z * z') = conj z * conj z' :=1372  FRC.Extension.Ext.conj_mul z z'13731374theorem conj_add (z z' : Ext F ν) : conj (z + z') = conj z + conj z' :=1375  FRC.Extension.Ext.conj_add z z'13761377theorem conj_conj (z : Ext F ν) : conj (conj z) = z :=1378  FRC.Extension.Ext.conj_conj z13791380theorem conj_one : conj (1 : Ext F ν) = 1 :=1381  FRC.Extension.Ext.conj_one13821383theorem mul_conj (z : Ext F ν) : z * conj z = ofBase (norm z) :=1384  FRC.Extension.Ext.mul_conj z13851386/-- 8:A2 — the norm is multiplicative: `N(zz') = N(z)N(z')`. -/1387theorem norm_mul (z z' : Ext F ν) : norm (z * z') = norm z * norm z' :=1388  FRC.Extension.Ext.norm_mul z z'13891390theorem ofBase_mul (a b : F) : (ofBase (a * b) : Ext F ν) = ofBase a * ofBase b :=1391  FRC.Extension.Ext.ofBase_mul a b13921393theorem ofBase_add (a b : F) : (ofBase (a + b) : Ext F ν) = ofBase a + ofBase b :=1394  FRC.Extension.Ext.ofBase_add a b13951396theorem ofBase_one : (ofBase 1 : Ext F ν) = 1 :=1397  FRC.Extension.Ext.ofBase_one13981399theorem ofBase_zero : (ofBase 0 : Ext F ν) = 0 :=1400  FRC.Extension.Ext.ofBase_zero14011402theorem ofBase_injective : Function.Injective (ofBase : F → Ext F ν) :=1403  FRC.Extension.Ext.ofBase_injective14041405theorem conj_ofBase (a : F) : conj (ofBase a : Ext F ν) = ofBase a :=1406  FRC.Extension.Ext.conj_ofBase a14071408theorem conj_w : conj (w : Ext F ν) = -w :=1409  FRC.Extension.Ext.conj_w14101411theorem conj_eq_self_iff (z : Ext F ν) (h2 : (2 : F) ≠ 0) [NoZeroDivisors F] :1412    conj z = z ↔ z.im = 0 :=1413  FRC.Extension.Ext.conj_eq_self_iff z h214141415theorem conj_eq_neg_iff (z : Ext F ν) (h2 : (2 : F) ≠ 0) [NoZeroDivisors F] :1416    conj z = -z ↔ z.re = 0 :=1417  FRC.Extension.Ext.conj_eq_neg_iff z h214181419theorem star_def (z : Ext F ν) : star z = conj z :=1420  FRC.Extension.Ext.star_def z14211422/-- `w` generates: `z = re + im · w`. -/1423theorem eq_re_add_im_w (z : Ext F ν) : z = ofBase z.re + ofBase z.im * w :=1424  FRC.Extension.Ext.eq_re_add_im_w z14251426@[reducible] def instZero : Zero (Ext F ν) :=1427  FRC.Extension.Ext.instZero14281429@[reducible] def instOne : One (Ext F ν) :=1430  FRC.Extension.Ext.instOne14311432@[reducible] def instAdd : Add (Ext F ν) :=1433  FRC.Extension.Ext.instAdd14341435@[reducible] def instNeg : Neg (Ext F ν) :=1436  FRC.Extension.Ext.instNeg14371438@[reducible] def instSub : Sub (Ext F ν) :=1439  FRC.Extension.Ext.instSub14401441@[reducible] def instMul : Mul (Ext F ν) :=1442  FRC.Extension.Ext.instMul14431444@[reducible] def instSMulNat : SMul ℕ (Ext F ν) :=1445  FRC.Extension.Ext.instSMulNat14461447@[reducible] def instSMulInt : SMul ℤ (Ext F ν) :=1448  FRC.Extension.Ext.instSMulInt14491450@[reducible] def instCommRing : CommRing (Ext F ν) :=1451  FRC.Extension.Ext.instCommRing14521453@[reducible] def instStarRing : StarRing (Ext F ν) :=1454  FRC.Extension.Ext.instStarRing14551456end Ext14571458namespace Ext1459variable {F : Type*} [Field F] {ν : F}14601461theorem norm_eq_zero_iff (hν : ¬ IsSquare ν) (z : Ext F ν) : norm z = 0 ↔ z = 0 :=1462  FRC.Extension.Ext.norm_eq_zero_iff hν z14631464@[reducible] noncomputable def instInv : Inv (Ext F ν) :=1465  FRC.Extension.Ext.instInv14661467theorem inv_def (z : Ext F ν) : z⁻¹ = ofBase (norm z)⁻¹ * conj z :=1468  FRC.Extension.Ext.inv_def z14691470theorem mul_inv_cancel' (hν : ¬ IsSquare ν) (z : Ext F ν) (hz : z ≠ 0) : z * z⁻¹ = 1 :=1471  FRC.Extension.Ext.mul_inv_cancel' hν z hz14721473/-- 8:A2 — the field structure under `¬ IsSquare ν`, `z⁻¹ = z̄/N(z)` (a `def`, not an instance: the hypothesis is1474not a class). -/1475@[reducible] noncomputable def field (hν : ¬ IsSquare ν) : Field (Ext F ν) :=1476  FRC.Extension.Ext.field hν14771478end Ext147914801481-- Ledger predicates of 8-dirac (generated by make_predicates.py from docs/8-dirac/8-dirac-ledger.json; edit the ledger, not this section)1482/-- 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. Cited definitions (not proofs): FRC.Dirac.Ext.field. -/1483theorem p08002 : (∀ {F : Type u_1} [CommRing F] {ν : F} (z z' : FRC.Dirac.Ext F ν), (z * z').norm = z.norm * z'.norm) ∧ ∀ {F : Type u_2} [Field F] {ν : F}, ¬IsSquare ν → ∀ {u : (FRC.Dirac.Ext F ν)ˣ}, u ∈ FRC.Dirac.Ext.normOneGroup F ν → ∃ z, FRC.Dirac.Ext.boost z = u :=1484  And.intro @FRC.Dirac.Ext.norm_mul (@FRC.Dirac.Ext.exists_boost_eq)1485/-- 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$). -/1486theorem p08005 : (171106 : ℕ) * (171106 : ℕ) * (2 : ℕ) % (2408561 : ℕ) = (1 : ℕ) ∧ (2 : ℕ) * (1204281 : ℕ) % (2408561 : ℕ) = (1 : ℕ) ∧ (1204281 : ℕ) * (12 : ℕ) % (2408561 : ℕ) = (6 : ℕ) ∧ Nat.Prime (2408561 : ℕ) :=1487  @FRC.Dirac.carrier_constants1488/-- 8:B2 (p08008) — The class is the datum: $\Fpx/(\Fpx)^{2}$ has order two, any two nonsquares differ by a square factor, and the Lorentzian form depends on $\nu$ only through its class. -/1489theorem p08008 : (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ZMod p}, a ≠ (0 : ZMod p) → b ≠ (0 : ZMod p) → ¬IsSquare a → ¬IsSquare b → IsSquare (a * b)) ∧ ∀ {K : Type u_1} [CommRing K] (ν m x₀ x₁ x₂ x₃ : K), -(m ^ (2 : ℕ) * ν) * x₀ ^ (2 : ℕ) + x₁ ^ (2 : ℕ) + x₂ ^ (2 : ℕ) + x₃ ^ (2 : ℕ) = -ν * (m * x₀) ^ (2 : ℕ) + x₁ ^ (2 : ℕ) + x₂ ^ (2 : ℕ) + x₃ ^ (2 : ℕ) :=1490  And.intro @FRC.Dirac.class_datum (@FRC.Dirac.form_class)1491/-- 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$. -/1492theorem p08009 : (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, orderOf g = p - (1 : ℕ) → p % (2 : ℕ) = (1 : ℕ) → ¬IsSquare g ∧ ¬IsSquare g⁻¹) ∧ (∀ (κ : ℕ) [hp' : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] {g : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, orderOf g = (4 : ℕ) * κ → (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ↔ Even κ) ∧ (IsSquare (-2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (g ^ ((3 : ℕ) * κ)) ↔ Even κ) ∧ g ^ ((3 : ℕ) * κ) = -g ^ κ ∧ IsSquare (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))) ∧ (FRC.Dirac.Aent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (10 : ZMod (13 : ℕ)) ∧ FRC.Dirac.Bent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (2 : ZMod (13 : ℕ)) ∧ (10 : ZMod (13 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (13 : ℕ)) * (2 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) * (7 : ZMod (13 : ℕ)) = (1 : ZMod (13 : ℕ)) ∧ ¬IsSquare (7 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ ¬IsSquare (6 : ZMod (13 : ℕ)) ∧ orderOf (2 : ZMod (13 : ℕ)) = (12 : ℕ)) ∧ FRC.Dirac.Aent (3 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) = (15 : ZMod (17 : ℕ)) ∧ FRC.Dirac.Bent (3 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) = (1 : ZMod (17 : ℕ)) ∧ (15 : ZMod (17 : ℕ)) ^ (2 : ℕ) - (3 : ZMod (17 : ℕ)) * (1 : ZMod (17 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (17 : ℕ)) ∧ (3 : ZMod (17 : ℕ)) ^ (4 : ℕ) = (13 : ZMod (17 : ℕ)) ∧ (4 : ZMod (17 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (17 : ℕ)) ∧ IsSquare (2 : ZMod (17 : ℕ)) ∧ IsSquare (4 : ZMod (17 : ℕ)) ∧ IsSquare (13 : ZMod (17 : ℕ)) ∧ ¬IsSquare (3 : ZMod (17 : ℕ)) ∧ orderOf (3 : ZMod (17 : ℕ)) = (16 : ℕ) ∧ (17 : ℕ) % (12 : ℕ) = (5 : ℕ) ∧ (Even (4 : ℕ) ∧ (4 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ Nat.Prime (17 : ℕ)) ∧ ∀ κ < (4 : ℕ), ¬(Even κ ∧ κ % (3 : ℕ) = (1 : ℕ) ∧ Nat.Prime ((4 : ℕ) * κ + (1 : ℕ))) :=1493  And.intro @FRC.Dirac.drive_nonsquare (And.intro @FRC.Dirac.named_residues (And.intro @FRC.Dirac.shell13 (@FRC.Dirac.shell17)))1494/-- 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$). -/1495theorem p08010 : (∀ {K : Type u_1} [Field K] (g : K), (2 : K) ≠ (0 : K) → (2 : K)⁻¹ * ((2 : K) * g) = g) ∧ (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, g ≠ (0 : ZMod p) → ¬IsSquare g → (2 : ZMod p) ≠ (0 : ZMod p) → (IsSquare ((2 : ZMod p) * g) ↔ ¬IsSquare (2 : ZMod p))) ∧ (∀ (κ : ℕ) [hp' : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] {g : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, orderOf g = (4 : ℕ) * κ → (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ↔ Even κ) ∧ (IsSquare (-2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (g ^ ((3 : ℕ) * κ)) ↔ Even κ) ∧ g ^ ((3 : ℕ) * κ) = -g ^ κ ∧ IsSquare (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))) ∧ (FRC.Dirac.Aent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (10 : ZMod (13 : ℕ)) ∧ FRC.Dirac.Bent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (2 : ZMod (13 : ℕ)) ∧ (10 : ZMod (13 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (13 : ℕ)) * (2 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) * (7 : ZMod (13 : ℕ)) = (1 : ZMod (13 : ℕ)) ∧ ¬IsSquare (7 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ ¬IsSquare (6 : ZMod (13 : ℕ)) ∧ orderOf (2 : ZMod (13 : ℕ)) = (12 : ℕ)) ∧ (171106 : ℕ) * (171106 : ℕ) * (2 : ℕ) % (2408561 : ℕ) = (1 : ℕ) ∧ (2 : ℕ) * (1204281 : ℕ) % (2408561 : ℕ) = (1 : ℕ) ∧ (1204281 : ℕ) * (12 : ℕ) % (2408561 : ℕ) = (6 : ℕ) ∧ Nat.Prime (2408561 : ℕ) :=1496  And.intro @FRC.Dirac.nu_factorisation (And.intro @FRC.Dirac.two_g_class (And.intro @FRC.Dirac.named_residues (And.intro @FRC.Dirac.shell13 (@FRC.Dirac.carrier_constants))))1497/-- 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$. -/1498theorem p08011 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, orderOf g = p - (1 : ℕ) → p % (2 : ℕ) = (1 : ℕ) → ∀ (k : ℕ), IsSquare (g ^ k) ↔ Even k :=1499  @FRC.LedgerML.p080111500/-- 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. -/1501theorem p08012 : ∀ {K : Type u_1} [Field K] {ν : K} (g : K) (z : FRC.Dirac.Ext K ν), (FRC.Dirac.Ext.ofBase g * z).norm = g ^ (2 : ℕ) * z.norm :=1502  @FRC.Dirac.norm_growth1503/-- 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. -/1504theorem p08013 : ∀ {p : Nat} [hp : Fact (Nat.Prime p)] {ν : ZMod p}, Not (@IsSquare (ZMod p) (@Distrib.toMul (ZMod p) (@instDistribOfSemiring (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) ν) → ∀ (a : ZMod p), @IsSquare (FRC.Dirac.Ext (ZMod p) ν) (@FRC.Dirac.Ext.instMul (ZMod p) (ZMod.commRing p) ν) (@FRC.Dirac.Ext.ofBase (ZMod p) (ZMod.commRing p) ν a) :=1505  @FRC.Dirac.ext_square1506/-- 8:C2 (p08016) — The form is Hermitian and nondegenerate; $T_u$ is unitary with $T_u^{\dagger}=T_{-u}$; $\Delta_E$ and $H_{E,V,\vkap}$ are self-adjoint; under $A\in\mathrm{GL}_d(\Fp)$ the pullback $A_*$ intertwines translations, differences and Laplacians of the two frames. -/1507theorem p08016 : (∀ {K : Type u_1} [CommRing K] [StarRing K] {X : Type u_5} [Fintype X] (ψ φ : X → K), star (FRC.Dirac.herm ψ φ) = FRC.Dirac.herm φ ψ) ∧ (∀ {K : Type u_6} [CommRing K] [StarRing K] {X : Type u_7} [Fintype X] [DecidableEq X] (ψ : X → K), (∀ (φ : X → K), FRC.Dirac.herm ψ φ = (0 : K)) → ψ = (0 : X → K)) ∧ (∀ {K : Type u_8} [CommRing K] [StarRing K] {G : Type u_9} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K), FRC.Dirac.herm (FRC.Dirac.translate u ψ) (FRC.Dirac.translate u φ) = FRC.Dirac.herm ψ φ) ∧ (∀ {K : Type u_10} [CommRing K] [StarRing K] {G : Type u_11} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K), FRC.Dirac.herm (FRC.Dirac.translate u ψ) φ = FRC.Dirac.herm ψ (FRC.Dirac.translate (-u) φ)) ∧ (∀ {K : Type u_12} [CommRing K] [StarRing K] {G : Type u_2} [AddGroup G] [Fintype G] (e : G) (ψ φ : G → K), FRC.Dirac.herm (FRC.Dirac.laplacian e ψ) φ = FRC.Dirac.herm ψ (FRC.Dirac.laplacian e φ)) ∧ ∀ {K : Type u_3} [CommRing K] [StarRing K] {G : Type u_4} [AddGroup G] [Fintype G] (e : G) (ϰ : K), star ϰ = ϰ → ∀ (V : G → K), (∀ (x : G), star (V x) = V x) → ∀ (ψ φ : G → K), FRC.Dirac.herm (FRC.Dirac.hamiltonian e ϰ V ψ) φ = FRC.Dirac.herm ψ (FRC.Dirac.hamiltonian e ϰ V φ) :=1508  And.intro @FRC.Dirac.herm_star (And.intro @FRC.Dirac.herm_nondegenerate (And.intro @FRC.Dirac.herm_translate (And.intro @FRC.Dirac.herm_translate_adjoint (And.intro @FRC.Dirac.herm_laplacian (@FRC.Dirac.herm_hamiltonian)))))1509/-- 8:C4 (p08018) — Exact Hermitian preservation: for self-adjoint $H$ and admissible $\alpha$ the Cayley step is unitary, and every orbit is periodic. -/1510theorem p08018 : (∀ {R : Type u_1} [Ring R] (σ : R → R), (∀ (x y : R), σ (x * y) = σ y * σ x) → (∀ (x y : R), σ (x + y) = σ x + σ y) → σ (1 : R) = (1 : R) → (∀ (x : R), σ (-x) = -σ x) → ∀ {h a : R}, σ h = h → σ a = -a → (∀ (x : R), Commute a x) → ∀ (hu : IsUnit ((1 : R) - a * h)), have u := ↑hu.unit⁻¹ * ((1 : R) + a * h); σ u * u = (1 : R)) ∧ ∀ {R : Type u_2} [Ring R] [Finite R] (u : Rˣ), IsOfFinOrder u :=1511  And.intro @FRC.Dirac.cayley_unitary (@FRC.Dirac.cayley_periodic)1512set_option linter.defProp false in1513/-- 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. -/1514def p08019 := And.intro @FRC.Dirac.Ext.cayley_norm (And.intro @FRC.Dirac.Ext.cayley_injective (And.intro @FRC.Dirac.Ext.card_normOneGroup (@FRC.Dirac.Ext.cayley_gauge)))1515set_option linter.defProp false in1516/-- 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. -/1517def p08020 := And.intro @FRC.Dirac.kinetic_nilpotent (@FRC.Dirac.cayley_period)1518/-- 8:D2 (p08022) — The Clifford relations $\gamma^{\mu}\gamma^{\nu}+\gamma^{\nu}\gamma^{\mu}=2\eta_{\mu\nu}I_4$. -/1519theorem p08022 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → FRC.Dirac.γ0 i w * FRC.Dirac.γ0 i w = -ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ1 i * FRC.Dirac.γ1 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ2 i * FRC.Dirac.γ2 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ3 i * FRC.Dirac.γ3 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ0 i w * FRC.Dirac.γ1 i + FRC.Dirac.γ1 i * FRC.Dirac.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ0 i w * FRC.Dirac.γ2 i + FRC.Dirac.γ2 i * FRC.Dirac.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ0 i w * FRC.Dirac.γ3 i + FRC.Dirac.γ3 i * FRC.Dirac.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ1 i * FRC.Dirac.γ2 i + FRC.Dirac.γ2 i * FRC.Dirac.γ1 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ1 i * FRC.Dirac.γ3 i + FRC.Dirac.γ3 i * FRC.Dirac.γ1 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.γ2 i * FRC.Dirac.γ3 i + FRC.Dirac.γ3 i * FRC.Dirac.γ2 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K)) ∧ ∀ {K : Type u_2} [CommRing K] {i : K}, i * i = (-1 : K) → FRC.Dirac.σ1 * FRC.Dirac.σ1 = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Dirac.σ2 i * FRC.Dirac.σ2 i = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Dirac.σ3 * FRC.Dirac.σ3 = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Dirac.σ1 * FRC.Dirac.σ2 i + FRC.Dirac.σ2 i * FRC.Dirac.σ1 = (0 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Dirac.σ1 * FRC.Dirac.σ3 + FRC.Dirac.σ3 * FRC.Dirac.σ1 = (0 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Dirac.σ2 i * FRC.Dirac.σ3 + FRC.Dirac.σ3 * FRC.Dirac.σ2 i = (0 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) :=1520  And.intro @FRC.Dirac.clifford (@FRC.Dirac.pauli)1521set_option linter.defProp false in1522/-- 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$). -/1523def p08025 := And.intro @FRC.Dirac.boost_entries (And.intro @FRC.Dirac.Ext.boost_mem (And.intro @FRC.Dirac.Ext.boost_eq_one_iff (And.intro @FRC.Dirac.Ext.boost_range (And.intro @FRC.Dirac.Ext.card_normOneGroup (And.intro @FRC.Dirac.Ext.normOne_cyclic (@FRC.Dirac.Ext.order_three_iff))))))1524/-- 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. -/1525theorem p08026 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → ∀ (x y : K), FRC.Dirac.Mγ i w * FRC.Dirac.Mγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.Dirac.Mγ i w) * FRC.Dirac.γ0 i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w) = (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.Dirac.γ0 i w + -((2 : K) * x * y * ν) • FRC.Dirac.γ1 i ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.Dirac.Mγ i w) * FRC.Dirac.γ1 i * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w) = -((2 : K) * x * y) • FRC.Dirac.γ0 i w + (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.Dirac.γ1 i ∧ FRC.Dirac.Mγ i w * FRC.Dirac.γ2 i = FRC.Dirac.γ2 i * FRC.Dirac.Mγ i w ∧ FRC.Dirac.Mγ i w * FRC.Dirac.γ3 i = FRC.Dirac.γ3 i * FRC.Dirac.Mγ i w) ∧ ∀ {F : Type u_2} [Field F] {i w ν x y : F}, i * i = (-1 : F) → w * w = ν → x ^ (2 : ℕ) - ν * y ^ (2 : ℕ) ≠ (0 : F) → (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ))⁻¹ • (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + -y • FRC.Dirac.Mγ i w) * FRC.Dirac.γ0 i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + y • FRC.Dirac.Mγ i w) = FRC.Dirac.Aent ν x y • FRC.Dirac.γ0 i w + (ν * FRC.Dirac.Bent ν x y) • FRC.Dirac.γ1 i ∧ (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ))⁻¹ • (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + -y • FRC.Dirac.Mγ i w) * FRC.Dirac.γ1 i * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + y • FRC.Dirac.Mγ i w) = FRC.Dirac.Bent ν x y • FRC.Dirac.γ0 i w + FRC.Dirac.Aent ν x y • FRC.Dirac.γ1 i :=1526  And.intro @FRC.Dirac.spin_conjugation (@FRC.Dirac.spin_conjugation_AB)1527/-- 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. -/1528theorem p08027 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → ∀ (x y : K), FRC.Dirac.Mγ i w * FRC.Dirac.Mγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.Dirac.Mγ i w) * FRC.Dirac.γ0 i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w) = (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.Dirac.γ0 i w + -((2 : K) * x * y * ν) • FRC.Dirac.γ1 i ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.Dirac.Mγ i w) * FRC.Dirac.γ1 i * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w) = -((2 : K) * x * y) • FRC.Dirac.γ0 i w + (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.Dirac.γ1 i ∧ FRC.Dirac.Mγ i w * FRC.Dirac.γ2 i = FRC.Dirac.γ2 i * FRC.Dirac.Mγ i w ∧ FRC.Dirac.Mγ i w * FRC.Dirac.γ3 i = FRC.Dirac.γ3 i * FRC.Dirac.Mγ i w) ∧ ∀ {F : Type u_2} [Field F] (ν x y u v : F), x ^ (2 : ℕ) - ν * y ^ (2 : ℕ) ≠ (0 : F) → u ^ (2 : ℕ) - ν * v ^ (2 : ℕ) ≠ (0 : F) → FRC.Dirac.Aent ν x y ^ (2 : ℕ) - ν * FRC.Dirac.Bent ν x y ^ (2 : ℕ) = (1 : F) ∧ FRC.Dirac.Aent ν x y * FRC.Dirac.Aent ν u v + ν * (FRC.Dirac.Bent ν x y * FRC.Dirac.Bent ν u v) = FRC.Dirac.Aent ν (x * u + ν * y * v) (x * v + y * u) ∧ FRC.Dirac.Aent ν x y * FRC.Dirac.Bent ν u v + FRC.Dirac.Bent ν x y * FRC.Dirac.Aent ν u v = FRC.Dirac.Bent ν (x * u + ν * y * v) (x * v + y * u) ∧ FRC.Dirac.Aent ν (1 : F) (0 : F) = (1 : F) ∧ FRC.Dirac.Bent ν (1 : F) (0 : F) = (0 : F) ∧ FRC.Dirac.Aent ν x (-y) = FRC.Dirac.Aent ν x y ∧ FRC.Dirac.Bent ν x (-y) = -FRC.Dirac.Bent ν x y :=1529  And.intro @FRC.Dirac.spin_conjugation (@FRC.Dirac.boost_entries)1530/-- 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$). -/1531theorem p08029 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → FRC.Dirac.Xγ i w * FRC.Dirac.Xγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.Dirac.Xγ i w * FRC.Dirac.γ0 i w = FRC.Dirac.γ0 i w * FRC.Dirac.Xγ i w ∧ FRC.Dirac.Xγ i w * FRC.Dirac.γ1 i = FRC.Dirac.γ1 i * FRC.Dirac.Xγ i w ∧ FRC.Dirac.Xγ i w * FRC.Dirac.γ3 i = FRC.Dirac.γ3 i * FRC.Dirac.Xγ i w ∧ FRC.Dirac.Xγ i w * FRC.Dirac.γ2 i = -(FRC.Dirac.γ2 i * FRC.Dirac.Xγ i w)) ∧ (∀ {K : Type u_2} [CommRing K] [StarRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → (FRC.Dirac.γ0 i w).conjTranspose = -FRC.Dirac.γ0 i w ∧ (FRC.Dirac.γ1 i).conjTranspose = -FRC.Dirac.γ1 i ∧ (FRC.Dirac.γ2 i).conjTranspose = FRC.Dirac.γ2 i ∧ (FRC.Dirac.γ3 i).conjTranspose = -FRC.Dirac.γ3 i ∧ (FRC.Dirac.Xγ i w).conjTranspose = FRC.Dirac.Xγ i w) ∧ ∀ {K : Type u_3} [CommRing K] [StarRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → (FRC.Dirac.γ0 i w).conjTranspose * FRC.Dirac.Xγ i w = -(FRC.Dirac.Xγ i w * FRC.Dirac.γ0 i w) ∧ (FRC.Dirac.γ1 i).conjTranspose * FRC.Dirac.Xγ i w = -(FRC.Dirac.Xγ i w * FRC.Dirac.γ1 i) ∧ (FRC.Dirac.γ2 i).conjTranspose * FRC.Dirac.Xγ i w = -(FRC.Dirac.Xγ i w * FRC.Dirac.γ2 i) ∧ (FRC.Dirac.γ3 i).conjTranspose * FRC.Dirac.Xγ i w = -(FRC.Dirac.Xγ i w * FRC.Dirac.γ3 i) ∧ (FRC.Dirac.γ0 i w).conjTranspose * FRC.Dirac.γ0 i w = -(FRC.Dirac.γ0 i w * FRC.Dirac.γ0 i w) ∧ (FRC.Dirac.γ1 i).conjTranspose * FRC.Dirac.γ0 i w = FRC.Dirac.γ0 i w * FRC.Dirac.γ1 i :=1532  And.intro @FRC.Dirac.spinor_twist (And.intro @FRC.Dirac.gamma_dagger (@FRC.Dirac.twist_adjoint))1533/-- 8:D10 (p08030) — Exact Dirac evolution: the Cayley step of $H=\mathcal D^{s}-mI$ preserves $\langle\cdot,\cdot\rangle_X$; for $m=0$ admissibility is automatic, $U$ unipotent with order a power of $\p$ ($25=\p^{2}$ in the $1{+}1$ computation at $\p=5$); for $m\ne0$, $U=\varphi(-m)V$ and $\operatorname{ord}(U)=\operatorname{lcm}(\p^{a},\operatorname{ord}_{N^{1}}\varphi(-m))$ ($75$, $150$ at $m=1,2$). -/1534theorem p08030 : (∀ {R : Type u_1} [Ring R] (σ : R → R), (∀ (x y : R), σ (x * y) = σ y * σ x) → (∀ (x y : R), σ (x + y) = σ x + σ y) → σ (1 : R) = (1 : R) → (∀ (x : R), σ (-x) = -σ x) → ∀ {h a : R}, σ h = h → σ a = -a → (∀ (x : R), Commute a x) → ∀ (hu : IsUnit ((1 : R) - a * h)), have u := ↑hu.unit⁻¹ * ((1 : R) + a * h); σ u * u = (1 : R)) ∧ ∀ {R : Type u_2} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {t : R}, t ^ p = (1 : R) → (t - (1 : R)) ^ p = (0 : R) :=1535  And.intro @FRC.Dirac.cayley_unitary (@FRC.Dirac.translation_nilpotent)1536/-- 8:D11 (p08031) — The two Dirac operators are one covariant family: the pullback identity holds for the symmetric differences, $\mathcal T_{\Lambda,S}$ carries $\mathcal D^{s}$ to its transported form, and the spinor form transports by the norm, $S(x,y)^{\#}=S(x,-y)=\delta S^{-1}$: norm-one lifts preserve $\langle\cdot,\cdot\rangle_X$ exactly, the odd coset scales it by the nonsquare class. -/1537theorem p08031 : (∀ {K : Type u_1} [CommRing K] [StarRing K] {i w ν x y : K}, i * i = (-1 : K) → w * w = ν → star w = -w → star x = x → star y = y → (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w).conjTranspose = x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.Dirac.Mγ i w ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.Dirac.Mγ i w) * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w) = (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ)) • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K)) ∧ ∀ {K : Type u_2} [CommRing K] [StarRing K] {i w ν x y : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → star x = x → star y = y → (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w).conjTranspose * FRC.Dirac.Xγ i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.Dirac.Mγ i w) = (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ)) • FRC.Dirac.Xγ i w :=1538  And.intro @FRC.Dirac.lift_adjoint (@FRC.Dirac.lift_transport)1539/-- 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. -/1540theorem p08032 : (FRC.Dirac.Aent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (10 : ZMod (13 : ℕ)) ∧ FRC.Dirac.Bent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (2 : ZMod (13 : ℕ)) ∧ (10 : ZMod (13 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (13 : ℕ)) * (2 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) * (7 : ZMod (13 : ℕ)) = (1 : ZMod (13 : ℕ)) ∧ ¬IsSquare (7 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ ¬IsSquare (6 : ZMod (13 : ℕ)) ∧ orderOf (2 : ZMod (13 : ℕ)) = (12 : ℕ)) ∧ FRC.Dirac.Aent (3 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) = (15 : ZMod (17 : ℕ)) ∧ FRC.Dirac.Bent (3 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) (1 : ZMod (17 : ℕ)) = (1 : ZMod (17 : ℕ)) ∧ (15 : ZMod (17 : ℕ)) ^ (2 : ℕ) - (3 : ZMod (17 : ℕ)) * (1 : ZMod (17 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (17 : ℕ)) ∧ (3 : ZMod (17 : ℕ)) ^ (4 : ℕ) = (13 : ZMod (17 : ℕ)) ∧ (4 : ZMod (17 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (17 : ℕ)) ∧ IsSquare (2 : ZMod (17 : ℕ)) ∧ IsSquare (4 : ZMod (17 : ℕ)) ∧ IsSquare (13 : ZMod (17 : ℕ)) ∧ ¬IsSquare (3 : ZMod (17 : ℕ)) ∧ orderOf (3 : ZMod (17 : ℕ)) = (16 : ℕ) ∧ (17 : ℕ) % (12 : ℕ) = (5 : ℕ) ∧ (Even (4 : ℕ) ∧ (4 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ Nat.Prime (17 : ℕ)) ∧ ∀ κ < (4 : ℕ), ¬(Even κ ∧ κ % (3 : ℕ) = (1 : ℕ) ∧ Nat.Prime ((4 : ℕ) * κ + (1 : ℕ))) :=1541  And.intro @FRC.Dirac.shell13 (@FRC.Dirac.shell17)1542set_option linter.defProp false in1543/-- 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}$). -/1544def p08035 := And.intro @FRC.Dirac.loss_factor_one (@FRC.Dirac.power_map_count)1545set_option linter.defProp false in1546/-- 8:E3 (p08036) — Cayley propagators and boost transports have loss factor one: the wave dynamics is isentropic, compression confined to the power-map layer. -/1547def p08036 := @FRC.Dirac.unit_loss_factor_one1548set_option linter.defProp false in1549/-- 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. -/1550def p08037 := And.intro @FRC.Dirac.cayley_period (And.intro @FRC.Dirac.kinetic_nilpotent (@FRC.Dirac.Ext.torus_period))1551/-- 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. -/1552theorem p08039 : ∀ (κ : ℕ) [hp : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] {g : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, orderOf g = (4 : ℕ) * κ → (4 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * ↑κ = (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ∧ ↑κ = -(4 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ∧ (1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) + ↑κ = (3 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * (4 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ∧ (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * ↑κ = -(2 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ∧ g ^ κ = -g ^ ((3 : ℕ) * κ) ∧ κ + (1 : ℕ) ≤ (2 : ℕ) * κ :=1553  @FRC.Dirac.latitude_identities1554set_option linter.defProp false in1555/-- 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}$. -/1556def p08040 := And.intro @FRC.Dirac.drive_chi (And.intro @FRC.Dirac.drive_sum (And.intro @FRC.Dirac.chi_isotropy (@FRC.Dirac.exceptional_eigen)))1557set_option linter.defProp false in1558/-- 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. -/1559def p08041 := And.intro @FRC.Dirac.sector_separation (And.intro @FRC.Dirac.dispersion (@FRC.Dirac.exceptional_eigen))1560-- end ledger predicates15611562end FRC.Dirac1563