Theme/Dirac.lean — FrcMathlib

1import Mathlib2import FrcMathlib.Theme.Extension3import FrcMathlib.Theme.Frame45/-!6# The Dirac theme on Mathlib — Schrödinger and Dirac dynamics over the finite substrate (2026-09-20; the theme file7since the migration of 8-dirac, 1 November 2026)89The Mathlib content of *Schrödinger and Dirac Dynamics over Finite Substrate* (8-dirac, tree `8-dirac-20260709`), in10the namespace `FRC.DiracML`; the paper module `FrcMathlib/Dirac.lean` carries every cited name as an alias under11`FRC.Dirac` and the ledger's predicate declarations. The coefficient field `K = F[w]/(w² − ν)` on components with its Frobenius conjugation12and norm, a field when `ν` is a nonsquare, `|K| = |F|²` (A2, B1); the square-class arithmetic on13`ZMod p`: two nonsquares differ by a square and the Lorentzian form depends on `ν` through its class alone14(B2); chronon parity — `g^k` is a square exactly when `k` is even, so the drive and its inverse are15nonsquares and `2`, `2⁻¹`, `−2` and the quarter-turn `i = g^{3κ}` are squares exactly when `κ` is even (B3,16B5); the factorisation `ν = g = 2⁻¹·(2g)` with the classes of the two factors (B4); the norm growth `N(gz) = g² N(z)` (B6); over `K` every base element17is a square, the dichotomy collapsing (B7). The Hermitian form on functions of a finite set — symmetric,18nondegenerate, the translations unitary with `T_u† = T_{−u}`, the Laplacian and the Hamiltonians19self-adjoint (C2); the Cayley step unitary for any anti-involution, hence for the form and for the `X`-form20(C4, D10); the Cayley transform norm-one valued, injective, inverted by the orientation gauge, and the torus21of `|F| + 1` points (C5); kinetic Hamiltonians nilpotent with `𝒜(H) = K⁻`, the Cayley step of period exactly22`p` (C6, E4). The Clifford relations from `i² = −1`, `w² = ν` alone, by the block computation of the paper's23proof (D2); the boost torus — `A² − νB² = 1`, the group law of the entries, the boost `z ↦ z/z̄` a24homomorphism onto `N¹` with kernel the scalar line (Hilbert 90), `N¹ ≅ C_{p+1}` cyclic, an element of order25three exactly when `3 ∣ p + 1` (D5); spin conjugation and the transported gammas (D6, D7); the spinor twist26`X = γ⁰γ¹γ³` with `X² = ν`, its commutations, the dagger signs with `γ²` the obstruction, `(γ^μ)†X = −Xγ^μ`27and the failure of the `γ⁰`-twist (D9); the transport of the form `S†XS = δX` (D11); the worked shells28`𝔽₁₃`, `𝔽₁₇₃` and the laboratory Carrier (D12, B4). The loss factor and the power-map counts on the cyclic29group `(ZMod p)ˣ` (E2, E3), the potential period `p + 1` attained (E4); the latitude identities (F2); the30drive on the characters — the eigenvalues `g^{−k}`, the isotropy `Σ_x x^{2k}` by the character sum, the31exceptional lines `±1` (F3); the sector separation, no meridional plane waves, the dispersion relation (F4).32Classical (tier 2) on Mathlib's hierarchy; the finite content — parity, latitude and spectral rows on every33frame, the worked shells decided by the kernel — is proved with no axioms in `FrcCore/Theme/Dirac.lean`. Outside34both modules: the factorization `(𝒟 − m)(𝒟 + m) = KG − m²` (D3), the pullback identity and the transported35factorization (D7), the covariance of the transported family (D8), the operator clauses of D9 (`T − T⁻¹`36nilpotent and anti-self-adjoint, `𝒟^s` `X`-self-adjoint and nilpotent — the package's instances), the massless37clause and the numerals `5`, `75`, `150` of D10 (the Cayley step's `X`-unitarity is `cayley_unitary` given that38self-adjointness), the pullback and transport clauses of D11, the frame covariance of C2, the surjectivity39of the Cayley transform onto `N¹ ∖ {−1}` (C5 — injectivity and the count are proved), the mixed datum `1563`40of E4, the general count of the unit-norm circle (F2 — instances in the core), and the realisation rows B8,41D13, F5.42-/4344namespace FRC.DiracML4546section47open FRC.Extension (Ext)48open FRC.Extension.Ext49open FRC.Frame (parity_iff drive_nonsquare)5051/-! ## The norm-one torus and the Cayley transform -/52namespace Ext53variable {F : Type*} [Field F] {ν : F}5455/-- The finite Cayley transform `φ_α(t) = (1 + αt)/(1 − αt)` for `α = k w`, computed by the conjugate:56`(1 + αt) · conj(1 − αt) / N(1 − αt)`. -/57noncomputable def cayley (k t : F) : Ext F ν :=58  (1 + ofBase (k * t) * w) * (1 - ofBase (k * t) * w)⁻¹5960theorem norm_ofBase_mul (a : F) (z : Ext F ν) : Ext.norm (ofBase a * z) = a ^ 2 * Ext.norm z := by61  simp only [Ext.norm, mul_re, mul_im, ofBase_re, ofBase_im]; ring6263theorem norm_one_add_kw (k t : F) : Ext.norm ((1 : Ext F ν) + ofBase (k * t) * w) = 1 - ν * (k * t) ^ 2 := by64  simp only [Ext.norm, add_re, add_im, one_re, one_im, mul_re, mul_im, ofBase_re, ofBase_im, w_re, w_im]; ring6566theorem norm_one_sub_kw (k t : F) : Ext.norm ((1 : Ext F ν) - ofBase (k * t) * w) = 1 - ν * (k * t) ^ 2 := by67  simp only [Ext.norm, sub_re, sub_im, one_re, one_im, mul_re, mul_im, ofBase_re, ofBase_im, w_re, w_im]; ring6869theorem norm_conj (z : Ext F ν) : Ext.norm (conj z) = Ext.norm z := by simp [Ext.norm]7071/-- `N(z⁻¹) = N(z)⁻¹`. -/72theorem norm_inv (hν : ¬ IsSquare ν) (z : Ext F ν) : Ext.norm z⁻¹ = (Ext.norm z)⁻¹ := by73  by_cases hz : z = 074  · subst hz75    rw [inv_def]76    simp [Ext.norm]77  · rw [inv_def, norm_ofBase_mul, norm_conj]78    have := (norm_eq_zero_iff hν z).not.2 hz79    field_simp8081theorem one_sub_nu_sq_ne_zero (hν : ¬ IsSquare ν) (t : F) : 1 - ν * t ^ 2 ≠ 0 := by82  intro h83  by_cases ht : t = 084  · simp [ht] at h85  · apply hν86    refine ⟨t⁻¹, ?_⟩87    field_simp88    linear_combination -h8990/-- 8:C5 — the Cayley transform takes values in the norm-one torus: `N(φ_α(λ)) = 1` for every `λ ∈ F`, the91denominator never vanishing (Theorem `cayley-transform`). -/92theorem cayley_norm (hν : ¬ IsSquare ν) (k t : F) : Ext.norm (cayley k t : Ext F ν) = 1 := by93  unfold cayley94  rw [Ext.norm_mul, norm_inv hν, norm_one_add_kw, norm_one_sub_kw]95  exact mul_inv_cancel₀ (one_sub_nu_sq_ne_zero hν _)9697end Ext9899/-! ## The norm-one torus as a group, the boost homomorphism and Hilbert 90 (8:D5, C5) -/100namespace Ext101variable {F : Type*} [Field F] {ν : F}102103/-- Conjugation as a ring homomorphism. -/104def conjHom : Ext F ν →+* Ext F ν where105  toFun := conj106  map_one' := conj_one107  map_mul' := Ext.conj_mul108  map_zero' := by ext <;> simp109  map_add' := conj_add110111@[simp] theorem conjHom_apply (z : Ext F ν) : conjHom z = conj z := rfl112113instance : Nontrivial (Ext F ν) := ⟨⟨0, 1, fun h => by simpa using congrArg re h⟩⟩114115/-- The base field as a ring homomorphism into `K`. -/116def ofBaseHom : F →+* Ext F ν where117  toFun := ofBase118  map_one' := rfl119  map_mul' := ofBase_mul120  map_zero' := rfl121  map_add' := ofBase_add122123@[simp] theorem ofBaseHom_apply (a : F) : ofBaseHom a = (ofBase a : Ext F ν) := rfl124125theorem norm_one : Ext.norm (1 : Ext F ν) = 1 := by simp [Ext.norm]126127/-- `N¹`, the norm-one torus, as a subgroup of the units of `K` (no field structure needed). -/128def normOneGroup (F : Type*) [Field F] (ν : F) : Subgroup (Ext F ν)ˣ where129  carrier := {u | Ext.norm (u : Ext F ν) = 1}130  mul_mem' {a b} ha hb := by131    simp only [Set.mem_setOf_eq, Units.val_mul] at *132    rw [Ext.norm_mul, ha, hb, one_mul]133  one_mem' := by simp [norm_one]134  inv_mem' {a} ha := by135    simp only [Set.mem_setOf_eq] at *136    have h := Ext.norm_mul (a : Ext F ν) (↑a⁻¹ : Ext F ν)137    rw [Units.mul_inv, norm_one, ha, one_mul] at h138    exact h.symm139140theorem mem_normOneGroup {u : (Ext F ν)ˣ} : u ∈ normOneGroup F ν ↔ Ext.norm (u : Ext F ν) = 1 := Iff.rfl141142/-- Conjugation on the units. -/143def conjUnits : (Ext F ν)ˣ →* (Ext F ν)ˣ where144  toFun z := ⟨conj z, conj (↑z⁻¹ : Ext F ν), by rw [← Ext.conj_mul, Units.mul_inv, conj_one],145    by rw [← Ext.conj_mul, Units.inv_mul, conj_one]⟩146  map_one' := Units.ext (by simp [conj_one])147  map_mul' z z' := Units.ext (by simp [Ext.conj_mul])148149@[simp] theorem conjUnits_val (z : (Ext F ν)ˣ) : ((conjUnits z : (Ext F ν)ˣ) : Ext F ν) = conj z := rfl150151/-- The boost map `z ↦ z / z̄` on the units, a homomorphism (Lemma `boost-torus`). -/152def boost : (Ext F ν)ˣ →* (Ext F ν)ˣ where153  toFun z := z * (conjUnits z)⁻¹154  map_one' := by simp155  map_mul' z z' := by156    simp only [map_mul, mul_inv]157    exact mul_mul_mul_comm _ _ _ _158159theorem boost_def (z : (Ext F ν)ˣ) : boost z = z * (conjUnits z)⁻¹ := rfl160161theorem boost_val (z : (Ext F ν)ˣ) : (boost z : Ext F ν) * conj (z : Ext F ν) = (z : Ext F ν) := by162  rw [boost_def, Units.val_mul, mul_assoc, ← conjUnits_val, ← Units.val_mul, inv_mul_cancel, Units.val_one,163    mul_one]164165/-- 8:D14 — the boost of every unit lies in `N¹`: `N(z/z̄) = 1`. -/166theorem boost_mem (z : (Ext F ν)ˣ) : boost z ∈ normOneGroup F ν := by167  rw [mem_normOneGroup]168  have h := congrArg Ext.norm (boost_val z)169  rw [Ext.norm_mul, norm_conj] at h170  have hz : Ext.norm (z : Ext F ν) ≠ 0 := by171    intro h0172    have := Ext.norm_mul (z : Ext F ν) (↑z⁻¹ : Ext F ν)173    rw [Units.mul_inv, norm_one, h0, zero_mul] at this174    exact one_ne_zero this175  exact mul_right_cancel₀ hz (by rw [h, one_mul])176177/-- 8:D5 — the kernel of the boost is the scalar line: `z/z̄ = 1 ⟺ z̄ = z ⟺ z ∈ F`. -/178theorem boost_eq_one_iff (h2 : (2 : F) ≠ 0) [NoZeroDivisors F] (z : (Ext F ν)ˣ) :179    boost z = 1 ↔ (z : Ext F ν).im = 0 := by180  rw [← conj_eq_self_iff (z : Ext F ν) h2, boost_def, mul_inv_eq_one]181  constructor182  · intro h; exact (congrArg Units.val h).symm183  · intro h; exact Units.ext h.symm184185/-- 8:D5 — Hilbert 90 on the torus: every `u ∈ N¹` is a boost — `u = (1 + u)/(1 + ū)` for `u ≠ −1`, and186`−1 = w/w̄`. -/187theorem exists_boost_eq (hν : ¬ IsSquare ν) {u : (Ext F ν)ˣ} (hu : u ∈ normOneGroup F ν) :188    ∃ z : (Ext F ν)ˣ, boost z = u := by189  letI := field hν190  rw [mem_normOneGroup] at hu191  have hconj : conj (u : Ext F ν) = ((u⁻¹ : (Ext F ν)ˣ) : Ext F ν) := by192    have := mul_conj (u : Ext F ν)193    rw [hu, ofBase_one] at this194    exact (Units.inv_eq_of_mul_eq_one_right this).symm195  by_cases hm : (u : Ext F ν) = -1196  · -- `u = −1 = w / w̄`197    have hw : (w : Ext F ν) ≠ 0 := fun h => by simpa using congrArg im h198    refine ⟨Units.mk0 w hw, Units.ext ?_⟩199    apply mul_right_cancel₀ (show conj (w : Ext F ν) ≠ 0 by rw [conj_w]; exact neg_ne_zero.2 hw)200    have hb := boost_val (Units.mk0 w hw)201    rw [Units.val_mk0] at hb202    rw [hb, hm, conj_w, neg_one_mul, neg_neg]203  · have h1 : (1 : Ext F ν) + (u : Ext F ν) ≠ 0 := fun h => hm (by linear_combination h)204    refine ⟨Units.mk0 ((1 : Ext F ν) + (u : Ext F ν)) h1, Units.ext ?_⟩205    apply mul_right_cancel₀ (show conj ((1 : Ext F ν) + (u : Ext F ν)) ≠ 0 by206      intro h207      have := congrArg conj h208      rw [conj_conj] at this209      exact h1 (this.trans (by ext <;> simp)))210    have hb := boost_val (Units.mk0 ((1 : Ext F ν) + (u : Ext F ν)) h1)211    rw [Units.val_mk0] at hb212    rw [hb, conj_add, conj_one, hconj]213    have : (u : Ext F ν) * ((u⁻¹ : (Ext F ν)ˣ) : Ext F ν) = 1 := Units.mul_inv u214    linear_combination -this215216end Ext217218/-! ## The cardinalities: `|K| = |F|²`, `|N¹| = |F| + 1` (8:C5, D5) -/219namespace Ext220variable {F : Type*} [Field F] {ν : F}221222/-- `K ≃ F × F` on components. -/223def equivProd : Ext F ν ≃ F × F where224  toFun z := (z.re, z.im)225  invFun x := ⟨x.1, x.2⟩226  left_inv z := by cases z; rfl227  right_inv x := by cases x; rfl228229instance [Finite F] : Finite (Ext F ν) := Finite.of_equiv _ (equivProd (ν := ν)).symm230231omit [Field F] in232theorem card_ext [CommRing F] [Finite F] : Nat.card (Ext F ν) = Nat.card F ^ 2 := by233  rw [Nat.card_congr (equivProd (ν := ν)), Nat.card_prod, sq]234235/-- The kernel of the boost is the image of `Fˣ`: its cardinality is `|F| − 1`. -/236def baseUnits (h2 : (2 : F) ≠ 0) : Fˣ ≃ (boost (F := F) (ν := ν)).ker where237  toFun a := ⟨Units.map (ofBaseHom (ν := ν)).toMonoidHom a, by238      rw [MonoidHom.mem_ker, boost_eq_one_iff h2]; rfl⟩239  invFun z := Units.mk0 ((z : (Ext F ν)ˣ) : Ext F ν).re (by240      intro h241      have hz := (z : (Ext F ν)ˣ).ne_zero242      have him : ((z : (Ext F ν)ˣ) : Ext F ν).im = 0 := (boost_eq_one_iff h2 _).1 (MonoidHom.mem_ker.1 z.2)243      exact hz (by ext <;> simp [h, him]))244  left_inv a := by ext; rfl245  right_inv z := by246    have him : ((z : (Ext F ν)ˣ) : Ext F ν).im = 0 := (boost_eq_one_iff h2 _).1 (MonoidHom.mem_ker.1 z.2)247    apply Subtype.ext; apply Units.ext248    ext249    · rfl250    · exact him.symm251252/-- 8:D5, 8:C5, 8:F6 — the torus has `|F| + 1` elements: `|Kˣ| = |ker| · |N¹|`, `(q² − 1) = (q − 1)(q + 1)`. -/253theorem card_normOneGroup [Finite F] (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) :254    Nat.card (normOneGroup F ν) = Nat.card F + 1 := by255  letI := field hν256  have hrange : (boost (F := F) (ν := ν)).range = normOneGroup F ν := by257    ext u258    constructor259    · rintro ⟨z, rfl⟩; exact boost_mem z260    · intro hu; exact exists_boost_eq hν hu261  have h1 : Nat.card (Ext F ν)ˣ = Nat.card (Ext F ν) - 1 := Nat.card_units _262  have h2' : Nat.card (Ext F ν)ˣ = Nat.card ((Ext F ν)ˣ ⧸ (boost (F := F) (ν := ν)).ker) * Nat.card (boost (F := F) (ν := ν)).ker :=263    Subgroup.card_eq_card_quotient_mul_card_subgroup _264  have h3 : Nat.card ((Ext F ν)ˣ ⧸ (boost (F := F) (ν := ν)).ker) = Nat.card (normOneGroup F ν) := by265    rw [Nat.card_congr (QuotientGroup.quotientKerEquivRange (boost (F := F) (ν := ν))).toEquiv, hrange]266  have h4 : Nat.card (boost (F := F) (ν := ν)).ker = Nat.card F - 1 := by267    rw [← Nat.card_congr (baseUnits h2), Nat.card_units]268  have hq : 2 ≤ Nat.card F := by269    have := Nat.card_pos (α := F)270    by_contra hlt271    have h1' : Nat.card F = 1 := by omega272    have := Nat.card_eq_one_iff_unique.1 h1'273    obtain ⟨hsub, _⟩ := this274    exact one_ne_zero (hsub.elim 1 0)275  rw [h3, h4] at h2'276  rw [card_ext] at h1277  -- (q² − 1) = N · (q − 1)  ⇒  N = q + 1278  have key : Nat.card F ^ 2 - 1 = Nat.card (normOneGroup F ν) * (Nat.card F - 1) := by rw [← h1]; exact h2'279  have hsq : Nat.card F ^ 2 - 1 = (Nat.card F + 1) * (Nat.card F - 1) := by280    have := sq_tsub_sq (Nat.card F) 1281    rw [one_pow] at this282    exact this283  rw [hsq] at key284  exact (Nat.eq_of_mul_eq_mul_right (by omega) key).symm285286end Ext287288/-! ## Field-generic lemmas (the `ZMod p` instances under `Fact p.Prime` are not `ring`-friendly) -/289section generic290variable {K : Type*} [Field K]291292theorem inv_square_iff (a : K) : IsSquare a⁻¹ ↔ IsSquare a := by293  constructor294  · rintro ⟨r, hr⟩; exact ⟨r⁻¹, by rw [← mul_inv, ← hr, inv_inv]⟩295  · rintro ⟨r, hr⟩; exact ⟨r⁻¹, by rw [← mul_inv, ← hr]⟩296297theorem neg_two_square_iff {i : K} (hi : -1 = i * i) : IsSquare (-2 : K) ↔ IsSquare (2 : K) := by298  constructor299  · rintro ⟨r, hr⟩; exact ⟨i * r, by linear_combination (r * r) * hi - hr⟩300  · rintro ⟨r, hr⟩; exact ⟨i * r, by linear_combination (r * r) * hi - hr⟩301302theorem three_kappa_pow (g : K) (κ : ℕ) (h : g ^ (2 * κ) = -1) : g ^ (3 * κ) = -g ^ κ := by303  rw [show 3 * κ = 2 * κ + κ by ring, pow_add, h, neg_one_mul]304305theorem sq_eq_one_cases {x : K} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by306  rw [sq] at h; exact mul_self_eq_one_iff.1 h307308theorem neg_inv_of_mul {a c : K} (hc : c ≠ 0) (h : c * a = -1) : a = -c⁻¹ := by309  field_simp; linear_combination h310311theorem three_quarters {a : K} (h4 : (4 : K) ≠ 0) (h : a = -4⁻¹) : 1 + a = 3 * 4⁻¹ := by312  rw [h]; field_simp; ring313314theorem half_neg {a : K} (h2 : (2 : K) ≠ 0) (h : 4 * a = -1) : 2 * a = -2⁻¹ := by315  field_simp; linear_combination h316317theorem four_ne_zero_of_two {K : Type*} [Ring K] (h : (2 : K) ≠ 0) [NoZeroDivisors K] : (4 : K) ≠ 0 := by318  intro h4; apply h319  have : (4 : K) = 2 * 2 := by norm_num320  rw [this] at h4321  rcases mul_eq_zero.1 h4 with h0 | h0 <;> exact h0322323end generic324325/-! ## Chronon parity (8:B5, B3, B4) on `ZMod p` -/326section parity327variable {p : ℕ} [hp : Fact (Nat.Prime p)]328329/-- 8:B3, 8:B4 — on the shell `p = 4κ + 1`: `2` is a square ⟺ `κ` even (the second supplementary law), and330so `2⁻¹ = c²` and `−2` (`−1` a square); the quarter-turn `i = g^{−κ} = g^{3κ}` is a square ⟺ `κ` even. -/331theorem named_residues (κ : ℕ) [hp' : Fact (Nat.Prime (4 * κ + 1))] {g : ZMod (4 * κ + 1)}332    (hg : orderOf g = 4 * κ) :333    (IsSquare (2 : ZMod (4 * κ + 1)) ↔ Even κ) ∧ (IsSquare (2⁻¹ : ZMod (4 * κ + 1)) ↔ Even κ) ∧334    (IsSquare (-2 : ZMod (4 * κ + 1)) ↔ Even κ) ∧ (IsSquare (g ^ (3 * κ)) ↔ Even κ) ∧335    g ^ (3 * κ) = -g ^ κ ∧ IsSquare (-1 : ZMod (4 * κ + 1)) := by336  have hne : 4 * κ + 1 ≠ 2 := by omega337  have h2 : IsSquare (2 : ZMod (4 * κ + 1)) ↔ Even κ := by338    rw [ZMod.exists_sq_eq_two_iff hne, Nat.even_iff]; omega339  have hm1 : IsSquare (-1 : ZMod (4 * κ + 1)) := (ZMod.exists_sq_eq_neg_one_iff (p := 4 * κ + 1)).2 (by omega)340  have h2z : (2 : ZMod (4 * κ + 1)) ≠ 0 := by341    intro h342    have := (ZMod.natCast_eq_zero_iff 2 (4 * κ + 1)).1 (by exact_mod_cast h)343    have := Nat.le_of_dvd (by norm_num) this344    have := hp'.out.two_le345    omega346  have hodd : (4 * κ + 1) % 2 = 1 := by omega347  have hg' : orderOf g = 4 * κ + 1 - 1 := by rw [hg]; rfl348  have hhalf : g ^ (2 * κ) = -1 := by349    have h1 := pow_orderOf_eq_one g350    rw [hg] at h1351    have h2' : (g ^ (2 * κ)) ^ 2 = 1 := by rw [← pow_mul, show 2 * κ * 2 = 4 * κ by ring]; exact h1352    rcases sq_eq_one_cases h2' with h | h353    · exfalso354      have := orderOf_dvd_iff_pow_eq_one.2 h355      rw [hg] at this356      have hκ : 0 < κ := by357        by_contra hk; push_neg at hk358        have : κ = 0 := by omega359        subst this; exact absurd hp'.out (by decide)360      have := Nat.le_of_dvd (by omega) this361      omega362    · exact h363  refine ⟨h2, ?_, ?_, ?_, ?_, hm1⟩364  · exact (inv_square_iff (2 : ZMod (4 * κ + 1))).trans h2365  · obtain ⟨i, hi⟩ := hm1366    exact (neg_two_square_iff hi).trans h2367  · rw [parity_iff hg' hodd, Nat.even_mul]368    constructor369    · rintro (h | h)370      · exact absurd h (by decide)371      · exact h372    · intro h; exact Or.inr h373  · exact three_kappa_pow g κ hhalf374375end parity376377/-! ## The Cayley step preserves any Hermitian pairing (8:C4, D10) -/378section cayley379variable {R : Type*} [Ring R]380381/-- 8:C4, 8:D10, 8:X3 — the exact Hermitian preservation, for any anti-involution `σ` of the operator ring (the382adjoint of a nondegenerate Hermitian form, or the `X`-adjoint of the spinor form): if `σ h = h`, the scalar383`a` is central with `σ a = −a`, and `1 − a h` is a unit, then `u = (1 − a h)⁻¹ (1 + a h)` satisfies384`σ u · u = 1` — the Cayley step is unitary (Theorem `cayley-preservation`). For D10 the premise385`σ h = h` is the `X`-self-adjointness of `𝒟^s − m` (D9's operator clause, decided by the package at386`p = 13, 173` and not proved here). -/387theorem cayley_unitary (σ : R → R) (hmul : ∀ x y, σ (x * y) = σ y * σ x) (hadd : ∀ x y, σ (x + y) = σ x + σ y)388    (hone : σ 1 = 1) (hneg : ∀ x, σ (-x) = -σ x)389    {h a : R} (hh : σ h = h) (ha : σ a = -a) (hc : ∀ x, Commute a x)390    (hu : IsUnit (1 - a * h)) :391    let u := (hu.unit⁻¹ : Rˣ) * (1 + a * h)392    σ (u : R) * u = 1 := by393  intro u394  -- σ(1 − a h) = 1 + a h and σ(1 + a h) = 1 − a h395  have hsub : σ (1 - a * h) = 1 + a * h := by396    rw [sub_eq_add_neg, hadd, hone, hneg, hmul, hh, ha, mul_neg, neg_neg, (hc h).eq]397  have hadd' : σ (1 + a * h) = 1 - a * h := by398    rw [hadd, hone, hmul, hh, ha, mul_neg, (hc h).eq, sub_eq_add_neg]399  -- the inverse commutes with 1 + a h400  have hcomm : Commute (1 - a * h) (1 + a * h) :=401    (Commute.one_left _).sub_left ((Commute.one_right (a * h)).add_right (Commute.refl (a * h)))402  have hinv_comm : Commute ((hu.unit⁻¹ : Rˣ) : R) (1 + a * h) := by403    have hcu : Commute (hu.unit : R) (1 + a * h) := by rw [IsUnit.unit_spec]; exact hcomm404    exact (Commute.units_inv_left_iff).2 hcu405  -- σ of the inverse is the inverse of σ406  have hσinv : σ ((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h) = 1 := by407    have e : (1 - a * h) * ((hu.unit⁻¹ : Rˣ) : R) = 1 := by408      have := hu.unit.mul_inv409      rw [IsUnit.unit_spec] at this410      exact this411    have := congrArg σ e412    rw [hmul, hsub, hone] at this413    exact this414  show σ (((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h)) * (((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h)) = 1415  rw [hmul, hadd']416  -- (1 − a h) · σ(inv) · inv · (1 + a h): use σ(inv)(1 + a h) = 1 and commutation417  calc (1 - a * h) * σ ((hu.unit⁻¹ : Rˣ) : R) * (((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h))418      = (1 - a * h) * σ ((hu.unit⁻¹ : Rˣ) : R) * ((1 + a * h) * ((hu.unit⁻¹ : Rˣ) : R)) := by419        rw [hinv_comm.eq]420    _ = (1 - a * h) * (σ ((hu.unit⁻¹ : Rˣ) : R) * (1 + a * h)) * ((hu.unit⁻¹ : Rˣ) : R) := by421        simp only [mul_assoc]422    _ = (1 - a * h) * ((hu.unit⁻¹ : Rˣ) : R) := by rw [hσinv, mul_one]423    _ = 1 := by424        have := hu.unit.mul_inv425        rw [IsUnit.unit_spec] at this426        exact this427428/-- 8:C15 — every orbit is periodic: a unit of a finite ring has finite order (Corollary429`finite-periodicity`). -/430theorem cayley_periodic {R : Type*} [Ring R] [Finite R] (u : Rˣ) : IsOfFinOrder u := isOfFinOrder_of_finite u431432433/-- 8:F6, 8:F7, 8:X3 — the Cayley step of a nilpotent shift: for `α` and `m` central, `N` nilpotent (the symmetric Dirac operator) and434`1 ± αm` units, the step `U = (1 − α(N − m))⁻¹ (1 + α(N − m))` of `H = N − m` differs from the scalar435`φ(−m) = (1 − αm)(1 + αm)⁻¹` by a nilpotent: `U` is the mass phase times a unipotent, its single eigenvalue the Cayley image436of the mass (Proposition `two-spectra`, Theorem `dirac-evolution`). -/437theorem cayley_nilpotent_shift {α m N : R} (hα : ∀ x, Commute α x) (hm : ∀ x, Commute m x)438    (hN : IsNilpotent N) (ha : IsUnit (1 + α * m)) (hb : IsUnit (1 - α * m)) :439    ∃ hu : IsUnit (1 - α * (N - m)),440      IsNilpotent (((hu.unit⁻¹ : Rˣ) : R) * (1 + α * (N - m)) - ((hb.unit * ha.unit⁻¹ : Rˣ) : R)) := by441  have hαm : ∀ x, Commute (α * m) x := fun x => (hα x).mul_left (hm x)442  have hac : ∀ x, Commute (1 + α * m) x := fun x => (Commute.one_left x).add_left (hαm x)443  have hbc : ∀ x, Commute (1 - α * m) x := fun x => (Commute.one_left x).sub_left (hαm x)444  have hai : ∀ x, Commute ((ha.unit⁻¹ : Rˣ) : R) x := fun x =>445    (Commute.units_inv_left_iff).2 (by rw [IsUnit.unit_spec]; exact hac x)446  have hαN : IsNilpotent (α * N) := (hα N).isNilpotent_mul_left hN447  have hX : IsNilpotent (((ha.unit⁻¹ : Rˣ) : R) * (α * N)) := (hai (α * N)).isNilpotent_mul_left hαN448  have hsplit : 1 - α * (N - m) = (1 + α * m) - α * N := by noncomm_ring449  have hfac : (1 + α * m) - α * N = (ha.unit : R) * (1 - ((ha.unit⁻¹ : Rˣ) : R) * (α * N)) := by450    rw [mul_sub, mul_one, ← mul_assoc, Units.mul_inv, one_mul, IsUnit.unit_spec]451  have hu : IsUnit (1 - α * (N - m)) := by452    rw [hsplit, hfac]; exact ha.unit.isUnit.mul hX.isUnit_one_sub453  refine ⟨hu, ?_⟩454  have huD : ((hu.unit⁻¹ : Rˣ) : R) * (1 - α * (N - m)) = 1 := hu.val_inv_mul455  have hcc : ∀ x, Commute ((hb.unit * ha.unit⁻¹ : Rˣ) : R) x := fun x => by456    rw [Units.val_mul]; exact (hbc x).mul_left (hai x)457  have hac_c : (1 + α * m) * ((hb.unit * ha.unit⁻¹ : Rˣ) : R) = 1 - α * m := by458    rw [Units.val_mul, (hac _).eq, mul_assoc, ha.val_inv_mul, mul_one, IsUnit.unit_spec]459  have key : (1 - α * (N - m)) * (((hu.unit⁻¹ : Rˣ) : R) * (1 + α * (N - m)) - ((hb.unit * ha.unit⁻¹ : Rˣ) : R))460      = α * N * (1 + ((hb.unit * ha.unit⁻¹ : Rˣ) : R)) := by461    rw [mul_sub, ← mul_assoc, hu.mul_val_inv, one_mul, hsplit, sub_mul, hac_c]462    noncomm_ring463  have hnil : IsNilpotent (α * N * (1 + ((hb.unit * ha.unit⁻¹ : Rˣ) : R))) :=464    (((Commute.one_right _).add_right (hcc _).symm)).isNilpotent_mul_right hαN465  have hcomm : Commute ((hu.unit⁻¹ : Rˣ) : R) (α * N * (1 + ((hb.unit * ha.unit⁻¹ : Rˣ) : R))) := by466    refine (Commute.units_inv_left_iff).2 ?_467    rw [IsUnit.unit_spec, hsplit]468    have h1 : Commute (α * N) (α * N * (1 + ((hb.unit * ha.unit⁻¹ : Rˣ) : R))) :=469      (Commute.refl _).mul_right ((Commute.one_right _).add_right (hcc _).symm)470    exact (hac _).sub_left h1471  have : ((hu.unit⁻¹ : Rˣ) : R) * (1 + α * (N - m)) - ((hb.unit * ha.unit⁻¹ : Rˣ) : R)472      = ((hu.unit⁻¹ : Rˣ) : R) * (α * N * (1 + ((hb.unit * ha.unit⁻¹ : Rˣ) : R))) := by473    rw [← key, ← mul_assoc, huD, one_mul]474  rw [this]475  exact hcomm.isNilpotent_mul_left hnil476477end cayley478479/-! ## Kinetic Hamiltonians: nilpotent, fully admissible, of period `p` (8:C6, E4) -/480section kinetic481variable {R : Type*} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p]482483/-- 8:E4 (1), 8:E7, 8:F7, 8:C6, 8:D10, 8:X3 — the translation `t` of order `p` (`t^p = 1`) has `(t − 1)^p = 0` in484characteristic `p`: the kinetic Hamiltonians and the symmetric differences are nilpotent (Theorem485`period-dichotomy` (1), Corollary `kinetic-admissible`). -/486theorem translation_nilpotent {t : R} (ht : t ^ p = 1) : (t - 1) ^ p = 0 := by487  rw [sub_pow_char_of_commute p (Commute.one_right t), ht, one_pow, sub_self]488489/-- 8:E4 (1), 8:E7, 8:C6 — `h = c (t + t^{p−1} − 2) = c t^{p−1} (t − 1)²` and with it `a h` for any `a` commuting with490`t` and `c` is nilpotent, `(a h)^p = 0`, so `1 − a h` is a unit: the Cayley step is defined for every `a` —491`𝒜(H) = K⁻` (Corollary `kinetic-admissible`; `H = −Δ` at `c = −1`). -/492theorem kinetic_nilpotent {t c a : R} (ht : t ^ p = 1) (hct : Commute c t) (hat : Commute a t)493    (hac : Commute a c) :494    let h := c * (t + t ^ (p - 1) - 2)495    (a * h) ^ p = 0 ∧ IsNilpotent (a * h) ∧ IsUnit (1 - a * h) := by496  intro h497  have hp1 : (p - 1) + 1 = p := Nat.sub_add_cancel hp.out.one_le498  -- h = c t^{p−1} (t − 1)²499  have hfac : h = c * t ^ (p - 1) * (t - 1) ^ 2 := by500    show c * (t + t ^ (p - 1) - 2) = c * t ^ (p - 1) * (t - 1) ^ 2501    have e : t ^ (p - 1) * (t - 1) ^ 2 = t + t ^ (p - 1) - 2 := by502      have : t ^ (p - 1) * t = 1 := by rw [← pow_succ, hp1, ht]503      have h2 : t ^ (p - 1) * t ^ 2 = t := by rw [pow_two, ← mul_assoc, this, one_mul]504      calc t ^ (p - 1) * (t - 1) ^ 2 = t ^ (p - 1) * t ^ 2 - 2 * (t ^ (p - 1) * t) + t ^ (p - 1) := by505            noncomm_ring506        _ = t + t ^ (p - 1) - 2 := by rw [h2, this, mul_one]; noncomm_ring507    rw [mul_assoc, e]508  have hcomm : Commute a (c * t ^ (p - 1) * (t - 1) ^ 2) :=509    (hac.mul_right (hat.pow_right _)).mul_right ((hat.sub_right (Commute.one_right a)).pow_right 2)510  have hcomm2 : Commute (a * (c * t ^ (p - 1))) ((t - 1) ^ 2) := by511    have h1 : Commute a ((t - 1) ^ 2) := (hat.sub_right (Commute.one_right a)).pow_right 2512    have h2 : Commute (c * t ^ (p - 1)) ((t - 1) ^ 2) :=513      ((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)514    exact h1.mul_left h2515  have key : (a * h) ^ p = 0 := by516    rw [hfac, ← mul_assoc, hcomm2.mul_pow, ← pow_mul, show 2 * p = p + p by ring, pow_add,517      translation_nilpotent ht, mul_zero, mul_zero]518  refine ⟨key, ⟨p, key⟩, IsNilpotent.isUnit_one_sub ⟨p, key⟩⟩519520/-- 8:E4 (1), 8:C6 — the period: for a nilpotent `n` with `n^p = 0` and `2` a unit, the Cayley step521`u = (1 − n)⁻¹(1 + n)` is unipotent — `u − 1 = 2(1 − n)⁻¹ n`, `(u − 1)^p = 0`, `u^p = 1` — and `u ≠ 1` when522`n ≠ 0`, so in the prime characteristic `ord(U) = p` exactly (Theorem `period-dichotomy` (1); on `𝔽₁₃`,523`ord(U_{kw, −Δ}) = 13` for every `k ≠ 0`, Example `cayley-13`). -/524theorem cayley_period {n : R} (hn : n ^ p = 0) (h2 : IsUnit (2 : R)) (hn0 : n ≠ 0) :525    let hu : IsUnit (1 - n) := IsNilpotent.isUnit_one_sub ⟨p, hn⟩526    let hu' : IsUnit (1 + n) := by527      rw [← sub_neg_eq_add]; exact IsNilpotent.isUnit_one_sub ⟨p, by rw [neg_pow, hn, mul_zero]⟩528    let u : Rˣ := hu.unit⁻¹ * hu'.unit529    (u : R) = ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) ∧ u ^ p = 1 ∧ u ≠ 1 ∧ orderOf u = p := by530  intro hu hu' u531  have hval : (u : R) = ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) := by532    show ((hu.unit⁻¹ : Rˣ) : R) * (hu'.unit : R) = _533    rw [IsUnit.unit_spec]534  have hv : ((hu.unit⁻¹ : Rˣ) : R) * (1 - n) = 1 := by535    have := hu.unit.inv_mul; rwa [IsUnit.unit_spec] at this536  have hvn : Commute ((hu.unit⁻¹ : Rˣ) : R) n := by537    have : Commute (hu.unit : R) n := by538      rw [IsUnit.unit_spec]; exact (Commute.one_left n).sub_left (Commute.refl n)539    exact (Commute.units_inv_left_iff).2 this540  have hu1 : (u : R) - 1 = 2 * (((hu.unit⁻¹ : Rˣ) : R) * n) := by541    rw [hval]542    calc ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) - 1543        = ((hu.unit⁻¹ : Rˣ) : R) * (1 + n) - ((hu.unit⁻¹ : Rˣ) : R) * (1 - n) := by rw [hv]544      _ = 2 * (((hu.unit⁻¹ : Rˣ) : R) * n) := by noncomm_ring545  have hpow : ((u : R) - 1) ^ p = 0 := by546    rw [hu1, (Commute.ofNat_left 2 _).mul_pow, hvn.mul_pow, hn, mul_zero, mul_zero]547  have hup : u ^ p = 1 := by548    apply Units.ext549    rw [Units.val_pow_eq_pow_val, Units.val_one]550    have : (u : R) = ((u : R) - 1) + 1 := (sub_add_cancel _ _).symm551    rw [this, add_pow_char_of_commute p (Commute.one_right _), hpow, one_pow, zero_add]552  have hne : u ≠ 1 := by553    intro h554    have : (u : R) - 1 = 0 := by rw [h, Units.val_one, sub_self]555    rw [hu1] at this556    have := (h2.mul_right_eq_zero).1 this557    have := ((Units.isUnit (hu.unit⁻¹)).mul_right_eq_zero).1 this558    exact hn0 this559  exact ⟨hval, hup, hne, orderOf_eq_prime hup hne⟩560561end kinetic562563/-! ## The Hermitian form on a finite configuration space (8:C2) -/564section hermitian565variable {K : Type*} [CommRing K] [StarRing K] {X : Type*} [Fintype X]566567/-- `⟨ψ, φ⟩_X = Σ_x ψ(x)* φ(x)` (Definition `hermitian-form`). -/568def herm (ψ φ : X → K) : K := ∑ x, star (ψ x) * φ x569570/-- 8:C2 — Hermitian symmetry `⟨ψ, φ⟩* = ⟨φ, ψ⟩`; linearity in the second slot, conjugate-linearity in the first. -/571theorem herm_star (ψ φ : X → K) : star (herm ψ φ) = herm φ ψ := by572  simp [herm, star_sum, star_mul, mul_comm]573574theorem herm_add_right (ψ φ φ' : X → K) : herm ψ (φ + φ') = herm ψ φ + herm ψ φ' := by575  simp [herm, mul_add, Finset.sum_add_distrib]576577theorem herm_sub_right (ψ φ φ' : X → K) : herm ψ (φ - φ') = herm ψ φ - herm ψ φ' := by578  simp [herm, mul_sub, Finset.sum_sub_distrib]579580theorem herm_smul_right (ψ φ : X → K) (c : K) : herm ψ (c • φ) = c * herm ψ φ := by581  simp [herm, Finset.mul_sum, mul_left_comm]582583theorem herm_add_left (ψ ψ' φ : X → K) : herm (ψ + ψ') φ = herm ψ φ + herm ψ' φ := by584  simp [herm, add_mul, Finset.sum_add_distrib]585586theorem herm_sub_left (ψ ψ' φ : X → K) : herm (ψ - ψ') φ = herm ψ φ - herm ψ' φ := by587  simp [herm, sub_mul, Finset.sum_sub_distrib]588589theorem herm_smul_left (ψ φ : X → K) (c : K) : herm (c • ψ) φ = star c * herm ψ φ := by590  simp [herm, Finset.mul_sum, mul_assoc]591592/-- 8:C2 — nondegeneracy: `⟨ψ, φ⟩ = 0` for every `φ` forces `ψ = 0` (Lemma `hermitian-nondeg`; the test593function is the point mass at `x₀`). -/594theorem herm_nondegenerate [DecidableEq X] (ψ : X → K) (h : ∀ φ, herm ψ φ = 0) : ψ = 0 := by595  funext x₀596  have := h (Pi.single x₀ 1)597  simp [herm, Pi.single_apply] at this598  have h2 := congrArg star this599  simpa using h2600601/-- The translation `(T_u ψ)(x) = ψ(x + u)` on an additive group. -/602def translate {G : Type*} [AddGroup G] (u : G) (ψ : G → K) : G → K := fun x => ψ (x + u)603604/-- 8:C8 — every translation is unitary for the form, and `T_u† = T_{−u}` (Proposition605`translation-unitary`). -/606theorem herm_translate {G : Type*} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K) :607    herm (translate u ψ) (translate u φ) = herm ψ φ := by608  unfold herm translate609  exact Fintype.sum_equiv (Equiv.addRight u) _ _ (fun x => rfl)610611/-- 8:C8 — the adjoint of a translation is the opposite translation, `T_u† = T_{−u}` (Proposition612`translation-unitary`). -/613theorem herm_translate_adjoint {G : Type*} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K) :614    herm (translate u ψ) φ = herm ψ (translate (-u) φ) := by615  unfold herm translate616  refine (Fintype.sum_equiv (Equiv.addRight u) _ _ (fun x => ?_))617  simp618619/-- The pullback of a function along an additive automorphism `A` of the frame, `(A_* ψ)(x) = ψ(A⁻¹ x)`. -/620def pullback {G : Type*} [AddGroup G] (A : G ≃+ G) (ψ : G → K) : G → K := fun x => ψ (A.symm x)621622omit [CommRing K] [StarRing K] in623/-- 8:C13, 8:D7 — the pullback intertwines the translation by `e` with the translation by `A e`, `T_{Ae} A_* = A_* T_e`:624`ψ(A⁻¹(x + Ae)) = ψ(A⁻¹x + e)` (Lemma `frame-covariance`; with `A = Λ` the boost, componentwise on the spinor, Lemma625`difference-pullback`). -/626theorem translate_pullback {G : Type*} [AddGroup G] (A : G ≃+ G) (e : G) (ψ : G → K) :627    translate (A e) (pullback A ψ) = pullback A (translate e ψ) := by628  funext x629  show ψ (A.symm (x + A e)) = ψ (A.symm x + e)630  rw [map_add, AddEquiv.symm_apply_apply]631632/-- The finite Laplacian along one direction, `Δ = T_e + T_{−e} − 2`, and the Hamiltonian633`H = −ϰ Δ + M_V` (`(M_V ψ)(x) = V(x) ψ(x)`). -/634def laplacian {G : Type*} [AddGroup G] (e : G) (ψ : G → K) : G → K :=635  translate e ψ + translate (-e) ψ - (2 : K) • ψ636637def hamiltonian {G : Type*} [AddGroup G] (e : G) (ϰ : K) (V : G → K) (ψ : G → K) : G → K :=638  (-ϰ) • laplacian e ψ + fun x => V x * ψ x639640/-- 8:C9 — the Laplacian along one direction is self-adjoint, `⟨Δψ, φ⟩ = ⟨ψ, Δφ⟩` (Proposition641`laplacian-sa`; the `d`-dimensional Laplacian is the sum over the directions), and with it every Hamiltonian642`−ϰΔ + M_V` with `ϰ` and `V` Frobenius-fixed (Corollary `hamiltonian-sa`). -/643theorem herm_laplacian {G : Type*} [AddGroup G] [Fintype G] (e : G) (ψ φ : G → K) :644    herm (laplacian e ψ) φ = herm ψ (laplacian e φ) := by645  unfold laplacian646  rw [herm_sub_left, herm_add_left, herm_smul_left, herm_sub_right, herm_add_right, herm_smul_right,647    herm_translate_adjoint, herm_translate_adjoint (-e), neg_neg, star_ofNat, add_comm (herm ψ (translate (-e) φ))]648649omit [StarRing K] in650/-- 8:C13, 8:D7 — frame covariance: the pullback along an additive automorphism `A` intertwines the translations and the651Laplacians of the two frames, `T_{Ae} A_* = A_* T_e` and `Δ_{Ae} A_* = A_* Δ_e` (Lemma `frame-covariance`; the differences652`T_e − 1` follow by linearity, and with `A = Λ` the boost, componentwise on the spinor, Lemma `difference-pullback`). -/653theorem translate_covariance {G : Type*} [AddGroup G] (A : G ≃+ G) (e : G) (ψ : G → K) :654    translate (A e) (pullback A ψ) = pullback A (translate e ψ) ∧655    laplacian (A e) (pullback A ψ) = pullback A (laplacian e ψ) := by656  refine ⟨translate_pullback A e ψ, ?_⟩657  funext x658  show translate (A e) (pullback A ψ) x + translate (-(A e)) (pullback A ψ) x - (2 : K) * pullback A ψ x659      = translate e ψ (A.symm x) + translate (-e) ψ (A.symm x) - (2 : K) * ψ (A.symm x)660  rw [translate_pullback, ← map_neg, translate_pullback]661  rfl662663/-- 8:C11 — every Hamiltonian `−ϰΔ + M_V` with `ϰ` and `V` Frobenius-fixed is self-adjoint (Corollary664`hamiltonian-sa`). -/665theorem herm_hamiltonian {G : Type*} [AddGroup G] [Fintype G] (e : G) (ϰ : K) (hϰ : star ϰ = ϰ)666    (V : G → K) (hV : ∀ x, star (V x) = V x) (ψ φ : G → K) :667    herm (hamiltonian e ϰ V ψ) φ = herm ψ (hamiltonian e ϰ V φ) := by668  unfold hamiltonian669  rw [herm_add_left, herm_smul_left, herm_laplacian, herm_add_right, herm_smul_right, star_neg, hϰ]670  congr 1671  unfold herm672  refine Finset.sum_congr rfl (fun x _ => ?_)673  rw [star_mul, hV]; ring674675end hermitian676677678/-! ## The free evolution is the drive: the characters, the spectrum and the isotropy (8:F3, F4) -/679section drive680variable {p : ℕ} [hp : Fact (Nat.Prime p)]681682/-- The drive pullback on functions of the phase cycle `Φ = (ZMod p)ˣ`: `(Dψ)(x) = ψ(g⁻¹ x)`. -/683def drive (g : (ZMod p)ˣ) (ψ : (ZMod p)ˣ → ZMod p) : (ZMod p)ˣ → ZMod p := fun x => ψ (g⁻¹ * x)684685/-- The multiplicative characters `χ_k(x) = x^k` (the winding-`k` modes). -/686def chi (k : ℕ) : (ZMod p)ˣ → ZMod p := fun x => (x : ZMod p) ^ k687688/-- 8:F3 (2), 8:F6 — the characters are eigenvectors of the drive with eigenvalue `g^{−k}`: the winding-`k` mode689acquires the phase `g^{−k}` per chronon (Theorem `zonal`). -/690theorem drive_chi (g : (ZMod p)ˣ) (k : ℕ) : drive g (chi k) = fun x => ((g⁻¹ : (ZMod p)ˣ) : ZMod p) ^ k * chi k x := by691  funext x692  simp only [drive, chi, Units.val_mul, mul_pow]693694/-- 8:F3 (1) — the drive is a permutation of the cycle: it preserves the sum defining the form (unitary). -/695theorem drive_sum (g : (ZMod p)ˣ) (f : (ZMod p)ˣ → ZMod p) : ∑ x, f (g⁻¹ * x) = ∑ x, f x :=696  Fintype.sum_equiv (Equiv.mulLeft g⁻¹) _ _ (fun _ => rfl)697698/-- 8:F3 (3) — isotropy: the character values are Frobenius-fixed, so `⟨χ_k, χ_k⟩ = Σ_x x^{2k}`, which is699`0` unless `(p − 1) ∣ 2k` and `−1` otherwise (Mathlib's `FiniteField.sum_pow_units`): every character line is700isotropic except `k = 0` and `k = (p − 1)/2`. -/701theorem chi_isotropy (k : ℕ) :702    (∑ x : (ZMod p)ˣ, chi k x * chi k x) = if p - 1 ∣ 2 * k then -1 else 0 := by703  rw [show (∑ x : (ZMod p)ˣ, chi k x * chi k x) = ∑ x : (ZMod p)ˣ, (x : ZMod p) ^ (2 * k) from704    Finset.sum_congr rfl (fun x _ => by rw [chi, ← mul_pow, ← sq, ← pow_mul])]705  have := FiniteField.sum_pow_units (K := ZMod p) (2 * k)706  rwa [ZMod.card] at this707708/-- 8:F3 (3), 8:F4 — the exceptional eigenvalues are `±1`: on the shell `p = 4κ + 1` with `g` of order `4κ`,709`k = 2κ` gives `g^{−2κ} = −1` (and `k = 0` gives `1`); and these are all of `N¹ ∩ 𝔽_p`: a base-field element710of norm one (`u ū = u² = 1`) is `±1` (Corollary `sectors`). -/711theorem exceptional_eigen (κ : ℕ) [Fact (Nat.Prime (4 * κ + 1))] (g : (ZMod (4 * κ + 1))ˣ)712    (hg : orderOf g = 4 * κ) :713    ((g⁻¹ : (ZMod (4 * κ + 1))ˣ) : ZMod (4 * κ + 1)) ^ (2 * κ) = -1 ∧714    ∀ u : ZMod (4 * κ + 1), u * u = 1 → u = 1 ∨ u = -1 := by715  refine ⟨?_, fun u hu => mul_self_eq_one_iff.1 hu⟩716  have h4 : g ^ (4 * κ) = 1 := by have := pow_orderOf_eq_one g; rwa [hg] at this717  have h2 : (g ^ (2 * κ)) ^ 2 = 1 := by rw [← pow_mul, show 2 * κ * 2 = 4 * κ by ring, h4]718  have hne : g ^ (2 * κ) ≠ 1 := by719    intro h720    have := orderOf_dvd_iff_pow_eq_one.2 h721    rw [hg] at this722    have hκ : 0 < κ := by723      rcases Nat.eq_zero_or_pos κ with h0 | h0724      · subst h0; exact absurd (Fact.out : Nat.Prime (4 * 0 + 1)) (by decide)725      · exact h0726    have := Nat.le_of_dvd (by omega) this727    omega728  have hval : ((g ^ (2 * κ) : (ZMod (4 * κ + 1))ˣ) : ZMod (4 * κ + 1)) = -1 := by729    have h2' : (((g ^ (2 * κ) : (ZMod (4 * κ + 1))ˣ) : ZMod (4 * κ + 1))) ^ 2 = 1 := by730      rw [← Units.val_pow_eq_pow_val, h2, Units.val_one]731    rw [sq] at h2'732    rcases mul_self_eq_one_iff.1 h2' with h | h733    · exact absurd (Units.ext h) hne734    · exact h735  rw [← Units.val_pow_eq_pow_val, inv_pow, ← hval]736  have : (g ^ (2 * κ))⁻¹ = g ^ (2 * κ) := by737    rw [inv_eq_iff_mul_eq_one, ← sq, h2]738  rw [this]739740/-- 8:F4, 8:F6, 8:X1 — the sector separation: `ord(g⁻¹) = ord(g) = p − 1`, the drive's phases run on the split cycle741`μ_{p−1}`, while the norm-one torus has order `p + 1`; and there are no meridional plane waves: no742`K`-valued character of the translation cycle `C_p`, since `p ∤ p² − 1` — no unit of `K` has order `p`743(`gcd(p, |Kˣ|) = 1`). -/744theorem sector_separation {K : Type*} [Field K] [Finite K] (hK : Nat.card K = p ^ 2)745    (g : (ZMod p)ˣ) (hg : orderOf g = p - 1) :746    orderOf g⁻¹ = p - 1 ∧ ∀ x : Kˣ, orderOf x ≠ p := by747  refine ⟨by rw [orderOf_inv, hg], fun x hx => ?_⟩748  have hd := orderOf_dvd_natCard x749  rw [Nat.card_units, hK, hx] at hd750  have hp2 : p ∣ p ^ 2 := dvd_pow_self p two_ne_zero751  have h1 : p ∣ 1 := by752    have := Nat.dvd_sub hp2 hd753    have hle : 1 ≤ p ^ 2 := Nat.one_le_pow _ _ hp.out.pos754    rwa [Nat.sub_sub_self hle] at this755  exact hp.out.one_lt.ne' (Nat.dvd_one.1 h1)756757/-- The dispersion identity in any commutative ring. -/758theorem dispersion_generic {R : Type*} [CommRing R] (a b c : R) (k : ℕ) :759    -((a * c) ^ k + (b * c) ^ k - 2 * c ^ k) = (2 - b ^ k - a ^ k) * c ^ k := by ring760761/-- 8:F7 — the dispersion relation on the cycle: `−Δ_Φ χ_k = (2 − g^k − g^{−k}) χ_k` with762`Δ_Φ = D + D⁻¹ − 2` (the finite band curve). -/763theorem dispersion (g : (ZMod p)ˣ) (k : ℕ) :764    (fun x => -(drive g (chi k) x + drive g⁻¹ (chi k) x - 2 * chi k x)) =765      fun x => (2 - ((g : ZMod p)) ^ k - ((g⁻¹ : (ZMod p)ˣ) : ZMod p) ^ k) * chi k x := by766  funext x767  simp only [drive, chi, inv_inv, Units.val_mul]768  exact dispersion_generic _ _ _ k769770end drive771772/-! ## Reversibility and the information counts (8:E2, E3) -/773section counts774variable {X : Type*} [Fintype X] [DecidableEq X]775776/-- 8:E2 — a self-map of a finite set is bijective exactly when its image count is the whole count (loss777factor `1`): `|f(X)| = |X| ⟺ f bijective` (Proposition `loss-factor-one`). -/778theorem loss_factor_one (f : X → X) : (Finset.univ.image f).card = Fintype.card X ↔ Function.Bijective f := by779  rw [← Finset.card_univ, Finset.card_image_iff, Finset.coe_univ, Set.injOn_univ]780  exact Finite.injective_iff_bijective781782/-- 8:E3, 8:E6 — an invertible map has loss factor one: left multiplication by a unit is a bijection (the Cayley783propagators and the boost transports). -/784theorem unit_loss_factor_one {R : Type*} [Monoid R] (u : Rˣ) : Function.Bijective (fun x : R => (u : R) * x) :=785  (Units.mulLeft u).bijective786787variable {p : ℕ} [hp : Fact (Nat.Prime p)]788789/-- 8:E5 — the power-map count on the phase cycle: `x ↦ x^ε` on `(ZMod p)ˣ` has image of size790`(p − 1)/gcd(ε, p − 1)`, and its kernel — the fibre over `1`, of which every nonempty fibre is a coset —791has `gcd(ε, p − 1)` elements (Proposition `power-map-count`, on the cyclic group of order `p − 1`). -/792theorem power_map_count (ε : ℕ) :793    Nat.card ((powMonoidHom ε : (ZMod p)ˣ →* (ZMod p)ˣ).ker) = Nat.gcd (p - 1) ε ∧794    Nat.card ((powMonoidHom ε : (ZMod p)ˣ →* (ZMod p)ˣ).range) = (p - 1) / Nat.gcd (p - 1) ε := by795  have hc : Nat.card (ZMod p)ˣ = p - 1 := by rw [Nat.card_eq_fintype_card, ZMod.card_units]796  refine ⟨?_, ?_⟩797  · rw [IsCyclic.card_powMonoidHom_ker, hc]798  · rw [IsCyclic.card_powMonoidHom_range, hc]799800end counts801802803/-! ## The torus as a cyclic group of order `p + 1`: the potential periods and the triality clause (8:D5, E4) -/804namespace Ext805variable {F : Type*} [Field F] {ν : F}806807/-- 8:D5 — the range of the boost is exactly `N¹` (Lemma `boost-torus`: `G_ν ≅ K^×/F^× ≅ N¹`). -/808theorem boost_range (hν : ¬ IsSquare ν) :809    (boost (F := F) (ν := ν)).range = normOneGroup F ν := by810  ext u811  constructor812  · rintro ⟨z, rfl⟩; exact boost_mem z813  · intro hu; exact exists_boost_eq hν hu814815/-- 8:D5, 8:C5 — `N¹` is cyclic (a finite subgroup of the units of a field), of order `p + 1` on `F = 𝔽_p`:816`N¹ ≅ C_{p+1}`. -/817theorem normOne_cyclic [Finite F] (hν : ¬ IsSquare ν) :818    letI := field hν; IsCyclic (normOneGroup F ν) := by819  letI := field hν820  infer_instance821822/-- 8:E4 (2) — every phase on the torus has `u^{p+1} = 1`: a potential propagator, diagonal with entries in823`N¹`, has order dividing `p + 1`; and some phase has order exactly `p + 1` (the torus is cyclic), so the bound824is attained (Theorem `period-dichotomy` (2)). -/825theorem torus_period [Finite F] (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) :826    (∀ u : normOneGroup F ν, u ^ (Nat.card F + 1) = 1) ∧ ∃ u : normOneGroup F ν, orderOf u = Nat.card F + 1 := by827  letI := field hν828  have hc := card_normOneGroup hν h2829  refine ⟨fun u => by rw [← hc]; exact pow_card_eq_one', ?_⟩830  obtain ⟨u, hu⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := normOneGroup F ν)831  exact ⟨u, by rw [hu, hc]⟩832833/-- 8:D5 — the triality clause: the torus carries an element of order three exactly when `3 ∣ p + 1`834(Cauchy in the cyclic group `C_{p+1}`; `|G_2| = 174` at `173`, `|G_2| = 14` at `13`). -/835theorem order_three_iff [Finite F] (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) :836    (∃ u : normOneGroup F ν, orderOf u = 3) ↔ 3 ∣ Nat.card F + 1 := by837  have hc := card_normOneGroup hν h2838  constructor839  · rintro ⟨u, hu⟩840    rw [← hc, ← hu]; exact orderOf_dvd_natCard u841  · intro h842    rw [← hc] at h843    exact exists_prime_orderOf_dvd_card' 3 h844845end Ext846847/-! ## The Cayley transform: injective, norm-one valued, inverted by the orientation gauge (8:C5) -/848namespace Ext849variable {F : Type*} [Field F] {ν : F}850851/-- 8:C5, 8:F6 — `φ_α(λ) = (1 + αλ)/(1 − αλ)`, `α = kw ≠ 0`, is injective on `F` (a nonconstant Möbius map): the852self-adjoint line embeds in the torus (Theorem `cayley-transform`). -/853theorem cayley_injective (hν : ¬ IsSquare ν) (h2 : (2 : F) ≠ 0) {k : F} (hk : k ≠ 0) :854    Function.Injective (cayley (ν := ν) k) := by855  letI := field hν856  intro s t hst857  unfold cayley at hst858  have hs := one_sub_nu_sq_ne_zero hν (k * s)859  have ht := one_sub_nu_sq_ne_zero hν (k * t)860  have hs' : (1 : Ext F ν) - ofBase (k * s) * w ≠ 0 := fun h => hs (by rw [← norm_one_sub_kw, h]; simp [Ext.norm])861  have ht' : (1 : Ext F ν) - ofBase (k * t) * w ≠ 0 := fun h => ht (by rw [← norm_one_sub_kw, h]; simp [Ext.norm])862  rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff hs' ht'] at hst863  -- (1 + αs)(1 − αt) = (1 + αt)(1 − αs) ⇒ 2α(s − t) = 0864  have him := congrArg im hst865  simp at him866  have : (2 : F) * (k * (s - t)) = 0 := by linear_combination him867  rcases mul_eq_zero.1 this with h | h868  · exact absurd h h2869  · rcases mul_eq_zero.1 h with h | h870    · exact absurd h hk871    · exact sub_eq_zero.1 h872873/-- 8:C16 — the orientation gauge `α ↦ −α` inverts every value: `φ_{−α}(λ) · φ_α(λ) = 1` (Remark874`forward-step`: the forward step imports the derived orientation of the shell). -/875theorem cayley_gauge (hν : ¬ IsSquare ν) (k t : F) :876    (cayley (ν := ν) (-k) t) * cayley k t = 1 := by877  letI := field hν878  unfold cayley879  have h1 := one_sub_nu_sq_ne_zero hν (k * t)880  have hs' : (1 : Ext F ν) - ofBase (k * t) * w ≠ 0 := fun h => h1 (by rw [← norm_one_sub_kw, h]; simp [Ext.norm])881  have ha' : (1 : Ext F ν) + ofBase (k * t) * w ≠ 0 := fun h => h1 (by rw [← norm_one_add_kw, h]; simp [Ext.norm])882  have e1 : (1 : Ext F ν) + ofBase (-k * t) * w = 1 - ofBase (k * t) * w := by ext <;> simp883  have e2 : (1 : Ext F ν) - ofBase (-k * t) * w = 1 + ofBase (k * t) * w := by ext <;> simp884  rw [e1, e2, ← div_eq_mul_inv, ← div_eq_mul_inv, div_mul_div_comm,885    mul_comm ((1 : Ext F ν) - ofBase (k * t) * w) (1 + ofBase (k * t) * w), div_self (mul_ne_zero ha' hs')]886887end Ext888889/-! ## The class is the datum, and the extension erases it (8:B2, B7) -/890section classes891variable {p : ℕ} [hp : Fact (Nat.Prime p)]892893/-- 8:B2 — two nonsquares differ by a square factor: `F^×/(F^×)²` has order two (Lemma `class-datum`); the894Lorentzian form then depends on `ν` only through its class, `−(m²ν) x₀² = −ν (m x₀)²`. -/895theorem class_datum {a b : ZMod p} (ha0 : a ≠ 0) (hb0 : b ≠ 0) (ha : ¬ IsSquare a) (hb : ¬ IsSquare b) :896    IsSquare (a * b) := by897  have h := quadraticChar_one_iff_isSquare (F := ZMod p) (mul_ne_zero ha0 hb0)898  rw [← h, map_mul, (quadraticChar_neg_one_iff_not_isSquare (F := ZMod p)).2 ha,899    (quadraticChar_neg_one_iff_not_isSquare (F := ZMod p)).2 hb]900  norm_num901902/-- 8:B2 — the rescaling `x₀ ↦ m x₀` identifies the forms of `ν` and `m²ν`: a ring identity, the content of903the clause "the form depends on `ν` only through its class". -/904theorem form_class {K : Type*} [CommRing K] (ν m x₀ x₁ x₂ x₃ : K) :905    -(m ^ 2 * ν) * x₀ ^ 2 + x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 = -ν * (m * x₀) ^ 2 + x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 := by ring906907/-- 8:B7 — over the quadratic extension every element of `F_p` is a square: a nonsquare `a = m² ν` becomes908`(m w)²`, so the Euclidean–Lorentzian dichotomy collapses in `K` (Remark `signature-record`). -/909theorem ext_square (hν : ¬ IsSquare (ν : ZMod p)) (a : ZMod p) : IsSquare (Ext.ofBase a : Ext (ZMod p) ν) := by910  by_cases ha : IsSquare a911  · obtain ⟨r, hr⟩ := ha912    exact ⟨Ext.ofBase r, by rw [hr, Ext.ofBase_mul]⟩913  · by_cases ha0 : a = 0914    · exact ⟨0, by rw [ha0, mul_zero]; exact Ext.ofBase_zero⟩915    · have hν0 : ν ≠ 0 := fun h => hν ⟨0, by rw [h]; ring⟩916      obtain ⟨m, hm⟩ := class_datum ha0 hν0 ha hν917      -- a ν = m², so a = (m/ν)² ν = (m/ν · w)²918      refine ⟨Ext.ofBase (m / ν) * Ext.w, ?_⟩919      ext920      · simp; field_simp; linear_combination hm921      · simp922923end classes924925/-! ## The factorisation of the coefficient and the norm growth (8:B4, B6) -/926section factorisation927variable {K : Type*} [Field K]928929/-- 8:B4, 8:X2 — the temporal coefficient factors identically, `ν = g = 2⁻¹ · (2g)`, on every shell (Corollary930`coefficient-factors`; the classes of the two factors: `named_residues`, `two_g_class`); the one-way coefficient is the931odd step `g`, the two-way constant the Carrier's. -/932theorem nu_factorisation (g : K) (h2 : (2 : K) ≠ 0) : (2 : K)⁻¹ * (2 * g) = g := by933  field_simp934935/-- 8:B6 — norm growth: `N(gz) = g² N(z)` (Theorem `even-transport`; `g²` is even by `parity_iff`). -/936theorem norm_growth {ν : K} (g : K) (z : FRC.Extension.Ext K ν) :937    Ext.norm (Ext.ofBase g * z) = g ^ 2 * Ext.norm z :=938  Ext.norm_ofBase_mul g z939940end factorisation941942section twog943variable {p : ℕ} [hp : Fact (Nat.Prime p)]944945/-- 8:B4 — the cofactor's class: for a primitive root `g` (a nonsquare), `2g` is a square exactly when `2` is946not, i.e. exactly when `κ` is odd on the shell `p = 4κ + 1` (`named_residues`): the product `ν = g` is odd947always, `2⁻¹` even exactly on the κ-even shells. -/948theorem two_g_class {g : ZMod p} (hg0 : g ≠ 0) (hg : ¬ IsSquare g) (h2 : (2 : ZMod p) ≠ 0) :949    IsSquare (2 * g) ↔ ¬ IsSquare (2 : ZMod p) := by950  have h := quadraticChar_one_iff_isSquare (F := ZMod p) (mul_ne_zero h2 hg0)951  rw [← h, map_mul, (quadraticChar_neg_one_iff_not_isSquare (F := ZMod p)).2 hg, mul_neg_one, neg_eq_iff_eq_neg,952    quadraticChar_neg_one_iff_not_isSquare]953954end twog955956/-! ## The latitude identities (8:F2) -/957section latitude958959/-- 8:F2 — on the shell `p = 4κ + 1`: `4κ = −1`, so `κ = −4⁻¹`, the energy radius `1 + κ = 3·4⁻¹`,960`π = 2κ = −2⁻¹`; `g^κ = −i` for `i = g^{−κ} = g^{3κ}` (`−1 = g^{2κ}`); and `κ + 1`, the first rung past the961midpoint of the ladder `1, …, 2κ`, is still a rung. -/962theorem latitude_identities (κ : ℕ) [hp : Fact (Nat.Prime (4 * κ + 1))] {g : ZMod (4 * κ + 1)}963    (hg : orderOf g = 4 * κ) :964    (4 * κ : ZMod (4 * κ + 1)) = -1 ∧ (κ : ZMod (4 * κ + 1)) = -4⁻¹ ∧965    (1 + κ : ZMod (4 * κ + 1)) = 3 * 4⁻¹ ∧ (2 * κ : ZMod (4 * κ + 1)) = -2⁻¹ ∧966    g ^ κ = -g ^ (3 * κ) ∧ κ + 1 ≤ 2 * κ := by967  have h4 : (4 * κ : ZMod (4 * κ + 1)) = -1 := by968    have := ZMod.natCast_self (4 * κ + 1)969    push_cast at this970    exact eq_neg_of_add_eq_zero_left this971  have hκ0 : 0 < κ := by972    rcases Nat.eq_zero_or_pos κ with h0 | h0973    · subst h0; exact absurd hp.out (by decide)974    · exact h0975  have h2z : (2 : ZMod (4 * κ + 1)) ≠ 0 := by976    intro h977    have := (ZMod.natCast_eq_zero_iff 2 (4 * κ + 1)).1 (by exact_mod_cast h)978    have := Nat.le_of_dvd (by norm_num) this979    omega980  have h4z : (4 : ZMod (4 * κ + 1)) ≠ 0 := four_ne_zero_of_two h2z981  have hκ : (κ : ZMod (4 * κ + 1)) = -4⁻¹ := neg_inv_of_mul h4z h4982  refine ⟨h4, hκ, three_quarters h4z hκ, half_neg h2z h4, ?_, by omega⟩983  have hh : g ^ (2 * κ) = -1 := by984    have h1 := pow_orderOf_eq_one g985    rw [hg] at h1986    have h2' : (g ^ (2 * κ)) ^ 2 = 1 := by rw [← pow_mul, show 2 * κ * 2 = 4 * κ by ring]; exact h1987    rcases sq_eq_one_cases h2' with h | h988    · exfalso989      have := orderOf_dvd_iff_pow_eq_one.2 h990      rw [hg] at this991      have := Nat.le_of_dvd (by omega) this992      omega993    · exact h994  rw [three_kappa_pow g κ hh]995  exact (neg_neg _).symm996997end latitude9989991000/-! ## The gamma matrices in blocks, and the Clifford relations (8:D2) -/1001section clifford1002variable {K : Type*} [CommRing K]1003open Matrix10041005/-- The Pauli matrices over `K`, with the shell's quarter-turn `i` (`i² = −1`) in `σ²`. -/1006def σ1 : Matrix (Fin 2) (Fin 2) K := !![0, 1; 1, 0]1007def σ2 (i : K) : Matrix (Fin 2) (Fin 2) K := !![0, -i; i, 0]1008def σ3 : Matrix (Fin 2) (Fin 2) K := !![1, 0; 0, -1]1009/-- `J = σ¹σ³ = (0 −1; 1 0)`, the block of the spinor twist. -/1010def J : Matrix (Fin 2) (Fin 2) K := !![0, -1; 1, 0]10111012/-- `β = (0 I; I 0)` and `ρ(σ) = (0 σ; −σ 0)` on `K² ⊕ K²`. -/1013def β : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := fromBlocks 0 1 1 01014def ρ (s : Matrix (Fin 2) (Fin 2) K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := fromBlocks 0 s (-s) 010151016/-- The gamma matrices of `(eq:gamma-definition)`: `γ⁰ = i w β`, `γ^k = i ρ(σ^k)`. -/1017def γ0 (i w : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := (i * w) • β1018def γ1 (i : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := i • ρ σ11019def γ2 (i : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := i • ρ (σ2 i)1020def γ3 (i : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := i • ρ σ310211022/-- 8:D2 — the Pauli identities `σ^j σ^k + σ^k σ^j = 2 δ_{jk} I₂` over `K`, from `i² = −1`. -/1023theorem pauli {i : K} (hi : i * i = -1) :1024    σ1 * σ1 = (1 : Matrix (Fin 2) (Fin 2) K) ∧ σ2 i * σ2 i = 1 ∧ σ3 * σ3 = (1 : Matrix (Fin 2) (Fin 2) K) ∧1025    σ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 := by1026  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;>1027  · ext a b1028    fin_cases a <;> fin_cases b <;>1029    simp [σ1, σ2, σ3, Matrix.mul_apply, Fin.sum_univ_two, Matrix.one_apply] <;>1030    linear_combination (-1 : K) * hi10311032theorem β_sq : (β : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) * β = 1 := by1033  simp [β, fromBlocks_multiply, fromBlocks_one]10341035theorem ρ_mul (s t : Matrix (Fin 2) (Fin 2) K) : ρ s * ρ t = fromBlocks (-(s * t)) 0 0 (-(s * t)) := by1036  simp [ρ, fromBlocks_multiply]10371038theorem β_ρ_anticomm (s : Matrix (Fin 2) (Fin 2) K) : β * ρ s + ρ s * β = 0 := by1039  simp [β, ρ, fromBlocks_multiply, fromBlocks_add]10401041/-- 8:D17 — conjugation preserves anticommutators: for a unit `S`, `(SaS⁻¹)(SbS⁻¹) + (SbS⁻¹)(SaS⁻¹) = S(ab + ba)S⁻¹`, so the1042transported gamma matrices `Sγ^μS⁻¹` satisfy the Clifford relations of the standard ones (Corollary1043`transported-clifford`). -/1044theorem conj_anticomm {R : Type*} [Ring R] (S : Rˣ) (a b : R) :1045    (S * a * ↑S⁻¹) * (S * b * ↑S⁻¹) + (S * b * ↑S⁻¹) * (S * a * ↑S⁻¹) = S * (a * b + b * a) * ↑S⁻¹ := by1046  simp only [mul_add, add_mul, mul_assoc, Units.inv_mul_cancel_left]10471048/-- 8:D2, 8:D17 — the Clifford relations `γ^μ γ^ν + γ^ν γ^μ = 2 η_{μν} I₄`, `η = diag(−ν, 1, 1, 1)`, from `i² = −1` and1049`w² = ν` alone (Proposition `clifford`), by the block computation of its proof: `β² = I`, `(ρ^k)² = −I`,1050`ρ^jρ^k + ρ^kρ^j = 0`, `βρ^k + ρ^kβ = 0`. -/1051theorem clifford {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1052    γ0 i w * γ0 i w = (-ν) • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) ∧1053    γ1 i * γ1 i = 1 ∧ γ2 i * γ2 i = 1 ∧ γ3 i * γ3 i = 1 ∧1054    γ0 i w * γ1 i + γ1 i * γ0 i w = 0 ∧ γ0 i w * γ2 i + γ2 i * γ0 i w = 0 ∧1055    γ0 i w * γ3 i + γ3 i * γ0 i w = 0 ∧ γ1 i * γ2 i + γ2 i * γ1 i = 0 ∧1056    γ1 i * γ3 i + γ3 i * γ1 i = 0 ∧ γ2 i * γ3 i + γ3 i * γ2 i = 0 := by1057  obtain ⟨h11, h22, h33, h12, h13, h23⟩ := pauli hi1058  have hsq : ∀ s : Matrix (Fin 2) (Fin 2) K, s * s = 1 → (i • ρ s) * (i • ρ s) = 1 := fun s hs => by1059    rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, ρ_mul, hs, hi]1060    simp [fromBlocks_one, fromBlocks_neg]1061  have hanti : ∀ s t : Matrix (Fin 2) (Fin 2) K, s * t + t * s = 0 →1062      (i • ρ s) * (i • ρ t) + (i • ρ t) * (i • ρ s) = 0 := fun s t hst => by1063    rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, Matrix.smul_mul, Matrix.mul_smul, smul_smul, ← smul_add,1064      ρ_mul, ρ_mul, fromBlocks_add]1065    have : -(s * t) + -(t * s) = 0 := by rw [← neg_add, hst, neg_zero]1066    simp [this]1067  have h0k : ∀ s : Matrix (Fin 2) (Fin 2) K, γ0 i w * (i • ρ s) + (i • ρ s) * γ0 i w = 0 := fun s => by1068    unfold γ01069    rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, Matrix.smul_mul, Matrix.mul_smul, smul_smul,1070      mul_comm i (i * w), ← smul_add, β_ρ_anticomm, smul_zero]1071  refine ⟨?_, hsq _ h11, hsq _ h22, hsq _ h33, h0k _, h0k _, h0k _, hanti _ _ h12, hanti _ _ h13, hanti _ _ h23⟩1072  unfold γ01073  rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, β_sq]1074  congr 11075  linear_combination (w * w) * hi - hw10761077/-- `M = γ⁰γ¹` and the spinor twist `X = γ⁰γ¹γ³`. -/1078def Mγ (i w : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := γ0 i w * γ1 i1079def Xγ (i w : K) : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K := γ0 i w * γ1 i * γ3 i10801081/-- Push a block identity down to its four `2 × 2` blocks and close each entrywise, reducing the powers of1082`i` and `w`. -/1083macro "block_entries" hs:term : tactic =>1084  `(tactic| (rw [fromBlocks_inj]; refine ⟨?_, ?_, ?_, ?_⟩ <;>1085      (ext a b; fin_cases a <;> fin_cases b <;>1086        (try simp [σ1, σ2, σ3, J, Matrix.mul_apply, Fin.sum_univ_two, Matrix.one_apply, Matrix.conjTranspose_apply,1087          $hs:term]) <;>1088        (try ring_nf) <;> (try simp only [$hs:term]) <;> (try ring_nf))))10891090theorem powers {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1091    i ^ 2 = -1 ∧ i ^ 3 = -i ∧ i ^ 4 = 1 ∧ i ^ 5 = i ∧ i ^ 6 = -1 ∧ i ^ 7 = -i ∧ i ^ 8 = 1 ∧1092    w ^ 2 = ν ∧ w ^ 3 = ν * w ∧ w ^ 4 = ν ^ 2 ∧ w ^ 5 = ν ^ 2 * w := by1093  have hi2 : i ^ 2 = -1 := by rw [sq]; exact hi1094  have hw2 : w ^ 2 = ν := by rw [sq]; exact hw1095  refine ⟨hi2, ?_, ?_, ?_, ?_, ?_, ?_, hw2, ?_, ?_, ?_⟩1096  · rw [pow_succ, hi2]; ring1097  · rw [show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hi2]; ring1098  · rw [pow_succ, show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hi2]; ring1099  · rw [show (6 : ℕ) = 2 * 3 by rfl, pow_mul, hi2]; ring1100  · rw [pow_succ, show (6 : ℕ) = 2 * 3 by rfl, pow_mul, hi2]; ring1101  · rw [show (8 : ℕ) = 2 * 4 by rfl, pow_mul, hi2]; ring1102  · rw [pow_succ, hw2]1103  · rw [show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hw2]1104  · rw [pow_succ, show (4 : ℕ) = 2 * 2 by rfl, pow_mul, hw2]11051106/-- `M = γ⁰γ¹ = diag(w σ¹, −w σ¹)` in blocks. -/1107theorem Mγ_eq {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1108    Mγ i w = fromBlocks (w • σ1) 0 0 (-(w • σ1)) := by1109  have hs := powers hi hw1110  simp only [Mγ, γ0, γ1, β, ρ, Matrix.smul_mul, Matrix.mul_smul, smul_smul, fromBlocks_multiply, fromBlocks_smul]1111  block_entries hs11121113/-- `X = γ⁰γ¹γ³ = (0, i w J; i w J, 0)` in blocks, `J = σ¹σ³`. -/1114theorem Xγ_eq {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1115    Xγ i w = fromBlocks 0 ((i * w) • J) ((i * w) • J) 0 := by1116  have hs := powers hi hw1117  have : Xγ i w = Mγ i w * γ3 i := rfl1118  rw [this, Mγ_eq hi hw]1119  simp only [γ3, ρ, Matrix.smul_mul, Matrix.mul_smul, smul_smul, fromBlocks_multiply, fromBlocks_smul]1120  block_entries hs11211122/-- 8:D6, 8:D16 (the transported gammas) — spin conjugation up to the scalar `δ`: `M² = ν`,1123`(x − yM) γ⁰ (x + yM) = (x² + νy²) γ⁰ − 2xyν γ¹`, `(x − yM) γ¹ (x + yM) = −2xy γ⁰ + (x² + νy²) γ¹`, and `M`1124commutes with `γ²` and `γ³` (Proposition `spin-conjugation`; the division by `δ = x² − νy²` onto1125`A = (x² + νy²)/δ`, `B = −2xy/δ` is `spin_conjugation_AB`); `y ↦ −y` gives the transported gammas1126`γ̂⁰ = Aγ⁰ − νBγ¹`, `γ̂¹ = −Bγ⁰ + Aγ¹` (Proposition `transported-dirac-form`, the pullback identity and the1127transported factorization not formalised). -/1128theorem spin_conjugation {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (x y : K) :1129    Mγ i w * Mγ i w = ν • 1 ∧1130    (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 ∧1131    (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 ∧1132    Mγ i w * γ2 i = γ2 i * Mγ i w ∧ Mγ i w * γ3 i = γ3 i * Mγ i w := by1133  have hs := powers hi hw1134  rw [Mγ_eq hi hw]1135  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>1136  · simp only [γ0, γ1, γ2, γ3, β, ρ, ← fromBlocks_one, Matrix.smul_mul, Matrix.mul_smul, smul_smul,1137      fromBlocks_multiply, fromBlocks_smul, fromBlocks_add, fromBlocks_neg]1138    block_entries hs11391140/-- 8:D9, 8:X4 — the spinor twist: `X² = ν`, `X` commutes with `γ⁰, γ¹, γ³` and anticommutes with `γ²` (Lemma1141`spinor-form`, the algebraic part). -/1142theorem spinor_twist {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) :1143    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 ∧1144    Xγ i w * γ3 i = γ3 i * Xγ i w ∧ Xγ i w * γ2 i = -(γ2 i * Xγ i w) := by1145  have hs := powers hi hw1146  rw [Xγ_eq hi hw]1147  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>1148  · simp only [γ0, γ1, γ2, γ3, β, ρ, ← fromBlocks_one, Matrix.smul_mul, Matrix.mul_smul, smul_smul,1149      fromBlocks_multiply, fromBlocks_smul, fromBlocks_add, fromBlocks_neg]1150    block_entries hs11511152end clifford115311541155section spinorform1156variable {K : Type*} [CommRing K] [StarRing K]1157open Matrix11581159theorem σ1_dagger : (σ1 : Matrix (Fin 2) (Fin 2) K)ᴴ = σ1 := by1160  ext a b; fin_cases a <;> fin_cases b <;> simp [σ1, Matrix.conjTranspose_apply]1161theorem σ3_dagger : (σ3 : Matrix (Fin 2) (Fin 2) K)ᴴ = σ3 := by1162  ext a b; fin_cases a <;> fin_cases b <;> simp [σ3, Matrix.conjTranspose_apply]1163theorem J_dagger : (J : Matrix (Fin 2) (Fin 2) K)ᴴ = -J := by1164  ext a b; fin_cases a <;> fin_cases b <;> simp [J, Matrix.conjTranspose_apply]1165theorem σ2_dagger {i : K} (hsi : star i = i) : (σ2 i)ᴴ = -σ2 i := by1166  ext a b; fin_cases a <;> fin_cases b <;> simp [σ2, Matrix.conjTranspose_apply, hsi]11671168/-- 8:D9, 8:X4 — under the conjugate transpose (Frobenius fixing `i`, negating `w`): `(γ⁰)† = −γ⁰`, `(γ¹)† = −γ¹`,1169`(γ²)† = +γ²` (the obstruction: `σ²` is antisymmetric with `i` Frobenius-fixed), `(γ³)† = −γ³`, and1170`X† = X` for the twist `X = γ⁰γ¹γ³` (Lemma `spinor-form`). -/1171theorem gamma_dagger {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (hsi : star i = i) (hsw : star w = -w) :1172    (γ0 i w)ᴴ = -γ0 i w ∧ (γ1 i)ᴴ = -γ1 i ∧ (γ2 i)ᴴ = γ2 i ∧ (γ3 i)ᴴ = -γ3 i ∧ (Xγ i w)ᴴ = Xγ i w := by1173  refine ⟨?_, ?_, ?_, ?_, ?_⟩1174  · simp only [γ0, β, Matrix.conjTranspose_smul, star_mul', hsi, hsw, fromBlocks_conjTranspose,1175      Matrix.conjTranspose_zero, Matrix.conjTranspose_one, ← neg_smul]1176    congr 1; ring1177  · simp only [γ1, ρ, Matrix.conjTranspose_smul, hsi, fromBlocks_conjTranspose, Matrix.conjTranspose_zero,1178      Matrix.conjTranspose_neg, σ1_dagger, ← smul_neg, fromBlocks_neg, neg_neg, neg_zero]1179  · simp only [γ2, ρ, Matrix.conjTranspose_smul, hsi, fromBlocks_conjTranspose, Matrix.conjTranspose_zero,1180      Matrix.conjTranspose_neg, σ2_dagger hsi, neg_neg]1181  · simp only [γ3, ρ, Matrix.conjTranspose_smul, hsi, fromBlocks_conjTranspose, Matrix.conjTranspose_zero,1182      Matrix.conjTranspose_neg, σ3_dagger, ← smul_neg, fromBlocks_neg, neg_neg, neg_zero]1183  · rw [Xγ_eq hi hw]1184    simp only [fromBlocks_conjTranspose, Matrix.conjTranspose_zero, Matrix.conjTranspose_smul, star_mul', hsi, hsw,1185      J_dagger, smul_neg, neg_smul, neg_neg, mul_neg]11861187/-- 8:D9 — the twist conjugates every gamma to its negative, `(γ^μ)† X = −X γ^μ` (so `X⁻¹(γ^μ)†X = −γ^μ`),1188while the `γ⁰`-twist leaves mixed signs: `(γ⁰)† γ⁰ = −γ⁰γ⁰` but `(γ¹)† γ⁰ = +γ⁰γ¹` (Lemma `spinor-form`). -/1189theorem twist_adjoint {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (hsi : star i = i) (hsw : star w = -w) :1190    (γ0 i w)ᴴ * Xγ i w = -(Xγ i w * γ0 i w) ∧ (γ1 i)ᴴ * Xγ i w = -(Xγ i w * γ1 i) ∧1191    (γ2 i)ᴴ * Xγ i w = -(Xγ i w * γ2 i) ∧ (γ3 i)ᴴ * Xγ i w = -(Xγ i w * γ3 i) ∧1192    (γ0 i w)ᴴ * γ0 i w = -(γ0 i w * γ0 i w) ∧ (γ1 i)ᴴ * γ0 i w = γ0 i w * γ1 i := by1193  obtain ⟨d0, d1, d2, d3, _⟩ := gamma_dagger hi hw hsi hsw1194  obtain ⟨_, c0, c1, c3, a2⟩ := spinor_twist hi hw1195  have hs := powers hi hw1196  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩1197  · rw [d0, neg_mul, c0]1198  · rw [d1, neg_mul, c1]1199  · rw [d2, a2, neg_neg]1200  · rw [d3, neg_mul, c3]1201  · rw [d0, neg_mul]1202  · rw [d1, neg_mul, neg_eq_iff_eq_neg]1203    simp only [γ0, γ1, β, ρ, Matrix.smul_mul, Matrix.mul_smul, smul_smul, fromBlocks_multiply, fromBlocks_smul,1204      fromBlocks_neg]1205    block_entries hs12061207/-- `M† = −M`. -/1208theorem Mγ_dagger {i w ν : K} (hi : i * i = -1) (hw : w * w = ν) (hsw : star w = -w) :1209    (Mγ i w)ᴴ = -(Mγ i w) := by1210  rw [Mγ_eq hi hw]1211  simp only [fromBlocks_conjTranspose, Matrix.conjTranspose_smul, Matrix.conjTranspose_neg,1212    Matrix.conjTranspose_zero, fromBlocks_neg, hsw, σ1_dagger, neg_smul, neg_neg, neg_zero]12131214/-- 8:D11 — the lift's adjoint: `S† = S(x, −y)` for Frobenius-fixed `x, y` (so, `X` commuting with `M`,1215`S^# = X⁻¹S†X = S(x, −y)`), and `S(x, −y) S(x, y) = (x² − νy²) I = δ I` (Proposition `two-diracs`). -/1216theorem lift_adjoint {i w ν x y : K} (hi : i * i = -1) (hw : w * w = ν) (hsw : star w = -w)1217    (hx : star x = x) (hy : star y = y) :1218    (x • 1 + y • Mγ i w)ᴴ = x • 1 + (-y) • Mγ i w ∧1219    (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) := by1220  obtain ⟨hM2, _, _, _, _⟩ := spin_conjugation hi hw x y1221  refine ⟨?_, ?_⟩1222  · rw [Matrix.conjTranspose_add, Matrix.conjTranspose_smul, Matrix.conjTranspose_smul, Matrix.conjTranspose_one,1223      Mγ_dagger hi hw hsw, hx, hy, smul_neg, neg_smul]1224  · simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, neg_mul, mul_neg, smul_smul,1225      smul_neg, smul_add, neg_smul, hM2]1226    module12271228/-- 8:D11 — the transport of the spinor form: for a lift `S = x + yM` with Frobenius-fixed `x, y`,1229`S† X S = (x² − νy²) X = δ X` — norm-one lifts preserve the form exactly, and the odd coset scales it by1230the lift norm `δ` (Proposition `two-diracs`). -/1231theorem lift_transport {i w ν x y : K} (hi : i * i = -1) (hw : w * w = ν) (hsi : star i = i) (hsw : star w = -w)1232    (hx : star x = x) (hy : star y = y) :1233    (x • 1 + y • Mγ i w)ᴴ * Xγ i w * (x • 1 + y • Mγ i w) = (x ^ 2 - ν * y ^ 2) • Xγ i w := by1234  obtain ⟨hM2, _, _, _, _⟩ := spin_conjugation hi hw x y1235  obtain ⟨_, c0, c1, _, _⟩ := spinor_twist hi hw1236  have hXM : Xγ i w * Mγ i w = Mγ i w * Xγ i w := by1237    show Xγ i w * (γ0 i w * γ1 i) = γ0 i w * γ1 i * Xγ i w1238    rw [← mul_assoc, c0, mul_assoc, c1, ← mul_assoc]1239  rw [Matrix.conjTranspose_add, Matrix.conjTranspose_smul, Matrix.conjTranspose_smul, Matrix.conjTranspose_one,1240    Mγ_dagger hi hw hsw, hx, hy]1241  have e1 : (x • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) + y • -Mγ i w) * Xγ i w =1242      Xγ i w * (x • 1 + y • -Mγ i w) := by1243    simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, neg_mul, mul_neg, hXM]1244  rw [e1, mul_assoc]1245  have e2 : (x • (1 : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K) + y • -Mγ i w) * (x • 1 + y • Mγ i w) =1246      (x ^ 2 - ν * y ^ 2) • 1 := by1247    simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, neg_mul, mul_neg, smul_smul,1248      smul_neg, smul_add, hM2]1249    module1250  rw [e2, mul_smul_comm, mul_one]12511252end spinorform12531254/-! ## The coordinate boost (8:D5) -/1255section boostmatrix1256variable {F : Type*} [Field F]12571258/-- The boost entries `A = (x² + νy²)/δ`, `B = −2xy/δ`, `δ = x² − νy²`. -/1259noncomputable def Aent (ν x y : F) : F := (x ^ 2 + ν * y ^ 2) / (x ^ 2 - ν * y ^ 2)1260noncomputable def Bent (ν x y : F) : F := -(2 * x * y) / (x ^ 2 - ν * y ^ 2)12611262/-- 8:D14, 8:D15 — `Λ(x, y) ∈ O(Q_ν)`: `A² − νB² = 1` (Proposition `boost-orthogonal`); and the group law1263`Λ(x, y)Λ(u, v) = Λ(xu + νyv, xv + yu)` on the entries, with `Λ(1, 0) = I` and `Λ(x, −y) = Λ(x, y)⁻¹`1264(Proposition `boost-subgroup`). -/1265theorem boost_entries (ν x y u v : F) (hd : x ^ 2 - ν * y ^ 2 ≠ 0) (hd' : u ^ 2 - ν * v ^ 2 ≠ 0) :1266    Aent ν x y ^ 2 - ν * Bent ν x y ^ 2 = 1 ∧1267    Aent ν x y * Aent ν u v + ν * (Bent ν x y * Bent ν u v) = Aent ν (x * u + ν * y * v) (x * v + y * u) ∧1268    Aent ν x y * Bent ν u v + Bent ν x y * Aent ν u v = Bent ν (x * u + ν * y * v) (x * v + y * u) ∧1269    Aent ν 1 0 = 1 ∧ Bent ν 1 0 = 0 ∧ Aent ν x (-y) = Aent ν x y ∧ Bent ν x (-y) = -Bent ν x y := by1270  have hdd : (x * u + ν * y * v) ^ 2 - ν * (x * v + y * u) ^ 2 = (x ^ 2 - ν * y ^ 2) * (u ^ 2 - ν * v ^ 2) := by1271    ring1272  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> simp only [Aent, Bent]1273  · field_simp; ring1274  · rw [hdd]; field_simp; ring1275  · rw [hdd]; field_simp; ring1276  · norm_num1277  · norm_num1278  · ring1279  · ring12801281/-- 8:D6 — the spin conjugation with the inverse: for `δ = x² − νy² ≠ 0`, `S⁻¹ = δ⁻¹(x − yM)` and1282`S⁻¹γ⁰S = Aγ⁰ + νBγ¹`, `S⁻¹γ¹S = Bγ⁰ + Aγ¹` with `A = (x² + νy²)/δ`, `B = −2xy/δ` (Proposition1283`spin-conjugation`). -/1284theorem spin_conjugation_AB {i w ν x y : F} (hi : i * i = -1) (hw : w * w = ν) (hd : x ^ 2 - ν * y ^ 2 ≠ 0) :1285    ((x ^ 2 - ν * y ^ 2)⁻¹ • (x • 1 + (-y) • Mγ i w)) * γ0 i w * (x • 1 + y • Mγ i w) =1286      Aent ν x y • γ0 i w + (ν * Bent ν x y) • γ1 i ∧1287    ((x ^ 2 - ν * y ^ 2)⁻¹ • (x • 1 + (-y) • Mγ i w)) * γ1 i * (x • 1 + y • Mγ i w) =1288      Bent ν x y • γ0 i w + Aent ν x y • γ1 i := by1289  obtain ⟨_, h0, h1, _, _⟩ := spin_conjugation hi hw x y1290  refine ⟨?_, ?_⟩1291  · rw [Matrix.smul_mul, Matrix.smul_mul, h0, smul_add, smul_smul, smul_smul]1292    simp only [Aent, Bent]1293    congr 2 <;> field_simp1294  · rw [Matrix.smul_mul, Matrix.smul_mul, h1, smul_add, smul_smul, smul_smul]1295    simp only [Aent, Bent]1296    congr 2 <;> field_simp12971298end boostmatrix12991300/-! ## The worked shells (8:D12, B4, B3) -/1301section shells13021303instance : Fact (Nat.Prime 13) := ⟨by norm_num⟩1304instance : Fact (Nat.Prime 173) := ⟨by norm_num⟩13051306/-- 8:D12, 8:B4, 8:B3 [value] — `𝔽₁₃` with `ν = g = 2`, `x = y = 1`: `A = 10`, `B = 2`, `A² − νB² = 1`;1307`2⁻¹ = 7` is a nonsquare and `e = 2^5 = 6` a nonsquare; `2` is primitive (`orderOf 2 = 12`). -/1308theorem shell13 :1309    Aent (2 : ZMod 13) 1 1 = 10 ∧ Bent (2 : ZMod 13) 1 1 = 2 ∧ (10 : ZMod 13) ^ 2 - 2 * 2 ^ 2 = 1 ∧1310    (2 : ZMod 13) * 7 = 1 ∧ ¬ IsSquare (7 : ZMod 13) ∧ (2 : ZMod 13) ^ 5 = 6 ∧ ¬ IsSquare (6 : ZMod 13) ∧1311    orderOf (2 : ZMod 13) = 12 := by1312  refine ⟨?_, ?_, by decide, by decide, by decide, by decide, by decide, ?_⟩1313  · simp only [Aent]; rw [div_eq_iff (by decide)]; decide1314  · simp only [Bent]; rw [div_eq_iff (by decide)]; decide1315  · rw [orderOf_eq_iff (by norm_num)]1316    exact ⟨by decide, fun m hm hm0 => by interval_cases m <;> decide⟩13171318/-- 8:D19, 8:B3 [value] — `𝔽₁₇₃` (`κ = 43`) with `ν = g = 2`, `i = 93`: `A = 170`, `B = 2`, `A² − νB² = 1`;1319`i² = −1`; `2⁻¹ = 87`, `e = 2^{93} = 45` and `π = 2κ = 86`, and `2`, `87`, `93`, `45`, `86` are nonsquares (the named1320residues all odd, `κ` odd); `2` is primitive (`orderOf 2 = 172`, by the prime divisors `2` and `43` of `172`). -/1321theorem shell173 :1322    Aent (2 : ZMod 173) 1 1 = 170 ∧ Bent (2 : ZMod 173) 1 1 = 2 ∧ (170 : ZMod 173) ^ 2 - 2 * 2 ^ 2 = 1 ∧1323    (93 : ZMod 173) ^ 2 = -1 ∧ (2 : ZMod 173) * 87 = 1 ∧ (2 : ZMod 173) ^ 93 = 45 ∧ (86 : ZMod 173) = 2 * 43 ∧1324    ¬ IsSquare (2 : ZMod 173) ∧ ¬ IsSquare (87 : ZMod 173) ∧ ¬ IsSquare (93 : ZMod 173) ∧1325    ¬ IsSquare (45 : ZMod 173) ∧ ¬ IsSquare (86 : ZMod 173) ∧ orderOf (2 : ZMod 173) = 172 := by1326  refine ⟨?_, ?_, by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel,1327    by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, ?_⟩1328  · simp only [Aent]; rw [div_eq_iff (by decide +kernel)]; decide +kernel1329  · simp only [Bent]; rw [div_eq_iff (by decide +kernel)]; decide +kernel1330  · refine orderOf_eq_of_pow_and_pow_div_prime (by norm_num) (by decide +kernel) ?_1331    intro q hq hdvd1332    have : q = 2 ∨ q = 43 := by1333      have h172 : (172 : ℕ) = 2 ^ 2 * 43 := by norm_num1334      rw [h172] at hdvd1335      rcases (Nat.Prime.dvd_mul hq).1 hdvd with h | h1336      · exact Or.inl ((Nat.prime_dvd_prime_iff_eq hq Nat.prime_two).1 (hq.dvd_of_dvd_pow h))1337      · exact Or.inr ((Nat.prime_dvd_prime_iff_eq hq (by norm_num)).1 h)1338    rcases this with rfl | rfl <;> decide +kernel13391340/-- 8:B4 [value] — the laboratory Carrier `Ω = 2 408 561`: the two-way constant `c = 171 106` is a Carrier residue with1341`c² = 2⁻¹` (`171106² · 2 ≡ 1`), `2⁻¹ = 1 204 281`, and the two factors compose: `2⁻¹ · 12 ≡ 6 = g`. -/1342theorem carrier_constants :1343    (171106 * 171106 * 2) % 2408561 = 1 ∧ (2 * 1204281) % 2408561 = 1 ∧ (1204281 * 12) % 2408561 = 6 ∧1344    Nat.Prime 2408561 := by1345  refine ⟨by norm_num, by norm_num, by norm_num, by norm_num⟩13461347end shells13481349end13501351/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/13521353section parity_aliases1354variable {p : ℕ} [hp : Fact (Nat.Prime p)]13551356/-- 8:B5, 8:X2 — the square class is chronon parity: for a primitive root `g` (`orderOf g = p − 1`), `g^k` is a1357square exactly when `k` is even (Theorem `parity`); registered transport `g²` is even, the one-way step `g` odd. -/1358theorem parity_iff {g : ZMod p} (hg : orderOf g = p - 1) (hodd : p % 2 = 1) (k : ℕ) :1359    IsSquare (g ^ k) ↔ Even k :=1360  FRC.Frame.parity_iff hg hodd k13611362/-- 8:B3 — the drive is a nonsquare (`g^{(p−1)/2} = −1`), and so is its inverse `g^{p−2}`: `[g⁻¹] = [g]`. -/1363theorem drive_nonsquare {g : ZMod p} (hg : orderOf g = p - 1) (hodd : p % 2 = 1) :1364    ¬ IsSquare g ∧ ¬ IsSquare g⁻¹ :=1365  FRC.Frame.drive_nonsquare hg hodd13661367end parity_aliases13681369@[reducible] def Ext := @FRC.Extension.Ext13701371namespace Ext1372variable {F : Type*} [CommRing F] {ν : F}13731374theorem zero_re : (0 : Ext F ν).re = 0 :=1375  FRC.Extension.Ext.zero_re13761377theorem zero_im : (0 : Ext F ν).im = 0 :=1378  FRC.Extension.Ext.zero_im13791380theorem one_re : (1 : Ext F ν).re = 1 :=1381  FRC.Extension.Ext.one_re13821383theorem one_im : (1 : Ext F ν).im = 0 :=1384  FRC.Extension.Ext.one_im13851386theorem add_re (z z' : Ext F ν) : (z + z').re = z.re + z'.re :=1387  FRC.Extension.Ext.add_re z z'13881389theorem add_im (z z' : Ext F ν) : (z + z').im = z.im + z'.im :=1390  FRC.Extension.Ext.add_im z z'13911392theorem neg_re (z : Ext F ν) : (-z).re = -z.re :=1393  FRC.Extension.Ext.neg_re z13941395theorem neg_im (z : Ext F ν) : (-z).im = -z.im :=1396  FRC.Extension.Ext.neg_im z13971398theorem sub_re (z z' : Ext F ν) : (z - z').re = z.re - z'.re :=1399  FRC.Extension.Ext.sub_re z z'14001401theorem sub_im (z z' : Ext F ν) : (z - z').im = z.im - z'.im :=1402  FRC.Extension.Ext.sub_im z z'14031404theorem mul_re (z z' : Ext F ν) : (z * z').re = z.re * z'.re + ν * (z.im * z'.im) :=1405  FRC.Extension.Ext.mul_re z z'14061407theorem mul_im (z z' : Ext F ν) : (z * z').im = z.re * z'.im + z.im * z'.re :=1408  FRC.Extension.Ext.mul_im z z'14091410theorem nsmul_re (n : ℕ) (z : Ext F ν) : (n • z).re = n • z.re :=1411  FRC.Extension.Ext.nsmul_re n z14121413theorem nsmul_im (n : ℕ) (z : Ext F ν) : (n • z).im = n • z.im :=1414  FRC.Extension.Ext.nsmul_im n z14151416theorem zsmul_re (n : ℤ) (z : Ext F ν) : (n • z).re = n • z.re :=1417  FRC.Extension.Ext.zsmul_re n z14181419theorem zsmul_im (n : ℤ) (z : Ext F ν) : (n • z).im = n • z.im :=1420  FRC.Extension.Ext.zsmul_im n z14211422@[reducible] def ofBase (a : F) : Ext F ν :=1423  FRC.Extension.Ext.ofBase a14241425@[reducible] def w : Ext F ν :=1426  FRC.Extension.Ext.w14271428@[reducible] def conj (z : Ext F ν) : Ext F ν :=1429  FRC.Extension.Ext.conj z14301431@[reducible] def norm (z : Ext F ν) : F :=1432  FRC.Extension.Ext.norm z14331434theorem ofBase_re (a : F) : (ofBase a : Ext F ν).re = a :=1435  FRC.Extension.Ext.ofBase_re a14361437theorem ofBase_im (a : F) : (ofBase a : Ext F ν).im = 0 :=1438  FRC.Extension.Ext.ofBase_im a14391440theorem w_re : (w : Ext F ν).re = 0 :=1441  FRC.Extension.Ext.w_re14421443theorem w_im : (w : Ext F ν).im = 1 :=1444  FRC.Extension.Ext.w_im14451446theorem conj_re (z : Ext F ν) : (conj z).re = z.re :=1447  FRC.Extension.Ext.conj_re z14481449theorem conj_im (z : Ext F ν) : (conj z).im = -z.im :=1450  FRC.Extension.Ext.conj_im z14511452theorem w_sq : (w : Ext F ν) ^ 2 = ofBase ν :=1453  FRC.Extension.Ext.w_sq14541455theorem conj_mul (z z' : Ext F ν) : conj (z * z') = conj z * conj z' :=1456  FRC.Extension.Ext.conj_mul z z'14571458theorem conj_add (z z' : Ext F ν) : conj (z + z') = conj z + conj z' :=1459  FRC.Extension.Ext.conj_add z z'14601461theorem conj_conj (z : Ext F ν) : conj (conj z) = z :=1462  FRC.Extension.Ext.conj_conj z14631464theorem conj_one : conj (1 : Ext F ν) = 1 :=1465  FRC.Extension.Ext.conj_one14661467theorem mul_conj (z : Ext F ν) : z * conj z = ofBase (norm z) :=1468  FRC.Extension.Ext.mul_conj z14691470/-- 8:B6 — the norm is multiplicative: `N(zz') = N(z)N(z')`. -/1471theorem norm_mul (z z' : Ext F ν) : norm (z * z') = norm z * norm z' :=1472  FRC.Extension.Ext.norm_mul z z'14731474theorem ofBase_mul (a b : F) : (ofBase (a * b) : Ext F ν) = ofBase a * ofBase b :=1475  FRC.Extension.Ext.ofBase_mul a b14761477theorem ofBase_add (a b : F) : (ofBase (a + b) : Ext F ν) = ofBase a + ofBase b :=1478  FRC.Extension.Ext.ofBase_add a b14791480theorem ofBase_one : (ofBase 1 : Ext F ν) = 1 :=1481  FRC.Extension.Ext.ofBase_one14821483theorem ofBase_zero : (ofBase 0 : Ext F ν) = 0 :=1484  FRC.Extension.Ext.ofBase_zero14851486theorem ofBase_injective : Function.Injective (ofBase : F → Ext F ν) :=1487  FRC.Extension.Ext.ofBase_injective14881489theorem conj_ofBase (a : F) : conj (ofBase a : Ext F ν) = ofBase a :=1490  FRC.Extension.Ext.conj_ofBase a14911492theorem conj_w : conj (w : Ext F ν) = -w :=1493  FRC.Extension.Ext.conj_w14941495theorem conj_eq_self_iff (z : Ext F ν) (h2 : (2 : F) ≠ 0) [NoZeroDivisors F] :1496    conj z = z ↔ z.im = 0 :=1497  FRC.Extension.Ext.conj_eq_self_iff z h214981499theorem conj_eq_neg_iff (z : Ext F ν) (h2 : (2 : F) ≠ 0) [NoZeroDivisors F] :1500    conj z = -z ↔ z.re = 0 :=1501  FRC.Extension.Ext.conj_eq_neg_iff z h215021503theorem star_def (z : Ext F ν) : star z = conj z :=1504  FRC.Extension.Ext.star_def z15051506/-- `w` generates: `z = re + im · w`. -/1507theorem eq_re_add_im_w (z : Ext F ν) : z = ofBase z.re + ofBase z.im * w :=1508  FRC.Extension.Ext.eq_re_add_im_w z15091510@[reducible] def instZero : Zero (Ext F ν) :=1511  FRC.Extension.Ext.instZero15121513@[reducible] def instOne : One (Ext F ν) :=1514  FRC.Extension.Ext.instOne15151516@[reducible] def instAdd : Add (Ext F ν) :=1517  FRC.Extension.Ext.instAdd15181519@[reducible] def instNeg : Neg (Ext F ν) :=1520  FRC.Extension.Ext.instNeg15211522@[reducible] def instSub : Sub (Ext F ν) :=1523  FRC.Extension.Ext.instSub15241525@[reducible] def instMul : Mul (Ext F ν) :=1526  FRC.Extension.Ext.instMul15271528@[reducible] def instSMulNat : SMul ℕ (Ext F ν) :=1529  FRC.Extension.Ext.instSMulNat15301531@[reducible] def instSMulInt : SMul ℤ (Ext F ν) :=1532  FRC.Extension.Ext.instSMulInt15331534@[reducible] def instCommRing : CommRing (Ext F ν) :=1535  FRC.Extension.Ext.instCommRing15361537@[reducible] def instStarRing : StarRing (Ext F ν) :=1538  FRC.Extension.Ext.instStarRing15391540end Ext15411542namespace Ext1543variable {F : Type*} [Field F] {ν : F}15441545theorem norm_eq_zero_iff (hν : ¬ IsSquare ν) (z : Ext F ν) : norm z = 0 ↔ z = 0 :=1546  FRC.Extension.Ext.norm_eq_zero_iff hν z15471548@[reducible] noncomputable def instInv : Inv (Ext F ν) :=1549  FRC.Extension.Ext.instInv15501551theorem inv_def (z : Ext F ν) : z⁻¹ = ofBase (norm z)⁻¹ * conj z :=1552  FRC.Extension.Ext.inv_def z15531554theorem mul_inv_cancel' (hν : ¬ IsSquare ν) (z : Ext F ν) (hz : z ≠ 0) : z * z⁻¹ = 1 :=1555  FRC.Extension.Ext.mul_inv_cancel' hν z hz15561557/-- 8:C5 — the field structure under `¬ IsSquare ν`, `z⁻¹ = z̄/N(z)` (a `def`, not an instance: the hypothesis is1558not a class). -/1559@[reducible] noncomputable def field (hν : ¬ IsSquare ν) : Field (Ext F ν) :=1560  FRC.Extension.Ext.field hν15611562end Ext1563156415651566end FRC.DiracML1567