Theme/Spinor.lean — FrcCore

1import FrcCore.Theme.Packed2import FrcCore.Theme.Unipotent3import FrcCore.Theme.Hermitian4import FrcCore.Theme.Dirac56/-!7# The spinor file of 8-dirac — the matrices as an operator ring, and the decided witnesses, no axioms89The sixth file of the dirac theme (5 November 2026, the core-proof programme): the `n × n` matrices over the coefficient10field `K = 𝔽_p(√ν)`, read as functions of two indices below `n`, form an `OpRing` (`MatE p ν n`) — two matrices are11congruent when their entries agree on the range, so no function extensionality is needed — with the conjugate transpose12as an `Adjoint`. The general theorems of the operator layer therefore hold for the Dirac operators of the paper as13matrices: the Cayley step of a self-adjoint matrix is unitary (C4), the nilpotent shift (D10, X3), the factorisation14(D3, D18), the transported Clifford relations (D17), the unipotent translations (F7). The decided witnesses on the15standard shells `𝔽₁₃`, `𝔽₁₇₃` (and `𝔽₁₅₄₉` where cheap), in the list form of the theme file: the translation and the16symmetric difference nilpotent on the cycle (`(T − 1)^p = 0`, `(∇^s)^p = 0`, by squaring), the Cayley step of `−Δ`17unitary, the factorisation `(𝒟^s − m)(𝒟^s + m) = ν(∇^s)² ⊗ I₄ − m²` on the `52 × 52` matrices of `0+1` at `p = 13`, and18the mixed step `−Δ + V_id` of E8 with `U^{13} ≠ I`, `U^{14} ≠ I`, `U^{182} ≠ I` on `𝔽₁₃` (its exact order, `(13¹³ + 1)/2`,19is the package's certificate). No axioms.20-/2122namespace FRC.Dirac.Spinor2324open FRC FRC.Shell FRC.Extension FRC.Dirac.Operator FRC.Dirac.Hermitian2526variable {p : Nat} [Pos p] {ν : Shell p}2728/-! ## The matrix ring -/2930/-- An `n × n` matrix over `K`, as a function of two indices read below `n`. -/31structure MatE (p : Nat) [Pos p] (ν : Shell p) (n : Nat) where32  f : Nat → Nat → Ext p ν3334namespace MatE3536variable {n : Nat}3738instance : Add (MatE p ν n) := ⟨fun A B => ⟨fun i j => A.f i j + B.f i j⟩⟩39instance : Neg (MatE p ν n) := ⟨fun A => ⟨fun i j => -(A.f i j)⟩⟩40instance : Mul (MatE p ν n) := ⟨fun A B => ⟨fun i j => esum (fun k => A.f i k * B.f k j) n⟩⟩41instance : OfNat (MatE p ν n) 0 := ⟨⟨fun _ _ => 0⟩⟩42instance : OfNat (MatE p ν n) 1 := ⟨⟨fun i j => if i = j then 1 else 0⟩⟩4344theorem add_f (A B : MatE p ν n) (i j : Nat) : (A + B).f i j = A.f i j + B.f i j := rfl45theorem neg_f (A : MatE p ν n) (i j : Nat) : (-A).f i j = -(A.f i j) := rfl46theorem mul_f (A B : MatE p ν n) (i j : Nat) : (A * B).f i j = esum (fun k => A.f i k * B.f k j) n := rfl47theorem zero_f (i j : Nat) : (0 : MatE p ν n).f i j = 0 := rfl48theorem one_f (i j : Nat) : (1 : MatE p ν n).f i j = if i = j then 1 else 0 := rfl4950/-- Congruence: equal entries on the range. -/51def eq (A B : MatE p ν n) : Prop := ∀ i, i < n → ∀ j, j < n → A.f i j = B.f i j5253/-- Double sums in the extension commute. -/54theorem esum_comm (F : Nat → Nat → Ext p ν) (m : Nat) : ∀ k,55    esum (fun i => esum (fun j => F i j) m) k = esum (fun j => esum (fun i => F i j) k) m56  | 0 => (esum_zero_of _ m fun _ _ => rfl).symm57  | k + 1 => by rw [esum_succ, esum_comm F m k, ← esum_add]; rfl5859theorem mul_assoc_f (A B C : MatE p ν n) (i j : Nat) : (A * B * C).f i j = (A * (B * C)).f i j := by60  show esum (fun k => esum (fun l => A.f i l * B.f l k) n * C.f k j) n =61    esum (fun l => A.f i l * esum (fun k => B.f l k * C.f k j) n) n62  calc esum (fun k => esum (fun l => A.f i l * B.f l k) n * C.f k j) n63      = esum (fun k => esum (fun l => A.f i l * B.f l k * C.f k j) n) n :=64        esum_congr n fun k _ => esum_mul_right _ _ n65    _ = esum (fun l => esum (fun k => A.f i l * B.f l k * C.f k j) n) n := esum_comm _ n n66    _ = esum (fun l => A.f i l * esum (fun k => B.f l k * C.f k j) n) n :=67        esum_congr n fun l _ => by68          rw [esum_mul_left]69          exact esum_congr n fun k _ => FRC.Extension.Ext.mul_assoc _ _ _7071theorem one_mul_f (A : MatE p ν n) {i j : Nat} (hi : i < n) : (1 * A).f i j = A.f i j := by72  show esum (fun k => (if i = k then 1 else 0) * A.f k j) n = A.f i j73  rw [esum_eq_single _ hi]74  · show (if i = i then 1 else 0) * A.f i j = A.f i j75    rw [ite_eq_left rfl]; exact FRC.Extension.Ext.one_mul _76  · intro k _ hk77    show (if i = k then 1 else 0) * A.f k j = 078    rw [ite_eq_right (fun e => hk e.symm)]; exact Hermitian.zero_mul _7980theorem mul_one_f (A : MatE p ν n) {i j : Nat} (hj : j < n) : (A * 1).f i j = A.f i j := by81  show esum (fun k => A.f i k * if k = j then 1 else 0) n = A.f i j82  rw [esum_eq_single _ hj]83  · show A.f i j * (if j = j then 1 else 0) = A.f i j84    rw [ite_eq_left rfl]; exact FRC.Extension.Ext.mul_one _85  · intro k _ hk86    show A.f i k * (if k = j then 1 else 0) = 087    rw [ite_eq_right hk]; exact Hermitian.mul_zero _8889instance instOpRing : OpRing (MatE p ν n) where90  eq := eq91  refl := fun _ _ _ _ _ => rfl92  symm := fun h i hi j hj => (h i hi j hj).symm93  trans := fun h h' i hi j hj => (h i hi j hj).trans (h' i hi j hj)94  add_congr := fun h h' i hi j hj => by rw [add_f, add_f, h i hi j hj, h' i hi j hj]95  mul_congr := fun h h' i hi j hj => by96    rw [mul_f, mul_f]; exact esum_congr n fun k hk => by rw [h i hi k hk, h' k hk j hj]97  neg_congr := fun h i hi j hj => by rw [neg_f, neg_f, h i hi j hj]98  add_comm := fun _ _ _ _ _ _ => Hermitian.add_comm _ _99  add_assoc := fun _ _ _ _ _ _ _ => Hermitian.add_assoc _ _ _100  zero_add := fun _ _ _ _ _ => Hermitian.zero_add _101  add_neg := fun _ _ _ _ _ => Hermitian.add_neg _102  mul_assoc := fun A B C i _ j _ => mul_assoc_f A B C i j103  one_mul := fun A i hi j _ => one_mul_f A hi104  mul_one := fun A i _ j hj => mul_one_f A hj105  left_distrib := fun A B C i _ j _ => by106    show esum (fun k => A.f i k * (B.f k j + C.f k j)) n =107      esum (fun k => A.f i k * B.f k j) n + esum (fun k => A.f i k * C.f k j) n108    rw [← esum_add]; exact esum_congr n fun k _ => Hermitian.mul_add _ _ _109  right_distrib := fun A B C i _ j _ => by110    show esum (fun k => (A.f i k + B.f i k) * C.f k j) n =111      esum (fun k => A.f i k * C.f k j) n + esum (fun k => B.f i k * C.f k j) n112    rw [← esum_add]; exact esum_congr n fun k _ => Hermitian.add_mul _ _ _113114/-! ### The conjugate transpose is an adjoint -/115116/-- The conjugate transpose `A† = conj Aᵀ`. -/117def dagger (A : MatE p ν n) : MatE p ν n := ⟨fun i j => FRC.Extension.Ext.conj (A.f j i)⟩118119theorem dagger_f (A : MatE p ν n) (i j : Nat) : (dagger A).f i j = FRC.Extension.Ext.conj (A.f j i) := rfl120121/-- 8:C4 — the conjugate transpose is an anti-automorphism of the matrix ring: `(AB)† = B†A†`, `(A+B)† = A†+B†`,122`1† = 1`, `(−A)† = −A†`, respecting the congruence. -/123theorem adjoint_dagger : Adjoint (dagger : MatE p ν n → MatE p ν n) where124  congr := fun h i hi j hj => by rw [dagger_f, dagger_f, h j hj i hi]125  mul := fun A B i _ j _ => by126    show FRC.Extension.Ext.conj (esum (fun k => A.f j k * B.f k i) n) =127      esum (fun k => FRC.Extension.Ext.conj (B.f k i) * FRC.Extension.Ext.conj (A.f j k)) n128    rw [esum_conj]129    exact esum_congr n fun k _ => by rw [FRC.Extension.Ext.conj_mul, FRC.Extension.Ext.mul_comm]130  add := fun A B i _ j _ => Hermitian.conj_add _ _131  one := fun i _ j _ => by132    show FRC.Extension.Ext.conj (if j = i then 1 else 0) = if i = j then 1 else 0133    cases Nat.decEq j i with134    | isTrue h => rw [ite_eq_left h, ite_eq_left h.symm]; exact Hermitian.conj_one135    | isFalse h => rw [ite_eq_right h, ite_eq_right (fun e => h e.symm)]; exact Hermitian.conj_zero136  neg := fun A i _ j _ => Hermitian.conj_neg _137138/-- 8:C4, 8:D10 — the `X`-adjoint `A ↦ X' A† X` of a unit `X` (`X X' ≈ 1`) is an adjoint too: the spinor form's139adjoint is an anti-automorphism, so the Cayley step of an `X`-self-adjoint operator preserves the `X`-form140(`cayley_unitary` with this adjoint). -/141theorem adjoint_twist {X X' : MatE p ν n} (hX : Inverse X X') :142    Adjoint (fun A : MatE p ν n => X' * dagger A * X) :=143  Adjoint.twist adjoint_dagger hX144145/-! ### The translation and the characteristic -/146147/-- The translation `T` on `n` sites: `(T ψ)(i) = ψ(i + 1)`, the matrix `T_{ij} = [j = i + 1 mod n]`. -/148def shift (n : Nat) : MatE p ν n := ⟨fun i j => if j = (i + 1) % n then 1 else 0⟩149150/-- `T^k` is the translation by `k`: `(T^k)_{ij} = [j = i + k mod n]`, on the range. -/151theorem shift_pow (hn : 0 < n) : ∀ k, opow (shift n : MatE p ν n) k ≈ ⟨fun i j => if j = (i + k) % n then 1 else 0⟩152  | 0 => fun i hi j _ => by153    show (if i = j then 1 else 0) = if j = (i + 0) % n then 1 else 0154    rw [Nat.add_zero, FRC.Nat.mod_eq_of_lt hi]155    cases Nat.decEq i j with156    | isTrue h => rw [ite_eq_left h, ite_eq_left h.symm]157    | isFalse h => rw [ite_eq_right h, ite_eq_right (fun e => h e.symm)]158  | k + 1 => by159    refine OpRing.trans (mul_congr_left (shift n) (shift_pow hn k)) ?_160    intro i hi j _161    show esum (fun l => (if l = (i + k) % n then 1 else 0) * (if j = (l + 1) % n then 1 else 0)) n =162      if j = (i + (k + 1)) % n then 1 else 0163    rw [esum_eq_single _ (FRC.Nat.mod_lt' (i + k) hn)]164    · show (if (i + k) % n = (i + k) % n then 1 else 0) * (if j = ((i + k) % n + 1) % n then 1 else 0) =165        if j = (i + (k + 1)) % n then 1 else 0166      rw [ite_eq_left rfl, FRC.Extension.Ext.one_mul, FRC.Nat.mod_add_mod _ _ _ hn, Nat.add_assoc]167    · intro l _ hl168      show (if l = (i + k) % n then 1 else 0) * (if j = (l + 1) % n then 1 else 0) = 0169      rw [ite_eq_right hl]; exact Hermitian.zero_mul _170171/-- 8:F7 — the translation on the cycle of `p` sites has `T^p ≈ 1`, on every shell. -/172theorem shift_pow_self : opow (shift p : MatE p ν p) p ≈ 1 := by173  refine OpRing.trans (shift_pow Pos.pos p) ?_174  intro i hi j _175  show (if j = (i + p) % p then 1 else 0) = if i = j then 1 else 0176  have h := FRC.Nat.add_mul_mod_self_left i 1 p Pos.pos177  rw [Nat.mul_one, Nat.add_comm p i] at h178  rw [h, FRC.Nat.mod_eq_of_lt hi]179  cases Nat.decEq i j with180  | isTrue e => rw [ite_eq_left e, ite_eq_left e.symm]181  | isFalse e => rw [ite_eq_right e, ite_eq_right (fun e' => e e'.symm)]182183/-- `k • 1` is the scalar `k` on the diagonal. -/184theorem nsmul_one_f : ∀ k, ∀ i j, (nsmul k (1 : MatE p ν n)).f i j = if i = j then FRC.Extension.Ext.ofShell (ofNat k) else 0185  | 0, i, j => by186    show (0 : Ext p ν) = if i = j then FRC.Extension.Ext.ofShell (ofNat 0) else 0187    cases Nat.decEq i j with188    | isTrue e => rw [ite_eq_left e]; exact FRC.Extension.Ext.ext rfl rfl189    | isFalse e => rw [ite_eq_right e]190  | k + 1, i, j => by191    show (nsmul k (1 : MatE p ν n)).f i j + (if i = j then 1 else 0) = if i = j then FRC.Extension.Ext.ofShell (ofNat (k + 1)) else 0192    rw [nsmul_one_f k i j]193    cases Nat.decEq i j with194    | isTrue e =>195      rw [ite_eq_left e, ite_eq_left e, ite_eq_left e]196      apply FRC.Extension.Ext.ext197      · show ofNat k + 1 = ofNat (k + 1)198        apply Shell.ext199        show (k % p + 1 % p) % p = (k + 1) % p200        rw [← FRC.Nat.add_mod _ _ _ Pos.pos]201      · exact Shell.add_zero 0202    | isFalse e => rw [ite_eq_right e, ite_eq_right e, ite_eq_right e]; exact Hermitian.add_zero 0203204/-- 8:F7, 8:D10 — the matrix ring has characteristic `p`: `p • 1 ≈ 0`. -/205theorem char_p : nsmul p (1 : MatE p ν n) ≈ 0 := fun i _ j _ => by206  rw [nsmul_one_f, ofNat_self]207  cases Nat.decEq i j with208  | isTrue e => rw [ite_eq_left e]; rfl209  | isFalse e => rw [ite_eq_right e]; rfl210211/-- 8:F7 — the translations are unipotent on every frame: `(T − 1)^p ≈ 0` on the cycle of `p` sites, by212`translation_nilpotent` with `T^p ≈ 1` and the characteristic. -/213theorem translation_unipotent {κ : Nat} {g : Shell p} (F : Frame p κ g) :214    opow (shift p + -1 : MatE p ν p) p ≈ 0 :=215  translation_nilpotent F char_p shift_pow_self216217/-- 8:D10, 8:X3 — the symmetric difference `∇^s = h (T − T⁻¹)` is nilpotent on every frame, `(∇^s)^p ≈ 0`:218`(T − T⁻¹)^p ≈ T^p + (−T⁻¹)^p ≈ 1 − 1` by the Frobenius, `T⁻¹ = T^{p−1}`, and the central `h` factors out. -/219theorem symdiff_nilpotent {κ : Nat} {g : Shell p} (F : Frame p κ g) {h : MatE p ν p} (hh : Central h) :220    opow (h * (shift p + -(opow (shift p) (p - 1))) : MatE p ν p) p ≈ 0 := by221  have hT : Comm (shift p : MatE p ν p) (-(opow (shift p) (p - 1))) :=222    Comm.neg_right (opow_self_comm (shift p) (p - 1)).symm223  have hinv : opow (opow (shift p : MatE p ν p) (p - 1)) p ≈ 1 := by224    have e : (p - 1) * p = p * (p - 1) := Nat.mul_comm _ _225    calc opow (opow (shift p : MatE p ν p) (p - 1)) p ≈ opow (shift p) ((p - 1) * p) := eq_symm (opow_mul _ _ _)226      _ ≈ opow (shift p) (p * (p - 1)) := eq_of_eq (by rw [e])227      _ ≈ opow (opow (shift p) p) (p - 1) := opow_mul _ _ _228      _ ≈ opow 1 (p - 1) := opow_congr shift_pow_self _229      _ ≈ 1 := opow_one_left _230  have hodd : opow (-1 : MatE p ν p) p ≈ -1 := by231    have e : p = 2 * (2 * κ) + 1 := by rw [F.cap, ← Nat.mul_assoc]232    exact OpRing.trans (eq_of_eq (congrArg (opow (-1 : MatE p ν p)) e)) (opow_neg_one_odd _)233  have hneg : opow (-(opow (shift p : MatE p ν p) (p - 1))) p ≈ -1 :=234    calc opow (-(opow (shift p : MatE p ν p) (p - 1))) p ≈ opow (-1 * opow (shift p) (p - 1)) p :=235          opow_congr (eq_symm (neg_one_mul _)) p236      _ ≈ opow (-1) p * opow (opow (shift p) (p - 1)) p := mul_opow (Central.neg Central.one _) p237      _ ≈ -1 * 1 := OpRing.mul_congr hodd hinv238      _ ≈ -1 := OpRing.mul_one _239  calc opow (h * (shift p + -(opow (shift p) (p - 1)))) p240      ≈ opow h p * opow (shift p + -(opow (shift p) (p - 1))) p := mul_opow (hh _) p241    _ ≈ opow h p * (opow (shift p) p + opow (-(opow (shift p) (p - 1))) p) :=242        mul_congr_right _ (frobenius_add F char_p hT)243    _ ≈ opow h p * (1 + -1) := mul_congr_right _ (OpRing.add_congr shift_pow_self hneg)244    _ ≈ opow h p * 0 := mul_congr_right _ (OpRing.add_neg 1)245    _ ≈ 0 := Operator.mul_zero _246247end MatE248249/-! ## The decided witnesses on the standard shells, on the packed arithmetic -/250section witnesses251open FRC.Dirac Mat FRC.Dirac.Packed252253/-! ### Rows of the cycle as rows of residues, kept packed between the products -/254255/-- A real row of the cycle (a row of residues), a row over `K` as the pair of its residue rows (the real and the256`w` parts), and their packed forms. -/257abbrev RRow := List Nat258abbrev NRow := List Nat × List Nat259abbrev PRow := Nat × Nat260def packRow (a : NRow) : PRow := (pack a.1, pack a.2)261def unpackRow (p n : Nat) (A : PRow) : NRow := (unpack p n A.1, unpack p n A.2)262263/-- The zero row, the identity, the translation `T` (first row `(0, 1, 0, …)`), `T − 1`, the symmetric difference264`h (T − T⁻¹)` and `−Δ = 2 − T − T⁻¹` (the theme's `kineticRow`) on the cycle of `p` sites, as rows of residues. -/265def zeroR (n : Nat) : RRow := List.replicate n 0266def idR (n : Nat) : RRow := (List.range n).map fun j => if j = 0 then 1 else 0267def shiftR (n : Nat) : RRow := (List.range n).map fun j => if j = 1 then 1 else 0268def shiftMinusOneR (p : Nat) : RRow := (List.range p).map fun j => if j = 0 then p - 1 else if j = 1 then 1 else 0269def symDiffR (p h : Nat) : RRow := (List.range p).map fun j => if j = 1 then h else if j + 1 = p then p - h else 0270def kineticR (p : Nat) : RRow :=271  (List.range p).map fun j => if j = 0 then 2 else if j = 1 ∨ j + 1 = p then p - 1 else 0272def idN (n : Nat) : NRow := (idR n, zeroR n)273/-- `α H` for `α = λ w` and a real row `H`: the real part zero, the `w` part `λ H`. -/274def wsmul (p lam : Nat) (H : RRow) : NRow := (List.replicate H.length 0, H.map fun x => lam * x % p)275276/-- The products and the sum on the cycle of `n` sites, on packed rows (`Packed.rmul`, `Packed.pmul`, `Packed.padd`;277sound by `Packed.rmul_eq`, `Packed.pmul_eq`, `Packed.padd_eq`, the slots by `Packed.le_two_pow_slots`), and the278product of two rows over `K`. -/279def rmulN (p n : Nat) (A C : Nat) : Nat := rmul p n (slots n) A C280def pmulN (p ν n : Nat) (A C : PRow) : PRow := pmul p ν n (slots n) A C281def paddN (p n : Nat) (A C : PRow) : PRow := (padd p (slots n) A.1 C.1, padd p (slots n) A.2 C.2)282def cmul (p ν n : Nat) (a b : NRow) : NRow := unpackRow p n (pmulN p ν n (packRow a) (packRow b))283284/-- Powers by squaring on packed rows (the exponent as its own fuel): real rows and rows over `K`. -/285def rpowP (p n : Nat) (A : Nat) : Nat → Nat → Nat286  | 0, _ => pack (idR n)287  | fuel + 1, e =>288    if e = 0 then pack (idR n)289    else290      let h := rpowP p n A fuel (e / 2)291      let sq := rmulN p n h h292      if e % 2 = 0 then sq else rmulN p n sq A293def rpow (p n : Nat) (a : RRow) (e : Nat) : RRow := unpack p n (rpowP p n (pack a) e e)294def cpowP (p ν n : Nat) (A : PRow) : Nat → Nat → PRow295  | 0, _ => packRow (idN n)296  | fuel + 1, e =>297    if e = 0 then packRow (idN n)298    else299      let h := cpowP p ν n A fuel (e / 2)300      let sq := pmulN p ν n h h301      if e % 2 = 0 then sq else pmulN p ν n sq A302def cpow (p ν n : Nat) (a : NRow) (e : Nat) : NRow := unpackRow p n (cpowP p ν n (packRow a) e e)303304/-- `(Π_{i<k} (1 + X^{2^i}), X^{2^k})`: the first is `Σ_{j<2^k} X^j`, the inverse of `1 − X` when `X^{2^k} = 0`, in305`2k` products. -/306def geomInvP (p ν n : Nat) (X : PRow) : Nat → PRow × PRow307  | 0 => (packRow (idN n), X)308  | k + 1 =>309    let r := geomInvP p ν n X k310    (pmulN p ν n r.1 (paddN p n (packRow (idN n)) r.2), pmulN p ν n r.2 r.2)311312/-- The Cayley step `U = (1 − αH)⁻¹(1 + αH)` of a real row `H` at `α = λ w` on the cycle of `p` sites, the inverse313by `geomInvP` over `slots p + 4` doublings (`2^{slots p + 4} = 16 · 2^{slots p} ≥ p` by `Packed.le_two_pow_slots`;314`(αH)^p = 0` is decided alongside). -/315def cayleyN (p ν lam : Nat) (H : RRow) : NRow :=316  let N := packRow (wsmul p lam H)317  unpackRow p p (pmulN p ν p (geomInvP p ν p N (slots p + 4)).1 (paddN p p (packRow (idN p)) N))318319/-- The conjugate transpose of a circulant, by its first row: `b_k = conj a_{−k}`, the row reversed past its320first entry and the `w` part negated. -/321def daggerN (p : Nat) (a : NRow) : NRow :=322  match a.1 with323  | x :: xs =>324    match a.2 with325    | y :: ys => (x :: xs.reverse, ((p - y) % p) :: (ys.reverse.map fun v => (p - v) % p))326    | [] => a327  | [] => a328329/-! ### The cycles: the translation, the differences and `−Δ` at 13, 173 and 1549 -/330331/-- 8:F7, 8:D10, 8:X3 [value] — on the cycle of `𝔽₁₃`: `T^p = 1`, `(T − 1)^p = 0`, the symmetric difference332`∇^s = 2⁻¹(T − T⁻¹)` has `(∇^s)^p = 0`, and `(−Δ)^p = 0` (the kinetic sector unipotent; the general statements333`translation_unipotent`, `symdiff_nilpotent`). -/334theorem translation_values13 :335    rpow 13 13 (shiftR 13) 13 = idR 13 ∧ rpow 13 13 (shiftMinusOneR 13) 13 = zeroR 13 ∧336      rpow 13 13 (symDiffR 13 7) 13 = zeroR 13 ∧ (2 : Shell 13) * 7 = 1 ∧ rpow 13 13 (kineticR 13) 13 = zeroR 13 := by337  decide +kernel338339/-- 8:F7, 8:D10, 8:X3 [value] — the same on the cycle of `𝔽₁₇₃`. -/340theorem translation_values173 :341    rpow 173 173 (shiftR 173) 173 = idR 173 ∧ rpow 173 173 (shiftMinusOneR 173) 173 = zeroR 173 ∧342      rpow 173 173 (symDiffR 173 87) 173 = zeroR 173 ∧ (2 : Shell 173) * 87 = 1 ∧343      rpow 173 173 (kineticR 173) 173 = zeroR 173 := by344  decide +kernel345346/-- 8:F7, 8:D10, 8:X3 [value] — on the cycle of `𝔽₁₅₄₉`: `T^p = 1` and `(T − 1)^p = 0`. -/347theorem translation_values1549 :348    rpow 1549 1549 (shiftR 1549) 1549 = idR 1549 ∧ rpow 1549 1549 (shiftMinusOneR 1549) 1549 = zeroR 1549 := by349  decide +kernel350351/-- 8:F7, 8:D10, 8:X3 [value] — on the cycle of `𝔽₁₅₄₉`: `(∇^s)^p = 0` with `2⁻¹ = 775`, and `(−Δ)^p = 0`. -/352theorem kinetic_values1549 :353    rpow 1549 1549 (symDiffR 1549 775) 1549 = zeroR 1549 ∧ (2 : Shell 1549) * 775 = 1 ∧354      rpow 1549 1549 (kineticR 1549) 1549 = zeroR 1549 := by355  decide +kernel356357/-! ### The Cayley step of `−Δ` at 173 and 1549 -/358359/-- 8:C4, 8:C6, 8:C15, 8:E4, 8:E7 [value] — the Cayley step `U = (1 − αH)⁻¹(1 + αH)` of `H = −Δ` on the cycle of360`𝔽₁₇₃`, at `α = w` and at `α = c = λw` with `λ = 87`, `c² = 87 = 2⁻¹`: `(wH)^p = 0` (so `geomInvP` is the inverse,361for `α = λw` too), `U ≠ 1` and `U^p = 1`, so the order is exactly `p`, and `U†U = 1` at `α = w` — the 173 sibling of362`cayley13_values`. -/363theorem cayley_values173 :364    cpow 173 2 173 (wsmul 173 1 (kineticR 173)) 173 = (zeroR 173, zeroR 173) ∧365      cayleyN 173 2 1 (kineticR 173) ≠ idN 173 ∧ cpow 173 2 173 (cayleyN 173 2 1 (kineticR 173)) 173 = idN 173 ∧366      cmul 173 2 173 (daggerN 173 (cayleyN 173 2 1 (kineticR 173))) (cayleyN 173 2 1 (kineticR 173)) = idN 173 ∧367      cayleyN 173 2 87 (kineticR 173) ≠ idN 173 ∧ cpow 173 2 173 (cayleyN 173 2 87 (kineticR 173)) 173 = idN 173 ∧368      ((⟨0, 87⟩ : Ext 173 2) * ⟨0, 87⟩ = 87 ∧ (2 : Shell 173) * 87 = 1) := by369  decide +kernel370371/-- 8:C4, 8:C6, 8:C15, 8:E4, 8:E7 [value] — on the cycle of `𝔽₁₅₄₉`, in four declarations (each decided within the372budget of a kernel call): `(wH)^p = 0` for `H = −Δ`, and the data of `c = λw`, `λ = 775`, `c² = 775 = 2⁻¹`. -/373theorem cayley_nilpotent1549 :374    cpow 1549 2 1549 (wsmul 1549 1 (kineticR 1549)) 1549 = (zeroR 1549, zeroR 1549) ∧375      ((⟨0, 775⟩ : Ext 1549 2) * ⟨0, 775⟩ = 775 ∧ (2 : Shell 1549) * 775 = 1) := by376  decide +kernel377378/-- 8:C4, 8:C6, 8:C15, 8:E4, 8:E7 [value] — on `𝔽₁₅₄₉`, the Cayley step of `−Δ` at `α = w`: `U ≠ 1`, `U^p = 1`. -/379theorem cayley_step1549 :380    cayleyN 1549 2 1 (kineticR 1549) ≠ idN 1549 ∧381      cpow 1549 2 1549 (cayleyN 1549 2 1 (kineticR 1549)) 1549 = idN 1549 := by382  decide +kernel383384/-- 8:C4, 8:C6, 8:E4 [value] — on `𝔽₁₅₄₉`, the Cayley step of `−Δ` at `α = w` is unitary: `U†U = 1`. -/385theorem cayley_unitary1549 :386    cmul 1549 2 1549 (daggerN 1549 (cayleyN 1549 2 1 (kineticR 1549))) (cayleyN 1549 2 1 (kineticR 1549)) =387      idN 1549 := by388  decide +kernel389390/-- 8:C15, 8:E7 [value] — on `𝔽₁₅₄₉`, the Cayley step of `−Δ` at `α = c = 775 w`: `U ≠ 1`, `U^p = 1`. -/391theorem cayley_step_c1549 :392    cayleyN 1549 2 775 (kineticR 1549) ≠ idN 1549 ∧393      cpow 1549 2 1549 (cayleyN 1549 2 775 (kineticR 1549)) 1549 = idN 1549 := by394  decide +kernel395396/-! ### Matrices as pairs of residue matrices, and their packed products -/397398/-- A matrix over `K` as the pair of its residue matrices; the residue matrices of a matrix of the theme file. -/399abbrev NMat := List (List Nat) × List (List Nat)400def toN (M : Mat p ν) : NMat := (M.map (·.map fun z => z.re.val), M.map (·.map fun z => z.im.val))401402/-- The product, by the packed combinations of rows (`Packed.mulExtPacked`, sound by `Packed.mulExtPacked_eq`). -/403def mmulN (p ν n : Nat) (A B : NMat) : NMat := mulExtPacked p ν n A (B.1.map pack, B.2.map pack)404405def identN (n : Nat) : NMat :=406  ((List.range n).map fun i => (List.range n).map fun j => if i = j then 1 else 0,407   (List.range n).map fun _ => List.replicate n 0)408409def mpowAux (p ν n : Nat) (A : NMat) : Nat → Nat → NMat410  | 0, _ => identN n411  | fuel + 1, e =>412    if e = 0 then identN n413    else414      let h := mpowAux p ν n A fuel (e / 2)415      let sq := mmulN p ν n h h416      if e % 2 = 0 then sq else mmulN p ν n sq A417def mpowN (p ν n : Nat) (A : NMat) (e : Nat) : NMat := mpowAux p ν n A e e418419/-- The circulant `n × n` matrix of a first row, and the Kronecker product of two list matrices (the theme's420matrices over `K`). -/421def circMat (n : Nat) (a : List (Ext p ν)) : Mat p ν :=422  (List.range n).map fun i => (List.range n).map fun j => nth 0 a ((j + n - i) % n)423def kron (A B : Mat p ν) : Mat p ν :=424  A.flatMap fun r => B.map fun s => r.flatMap fun x => s.map fun y => x * y425def symDiffRow (n : Nat) (h : Ext p ν) : List (Ext p ν) :=426  (List.range n).map fun j => if j = 1 then h else if j + 1 = n then -h else 0427428/-- 8:D3 [value] — the factorisation in `0+1` on `𝔽₁₃` (`ν = 2`, `i = 5`), on the `52 × 52` matrices: for429`𝒟^s = ∇^s ⊗ γ⁰` and `m = 1`, `(𝒟^s − 1)(𝒟^s + 1) = −ν (∇^s)² ⊗ I₄ − I₅₂`, as `dirac_factorisation` states with430`η₀ = γ⁰γ⁰ = −ν`; the product on the packed rows. -/431theorem factorisation_value :432    let d : List (Ext 13 2) := symDiffRow 13 7433    let D : Mat 13 2 := kron (circMat 13 d) (gamma0 5)434    mmulN 13 2 52 (toN (add D (neg (ident 52)))) (toN (add D (ident 52))) =435      toN (add (smul (-(2 : Ext 13 2)) (kron (circMat 13 (cyc 13 d d)) (ident 4))) (neg (ident 52))) := by436  decide +kernel437438/-- 8:E8 [value] — the three cycles in dynamical roles: `lcm(13, 14) = 182`, and the mixed step `U = M⁻¹P` of439`H = −Δ + V_id` on `𝔽₁₃` (`M = 1 − wH`, `P = 1 + wH`, commuting) has `U^{13} ≠ 1`, `U^{14} ≠ 1`, `U^{182} ≠ 1`,440since `U^k = 1` exactly when `P^k = M^k`: neither cycle, nor their least common period, is its period (the exact441order `(13¹³ + 1)/2` is the package's certificate). -/442theorem mixed_step_values :443    Nat.lcm 13 14 = 182 ∧444    let H : Mat 13 2 := add (circMat 13 (kineticRow 13 2))445      ((List.range 13).map fun i => (List.range 13).map fun j => if i = j then ⟨ofNat i, 0⟩ else 0)446    let M : NMat := toN (add (ident 13) (neg (smul ⟨0, 1⟩ H)))447    let P : NMat := toN (add (ident 13) (smul ⟨0, 1⟩ H))448    mmulN 13 2 13 M P = mmulN 13 2 13 P M ∧ mpowN 13 2 13 P 13 ≠ mpowN 13 2 13 M 13 ∧449      mpowN 13 2 13 P 14 ≠ mpowN 13 2 13 M 14 ∧ mpowN 13 2 13 P 182 ≠ mpowN 13 2 13 M 182 := by450  decide +kernel451452/-- 8:D11 [value] — the spinor form transports by the norm of the lift: `S† X S = N(z) X` for `S = x I₄ + y γ⁰γ¹`,453`X = γ⁰γ¹γ³`, at `x = y = 1` (`N = 1 − ν = −1`) on `𝔽₁₃`, `𝔽₁₇₃` and `𝔽₁₅₄₉`. -/454theorem lift_transport_values :455    (dagger (spinLift 5 1 1) * (gamma0 5 * gamma1 5 * gamma3 5) * spinLift 5 1 1 : Mat 13 2) =456      smul (-1) (gamma0 5 * gamma1 5 * gamma3 5) ∧457    (dagger (spinLift 93 1 1) * (gamma0 93 * gamma1 93 * gamma3 93) * spinLift 93 1 1 : Mat 173 2) =458      smul (-1) (gamma0 93 * gamma1 93 * gamma3 93) ∧459    (dagger (spinLift 1461 1 1) * (gamma0 1461 * gamma1 1461 * gamma3 1461) * spinLift 1461 1 1 : Mat 1549 2) =460      smul (-1) (gamma0 1461 * gamma1 1461 * gamma3 1461) := by461  decide +kernel462463end witnesses464465end FRC.Dirac.Spinor466