Theme/Spin.lean — FrcCore

1import FrcCore.Theme.Extension2import FrcCore.Theme.Projective34/-!5# FrcCore.Theme.Spin — the frame group has one form (00:C27) and the adjoint action of `PGL₂` (00:C22)67The projective theme's second core file (20 October 2026; the master's witnesses, group C). On a prime shell `p = 4κ + 1`8with its quadratic extension `𝔽_{p²} = 𝔽_p[w]`, `w² = ν` a nonsquare and `w^p = −w` (the Frobenius conjugate of `w` is9`−w`):1011* **The unitary form is the frame group** (00:C27). For the Hermitian form `wJ`, `J = [[0, 1], [−1, 0]]`, a matrix of12  determinant one over `𝔽_{p²}` is unitary exactly when its entries are Frobenius-fixed, i.e. lie in `𝔽_p`:13  `SU₂(𝔽_{p²}/𝔽_p) = SL₂(𝔽_p)` on the nose (`su2_eq_sl2`); the form is Hermitian because `conj w = −w` and `Jᵀ = −J`14  (`hermitian_wJ`). The proof is the two-by-two identity `Mᵀ J M = det(M) J`: unitarity reads `adj(M̄) M = I`, which15  with `adj(M) M = I` forces `M̄ = M`. Every element of `SL₂(𝔽_p)` has finite order (`finite_order`): the powers of16  `M` take at most `p⁴` values, so two of them coincide, and the adjugate cancels. The quadric clause — the sphere17  `x² + y² + z² + w² = 1` and `ad − bc = 1` correspond point by point through the quarter-turn `r² = −1` — is18  `Theme/Projective.lean`'s `sphere_det` and `Theme/Hopf.lean`'s `quat_bijective` (38:A7).19* **The adjoint action** (00:C22). Conjugation `X ↦ M X adj(M)` preserves the determinant up to `det(M)²` and scales20  the trace by `det M` (`ad_preserves`): on `SL₂` it is an orthogonal map of the trace-zero matrices for the form21  `−det`, the map `PGL₂ → SO₃`. A matrix commuting with `J` and with `diag(1, −1)` is scalar on an odd shell22  (`ad_kernel`): the kernel of the adjoint action is the centre, the map is injective.2324The identities over `𝔽_{p²}` are decided by the ring normaliser of `Ring.lean`, lifted to pairs (`XR`: a symbolic25element of the extension, the variable `0` standing for `ν`) and to two-by-two matrices of pairs (`MX`), as26`Theme/Extension.lean` lifts it to quaternions. No axioms.27-/2829namespace FRC.Spin3031open FRC.Shell FRC.Shell.Frame FRC.Extension3233variable {p : Nat} [Pos p] {ν : Shell p}3435/-! ## The ring normaliser on the quadratic extension -/3637/-- A symbolic element of `𝔽_{p²}`: its two parts as ring expressions; the variable `0` is `ν`. -/38structure XR where39  re : RE40  im : RE4142namespace XR4344/-- The value, the parts evaluated. -/45def eval (env : Nat → Shell p) (z : XR) : Ext p ν := ⟨z.re.eval env, z.im.eval env⟩4647def add (z w : XR) : XR := ⟨.add z.re w.re, .add z.im w.im⟩48def neg (z : XR) : XR := ⟨.neg z.re, .neg z.im⟩49/-- `(a + b w)(c + d w) = (ac + ν bd) + (ad + bc) w`, `ν` the variable `0`. -/50def mul (z w : XR) : XR :=51  ⟨.add (.mul z.re w.re) (.mul (.var 0) (.mul z.im w.im)), .add (.mul z.re w.im) (.mul z.im w.re)⟩52/-- The Frobenius conjugate `w ↦ −w`. -/53def conj (z : XR) : XR := ⟨z.re, .neg z.im⟩54/-- The element of the variables `i, i + 1`. -/55def v (i : Nat) : XR := ⟨.var i, .var (i + 1)⟩56def zero : XR := ⟨.zero, .zero⟩57def one : XR := ⟨.one, .zero⟩5859def check (l r : XR) : Bool := RE.check l.re r.re && RE.check l.im r.im6061theorem sound (env : Nat → Shell p) (l r : XR) (h : check l r = true) : l.eval (ν := ν) env = r.eval env :=62  Ext.ext (RE.sound env _ _ (and_true_left h)) (RE.sound env _ _ (and_true_right h))6364end XR6566/-- A two-by-two matrix over `𝔽_{p²}`. -/67structure M2x (p : Nat) [Pos p] (ν : Shell p) where68  a : Ext p ν69  b : Ext p ν70  c : Ext p ν71  d : Ext p ν7273namespace M2x7475theorem ext' {M N : M2x p ν} (ha : M.a = N.a) (hb : M.b = N.b) (hc : M.c = N.c) (hd : M.d = N.d) : M = N := by76  cases M; cases N; cases ha; cases hb; cases hc; cases hd; rfl7778theorem ext'_a {M N : M2x p ν} (h : M = N) : M.a = N.a := by cases h; rfl79theorem ext'_b {M N : M2x p ν} (h : M = N) : M.b = N.b := by cases h; rfl80theorem ext'_c {M N : M2x p ν} (h : M = N) : M.c = N.c := by cases h; rfl81theorem ext'_d {M N : M2x p ν} (h : M = N) : M.d = N.d := by cases h; rfl8283def mul (M N : M2x p ν) : M2x p ν :=84  ⟨M.a * N.a + M.b * N.c, M.a * N.b + M.b * N.d, M.c * N.a + M.d * N.c, M.c * N.b + M.d * N.d⟩85/-- The transpose. -/86def tr (M : M2x p ν) : M2x p ν := ⟨M.a, M.c, M.b, M.d⟩87/-- The entrywise Frobenius conjugate. -/88def conj (M : M2x p ν) : M2x p ν := ⟨Ext.conj M.a, Ext.conj M.b, Ext.conj M.c, Ext.conj M.d⟩89/-- The adjoint `M† = M̄ᵀ`. -/90def dagger (M : M2x p ν) : M2x p ν := M.conj.tr91def det (M : M2x p ν) : Ext p ν := M.a * M.d + -(M.b * M.c)92def adj (M : M2x p ν) : M2x p ν := ⟨M.d, -M.b, -M.c, M.a⟩93/-- The Hermitian form `wJ = [[0, w], [−w, 0]]`. -/94def wJ (w : Ext p ν) : M2x p ν := ⟨0, w, -w, 0⟩95/-- `M` is unitary for the form `H`: `M† H M = H`. -/96def unitary (H M : M2x p ν) : Prop := (M.dagger.mul H).mul M = H9798end M2x99100/-- A symbolic two-by-two matrix over the extension. -/101structure MX where102  a : XR103  b : XR104  c : XR105  d : XR106107namespace MX108109def eval (env : Nat → Shell p) (M : MX) : M2x p ν := ⟨M.a.eval env, M.b.eval env, M.c.eval env, M.d.eval env⟩110def mul (M N : MX) : MX :=111  ⟨XR.add (XR.mul M.a N.a) (XR.mul M.b N.c), XR.add (XR.mul M.a N.b) (XR.mul M.b N.d),112   XR.add (XR.mul M.c N.a) (XR.mul M.d N.c), XR.add (XR.mul M.c N.b) (XR.mul M.d N.d)⟩113def tr (M : MX) : MX := ⟨M.a, M.c, M.b, M.d⟩114def conj (M : MX) : MX := ⟨M.a.conj, M.b.conj, M.c.conj, M.d.conj⟩115def det (M : MX) : XR := XR.add (XR.mul M.a M.d) (XR.neg (XR.mul M.b M.c))116/-- The matrix of the variables `i, …, i + 7`. -/117def v (i : Nat) : MX := ⟨XR.v i, XR.v (i + 2), XR.v (i + 4), XR.v (i + 6)⟩118def wJ (w : XR) : MX := ⟨XR.zero, w, XR.neg w, XR.zero⟩119120def check (L R : MX) : Bool := XR.check L.a R.a && XR.check L.b R.b && (XR.check L.c R.c && XR.check L.d R.d)121122theorem sound (env : Nat → Shell p) (L R : MX) (h : check L R = true) : L.eval (ν := ν) env = R.eval env :=123  M2x.ext' (XR.sound env _ _ (and_true_left (and_true_left h))) (XR.sound env _ _ (and_true_right (and_true_left h)))124    (XR.sound env _ _ (and_true_left (and_true_right h))) (XR.sound env _ _ (and_true_right (and_true_right h)))125126end MX127128/-- The environment of a matrix `M` (variables `1 … 8`), a second matrix `N` (`9 … 16`) and an element `w` (`17, 18`)129after `ν` (`0`). -/130def env (M N : M2x p ν) (w : Ext p ν) : Nat → Shell p :=131  look [ν, M.a.re, M.a.im, M.b.re, M.b.im, M.c.re, M.c.im, M.d.re, M.d.im,132        N.a.re, N.a.im, N.b.re, N.b.im, N.c.re, N.c.im, N.d.re, N.d.im, w.re, w.im]133134/-! ## The frame group has one form (00:C27) -/135136/-- `Mᵀ (wJ) M = det(M) · wJ`: the symplectic identity of two-by-two matrices, over the extension. -/137theorem tr_wJ_mul (M : M2x p ν) (w : Ext p ν) :138    (M.tr.mul (M2x.wJ w)).mul M = ⟨0, w * M.det, -(w * M.det), 0⟩ :=139  MX.sound (env M M w) (MX.mul (MX.mul (MX.tr (MX.v 1)) (MX.wJ (XR.v 17))) (MX.v 1))140    ⟨XR.zero, XR.mul (XR.v 17) (MX.det (MX.v 1)), XR.neg (XR.mul (XR.v 17) (MX.det (MX.v 1))), XR.zero⟩ (by decide +kernel)141142/-- `Nᵀ (wJ) M` entrywise, for two matrices `N = [[a', b'], [c', d']]` and `M = [[a, b], [c, d]]`. -/143theorem tr_wJ_mul' (M N : M2x p ν) (w : Ext p ν) :144    (N.tr.mul (M2x.wJ w)).mul M =145      ⟨w * (N.a * M.c + -(N.c * M.a)), w * (N.a * M.d + -(N.c * M.b)),146       w * (N.b * M.c + -(N.d * M.a)), w * (N.b * M.d + -(N.d * M.b))⟩ :=147  MX.sound (env M N w) (MX.mul (MX.mul (MX.tr (MX.v 9)) (MX.wJ (XR.v 17))) (MX.v 1))148    ⟨XR.mul (XR.v 17) (XR.add (XR.mul (XR.v 9) (XR.v 5)) (XR.neg (XR.mul (XR.v 13) (XR.v 1)))),149     XR.mul (XR.v 17) (XR.add (XR.mul (XR.v 9) (XR.v 7)) (XR.neg (XR.mul (XR.v 13) (XR.v 3)))),150     XR.mul (XR.v 17) (XR.add (XR.mul (XR.v 11) (XR.v 5)) (XR.neg (XR.mul (XR.v 15) (XR.v 1)))),151     XR.mul (XR.v 17) (XR.add (XR.mul (XR.v 11) (XR.v 7)) (XR.neg (XR.mul (XR.v 15) (XR.v 3))))⟩ (by decide +kernel)152153/-- The four recovery identities: with `E₁ = a'c − c'a`, `E₂ = a'd − c'b − 1`, `E₃ = d'a − b'c − 1`, `E₄ = b'd − d'b`,154each `x' − x` is a combination of `1 − det M` and the `Eᵢ`. -/155theorem recover (M N : M2x p ν) :156    N.a + -M.a = N.a * (1 + -M.det) + (M.a * (N.a * M.d + -(N.c * M.b) + -1) + -(M.b * (N.a * M.c + -(N.c * M.a)))) ∧157    N.c + -M.c = N.c * (1 + -M.det) + (M.c * (N.a * M.d + -(N.c * M.b) + -1) + -(M.d * (N.a * M.c + -(N.c * M.a)))) ∧158    N.b + -M.b = N.b * (1 + -M.det) + (M.a * (N.b * M.d + -(N.d * M.b)) + M.b * (N.d * M.a + -(N.b * M.c) + -1)) ∧159    N.d + -M.d = N.d * (1 + -M.det) + (M.d * (N.d * M.a + -(N.b * M.c) + -1) + M.c * (N.b * M.d + -(N.d * M.b))) :=160  let e : Nat → Shell p := env M N 0161  let a := XR.v 1; let b := XR.v 3; let c := XR.v 5; let d := XR.v 7162  let a' := XR.v 9; let b' := XR.v 11; let c' := XR.v 13; let d' := XR.v 15163  let dt := MX.det (MX.v 1)164  let E1 := XR.add (XR.mul a' c) (XR.neg (XR.mul c' a))165  let E2 := XR.add (XR.add (XR.mul a' d) (XR.neg (XR.mul c' b))) (XR.neg XR.one)166  let E3 := XR.add (XR.add (XR.mul d' a) (XR.neg (XR.mul b' c))) (XR.neg XR.one)167  let E4 := XR.add (XR.mul b' d) (XR.neg (XR.mul d' b))168  let one_det := XR.add XR.one (XR.neg dt)169  ⟨XR.sound e (XR.add a' (XR.neg a)) (XR.add (XR.mul a' one_det) (XR.add (XR.mul a E2) (XR.neg (XR.mul b E1)))) (by decide +kernel),170   XR.sound e (XR.add c' (XR.neg c)) (XR.add (XR.mul c' one_det) (XR.add (XR.mul c E2) (XR.neg (XR.mul d E1)))) (by decide +kernel),171   XR.sound e (XR.add b' (XR.neg b)) (XR.add (XR.mul b' one_det) (XR.add (XR.mul a E4) (XR.mul b E3))) (by decide +kernel),172   XR.sound e (XR.add d' (XR.neg d)) (XR.add (XR.mul d' one_det) (XR.add (XR.mul d E3) (XR.mul c E4))) (by decide +kernel)⟩173174theorem ext_mul_zero (a : Ext p ν) : a * 0 = 0 :=175  XR.sound (look [ν, a.re, a.im]) (XR.mul (XR.v 1) XR.zero) XR.zero (by decide +kernel)176177theorem ext_add_zero (a : Ext p ν) : a + 0 = a := Ext.ext (Shell.add_zero _) (Shell.add_zero _)178179theorem ext_neg_zero : (-0 : Ext p ν) = 0 := Ext.ext Shell.neg_zero Shell.neg_zero180181theorem ext_mul_neg (a b : Ext p ν) : a * -b = -(a * b) :=182  XR.sound (look [ν, a.re, a.im, b.re, b.im]) (XR.mul (XR.v 1) (XR.neg (XR.v 3))) (XR.neg (XR.mul (XR.v 1) (XR.v 3))) (by decide +kernel)183184theorem ext_eq_of_add_neg_eq_zero {x y : Ext p ν} (h : x + -y = 0) : x = y :=185  Ext.ext (eq_of_add_neg_eq_zero (congrArg Ext.re h)) (eq_of_add_neg_eq_zero (congrArg Ext.im h))186187theorem ext_add_neg_self (x : Ext p ν) : x + -x = 0 := Ext.ext (Shell.add_neg x.re) (Shell.add_neg x.im)188189theorem ext_norm_zero : Ext.norm (0 : Ext p ν) = 0 := by190  show (0 : Shell p) * 0 + -(ν * (0 * 0)) = 0191  rw [mul_zero, mul_zero, neg_zero, add_zero]192193/-- On a field shell with `ν` a nonsquare, the extension has no zero divisors: `w x = 0` and `w ≠ 0` give `x = 0`. -/194theorem ext_eq_zero_of_mul (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) {w x : Ext p ν} (hw : w ≠ 0)195    (h : w * x = 0) : x = 0 := by196  have hn : Ext.norm w * Ext.norm x = 0 := by rw [← Ext.norm_mul, h, ext_norm_zero]197  have nz : ∀ z : Ext p ν, Ext.norm z = 0 → z = 0 := fun z hz =>198    match Shell.instDecidableEq z.re 0, Shell.instDecidableEq z.im 0 with199    | isTrue h1, isTrue h2 => Ext.ext h1 h2200    | isTrue h1, isFalse h2 => absurd hz (K.norm_ne_zero hν (Or.inr h2))201    | isFalse h1, _ => absurd hz (K.norm_ne_zero hν (Or.inl h1))202  exact match K.mul_eq_zero hn with203    | Or.inl e => absurd (nz w e) hw204    | Or.inr e => nz x e205206/-- 00:C27 — the form `wJ` is Hermitian: `(wJ)† = wJ`, because `conj w = −w` (`w^p = −w`) and `Jᵀ = −J`. -/207theorem hermitian_wJ {w : Ext p ν} (hw : Ext.conj w = -w) : (M2x.wJ w).dagger = M2x.wJ w := by208  have c0 : Ext.conj (0 : Ext p ν) = 0 := Ext.ext rfl Shell.neg_zero209  have cn : Ext.conj (-w) = w := by210    have e : Ext.conj (-w) = -(Ext.conj w) := rfl211    rw [e, hw]; exact Ext.ext (Shell.neg_neg w.re) (Shell.neg_neg w.im)212  exact M2x.ext' c0 cn (by show Ext.conj w = -w; exact hw) c0213214/-- 00:C27 — **the frame group has one form.** On a field shell, `ν` a nonsquare and `w ≠ 0` (the form `wJ` is Hermitian215for `conj w = −w`, `hermitian_wJ`): a matrix over `𝔽_{p²}` of determinant one is unitary for `wJ` exactly when its216entries are fixed by the Frobenius conjugation, i.e. lie in `𝔽_p` — `SU₂(𝔽_{p²}/𝔽_p) = SL₂(𝔽_p)`. -/217theorem su2_eq_sl2 (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) {w : Ext p ν} (hw0 : w ≠ 0)218    (M : M2x p ν) (hdet : M.det = 1) : M2x.unitary (M2x.wJ w) M ↔ M.conj = M := by219  constructor220  · intro hu221    have h := hu222    unfold M2x.unitary M2x.dagger at h223    rw [tr_wJ_mul' M M.conj w] at h224    have ha := M2x.ext'_a h; have hb := M2x.ext'_b h; have hc := M2x.ext'_c h; have hd := M2x.ext'_d h225    simp only [M2x.conj, M2x.wJ] at ha hb hc hd226    -- the four equations after cancelling `w`227    have E1 : Ext.conj M.a * M.c + -(Ext.conj M.c * M.a) = 0 := ext_eq_zero_of_mul K hν hw0 ha228    have E2 : Ext.conj M.a * M.d + -(Ext.conj M.c * M.b) + -1 = 0 := by229      have : w * (Ext.conj M.a * M.d + -(Ext.conj M.c * M.b) + -1) = 0 := by230        rw [ext_mul_add, hb, ext_mul_neg, Ext.mul_one]; exact ext_add_neg_self w231      exact ext_eq_zero_of_mul K hν hw0 this232    have E3 : Ext.conj M.d * M.a + -(Ext.conj M.b * M.c) + -1 = 0 := by233      have : w * (Ext.conj M.d * M.a + -(Ext.conj M.b * M.c) + -1) = 0 := by234        have e : w * (Ext.conj M.d * M.a + -(Ext.conj M.b * M.c) + -1) =235            -(w * (Ext.conj M.b * M.c + -(Ext.conj M.d * M.a))) + -w :=236          XR.sound (env M M.conj w)237            (XR.mul (XR.v 17) (XR.add (XR.add (XR.mul (XR.v 15) (XR.v 1)) (XR.neg (XR.mul (XR.v 11) (XR.v 5)))) (XR.neg XR.one)))238            (XR.add (XR.neg (XR.mul (XR.v 17) (XR.add (XR.mul (XR.v 11) (XR.v 5)) (XR.neg (XR.mul (XR.v 15) (XR.v 1)))))) (XR.neg (XR.v 17)))239            (by decide +kernel)240        rw [e, hc]241        exact Ext.ext (Shell.neg_add _ ) (Shell.neg_add _)242      exact ext_eq_zero_of_mul K hν hw0 this243    have E4 : Ext.conj M.b * M.d + -(Ext.conj M.d * M.b) = 0 := ext_eq_zero_of_mul K hν hw0 hd244    obtain ⟨ra, rc, rb, rd⟩ := recover M M.conj245    have hz : (1 : Ext p ν) + -M.det = 0 := by rw [hdet]; exact ext_add_neg_self 1246    simp only [M2x.conj] at ra rc rb rd247    rw [hz, E1, E2, ext_mul_zero, ext_mul_zero, ext_mul_zero, ext_neg_zero, ext_add_zero, ext_add_zero] at ra rc248    rw [hz, E3, E4, ext_mul_zero, ext_mul_zero, ext_mul_zero, ext_add_zero, ext_add_zero] at rb rd249    exact M2x.ext' (ext_eq_of_add_neg_eq_zero ra) (ext_eq_of_add_neg_eq_zero rb)250      (ext_eq_of_add_neg_eq_zero rc) (ext_eq_of_add_neg_eq_zero rd)251  · intro hM252    show (M.conj.tr.mul (M2x.wJ w)).mul M = M2x.wJ w253    rw [hM, tr_wJ_mul, hdet, Ext.mul_one]254    rfl255256/-! ## The sphere is `SL₂`, point by point (00:C27, 00:C22) -/257258/-- 00:C27, 00:C22 — the quaternion map is a bijection of `𝔽_p⁴` onto `M₂` on a field shell with `r² = −1` and `2h = 1`, the259inverse `M ↦ ((a + d) h, (a − d)(−r) h, (b − c) h, (b + c)(−r) h)`: with `sphere_det`, the norm-one sphere is the whole of260`SL₂`, point by point through the quarter-turn. The projective theme's statement of `Theme/Hopf.lean`'s `quat_bijective`261(38:A7, the subject theme), so that the master's keys of C22 and C27 ride on the projective theme (20 October 2026). -/262theorem sphere_bijective (K : Fld p) {r h : Shell p} (hr : r * r = -1) (h2 : (1 + 1) * h = 1) :263    (∀ M : M2 p, quat r ((M.a + M.d) * h) ((M.a + -M.d) * (-r * h)) ((M.b + -M.c) * h) ((M.b + M.c) * (-r * h)) = M) ∧264    (∀ x y z w x' y' z' w' : Shell p, quat r x y z w = quat r x' y' z' w' → x = x' ∧ y = y' ∧ z = z' ∧ w = w') := by265  have ca : ∀ a d : Shell p, (a + d) * h + r * ((a + -d) * (-r * h)) = a := fun a d => by266    have e1 : (a + d) * h + r * ((a + -d) * (-r * h)) = (a + d) * h + -(r * r) * ((a + -d) * h) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h, r]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.mul (.var 3) (.mul (.add (.var 0) (.neg (.var 1))) (.mul (.neg (.var 3)) (.var 2))))) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)))) (by decide +kernel)267    have e2 : (a + d) * h + (a + -d) * h = a * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.var 0) (.mul (.add .one .one) (.var 2))) (by decide +kernel)268    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]269  have cd : ∀ a d : Shell p, (a + d) * h + -(r * ((a + -d) * (-r * h))) = d := fun a d => by270    have e1 : (a + d) * h + -(r * ((a + -d) * (-r * h))) = (a + d) * h + -(-(r * r) * ((a + -d) * h)) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h, r]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.neg (.mul (.var 3) (.mul (.add (.var 0) (.neg (.var 1))) (.mul (.neg (.var 3)) (.var 2)))))) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.neg (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))))) (by decide +kernel)271    have e2 : (a + d) * h + -((a + -d) * h) = d * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [a, d, h]) (.add (.mul (.add (.var 0) (.var 1)) (.var 2)) (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)))) (.mul (.var 1) (.mul (.add .one .one) (.var 2))) (by decide +kernel)272    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]273  have cb : ∀ b c : Shell p, (b + -c) * h + r * ((b + c) * (-r * h)) = b := fun b c => by274    have e1 : (b + -c) * h + r * ((b + c) * (-r * h)) = (b + -c) * h + -(r * r) * ((b + c) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h, r]) (.add (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)) (.mul (.var 3) (.mul (.add (.var 0) (.var 1)) (.mul (.neg (.var 3)) (.var 2))))) (.add (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)) (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.var 1)) (.var 2)))) (by decide +kernel)275    have e2 : (b + -c) * h + (b + c) * h = b * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h]) (.add (.mul (.add (.var 0) (.neg (.var 1))) (.var 2)) (.mul (.add (.var 0) (.var 1)) (.var 2))) (.mul (.var 0) (.mul (.add .one .one) (.var 2))) (by decide +kernel)276    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]277  have cc : ∀ b c : Shell p, -((b + -c) * h) + r * ((b + c) * (-r * h)) = c := fun b c => by278    have e1 : -((b + -c) * h) + r * ((b + c) * (-r * h)) = -((b + -c) * h) + -(r * r) * ((b + c) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h, r]) (.add (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.var 3) (.mul (.add (.var 0) (.var 1)) (.mul (.neg (.var 3)) (.var 2))))) (.add (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.neg (.mul (.var 3) (.var 3))) (.mul (.add (.var 0) (.var 1)) (.var 2)))) (by decide +kernel)279    have e2 : -((b + -c) * h) + (b + c) * h = c * ((1 + 1) * h) := Shell.Frame.RE.sound (Shell.Frame.look [b, c, h]) (.add (.neg (.mul (.add (.var 0) (.neg (.var 1))) (.var 2))) (.mul (.add (.var 0) (.var 1)) (.var 2))) (.mul (.var 1) (.mul (.add .one .one) (.var 2))) (by decide +kernel)280    rw [e1, hr, neg_neg, one_mul, e2, h2, mul_one]281  have h2ne : (1 + 1 : Shell p) ≠ 0 := fun h0 => K.one_ne_zero (by rw [← h2, h0, zero_mul])282  have hrne : r ≠ 0 := fun h0 => K.one_ne_zero (by283    have := hr; rw [h0, zero_mul] at this; rw [← neg_neg (1 : Shell p), ← this, neg_zero])284  have ex : ∀ x y : Shell p, (1 + 1) * x = (x + r * y) + (x + -(r * y)) := fun x y => Shell.Frame.RE.sound (Shell.Frame.look [x, y, r]) (.mul (.add .one .one) (.var 0)) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.add (.var 0) (.neg (.mul (.var 2) (.var 1))))) (by decide +kernel)285  have ey : ∀ x y : Shell p, (1 + 1) * (r * y) = (x + r * y) + -(x + -(r * y)) := fun x y => Shell.Frame.RE.sound (Shell.Frame.look [x, y, r]) (.mul (.add .one .one) (.mul (.var 2) (.var 1))) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.neg (.add (.var 0) (.neg (.mul (.var 2) (.var 1)))))) (by decide +kernel)286  have ew : ∀ z w : Shell p, (1 + 1) * (r * w) = (z + r * w) + (-z + r * w) := fun z w => Shell.Frame.RE.sound (Shell.Frame.look [z, w, r]) (.mul (.add .one .one) (.mul (.var 2) (.var 1))) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.add (.neg (.var 0)) (.mul (.var 2) (.var 1)))) (by decide +kernel)287  have ez : ∀ z w : Shell p, (1 + 1) * z = (z + r * w) + -(-z + r * w) := fun z w => Shell.Frame.RE.sound (Shell.Frame.look [z, w, r]) (.mul (.add .one .one) (.var 0)) (.add (.add (.var 0) (.mul (.var 2) (.var 1))) (.neg (.add (.neg (.var 0)) (.mul (.var 2) (.var 1))))) (by decide +kernel)288  refine ⟨fun M => M2.ext' (ca M.a M.d) (cb M.b M.c) (cc M.b M.c) (cd M.a M.d), fun x y z w x' y' z' w' e => ?_⟩289  have ha : x + r * y = x' + r * y' := M2.ext'_a e290  have hb : z + r * w = z' + r * w' := M2.ext'_b e291  have hc : -z + r * w = -z' + r * w' := M2.ext'_c e292  have hd : x + -(r * y) = x' + -(r * y') := M2.ext'_d e293  refine ⟨K.mul_left_cancel h2ne (by rw [ex x y, ex x' y', ha, hd]),294    K.mul_left_cancel hrne (K.mul_left_cancel h2ne (by rw [ey x y, ey x' y', ha, hd])),295    K.mul_left_cancel h2ne (by rw [ez z w, ez z' w', hb, hc]),296    K.mul_left_cancel hrne (K.mul_left_cancel h2ne (by rw [ew z w, ew z' w', hb, hc]))⟩297298/-! ## Every element of the frame group has finite order (00:C27) -/299300/-- The identity matrix. -/301def I : M2 p := ⟨1, 0, 0, 1⟩302303/-- Powers of a matrix, `M⁰ = I`, `M^{n+1} = Mⁿ · M`. -/304def mpow (M : M2 p) : Nat → M2 p305  | 0 => I306  | n + 1 => (mpow M n).mul M307308theorem smul_one' (M : M2 p) : M2.smul 1 M = M :=309  M2.ext' (one_mul _) (one_mul _) (one_mul _) (one_mul _)310311theorem I_mul (M : M2 p) : I.mul M = M := by rw [I, M2.diag_mul, smul_one']312313theorem mul_I (M : M2 p) : M.mul I = M := by rw [I, M2.mul_diag, smul_one']314315theorem mpow_succ_left (M : M2 p) : ∀ n, mpow M (n + 1) = M.mul (mpow M n)316  | 0 => by show I.mul M = M.mul I; rw [I_mul, mul_I]317  | n + 1 => by show (mpow M (n + 1)).mul M = M.mul ((mpow M n).mul M); rw [mpow_succ_left M n, M2.mul_assoc']318319theorem mpow_add (M : M2 p) (m : Nat) : ∀ n, mpow M (m + n) = (mpow M m).mul (mpow M n)320  | 0 => by show mpow M m = (mpow M m).mul I; rw [mul_I]321  | n + 1 => by322    show (mpow M (m + n)).mul M = (mpow M m).mul ((mpow M n).mul M)323    rw [mpow_add M m n, M2.mul_assoc']324325/-- With `det M = 1`, `adj(M)ⁱ Mⁱ = I` for every `i`. -/326theorem adj_mpow_mul (M : M2 p) (hdet : M.det = 1) : ∀ i, (mpow M.adj i).mul (mpow M i) = I327  | 0 => by show I.mul I = I; exact I_mul I328  | i + 1 => by329    rw [mpow_succ_left M i]330    show ((mpow M.adj i).mul M.adj).mul (M.mul (mpow M i)) = I331    rw [M2.mul_assoc', ← M2.mul_assoc' M.adj, M2.adj_mul, hdet]332    show (mpow M.adj i).mul (I.mul (mpow M i)) = I333    rw [I_mul]; exact adj_mpow_mul M hdet i334335/-- The mixed-radix code of a matrix, below `p⁴`. -/336def code (M : M2 p) : Nat := M.a.val + p * (M.b.val + p * (M.c.val + p * M.d.val))337338omit [Pos p] in339theorem digit_lt {x X q : Nat} (hx : x < p) (hX : X < q) : x + p * X < p * q := by340  have h1 : x + p * X < p + p * X := Nat.add_lt_add_right hx _341  have h2 : p + p * X = p * (X + 1) := by rw [Nat.mul_succ, Nat.add_comm]342  rw [h2] at h1343  exact Nat.lt_of_lt_of_le h1 (Nat.mul_le_mul_left p (Nat.succ_le_of_lt hX))344345theorem code_lt (M : M2 p) : code M < p * (p * (p * p)) :=346  digit_lt M.a.lt (digit_lt M.b.lt (digit_lt M.c.lt M.d.lt))347348omit [Pos p] in349theorem digit_inj {x x' X X' : Nat} (hx : x < p) (hx' : x' < p) (h : x + p * X = x' + p * X') : x = x' ∧ X = X' := by350  have h' : p * X + x = p * X' + x' := by rw [Nat.add_comm, h, Nat.add_comm]351  have hX : X = X' := FRC.Nat.quot_unique hx hx' h'352  refine ⟨?_, hX⟩353  rw [hX] at h354  exact Nat.add_right_cancel h355356theorem code_inj {M N : M2 p} (h : code M = code N) : M = N := by357  have ⟨ha, h1⟩ := digit_inj M.a.lt N.a.lt h358  have ⟨hb, h2⟩ := digit_inj M.b.lt N.b.lt h1359  have ⟨hc, hd⟩ := digit_inj M.c.lt N.c.lt h2360  exact M2.ext' (Shell.ext ha) (Shell.ext hb) (Shell.ext hc) (Shell.ext hd)361362/-- A bounded search: some `i < n` has `f i = true`. -/363def anyLt (f : Nat → Bool) : Nat → Bool364  | 0 => false365  | n + 1 => anyLt f n || f n366367theorem anyLt_true {f : Nat → Bool} : ∀ {n}, anyLt f n = true → ∃ i, i < n ∧ f i = true368  | 0, h => nomatch h369  | n + 1, h =>370    match hn : anyLt f n, hf : f n with371    | true, _ => match anyLt_true hn with | ⟨i, hi, e⟩ => ⟨i, Nat.lt_succ_of_lt hi, e⟩372    | false, true => ⟨n, Nat.lt_succ_self n, hf⟩373    | false, false => by374      have h' : (anyLt f n || f n) = true := h375      rw [hn, hf] at h'376      exact nomatch h'377378theorem anyLt_false {f : Nat → Bool} : ∀ {n}, anyLt f n = false → ∀ i, i < n → f i = false379  | 0, _, i, hi => absurd hi (Nat.not_lt_zero i)380  | n + 1, h, i, hi =>381    have h' : (anyLt f n || f n) = false := h382    have hn : anyLt f n = false := by383      match e : anyLt f n with384      | false => rfl385      | true => rw [e] at h'; exact nomatch h'386    have hf : f n = false := by rw [hn] at h'; exact h'387    match Nat.lt_or_ge i n with388    | Or.inl hlt => anyLt_false hn i hlt389    | Or.inr hge => (Nat.le_antisymm (Nat.le_of_lt_succ hi) hge) ▸ hf390391/-- The pigeonhole on a sequence: `N + 1` values below `N` collide. -/392theorem collide (σ : Nat → Nat) (N : Nat) (hb : ∀ k, k ≤ N → σ k < N) : ∃ i j, i < j ∧ j ≤ N ∧ σ i = σ j := by393  match hs : anyLt (fun j => anyLt (fun i => decide (σ i = σ j)) j) (N + 1) with394  | true =>395    match anyLt_true hs with396    | ⟨j, hj, hj'⟩ => match anyLt_true hj' with397      | ⟨i, hi, e⟩ => exact ⟨i, j, hi, Nat.le_of_lt_succ hj, of_decide_eq_true e⟩398  | false =>399    have inj : ∀ i j, i < N + 1 → j < N + 1 → σ i = σ j → i = j := fun i j hi hj e =>400      match Nat.lt_or_ge i j with401      | Or.inl hlt => absurd (decide_eq_true e) (by rw [anyLt_false (anyLt_false hs j hj) i hlt]; decide)402      | Or.inr hge => match Nat.lt_or_ge j i with403        | Or.inl hlt => absurd (decide_eq_true e.symm) (by rw [anyLt_false (anyLt_false hs i hi) j hlt]; decide)404        | Or.inr hge' => Nat.le_antisymm hge' hge405    have nd := imageList_nodup inj (Nat.le_refl (N + 1))406    have hlt : ∀ e, Pigeonhole.mem e (imageList σ (N + 1)) → e < N := fun e he =>407      match mem_imageList he with408      | ⟨j, hj, ej⟩ => by rw [← ej]; exact hb j (Nat.le_of_lt_succ hj)409    have := Pigeonhole.length_le_of_nodup_lt N _ nd hlt410    rw [imageList_length] at this411    exact absurd this (Nat.not_succ_le_self N)412413/-- 00:C27 — every element of `SL₂` has finite order: with `det M = 1` some positive `n ≤ p⁴` has `Mⁿ = I` — the `p⁴ + 1`414powers `M⁰, …, M^{p⁴}` cannot be distinct, and the adjugate cancels the common factor. -/415theorem finite_order (M : M2 p) (hdet : M.det = 1) : ∃ n, 0 < n ∧ n ≤ p * (p * (p * p)) ∧ mpow M n = I := by416  match collide (fun k => code (mpow M k)) (p * (p * (p * p))) (fun k _ => code_lt (mpow M k)) with417  | ⟨i, j, hij, hjN, e⟩ =>418    have hpow : mpow M i = mpow M j := code_inj e419    have hj : j = i + (j - i) := (FRC.Nat.add_sub_of_le (Nat.le_of_lt hij)).symm420    have hpos : 0 < j - i := by                             -- without `Nat.sub_pos_of_lt`, which carries propext421      match e : j - i with422      | 0 =>423        have hji : j = i := by rw [e, Nat.add_zero] at hj; exact hj424        exact absurd (hji ▸ hij) (Nat.lt_irrefl i)425      | k + 1 => exact Nat.zero_lt_succ k426    refine ⟨j - i, hpos, Nat.le_trans (Nat.sub_le j i) hjN, ?_⟩427    have h1 : (mpow M i).mul (mpow M (j - i)) = (mpow M i).mul I := by428      rw [← mpow_add, ← hj, ← hpow, mul_I]429    have h2 := congrArg (fun X => (mpow M.adj i).mul X) h1430    rw [← M2.mul_assoc', ← M2.mul_assoc', adj_mpow_mul M hdet i, I_mul, I_mul] at h2431    exact h2432433/-! ## The adjoint action of `PGL₂` (00:C22) -/434435/-- 00:C22 — conjugation `X ↦ M X adj(M)` multiplies the determinant by `det(M)²` and the trace by `det M`: on `SL₂`436it preserves `−det` on the trace-zero matrices — the map `PGL₂(𝔽_p) → SO₃(𝔽_p)` of the row. -/437theorem ad_preserves (M X : M2 p) :438    ((M.mul X).mul M.adj).det = M.det * M.det * X.det ∧439    ((M.mul X).mul M.adj).a + ((M.mul X).mul M.adj).d = M.det * (X.a + X.d) :=440  ⟨RE.sound (look [M.a, M.b, M.c, M.d, X.a, X.b, X.c, X.d]) (.add (.mul (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 6))) (.var 3)) (.mul (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 7))) (.neg (.var 2)))) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) (.var 6))) (.neg (.var 1))) (.mul (.add (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 7))) (.var 0)))) (.neg (.mul (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 6))) (.neg (.var 1))) (.mul (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 7))) (.var 0))) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) (.var 6))) (.var 3)) (.mul (.add (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 7))) (.neg (.var 2))))))) (.mul (.mul (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2))))) (.add (.mul (.var 4) (.var 7)) (.neg (.mul (.var 5) (.var 6))))) (by decide +kernel),441   RE.sound (look [M.a, M.b, M.c, M.d, X.a, X.b, X.c, X.d]) (.add (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 6))) (.var 3)) (.mul (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 7))) (.neg (.var 2)))) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) (.var 6))) (.neg (.var 1))) (.mul (.add (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 7))) (.var 0)))) (.mul (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (.add (.var 4) (.var 7))) (by decide +kernel)⟩442443/-- The quarter-turn matrix `J = [[0, 1], [−1, 0]]` and the reflection `D = diag(1, −1)`. -/444def J : M2 p := ⟨0, 1, -1, 0⟩445def D : M2 p := ⟨1, 0, 0, -1⟩446447/-- 00:C22 — the kernel of the adjoint action is the centre: on a frame (an odd shell) a matrix commuting with `J` and448with `D` is scalar, `b = c = 0` and `a = d`; so `PGL₂ → SO₃` is injective. -/449theorem ad_kernel {κ : Nat} {g : Shell p} (F : Frame p κ g) (M : M2 p) (hJ : M.mul J = J.mul M) (hD : M.mul D = D.mul M) :450    M.b = 0 ∧ M.c = 0 ∧ M.a = M.d := by451  have ja : -M.b = M.c := by452    have e : M.a * 0 + M.b * -1 = 0 * M.a + 1 * M.c := M2.ext'_a hJ453    rw [mul_zero, zero_add, ← mul_neg, mul_one, zero_mul, zero_add, one_mul] at e454    exact e455  have jb : M.a = M.d := by456    have e : M.a * 1 + M.b * 0 = 0 * M.b + 1 * M.d := M2.ext'_b hJ457    rw [mul_one, mul_zero, add_zero, zero_mul, zero_add, one_mul] at e458    exact e459  have db : -M.b = M.b := by460    have e : M.a * 0 + M.b * -1 = 1 * M.b + 0 * M.d := M2.ext'_b hD461    rw [mul_zero, zero_add, ← mul_neg, mul_one, one_mul, zero_mul, add_zero] at e462    exact e463  have hb : M.b = 0 := by464    have h2 : (1 + 1) * M.b = 0 := by465      rw [right_distrib, one_mul]466      have e : M.b + M.b = -M.b + M.b := congrArg (fun x => x + M.b) db.symm467      rw [e]; exact Shell.neg_add M.b468    exact match F.mul_eq_zero h2 with469      | Or.inl h => absurd (by rw [two_eq_one_add_one]; exact h) F.two_ne_zero470      | Or.inr h => h471  exact ⟨hb, by rw [← ja, hb, neg_zero], jb⟩472473end FRC.Spin474