Theme/Unitary.lean — FrcCore

1import FrcCore.Ring2import FrcCore.Theme.Quadratic34/-!5# FrcCore.Theme.Unitary — SU(3) of a three-form over the quadratic extension, by elements (task LM41)67The exact clauses of master row G4 (p00069, 27:C7), stated by elements and never by counting the group (decision Q20).89* **The rank forced as the minimal triality frame.** Take a shell without zero divisors whose base has no root of10  `x² + x + 1`. On a prime `Ω > 3` with a quarter-turn this is B5's structural face, which holds iff `Ω ≡ 5 (mod 12)`11  (p00015, `Carrier.substrate_shell`). Then `−3` is not a square, so `Ext p (−3)` is the quadratic extension, and12  `ω = −h + h w` with `h = 1/2` is a root there. Every root `ω` of `x² + x + 1` in an extension `Ext p ν` lies off the13  base, has `ω̄ = ω²` and norm one, and `ωⁿ = 1` exactly when `3 ∣ n` (`triality_frame`). The scalar `ω Iₙ` is unitary14  for every `n`, since `ω̄ ω = 1`. Its determinant is `ωⁿ`, which is one exactly when `3 ∣ n`, so `n = 3` is the least15  rank whose special unitary group holds the triality scalar. At `n = 3` the scalar `ω I₃` lies in `SU(H)` for every16  three-form `H`. The file imports neither the Carrier nor the prime field, so that the interactions key file can bind17  it within the closure budget (G10). The binding supplies the hypotheses: `Shell.Prime.mul_eq_zero` (or a frame's18  `mul_eq_zero`) for the zero divisors, p00015 for the missing root, and `Carrier.csq` for the half.19* **The group of a three-form.** Over `Ext p ν`, the `3 × 3` matrices `U` with `U† H U = H` and `det U = 1` hold the20  identity and every scalar `c I₃` with `c̄ c = 1` and `c³ = 1`. They are closed under the product, and each has its21  adjugate as a two-sided inverse in the same set (`su_group`). The proof never uses `H† = H`, so it holds for the22  Hermitian forms of the row in particular.2324The identities over the extension are decided by a copy of the base normaliser's evaluation (`Ring.lean`) read in25`Ext p ν`. Its expansion and comparison are the base's, unchanged. Matrix associativity, `(AB)† = B†A†`,26`det (AB) = det A det B`, `U adj U = adj U U = det U · I` and `det (adj U) = (det U)²` are its instances. No axioms.27-/2829namespace FRC.Unitary3031open FRC.Shell FRC.Shell.Frame FRC.Extension3233variable {p : Nat} [Pos p] {ν : Shell p}3435/-! ## The ring laws of the quadratic extension, on components -/3637theorem x_add_comm (a b : Ext p ν) : a + b = b + a := Ext.ext (Shell.add_comm _ _) (Shell.add_comm _ _)38theorem x_add_assoc (a b c : Ext p ν) : a + b + c = a + (b + c) := Ext.ext (Shell.add_assoc _ _ _) (Shell.add_assoc _ _ _)39theorem x_add_left_comm (a b c : Ext p ν) : a + (b + c) = b + (a + c) :=40  Ext.ext (Shell.add_left_comm _ _ _) (Shell.add_left_comm _ _ _)41theorem x_zero_add (a : Ext p ν) : 0 + a = a := Ext.ext (Shell.zero_add _) (Shell.zero_add _)42theorem x_add_zero (a : Ext p ν) : a + 0 = a := Ext.ext (Shell.add_zero _) (Shell.add_zero _)43theorem x_neg_add (a : Ext p ν) : -a + a = 0 := Ext.ext (Shell.neg_add _) (Shell.neg_add _)44theorem x_neg_neg (a : Ext p ν) : - -a = a := Ext.ext (Shell.neg_neg _) (Shell.neg_neg _)45theorem x_neg_zero : (-0 : Ext p ν) = 0 := Ext.ext Shell.neg_zero Shell.neg_zero46theorem x_neg_add_rev (a b : Ext p ν) : -(a + b) = -a + -b := Ext.ext (Shell.neg_add_rev _ _) (Shell.neg_add_rev _ _)47theorem x_add_right_cancel {a b c : Ext p ν} (h : a + c = b + c) : a = b :=48  Ext.ext (Shell.add_right_cancel (Ext.re_congr h : a.re + c.re = b.re + c.re))49    (Shell.add_right_cancel (Ext.im_congr h : a.im + c.im = b.im + c.im))5051theorem x_zero_mul (a : Ext p ν) : 0 * a = 0 :=52  Ext.ext (RE.sound (look [ν, a.re, a.im]) (.add (.mul .zero (.var 1)) (.mul (.var 0) (.mul .zero (.var 2)))) .zero (by decide +kernel))53    (RE.sound (look [ν, a.re, a.im]) (.add (.mul .zero (.var 2)) (.mul .zero (.var 1))) .zero (by decide +kernel))5455theorem x_left_distrib (a b c : Ext p ν) : a * (b + c) = a * b + a * c :=56  Ext.ext (RE.sound (look [ν, a.re, a.im, b.re, b.im, c.re, c.im]) (.add (.mul (.var 1) (.add (.var 3) (.var 5))) (.mul (.var 0) (.mul (.var 2) (.add (.var 4) (.var 6))))) (.add (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4)))) (.add (.mul (.var 1) (.var 5)) (.mul (.var 0) (.mul (.var 2) (.var 6))))) (by decide +kernel))57    (RE.sound (look [ν, a.re, a.im, b.re, b.im, c.re, c.im]) (.add (.mul (.var 1) (.add (.var 4) (.var 6))) (.mul (.var 2) (.add (.var 3) (.var 5)))) (.add (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3))) (.add (.mul (.var 1) (.var 6)) (.mul (.var 2) (.var 5)))) (by decide +kernel))5859theorem x_neg_mul (a b : Ext p ν) : -(a * b) = -a * b :=60  Ext.ext (RE.sound (look [ν, a.re, a.im, b.re, b.im]) (.neg (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4))))) (.add (.mul (.neg (.var 1)) (.var 3)) (.mul (.var 0) (.mul (.neg (.var 2)) (.var 4)))) (by decide +kernel))61    (RE.sound (look [ν, a.re, a.im, b.re, b.im]) (.neg (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3)))) (.add (.mul (.neg (.var 1)) (.var 4)) (.mul (.neg (.var 2)) (.var 3))) (by decide +kernel))6263theorem x_mul_zero (a : Ext p ν) : a * 0 = 0 := by rw [Ext.mul_comm]; exact x_zero_mul a64theorem x_right_distrib (a b c : Ext p ν) : (a + b) * c = a * c + b * c := by65  rw [Ext.mul_comm (a + b) c, x_left_distrib, Ext.mul_comm c a, Ext.mul_comm c b]66theorem x_mul_neg (a b : Ext p ν) : -(a * b) = a * -b := by rw [Ext.mul_comm a b, x_neg_mul, Ext.mul_comm (-b) a]67theorem x_neg_mul_neg (a b : Ext p ν) : -a * -b = a * b := by rw [← x_neg_mul, ← x_mul_neg, x_neg_neg]68theorem x_mul_left_comm (a b c : Ext p ν) : a * (b * c) = b * (a * c) := by69  rw [← Ext.mul_assoc, Ext.mul_comm a b, Ext.mul_assoc]7071/-- Conjugation is additive. -/72theorem conj_add (a b : Ext p ν) : Ext.conj (a + b) = Ext.conj a + Ext.conj b := Ext.ext rfl (Shell.neg_add_rev _ _)7374/-! ## The normaliser read in the extension7576The expansion `RE.toP`, the normal form `nfP` and the comparison `pbeq` are the base's (`Ring.lean`). Only the evaluation77changes: an expression is read in `Ext p ν`, and soundness follows from the ring laws above. -/7879/-- An expression of the normaliser evaluated in the extension. -/80def xeval (env : Nat → Ext p ν) : RE → Ext p ν81  | .var i => env i82  | .zero => 083  | .one => 184  | .add a b => xeval env a + xeval env b85  | .mul a b => xeval env a * xeval env b86  | .neg a => -(xeval env a)8788/-- The assignment of extension values to the variables `0, 1, 2, …` of an expression. -/89def xlook : List (Ext p ν) → Nat → Ext p ν90  | [], _ => 091  | x :: _, 0 => x92  | _ :: l, n + 1 => xlook l n9394def xmEval (env : Nat → Ext p ν) : List Nat → Ext p ν95  | [] => 196  | i :: m => env i * xmEval env m9798def xpEval (env : Nat → Ext p ν) : List (List Nat) → Ext p ν99  | [] => 0100  | m :: P => xmEval env m + xpEval env P101102theorem xmEval_append (env : Nat → Ext p ν) (m n : List Nat) : xmEval env (m ++ n) = xmEval env m * xmEval env n := by103  induction m with104  | nil => exact (Ext.one_mul _).symm105  | cons i m ih => show env i * xmEval env (m ++ n) = env i * xmEval env m * xmEval env n; rw [ih, Ext.mul_assoc]106107theorem xpEval_append (env : Nat → Ext p ν) (P Q : List (List Nat)) :108    xpEval env (P ++ Q) = xpEval env P + xpEval env Q := by109  induction P with110  | nil => exact (x_zero_add _).symm111  | cons m P ih =>112    show xmEval env m + xpEval env (P ++ Q) = xmEval env m + xpEval env P + xpEval env Q; rw [ih, x_add_assoc]113114theorem xpEval_row (env : Nat → Ext p ν) (m : List Nat) (Q : List (List Nat)) :115    xpEval env (pRow m Q) = xmEval env m * xpEval env Q := by116  induction Q with117  | nil => exact (x_mul_zero _).symm118  | cons n Q ih =>119    show xmEval env (m ++ n) + xpEval env (pRow m Q) = xmEval env m * (xmEval env n + xpEval env Q)120    rw [ih, xmEval_append, x_left_distrib]121122theorem xpEval_mul (env : Nat → Ext p ν) (P Q : List (List Nat)) :123    xpEval env (pMul P Q) = xpEval env P * xpEval env Q := by124  induction P with125  | nil => exact (x_zero_mul _).symm126  | cons m P ih =>127    show xpEval env (pRow m Q ++ pMul P Q) = (xmEval env m + xpEval env P) * xpEval env Q128    rw [xpEval_append, xpEval_row, ih, x_right_distrib]129130theorem xring_add (A B C D : Ext p ν) : A + -B + (C + -D) = A + C + -(B + D) := by131  rw [x_neg_add_rev, x_add_assoc, x_add_assoc, x_add_left_comm (-B) C (-D)]132133theorem xring_mul (A B C D : Ext p ν) : (A + -B) * (C + -D) = A * C + B * D + -(A * D + B * C) := by134  rw [x_right_distrib, x_left_distrib, x_left_distrib, ← x_mul_neg, ← x_neg_mul, x_neg_mul_neg, x_neg_add_rev,135    x_add_assoc, x_add_assoc]136  refine congrArg (A * C + ·) ?_137  rw [x_add_comm (-(B * C)) (B * D), x_add_left_comm]138139theorem xring_neg (A B : Ext p ν) : -(A + -B) = B + -A := by rw [x_neg_add_rev, x_neg_neg, x_add_comm]140141theorem xtoP_eval (env : Nat → Ext p ν) (e : RE) : xeval env e = xpEval env e.toP.1 + -(xpEval env e.toP.2) := by142  induction e with143  | var i =>144    show env i = (env i * 1 + 0) + -(0 : Ext p ν)145    rw [Ext.mul_one, x_add_zero, x_neg_zero, x_add_zero]146  | zero => show (0 : Ext p ν) = 0 + -0; rw [x_neg_zero, x_add_zero]147  | one => show (1 : Ext p ν) = (1 + 0) + -(0 : Ext p ν); rw [x_add_zero, x_neg_zero, x_add_zero]148  | add a b iha ihb =>149    show xeval env a + xeval env b = xpEval env (a.toP.1 ++ b.toP.1) + -(xpEval env (a.toP.2 ++ b.toP.2))150    rw [iha, ihb, xpEval_append, xpEval_append, xring_add]151  | mul a b iha ihb =>152    show xeval env a * xeval env b = xpEval env (pMul a.toP.1 b.toP.1 ++ pMul a.toP.2 b.toP.2) +153      -(xpEval env (pMul a.toP.1 b.toP.2 ++ pMul a.toP.2 b.toP.1))154    rw [iha, ihb, xpEval_append, xpEval_append, xpEval_mul, xpEval_mul, xpEval_mul, xpEval_mul, xring_mul]155  | neg a iha =>156    show -(xeval env a) = xpEval env a.toP.2 + -(xpEval env a.toP.1)157    rw [iha, xring_neg]158159theorem xmEval_insM (env : Nat → Ext p ν) (i : Nat) (m : List Nat) : xmEval env (insM i m) = env i * xmEval env m := by160  induction m with161  | nil => rfl162  | cons j m ih =>163    show xmEval env (if Nat.ble i j then i :: j :: m else j :: insM i m) = env i * (env j * xmEval env m)164    cases Nat.ble i j with165    | true => rfl166    | false => show env j * xmEval env (insM i m) = _; rw [ih, x_mul_left_comm]167168theorem xmEval_sortM (env : Nat → Ext p ν) (m : List Nat) : xmEval env (sortM m) = xmEval env m := by169  induction m with170  | nil => rfl171  | cons i m ih => show xmEval env (insM i (sortM m)) = env i * xmEval env m; rw [xmEval_insM, ih]172173theorem xpEval_insP (env : Nat → Ext p ν) (m : List Nat) (P : List (List Nat)) :174    xpEval env (insP m P) = xmEval env m + xpEval env P := by175  induction P with176  | nil => rfl177  | cons n P ih =>178    show xpEval env (if lexLe m n then m :: n :: P else n :: insP m P) = xmEval env m + (xmEval env n + xpEval env P)179    cases lexLe m n with180    | true => rfl181    | false => show xmEval env n + xpEval env (insP m P) = _; rw [ih, x_add_left_comm]182183theorem xpEval_nfP (env : Nat → Ext p ν) (P : List (List Nat)) : xpEval env (nfP P) = xpEval env P := by184  induction P with185  | nil => rfl186  | cons m P ih =>187    show xpEval env (insP (sortM m) (nfP P)) = xmEval env m + xpEval env P; rw [xpEval_insP, ih, xmEval_sortM]188189/-- The normaliser's soundness in the extension: if the two cross lists agree after normalisation, the two sides are190equal on every assignment of extension values to the variables. -/191theorem xsound (env : Nat → Ext p ν) (l r : RE)192    (hb : pbeq (nfP (l.toP.1 ++ r.toP.2)) (nfP (r.toP.1 ++ l.toP.2)) = true) : xeval env l = xeval env r := by193  have h := pbeq_eq hb194  have h1 : xpEval env l.toP.1 + xpEval env r.toP.2 = xpEval env r.toP.1 + xpEval env l.toP.2 := by195    rw [← xpEval_append, ← xpEval_append, ← xpEval_nfP env (l.toP.1 ++ r.toP.2),196      ← xpEval_nfP env (r.toP.1 ++ l.toP.2), h]197  rw [xtoP_eval env l, xtoP_eval env r]198  apply x_add_right_cancel (c := xpEval env l.toP.2 + xpEval env r.toP.2)199  rw [← x_add_assoc, x_add_assoc (xpEval env l.toP.1), x_neg_add, x_add_zero,200      ← x_add_assoc, x_add_comm (xpEval env r.toP.1 + -(xpEval env r.toP.2)) (xpEval env l.toP.2), ← x_add_assoc,201      x_add_comm (xpEval env l.toP.2) (xpEval env r.toP.1), x_add_assoc, x_neg_add, x_add_zero, h1]202203/-! ## The triality frame: the cube roots of unity of the extension -/204205theorem red1 {L R A X : Shell p} (e : L = R + A * X) (ha : A = 0) : L = R :=206  e.trans ((congrArg (R + ·) (show A * X = 0 by rw [ha]; exact Shell.zero_mul _)).trans (Shell.add_zero R))207208theorem red2 {L R A B X Y : Shell p} (e : L = R + A * X + B * Y) (ha : A = 0) (hb : B = 0) : L = R :=209  red1 (red1 e hb) ha210211theorem red3 {L R A B C X Y Z : Shell p} (e : L = R + A * X + B * Y + C * Z) (ha : A = 0) (hb : B = 0) (hc : C = 0) :212    L = R :=213  red2 (red1 e hc) ha hb214215/-- Off the base: where the shell has no root of `x² + x + 1`, a root `z` in the extension has `z.im ≠ 0`. -/216theorem root_off_base (hno : ¬ ∃ a : Shell p, a * a + a + 1 = 0) {z : Ext p ν} (hz : z * z + z + 1 = 0) :217    z.im ≠ 0 := fun hb =>218  hno ⟨z.re, (red1 (RE.sound (look [ν, z.re, z.im]) (.add (.add (.mul (.var 1) (.var 1)) (.var 1)) .one) (.add (.add (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 1)) .one) (.mul (.var 2) (.neg (.mul (.var 0) (.var 2))))) (by decide +kernel) :219    z.re * z.re + z.re + 1 = z.re * z.re + ν * (z.im * z.im) + z.re + 1 + z.im * -(ν * z.im)) hb).trans (Ext.re_congr hz)⟩220221/-- Let `z` be a root of `x² + x + 1` off the base of a shell without zero divisors. Then `2 Re z + 1 = 0`, the222conjugate is the square, `z̄ = z²`, and the norm is one. -/223theorem cube_root_conj (hdom : ∀ a b : Shell p, a * b = 0 → a = 0 ∨ b = 0) {z : Ext p ν} (hz : z * z + z + 1 = 0) (hb : z.im ≠ 0) :224    z.re + z.re + 1 = 0 ∧ Ext.conj z = z * z ∧ Ext.norm z = 1 := by225  have er : z.re * z.re + ν * (z.im * z.im) + z.re + 1 = 0 := Ext.re_congr hz226  have ei : z.re * z.im + z.im * z.re + z.im + 0 = 0 := Ext.im_congr hz227  have hT : z.re + z.re + 1 = 0 :=228    match hdom _ _ ((RE.sound (look [ν, z.re, z.im]) (.mul (.var 2) (.add (.add (.var 1) (.var 1)) .one)) (.add (.add (.add (.mul (.var 1) (.var 2)) (.mul (.var 2) (.var 1))) (.var 2)) .zero) (by decide +kernel) :229        z.im * (z.re + z.re + 1) = z.re * z.im + z.im * z.re + z.im + 0).trans ei) with230    | .inl e => absurd e hb231    | .inr e => e232  refine ⟨hT, Ext.ext ?_ ?_, ?_⟩233  · exact red2 (RE.sound (look [ν, z.re, z.im]) (.var 1) (.add (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.mul (.add (.add (.var 1) (.var 1)) .one) .one)) (.mul (.add (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 1)) .one) (.neg .one))) (by decide +kernel) :234      z.re = z.re * z.re + ν * (z.im * z.im) + (z.re + z.re + 1) * 1 + (z.re * z.re + ν * (z.im * z.im) + z.re + 1) * -1)235      hT er236  · exact red1 (RE.sound (look [ν, z.re, z.im]) (.neg (.var 2)) (.add (.add (.mul (.var 1) (.var 2)) (.mul (.var 2) (.var 1))) (.mul (.add (.add (.var 1) (.var 1)) .one) (.neg (.var 2)))) (by decide +kernel) :237      -z.im = z.re * z.im + z.im * z.re + (z.re + z.re + 1) * -z.im) hT238  · exact red2 (RE.sound (look [ν, z.re, z.im]) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))) (.add (.add .one (.mul (.add (.add (.var 1) (.var 1)) .one) (.var 1))) (.mul (.add (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 1)) .one) (.neg .one))) (by decide +kernel) :239      z.re * z.re + -(ν * (z.im * z.im)) = 1 + (z.re + z.re + 1) * z.re + (z.re * z.re + ν * (z.im * z.im) + z.re + 1) * -1)240      hT er241242/-- A root of `x² + x + 1` is a cube root of unity: `z³ = 1 + (z − 1)(z² + z + 1)`. -/243theorem cube_one {z : Ext p ν} (hz : z * z + z + 1 = 0) : z ^ 3 = 1 := by244  have e : z ^ 3 = 1 + (z + -1) * (z * z + z + 1) := xsound (xlook [z]) (.mul (.mul (.mul .one (.var 0)) (.var 0)) (.var 0)) (.add .one (.mul (.add (.var 0) (.neg .one)) (.add (.add (.mul (.var 0) (.var 0)) (.var 0)) .one))) (by decide +kernel)245  rw [e, hz, x_mul_zero, x_add_zero]246247theorem mod3_step (n : Nat) : (n + 3) % 3 = n % 3 := by248  rw [Nat.add_comm]; exact FRC.Nat.add_mul_mod_self_left n 1 3 (by decide)249250theorem pow_mod_three {z : Ext p ν} (h3 : z ^ 3 = 1) : ∀ n : Nat, z ^ n = z ^ (n % 3)251  | 0 => rfl252  | 1 => rfl253  | 2 => rfl254  | n + 3 => by rw [Ext.pow_add z n 3, h3, Ext.mul_one, mod3_step n]; exact pow_mod_three h3 n255256/-- The order three: with `z³ = 1`, `z ≠ 1` and `z² ≠ 1`, `zⁿ = 1` exactly when `3 ∣ n`. -/257theorem pow_eq_one_iff {z : Ext p ν} (h3 : z ^ 3 = 1) (h1 : z ^ 1 ≠ 1) (h2 : z ^ 2 ≠ 1) (n : Nat) :258    z ^ n = 1 ↔ n % 3 = 0 := by259  rw [pow_mod_three h3 n]260  have hlt := Nat.mod_lt n (by decide : 0 < 3)261  generalize n % 3 = r at hlt ⊢262  match r, hlt with263  | 0, _ => exact ⟨fun _ => rfl, fun _ => rfl⟩264  | 1, _ => exact ⟨fun e => absurd e h1, fun e => absurd e (by decide)⟩265  | 2, _ => exact ⟨fun e => absurd e h2, fun e => absurd e (by decide)⟩266  | k + 3, hlt => exact absurd hlt (Nat.not_lt_of_le (Nat.le_add_left 3 k))267268/-- The triality scalar on a shell without zero divisors whose base has no root of `x² + x + 1`. Every root `ω` in the extension lies269off the base, with `ω̄ = ω²` and norm one. So `ω̄ ω = 1`, and the scalar `ω Iₙ` is unitary. Its determinant `ωⁿ` is one270exactly when `3 ∣ n`: `ω¹ ≠ 1`, `ω² ≠ 1` and `ω³ = 1`. -/271theorem triality_scalar (hdom : ∀ a b : Shell p, a * b = 0 → a = 0 ∨ b = 0) (hno : ¬ ∃ a : Shell p, a * a + a + 1 = 0) {ω : Ext p ν}272    (hω : ω * ω + ω + 1 = 0) :273    ω.im ≠ 0 ∧ Ext.conj ω = ω * ω ∧ Ext.norm ω = 1 ∧ Ext.conj ω * ω = 1 ∧274      ω ^ 1 ≠ 1 ∧ ω ^ 2 ≠ 1 ∧ ω ^ 3 = 1 ∧ ∀ n : Nat, ω ^ n = 1 ↔ n % 3 = 0 := by275  have hb := root_off_base hno hω276  obtain ⟨_, hc, hn⟩ := cube_root_conj hdom hω hb277  have h3 := cube_one hω278  have h1 : ω ^ 1 ≠ 1 := fun e => hb (Ext.im_congr ((Ext.one_mul ω).symm.trans e))279  have h2 : ω ^ 2 ≠ 1 := fun e =>280    hb (Ext.im_congr ((Ext.one_mul ω).symm.trans ((congrArg (· * ω) e).symm.trans h3)))281  have hu : Ext.conj ω * ω = 1 := by rw [Ext.mul_comm]; exact Ext.conj_inv_of_norm_one ω hn282  exact ⟨hb, hc, hn, hu, h1, h2, h3, pow_eq_one_iff h3 h1 h2⟩283284/-- `ω = −h + h w`. With `h = 1/2` and `ν = −3` it is a root of `x² + x + 1`. -/285def omega (h : Shell p) : Ext p ν := ⟨-h, h⟩286287theorem omega_root {h : Shell p} (hh : h + h = 1) (hν : ν + 1 + 1 + 1 = 0) :288    (omega h : Ext p ν) * omega h + omega h + 1 = 0 := by289  have hA : h + h + -1 = 0 := by rw [hh, Shell.add_neg]290  exact Ext.ext291    (red2 (RE.sound (look [ν, h]) (.add (.add (.add (.mul (.neg (.var 1)) (.neg (.var 1))) (.mul (.var 0) (.mul (.var 1) (.var 1)))) (.neg (.var 1))) .one) (.add (.add .zero (.mul (.add (.add (.var 1) (.var 1)) (.neg .one)) (.neg (.add (.var 1) .one)))) (.mul (.add (.add (.add (.var 0) .one) .one) .one) (.mul (.var 1) (.var 1)))) (by decide +kernel) :292      -h * -h + ν * (h * h) + -h + 1 = 0 + (h + h + -1) * -(h + 1) + (ν + 1 + 1 + 1) * (h * h)) hA hν)293    (red1 (RE.sound (look [ν, h]) (.add (.add (.add (.mul (.neg (.var 1)) (.var 1)) (.mul (.var 1) (.neg (.var 1)))) (.var 1)) .zero) (.add .zero (.mul (.add (.add (.var 1) (.var 1)) (.neg .one)) (.neg (.var 1)))) (by decide +kernel) :294      -h * h + h * -h + h + 0 = 0 + (h + h + -1) * -h) hA)295296/-- Where the shell has no root of `x² + x + 1`, `ν = −3` is not a square. A root `s` of `s² = −3` would give the root297`−h + h s` of `x² + x + 1` in the base. -/298theorem nonsquare (hno : ¬ ∃ a : Shell p, a * a + a + 1 = 0) {h : Shell p} (hh : h + h = 1) (hν : ν + 1 + 1 + 1 = 0) :299    ¬ ∃ s : Shell p, s * s = ν := fun ⟨s, hs⟩ => by300  have hA : h + h + -1 = 0 := by rw [hh, Shell.add_neg]301  have hs' : s * s + -ν = 0 := by rw [hs, Shell.add_neg]302  exact hno ⟨-h + h * s, red3 (RE.sound (look [ν, h, s]) (.add (.add (.mul (.add (.neg (.var 1)) (.mul (.var 1) (.var 2))) (.add (.neg (.var 1)) (.mul (.var 1) (.var 2)))) (.add (.neg (.var 1)) (.mul (.var 1) (.var 2)))) .one) (.add (.add (.add .zero (.mul (.add (.add (.var 1) (.var 1)) (.neg .one)) (.add (.neg (.add (.var 1) .one)) (.neg (.mul (.var 2) (.var 1)))))) (.mul (.add (.add (.add (.var 0) .one) .one) .one) (.mul (.var 1) (.var 1)))) (.mul (.add (.mul (.var 2) (.var 2)) (.neg (.var 0))) (.mul (.var 1) (.var 1)))) (by decide +kernel) :303    (-h + h * s) * (-h + h * s) + (-h + h * s) + 1 =304      0 + (h + h + -1) * (-(h + 1) + -(s * h)) + (ν + 1 + 1 + 1) * (h * h) + (s * s + -ν) * (h * h)) hA hν hs'⟩305306theorem three_eq : (3 : Shell p) = 1 + 1 + 1 :=307  Shell.ext (by308    show 3 % p = ((1 % p + 1 % p) % p + 1 % p) % p309    rw [← FRC.Nat.add_mod 1 1 p Pos.pos, ← FRC.Nat.add_mod (1 + 1) 1 p Pos.pos])310311theorem neg_three : (-3 : Shell p) + 1 + 1 + 1 = 0 := by312  rw [three_eq]313  exact RE.sound (look ([] : List (Shell p))) (.add (.add (.add (.neg (.add (.add .one .one) .one)) .one) .one) .one) .zero (by decide +kernel)314315/-! ## Three-forms over the extension: the group `SU(H)` by elements -/316317/-- A `3 × 3` matrix over the extension, by its nine entries. -/318structure M3 (p : Nat) [Pos p] (ν : Shell p) where319  a00 : Ext p ν320  a01 : Ext p ν321  a02 : Ext p ν322  a10 : Ext p ν323  a11 : Ext p ν324  a12 : Ext p ν325  a20 : Ext p ν326  a21 : Ext p ν327  a22 : Ext p ν328329theorem mext {A B : M3 p ν} (h00 : A.a00 = B.a00) (h01 : A.a01 = B.a01) (h02 : A.a02 = B.a02)330    (h10 : A.a10 = B.a10) (h11 : A.a11 = B.a11) (h12 : A.a12 = B.a12) (h20 : A.a20 = B.a20) (h21 : A.a21 = B.a21)331    (h22 : A.a22 = B.a22) : A = B := by332  cases A; cases B; cases h00; cases h01; cases h02; cases h10; cases h11; cases h12; cases h20; cases h21; cases h22333  rfl334335/-- The product of matrices. -/336def mmul (A B : M3 p ν) : M3 p ν :=337  ⟨A.a00 * B.a00 + A.a01 * B.a10 + A.a02 * B.a20, A.a00 * B.a01 + A.a01 * B.a11 + A.a02 * B.a21,338    A.a00 * B.a02 + A.a01 * B.a12 + A.a02 * B.a22,339   A.a10 * B.a00 + A.a11 * B.a10 + A.a12 * B.a20, A.a10 * B.a01 + A.a11 * B.a11 + A.a12 * B.a21,340    A.a10 * B.a02 + A.a11 * B.a12 + A.a12 * B.a22,341   A.a20 * B.a00 + A.a21 * B.a10 + A.a22 * B.a20, A.a20 * B.a01 + A.a21 * B.a11 + A.a22 * B.a21,342    A.a20 * B.a02 + A.a21 * B.a12 + A.a22 * B.a22⟩343344/-- The conjugate transpose `A†`. -/345def dag (A : M3 p ν) : M3 p ν :=346  ⟨Ext.conj A.a00, Ext.conj A.a10, Ext.conj A.a20, Ext.conj A.a01, Ext.conj A.a11, Ext.conj A.a21,347   Ext.conj A.a02, Ext.conj A.a12, Ext.conj A.a22⟩348349/-- The determinant, by the first row. -/350def det (A : M3 p ν) : Ext p ν :=351  A.a00 * (A.a11 * A.a22 + -(A.a12 * A.a21)) + -(A.a01 * (A.a10 * A.a22 + -(A.a12 * A.a20))) +352    A.a02 * (A.a10 * A.a21 + -(A.a11 * A.a20))353354/-- The adjugate, the transpose of the cofactors. -/355def adj (A : M3 p ν) : M3 p ν :=356  ⟨A.a11 * A.a22 + -(A.a12 * A.a21), A.a02 * A.a21 + -(A.a01 * A.a22), A.a01 * A.a12 + -(A.a02 * A.a11),357   A.a12 * A.a20 + -(A.a10 * A.a22), A.a00 * A.a22 + -(A.a02 * A.a20), A.a02 * A.a10 + -(A.a00 * A.a12),358   A.a10 * A.a21 + -(A.a11 * A.a20), A.a01 * A.a20 + -(A.a00 * A.a21), A.a00 * A.a11 + -(A.a01 * A.a10)⟩359360/-- The scalar matrix `c I₃`. -/361def scal (c : Ext p ν) : M3 p ν := ⟨c, 0, 0, 0, c, 0, 0, 0, c⟩362363/-- The identity `I₃`. -/364def mone : M3 p ν := scal 1365366/-- Every entry multiplied by `c`. -/367def smul (c : Ext p ν) (A : M3 p ν) : M3 p ν :=368  ⟨c * A.a00, c * A.a01, c * A.a02, c * A.a10, c * A.a11, c * A.a12, c * A.a20, c * A.a21, c * A.a22⟩369370/-- The nine entries in reading order, the variables of the normaliser. -/371def ents (A : M3 p ν) : List (Ext p ν) := [A.a00, A.a01, A.a02, A.a10, A.a11, A.a12, A.a20, A.a21, A.a22]372373/-- `U ∈ SU(H)`: `U` preserves the three-form `H`, `U† H U = H`, and has determinant one. -/374def SU (H U : M3 p ν) : Prop := mmul (mmul (dag U) H) U = H ∧ det U = 1375376theorem assoc_entry (x0 x1 x2 b00 b01 b02 b10 b11 b12 b20 b21 b22 y0 y1 y2 : Ext p ν) :377    (x0 * b00 + x1 * b10 + x2 * b20) * y0 + (x0 * b01 + x1 * b11 + x2 * b21) * y1 + (x0 * b02 + x1 * b12 + x2 * b22) * y2 =378      x0 * (b00 * y0 + b01 * y1 + b02 * y2) + x1 * (b10 * y0 + b11 * y1 + b12 * y2) + x2 * (b20 * y0 + b21 * y1 + b22 * y2) :=379  xsound (xlook [x0, x1, x2, b00, b01, b02, b10, b11, b12, b20, b21, b22, y0, y1, y2]) (.add (.add (.mul (.add (.add (.mul (.var 0) (.var 3)) (.mul (.var 1) (.var 6))) (.mul (.var 2) (.var 9))) (.var 12)) (.mul (.add (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 7))) (.mul (.var 2) (.var 10))) (.var 13))) (.mul (.add (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 8))) (.mul (.var 2) (.var 11))) (.var 14))) (.add (.add (.mul (.var 0) (.add (.add (.mul (.var 3) (.var 12)) (.mul (.var 4) (.var 13))) (.mul (.var 5) (.var 14)))) (.mul (.var 1) (.add (.add (.mul (.var 6) (.var 12)) (.mul (.var 7) (.var 13))) (.mul (.var 8) (.var 14))))) (.mul (.var 2) (.add (.add (.mul (.var 9) (.var 12)) (.mul (.var 10) (.var 13))) (.mul (.var 11) (.var 14)))))380    (by decide +kernel)381382/-- The product of matrices is associative. -/383theorem mmul_assoc (A B C : M3 p ν) : mmul (mmul A B) C = mmul A (mmul B C) :=384  mext (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)385    (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)386    (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)387    (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)388    (assoc_entry _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)389390theorem conj_dot (a0 a1 a2 b0 b1 b2 : Ext p ν) :391    Ext.conj (a0 * b0 + a1 * b1 + a2 * b2) =392      Ext.conj b0 * Ext.conj a0 + Ext.conj b1 * Ext.conj a1 + Ext.conj b2 * Ext.conj a2 := by393  rw [conj_add, conj_add, Ext.conj_mul, Ext.conj_mul, Ext.conj_mul, Ext.mul_comm (Ext.conj a0),394    Ext.mul_comm (Ext.conj a1), Ext.mul_comm (Ext.conj a2)]395396/-- `(A B)† = B† A†`. -/397theorem dag_mul (A B : M3 p ν) : dag (mmul A B) = mmul (dag B) (dag A) :=398  mext (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _)399    (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _) (conj_dot _ _ _ _ _ _)400401/-- The determinant is multiplicative: `det (A B) = det A · det B`. -/402theorem det_mul (A B : M3 p ν) : det (mmul A B) = det A * det B :=403  xsound (xlook (ents A ++ ents B)) (.add (.add (.mul (.add (.add (.mul (.var 0) (.var 9)) (.mul (.var 1) (.var 12))) (.mul (.var 2) (.var 15))) (.add (.mul (.add (.add (.mul (.var 3) (.var 10)) (.mul (.var 4) (.var 13))) (.mul (.var 5) (.var 16))) (.add (.add (.mul (.var 6) (.var 11)) (.mul (.var 7) (.var 14))) (.mul (.var 8) (.var 17)))) (.neg (.mul (.add (.add (.mul (.var 3) (.var 11)) (.mul (.var 4) (.var 14))) (.mul (.var 5) (.var 17))) (.add (.add (.mul (.var 6) (.var 10)) (.mul (.var 7) (.var 13))) (.mul (.var 8) (.var 16))))))) (.neg (.mul (.add (.add (.mul (.var 0) (.var 10)) (.mul (.var 1) (.var 13))) (.mul (.var 2) (.var 16))) (.add (.mul (.add (.add (.mul (.var 3) (.var 9)) (.mul (.var 4) (.var 12))) (.mul (.var 5) (.var 15))) (.add (.add (.mul (.var 6) (.var 11)) (.mul (.var 7) (.var 14))) (.mul (.var 8) (.var 17)))) (.neg (.mul (.add (.add (.mul (.var 3) (.var 11)) (.mul (.var 4) (.var 14))) (.mul (.var 5) (.var 17))) (.add (.add (.mul (.var 6) (.var 9)) (.mul (.var 7) (.var 12))) (.mul (.var 8) (.var 15))))))))) (.mul (.add (.add (.mul (.var 0) (.var 11)) (.mul (.var 1) (.var 14))) (.mul (.var 2) (.var 17))) (.add (.mul (.add (.add (.mul (.var 3) (.var 9)) (.mul (.var 4) (.var 12))) (.mul (.var 5) (.var 15))) (.add (.add (.mul (.var 6) (.var 10)) (.mul (.var 7) (.var 13))) (.mul (.var 8) (.var 16)))) (.neg (.mul (.add (.add (.mul (.var 3) (.var 10)) (.mul (.var 4) (.var 13))) (.mul (.var 5) (.var 16))) (.add (.add (.mul (.var 6) (.var 9)) (.mul (.var 7) (.var 12))) (.mul (.var 8) (.var 15)))))))) (.mul (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (.add (.add (.mul (.var 9) (.add (.mul (.var 13) (.var 17)) (.neg (.mul (.var 14) (.var 16))))) (.neg (.mul (.var 10) (.add (.mul (.var 12) (.var 17)) (.neg (.mul (.var 14) (.var 15))))))) (.mul (.var 11) (.add (.mul (.var 12) (.var 16)) (.neg (.mul (.var 13) (.var 15))))))) (by decide +kernel)404405/-- The form carried by a product: `(U V)† H (U V) = V† (U† H U) V`. -/406theorem sandwich (U V H : M3 p ν) :407    mmul (mmul (dag (mmul U V)) H) (mmul U V) = mmul (mmul (dag V) (mmul (mmul (dag U) H) U)) V := by408  rw [dag_mul, mmul_assoc (mmul (dag V) (dag U)) H (mmul U V), mmul_assoc (dag V) (dag U), mmul_assoc (dag V) _ V,409    mmul_assoc (mmul (dag U) H) U V, mmul_assoc (dag U) H (mmul U V)]410411theorem e0 (d x y w : Ext p ν) : d * x + 0 * y + 0 * w = d * x :=412  xsound (xlook [d, x, y, w]) (.add (.add (.mul (.var 0) (.var 1)) (.mul .zero (.var 2))) (.mul .zero (.var 3))) (.mul (.var 0) (.var 1)) (by decide +kernel)413theorem e1 (d x y w : Ext p ν) : 0 * x + d * y + 0 * w = d * y :=414  xsound (xlook [d, x, y, w]) (.add (.add (.mul .zero (.var 1)) (.mul (.var 0) (.var 2))) (.mul .zero (.var 3))) (.mul (.var 0) (.var 2)) (by decide +kernel)415theorem e2 (d x y w : Ext p ν) : 0 * x + 0 * y + d * w = d * w :=416  xsound (xlook [d, x, y, w]) (.add (.add (.mul .zero (.var 1)) (.mul .zero (.var 2))) (.mul (.var 0) (.var 3))) (.mul (.var 0) (.var 3)) (by decide +kernel)417theorem f0 (d x y w : Ext p ν) : x * d + y * 0 + w * 0 = d * x :=418  xsound (xlook [d, x, y, w]) (.add (.add (.mul (.var 1) (.var 0)) (.mul (.var 2) .zero)) (.mul (.var 3) .zero)) (.mul (.var 0) (.var 1)) (by decide +kernel)419theorem f1 (d x y w : Ext p ν) : x * 0 + y * d + w * 0 = d * y :=420  xsound (xlook [d, x, y, w]) (.add (.add (.mul (.var 1) .zero) (.mul (.var 2) (.var 0))) (.mul (.var 3) .zero)) (.mul (.var 0) (.var 2)) (by decide +kernel)421theorem f2 (d x y w : Ext p ν) : x * 0 + y * 0 + w * d = d * w :=422  xsound (xlook [d, x, y, w]) (.add (.add (.mul (.var 1) .zero) (.mul (.var 2) .zero)) (.mul (.var 3) (.var 0))) (.mul (.var 0) (.var 3)) (by decide +kernel)423424theorem scal_mul (d : Ext p ν) (A : M3 p ν) : mmul (scal d) A = smul d A :=425  mext (e0 _ _ _ _) (e0 _ _ _ _) (e0 _ _ _ _) (e1 _ _ _ _) (e1 _ _ _ _) (e1 _ _ _ _) (e2 _ _ _ _) (e2 _ _ _ _)426    (e2 _ _ _ _)427428theorem mul_scal (A : M3 p ν) (d : Ext p ν) : mmul A (scal d) = smul d A :=429  mext (f0 _ _ _ _) (f1 _ _ _ _) (f2 _ _ _ _) (f0 _ _ _ _) (f1 _ _ _ _) (f2 _ _ _ _) (f0 _ _ _ _) (f1 _ _ _ _)430    (f2 _ _ _ _)431432theorem smul_smul (c d : Ext p ν) (A : M3 p ν) : smul c (smul d A) = smul (c * d) A :=433  mext (Ext.mul_assoc _ _ _).symm (Ext.mul_assoc _ _ _).symm (Ext.mul_assoc _ _ _).symm (Ext.mul_assoc _ _ _).symm434    (Ext.mul_assoc _ _ _).symm (Ext.mul_assoc _ _ _).symm (Ext.mul_assoc _ _ _).symm (Ext.mul_assoc _ _ _).symm435    (Ext.mul_assoc _ _ _).symm436437theorem one_smul (A : M3 p ν) : smul 1 A = A :=438  mext (Ext.one_mul _) (Ext.one_mul _) (Ext.one_mul _) (Ext.one_mul _) (Ext.one_mul _) (Ext.one_mul _) (Ext.one_mul _)439    (Ext.one_mul _) (Ext.one_mul _)440441theorem conj_zero : Ext.conj (0 : Ext p ν) = 0 := Ext.ext rfl Shell.neg_zero442443theorem conj_one : Ext.conj (1 : Ext p ν) = 1 := Ext.ext rfl Shell.neg_zero444445theorem one_cube : (1 : Ext p ν) ^ 3 = 1 :=446  xsound (xlook ([] : List (Ext p ν))) (.mul (.mul (.mul .one .one) .one) .one) .one (by decide +kernel)447448theorem dag_scal (c : Ext p ν) : dag (scal c) = scal (Ext.conj c) :=449  mext rfl conj_zero conj_zero conj_zero rfl conj_zero conj_zero conj_zero rfl450451theorem det_scal (c : Ext p ν) : det (scal c) = c ^ 3 :=452  xsound (xlook [c]) (.add (.add (.mul (.var 0) (.add (.mul (.var 0) (.var 0)) (.neg (.mul .zero .zero)))) (.neg (.mul .zero (.add (.mul .zero (.var 0)) (.neg (.mul .zero .zero)))))) (.mul .zero (.add (.mul .zero .zero) (.neg (.mul (.var 0) .zero))))) (.mul (.mul (.mul .one (.var 0)) (.var 0)) (.var 0)) (by decide +kernel)453454/-- A scalar `c I₃` with `c̄ c = 1` and `c³ = 1` lies in `SU(H)` for every three-form `H`. -/455theorem scal_SU (H : M3 p ν) {c : Ext p ν} (hu : Ext.conj c * c = 1) (h3 : c ^ 3 = 1) : SU H (scal c) := by456  refine ⟨?_, by rw [det_scal, h3]⟩457  rw [dag_scal, scal_mul, mul_scal, smul_smul, Ext.mul_comm, hu, one_smul]458459/-- `U adj U = det U · I₃`. -/460theorem mul_adj (U : M3 p ν) : mmul U (adj U) = scal (det U) :=461  mext (xsound (xlook (ents U)) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.mul (.var 1) (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (by decide +kernel))462    (xsound (xlook (ents U)) (.add (.add (.mul (.var 0) (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8))))) (.mul (.var 1) (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))))) (.mul (.var 2) (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))))) .zero (by decide +kernel))463    (xsound (xlook (ents U)) (.add (.add (.mul (.var 0) (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4))))) (.mul (.var 1) (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))))) (.mul (.var 2) (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3)))))) .zero (by decide +kernel))464    (xsound (xlook (ents U)) (.add (.add (.mul (.var 3) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.mul (.var 4) (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))))) (.mul (.var 5) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) .zero (by decide +kernel))465    (xsound (xlook (ents U)) (.add (.add (.mul (.var 3) (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8))))) (.mul (.var 4) (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))))) (.mul (.var 5) (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (by decide +kernel))466    (xsound (xlook (ents U)) (.add (.add (.mul (.var 3) (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4))))) (.mul (.var 4) (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))))) (.mul (.var 5) (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3)))))) .zero (by decide +kernel))467    (xsound (xlook (ents U)) (.add (.add (.mul (.var 6) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.mul (.var 7) (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))))) (.mul (.var 8) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) .zero (by decide +kernel))468    (xsound (xlook (ents U)) (.add (.add (.mul (.var 6) (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8))))) (.mul (.var 7) (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))))) (.mul (.var 8) (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))))) .zero (by decide +kernel))469    (xsound (xlook (ents U)) (.add (.add (.mul (.var 6) (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4))))) (.mul (.var 7) (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))))) (.mul (.var 8) (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3)))))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (by decide +kernel))470471/-- `adj U · U = det U · I₃`. -/472theorem adj_mul (U : M3 p ν) : mmul (adj U) U = scal (det U) :=473  mext (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7)))) (.var 0)) (.mul (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8)))) (.var 3))) (.mul (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4)))) (.var 6))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (by decide +kernel))474    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7)))) (.var 1)) (.mul (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8)))) (.var 4))) (.mul (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4)))) (.var 7))) .zero (by decide +kernel))475    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7)))) (.var 2)) (.mul (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8)))) (.var 5))) (.mul (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4)))) (.var 8))) .zero (by decide +kernel))476    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))) (.var 0)) (.mul (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))) (.var 3))) (.mul (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))) (.var 6))) .zero (by decide +kernel))477    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))) (.var 1)) (.mul (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))) (.var 4))) (.mul (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))) (.var 7))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (by decide +kernel))478    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))) (.var 2)) (.mul (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))) (.var 5))) (.mul (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))) (.var 8))) .zero (by decide +kernel))479    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))) (.var 0)) (.mul (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))) (.var 3))) (.mul (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3)))) (.var 6))) .zero (by decide +kernel))480    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))) (.var 1)) (.mul (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))) (.var 4))) (.mul (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3)))) (.var 7))) .zero (by decide +kernel))481    (xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))) (.var 2)) (.mul (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))) (.var 5))) (.mul (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3)))) (.var 8))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (by decide +kernel))482483/-- `det (adj U) = (det U)²`. -/484theorem det_adj (U : M3 p ν) : det (adj U) = det U * det U :=485  xsound (xlook (ents U)) (.add (.add (.mul (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7)))) (.add (.mul (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))) (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3))))) (.neg (.mul (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))) (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7)))))))) (.neg (.mul (.add (.mul (.var 2) (.var 7)) (.neg (.mul (.var 1) (.var 8)))) (.add (.mul (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))) (.add (.mul (.var 0) (.var 4)) (.neg (.mul (.var 1) (.var 3))))) (.neg (.mul (.add (.mul (.var 2) (.var 3)) (.neg (.mul (.var 0) (.var 5)))) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))))))) (.mul (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 4)))) (.add (.mul (.add (.mul (.var 5) (.var 6)) (.neg (.mul (.var 3) (.var 8)))) (.add (.mul (.var 1) (.var 6)) (.neg (.mul (.var 0) (.var 7))))) (.neg (.mul (.add (.mul (.var 0) (.var 8)) (.neg (.mul (.var 2) (.var 6)))) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6))))))))) (.mul (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6)))))) (.add (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.neg (.mul (.var 5) (.var 7))))) (.neg (.mul (.var 1) (.add (.mul (.var 3) (.var 8)) (.neg (.mul (.var 5) (.var 6))))))) (.mul (.var 2) (.add (.mul (.var 3) (.var 7)) (.neg (.mul (.var 4) (.var 6))))))) (by decide +kernel)486487/-- **G4, the group of a three-form, by elements.** For every three-form `H` over the extension, the set `SU(H)` of the488`U` with `U† H U = H` and `det U = 1` holds the identity and every scalar `c I₃` with `c̄ c = 1` and `c³ = 1`. It is489closed under the product. Each member's adjugate is a two-sided inverse and a member. The proof never uses `H† = H`, so490it covers the Hermitian forms of the row. -/491theorem su_group (H : M3 p ν) :492    SU H mone ∧493    (∀ c : Ext p ν, Ext.conj c * c = 1 → c ^ 3 = 1 → SU H (scal c)) ∧494    (∀ U V : M3 p ν, SU H U → SU H V → SU H (mmul U V)) ∧495    ∀ U : M3 p ν, SU H U → SU H (adj U) ∧ mmul U (adj U) = mone ∧ mmul (adj U) U = mone := by496  have hone : SU H mone := scal_SU H (by rw [conj_one]; exact Ext.one_mul 1) one_cube497  refine ⟨hone, fun c hu h3 => scal_SU H hu h3, fun U V hU hV => ⟨?_, ?_⟩, fun U hU => ?_⟩498  · rw [sandwich, hU.1, hV.1]499  · rw [det_mul, hU.2, hV.2, Ext.one_mul]500  · have hr : mmul U (adj U) = mone := by rw [mul_adj, hU.2]; rfl501    have hl : mmul (adj U) U = mone := by rw [adj_mul, hU.2]; rfl502    have s := sandwich U (adj U) H503    rw [hr, hU.1, hone.1] at s504    exact ⟨⟨s.symm, by rw [det_adj, hU.2, Ext.one_mul]⟩, hr, hl⟩505506/-! ## G4: the rank forced as the minimal triality frame -/507508/-- **G4, the rank forced as the minimal triality frame.** Take a shell without zero divisors whose base has no root of509`x² + x + 1` (on the Carrier, B5: p00015), with a half `h + h = 1`. Then `−3` is not a square, and `Ext p (−3)` is the510quadratic extension. It holds a root `ω` of `x² + x + 1`. In every extension `Ext p ν`, each such root lies off the511base, with `ω̄ = ω²`, norm one and `ω̄ ω = 1`. So `ω Iₙ` is unitary for every `n`. Its determinant `ωⁿ` is one exactly512when `3 ∣ n`, with `ω¹ ≠ 1`, `ω² ≠ 1` and `ω³ = 1`. The least rank is therefore three, and `ω I₃` lies in `SU(H)` for513every three-form `H`. -/514theorem triality_frame (hdom : ∀ a b : Shell p, a * b = 0 → a = 0 ∨ b = 0)515    (hno : ¬ ∃ a : Shell p, a * a + a + 1 = 0) {h : Shell p} (hh : h + h = 1) :516    (¬ ∃ s : Shell p, s * s = -3) ∧ (∃ ω : Ext p (-3), ω * ω + ω + 1 = 0) ∧517    ∀ (ν : Shell p) (ω : Ext p ν), ω * ω + ω + 1 = 0 →518      ω.im ≠ 0 ∧ Ext.conj ω = ω * ω ∧ Ext.norm ω = 1 ∧ Ext.conj ω * ω = 1 ∧519      ω ^ 1 ≠ 1 ∧ ω ^ 2 ≠ 1 ∧ ω ^ 3 = 1 ∧ (∀ n : Nat, ω ^ n = 1 ↔ n % 3 = 0) ∧520      ∀ H : M3 p ν, SU H (scal ω) := by521  refine ⟨nonsquare hno hh neg_three, ⟨omega h, omega_root hh neg_three⟩, fun ν ω hω => ?_⟩522  obtain ⟨a, b, c, d, e, f, g, k⟩ := triality_scalar hdom hno hω523  exact ⟨a, b, c, d, e, f, g, k, fun H => scal_SU H d g⟩524525end FRC.Unitary526