Theme/Fields.lean — FrcCore

1import FrcCore.Theme.Interactions2import FrcCore.Theme.Unitary34/-!5# FrcCore.Theme.Fields — the interactions theme's kernel-decided certificates (27-fields, 16 October 2026)67The certificates of *Gauge Interactions over Finite Holographic Substrate* (tree `27-fields-20260625`) that the kernel8decides on the paper's exact data, as `frc/interactions.py` and `frc/ledgers/p27_fields.py` compute it:910* `tetrahedral_group` — `SU(2, 𝔽₃)` over `𝔽₉ = 𝔽₃[i]` (`Ext 3 (−1)`), the binary tetrahedral group `2T`: the `24` pairs11  `(a, b)` of unit norm `N(a) + N(b) = 1`, closed under the quaternion product, non-abelian, with the element orders12  `1, 2, 3, 4, 6` in multiplicities `1, 1, 8, 6, 8`, traces in the shell, and the drive `diag(i, −i)` of centraliser `4` (27:C1, C4);13* `green_torus` — the Coulomb Green's function of the `4³` torus as integers: `7680 · G` satisfies14  `6 g(x) − Σ_nb g = 7680 δ − 120` at every site, `U(1) = 257/7680` (27:C3);15* `admissible_two` — the two admissible range-1 actions at `L = 4` satisfy every one of the `1 023` constraint rows, and16  Maxwell's plaquette action is their difference, `2 · Maxwell = B − A` (27:C2, X3);17* `su3_centre`, `gluon_commutator` — over `𝔽₄` the scalar centre of `SU(3, 2)` is the three cube roots of unity, two18  explicit elements of `SU(3, 2)` do not commute (`U₁U₂U₁⁻¹U₂⁻¹ ≠ I`) while the abelian control returns `I` (27:C7, X7);19* `ckm_free` — Hermitian `3 × 3` mass matrices over `𝔽₁₇[√−3]` and `𝔽₅₃[√−3]` have determinants in the shell and do not20  commute (27:X11, P9).2122The theorems of the theme that these instantiate are `Theme/Interactions.lean`'s and `Theme/Unitary.lean`'s; the paper23module `FrcCore/Fields.lean` aliases every name under the paper's. No axioms (`check_core_axioms.py`).24-/2526namespace FRC.Interactions2728open FRC.Shell FRC.Extension FRC.Unitary293031/-! ## `SU(2, 𝔽₃) = 2T` over `𝔽₉` (27:C1, C4) -/3233/-- The nine elements of `𝔽₉ = 𝔽₃[i]`, `i² = −1 = 2`. -/34def f9 : List (Ext 3 2) := (List.range 9).map (fun n => ⟨ofNat (n / 3), ofNat (n % 3)⟩)3536/-- The quaternion product on pairs `(a, b)`, the matrix `[[a, b], [−b̄, ā]]`:37`(a, b)(c, d) = (ac − b d̄, ad + b c̄)`. -/38def qmul (x y : Ext 3 2 × Ext 3 2) : Ext 3 2 × Ext 3 2 :=39  (x.1 * y.1 + -(x.2 * Ext.conj y.2), x.1 * y.2 + x.2 * Ext.conj y.1)4041/-- The unit-norm pairs: `SU(2, 𝔽₃)`. -/42def su2 : List (Ext 3 2 × Ext 3 2) :=43  (f9.flatMap (fun a => f9.map (fun b => (a, b)))).filter (fun x => Ext.norm x.1 + Ext.norm x.2 == 1)4445def qone : Ext 3 2 × Ext 3 2 := (1, 0)4647def qpow (x : Ext 3 2 × Ext 3 2) : Nat → Ext 3 2 × Ext 3 248  | 0 => qone49  | n + 1 => qmul (qpow x n) x5051/-- The order of an element, among `1, 2, 3, 4, 6` (`0` if none). -/52def qord (x : Ext 3 2 × Ext 3 2) : Nat :=53  if qpow x 1 == qone then 1 else if qpow x 2 == qone then 2 else if qpow x 3 == qone then 354  else if qpow x 4 == qone then 4 else if qpow x 6 == qone then 6 else 05556/-- 27:C1, 27:C4 — `SU(2, 𝔽₃)` over `𝔽₉`: `24 = q(q² − 1)` elements, closed under the product, non-abelian, every trace57`a + ā` in the shell, the orders `1, 2, 3, 4, 6` in multiplicities `1, 1, 8, 6, 8` (the binary tetrahedral group),58the traces `0, 1, 2` in multiplicities `6, 9, 9`; the drive `diag(i, −i) = (i, 0)` lies in the group and its59centraliser has `4` elements. -/60theorem tetrahedral_group :61    su2.length = 24 ∧ 24 = 3 * (3 * 3 - 1) ∧62    su2.all (fun x => su2.all (fun y => su2.contains (qmul x y))) = true ∧63    su2.any (fun x => su2.any (fun y => qmul x y != qmul y x)) = true ∧64    su2.all (fun x => (x.1 + Ext.conj x.1).im == 0) = true ∧65    [1, 2, 3, 4, 6].map (fun k => (su2.filter (fun x => qord x == k)).length) = [1, 1, 8, 6, 8] ∧66    [0, 1, 2].map (fun t => (su2.filter (fun x => (x.1 + Ext.conj x.1).re == ofNat t)).length) = [6, 9, 9] ∧67    su2.contains (⟨0, 1⟩, 0) = true ∧68    (su2.filter (fun x => qmul x (⟨0, 1⟩, 0) == qmul (⟨0, 1⟩, 0) x)).length = 4 := by69  decide +kernel7071/-! ## The Coulomb Green's function of the `4³` torus (27:C3) -/7273/-- `7680 · G` on the `64` sites, index `x + 4y + 16z`. -/74def greenTable : List Int :=75  [1517, 257, 29, 257, 257, 29, -55, 29, 29, -55, -99, -55, 257, 29, -55, 29, 257, 29, -55, 29, 29, -55, -99, -55,76   -55, -99, -127, -99, 29, -55, -99, -55, 29, -55, -99, -55, -55, -99, -127, -99, -99, -127, -147, -127, -55, -99,77   -127, -99, 257, 29, -55, 29, 29, -55, -99, -55, -55, -99, -127, -99, 29, -55, -99, -55]7879/-- The entry of an integer list, `0` past its end. -/80def lget : List Int → Nat → Int81  | [], _ => 082  | x :: _, 0 => x83  | _ :: l, n + 1 => lget l n8485def green (x y z : Nat) : Int := lget greenTable (x % 4 + 4 * (y % 4) + 16 * (z % 4))8687/-- The lattice Laplacian `6 g − Σ_nb g` (the positive convention). -/88def greenLap (x y z : Nat) : Int :=89  6 * green x y z - (green (x + 1) y z + green (x + 3) y z + green x (y + 1) z + green x (y + 3) z +90    green x y (z + 1) + green x y (z + 3))9192/-- 27:C3 — the `L = 4` Coulomb Green's function in exact rationals: `7680 G` is the integer table, `ΔG = δ − 1/64`93at every site (`7680 Δg = 7680 δ − 120`), `G(1, 0, 0) = 257/7680` (two unit charges at separation `1`), the table is94cubic-symmetric on the axis and monotone `G(0) > G(1) > G(2)`, and its total is `0` (the zero mode removed). -/95theorem green_torus :96    greenTable.length = 64 ∧97    (List.range 64).all (fun n => greenLap (n % 4) (n / 4 % 4) (n / 16) == if n == 0 then 7680 - 120 else -120) = true ∧98    green 1 0 0 = 257 ∧ green 0 1 0 = 257 ∧ green 0 0 1 = 257 ∧ green 3 0 0 = 257 ∧99    green 0 0 0 > green 1 0 0 ∧ green 1 0 0 > green 2 0 0 ∧100    greenTable.foldl (· + ·) 0 = 0 ∧ 7680 / 64 = 120 := by101  decide +kernel102103/-! ## The admissible actions at `L = 4` (27:C2, X3) -/104105/-- The two admissible vectors of the range-1 translation-, gauge- and hypercubic-invariant quadratic actions at `L = 4`106(the nullspace of the constraint rows, scaled to integers; 123 parameters). -/107def admissibleA : List Int :=108  [0, 0, 0, 0, 0, 0, 0, 0, 0, -2, 2, -2, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, -1, 0, -1, 0, 0, 0, -1, 0, -1, 1,109  0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 1, -1, 0, -1, 1, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, -2, 2,110  -2, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 1, -1, 0, -1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, -1, 1, 0, 0,111  -2, 0, 0, 2, 0, 0, -2, 0, 0, 2, 0, 0, 0]112113def admissibleB : List Int :=114  [0, 0, 0, 0, 0, 0, 0, 0, 0, -2, 0, -2, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 1, -1, -2, -1, 0, 0, 0, -1, -2, -1,115  1, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 2, -2, 0, 1, -1, 0, -1, 1, 0, -2, 2, 0, -1, 1, 0, 0, 0, 0,116  -2, 0, -2, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 1, -1, 0, -1, 1, 0, 0, 0, 0, 2, -2, 0, -2, 2, 0, 0, 0, 0, 1, -1, 0, -1,117  1, 0, 0, -2, 0, 0, 0, 0, 0, -2, 0, 0, 0, 0, 0, 4]118119/-- Maxwell's plaquette action in the same 123 parameters. -/120def maxwellForm : List Int :=121  [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0, -1, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, -1, 0, 0, 0, 0, 0, -1, 0, 0, 1,122  0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, 0, 0, 0, 0, 0, 0, -1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -1, 0,123  0, 0, 0, 0, 0, 0, -1, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 0, -1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,124  0, 0, -1, 0, 0, 0, 0, 0, -1, 0, 0, 2]125126/-- The 1 023 constraint rows at `L = 4` distinct up to a scalar, each row flattened as `[index, coefficient, index, coefficient, …]`:127the translation, gauge and hypercubic conditions on the 123 parameters that `frc.interactions.maxwell_constraints` writes128(13 338 rows), normalised by sign and sorted, in four parts. -/129def constraintRows0 : List (List Int) :=130  [[0, 1], [0, 1, 2, -1], [0, 1, 6, -1], [0, 1, 8, -1], [0, 1, 9, -1, 23, -1, 50, -1], [0, 1, 9, -1, 37, -1, 40, 1,131  66, -1, 67, 1], [0, 1, 14, 1, 41, 1], [0, 1, 68, -1], [0, 1, 70, -1], [0, 1, 74, -1], [0, 1, 76, -1], [0, 1, 109,132  -1], [0, 1, 111, -1], [0, 1, 115, -1], [0, 1, 117, -1], [1, 1], [1, 1, 3, -1], [1, 1, 5, -1], [1, 1, 7, -1], [1, 1,133  10, -1, 24, -1, 50, 1, 51, -1], [1, 1, 10, -1, 36, -1, 39, 1, 65, -1, 66, 1], [1, 1, 15, 1, 41, -1, 42, 1], [1, 1,134  69, -1], [1, 1, 75, -1], [1, 1, 77, -1], [1, 1, 79, -1], [1, 1, 112, -1], [1, 1, 114, -1], [1, 1, 118, -1], [1, 1,135  120, -1], [2, 1], [2, 1, 6, -1], [2, 1, 8, -1], [2, 1, 11, -1, 25, -1, 51, 1, 52, -1], [2, 1, 11, -1, 35, -1, 38,136  1, 65, 1], [2, 1, 16, 1, 42, -1, 43, 1], [2, 1, 68, -1], [2, 1, 70, -1], [2, 1, 74, -1], [2, 1, 76, -1], [2, 1,137  109, -1], [2, 1, 111, -1], [2, 1, 115, -1], [2, 1, 117, -1], [3, 1], [3, 1, 5, -1], [3, 1, 7, -1], [3, 1, 12, -1,138  23, 1, 26, -1, 53, -1], [3, 1, 12, -1, 34, -1, 37, 1, 63, -1, 64, 1], [3, 1, 14, -1, 17, 1, 44, 1], [3, 1, 69, -1],139  [3, 1, 75, -1], [3, 1, 77, -1], [3, 1, 79, -1], [3, 1, 112, -1], [3, 1, 114, -1], [3, 1, 118, -1], [3, 1, 120, -1],140  [4, 1], [4, 1, 13, -2, 24, 1, 27, -1, 53, 1, 54, -1], [4, 1, 13, -2, 33, -1, 36, 1, 62, -1, 63, 1], [4, 1, 15, -1,141  18, 1, 44, -1, 45, 1], [4, 1, 78, -1], [4, 1, 121, -1], [5, 1], [5, 1, 7, -1], [5, 1, 12, -1, 25, 1, 28, -1, 54, 1,142  55, -1], [5, 1, 12, -1, 32, -1, 35, 1, 62, 1], [5, 1, 16, -1, 19, 1, 45, -1, 46, 1], [5, 1, 69, -1], [5, 1, 75,143  -1], [5, 1, 77, -1], [5, 1, 79, -1], [5, 1, 112, -1], [5, 1, 114, -1], [5, 1, 118, -1], [5, 1, 120, -1], [6, 1],144  [6, 1, 8, -1], [6, 1, 11, -1, 26, 1, 29, -1, 56, -1], [6, 1, 11, -1, 34, 1, 60, -1, 61, 1], [6, 1, 17, -1, 20, 1,145  47, 1], [6, 1, 68, -1], [6, 1, 70, -1], [6, 1, 74, -1], [6, 1, 76, -1], [6, 1, 109, -1], [6, 1, 111, -1], [6, 1,146  115, -1], [6, 1, 117, -1], [7, 1], [7, 1, 10, -1, 27, 1, 30, -1, 56, 1, 57, -1], [7, 1, 10, -1, 33, 1, 59, -1, 60,147  1], [7, 1, 18, -1, 21, 1, 47, -1, 48, 1], [7, 1, 69, -1], [7, 1, 75, -1], [7, 1, 77, -1], [7, 1, 79, -1], [7, 1,148  112, -1], [7, 1, 114, -1], [7, 1, 118, -1], [7, 1, 120, -1], [8, 1], [8, 1, 9, -1, 28, 1, 31, -1, 57, 1, 58, -1],149  [8, 1, 9, -1, 32, 1, 59, 1], [8, 1, 19, -1, 22, 1, 48, -1, 49, 1], [8, 1, 68, -1], [8, 1, 70, -1], [8, 1, 74, -1],150  [8, 1, 76, -1], [8, 1, 109, -1], [8, 1, 111, -1], [8, 1, 115, -1], [8, 1, 117, -1], [9, 1, 11, -1], [9, 1, 71, -1],151  [9, 1, 73, -1], [9, 1, 110, -1], [9, 1, 116, -1], [10, 1, 12, -1], [10, 1, 72, -1], [10, 1, 80, -1], [10, 1, 113,152  -1], [10, 1, 119, -1], [11, 1, 71, -1], [11, 1, 73, -1], [11, 1, 110, -1], [11, 1, 116, -1], [12, 1, 72, -1], [12,153  1, 80, -1], [12, 1, 113, -1], [12, 1, 119, -1], [13, 2, 81, -2], [13, 2, 122, -2], [14, 1], [14, 1, 16, -1], [14,154  1, 17, 1], [14, 1, 19, 1], [14, 1, 23, -1, 68, 1, 71, -1, 107, -1, 108, 1], [14, 1, 29, 1], [14, 1, 31, 1], [14, 1,155  38, -1], [14, 1, 40, -1], [14, 1, 41, -1], [14, 1, 42, 1], [14, 1, 47, -1], [14, 1, 48, 1], [14, 1, 52, 1], [14, 1,156  58, 1], [14, 1, 61, -1], [14, 1, 67, -1], [14, 1, 82, -1], [14, 1, 83, 1], [14, 1, 87, 1], [14, 1, 90, -1], [14, 1,157  100, -1], [14, 1, 101, 1], [14, 1, 105, 1], [14, 1, 108, -1], [15, 1], [15, 1, 18, 1], [15, 1, 24, -1, 69, 1, 72,158  -1, 106, -1, 107, 1], [15, 1, 30, 1], [15, 1, 39, -1], [15, 1, 44, -1], [15, 1, 45, 1], [15, 1, 55, 1], [15, 1, 64,159  -1], [15, 1, 91, -1], [15, 1, 92, 1], [15, 1, 96, 1], [15, 1, 99, -1], [16, 1], [16, 1, 17, 1], [16, 1, 19, 1],160  [16, 1, 25, -1, 70, 1, 73, -1, 106, 1], [16, 1, 29, 1], [16, 1, 31, 1], [16, 1, 38, -1], [16, 1, 40, -1], [16, 1,161  41, -1], [16, 1, 42, 1], [16, 1, 47, -1], [16, 1, 48, 1], [16, 1, 52, 1], [16, 1, 58, 1], [16, 1, 61, -1], [16, 1,162  67, -1], [16, 1, 82, -1], [16, 1, 83, 1], [16, 1, 87, 1], [16, 1, 90, -1], [16, 1, 100, -1], [16, 1, 101, 1], [16,163  1, 105, 1], [16, 1, 108, -1], [17, 1], [17, 1, 19, -1], [17, 1, 26, -1, 71, 1, 74, -1, 104, -1, 105, 1], [17, 1,164  29, -1], [17, 1, 31, -1], [17, 1, 38, 1], [17, 1, 40, 1], [17, 1, 41, 1], [17, 1, 42, -1], [17, 1, 47, 1], [17, 1,165  48, -1], [17, 1, 52, -1], [17, 1, 58, -1], [17, 1, 61, 1], [17, 1, 67, 1], [17, 1, 82, 1], [17, 1, 83, -1], [17, 1,166  87, -1], [17, 1, 90, 1], [17, 1, 100, 1], [17, 1, 101, -1], [17, 1, 105, -1], [17, 1, 108, 1], [18, 1], [18, 1, 27,167  -1, 72, 1, 75, -1, 103, -1, 104, 1], [18, 1, 30, -1], [18, 1, 39, 1], [18, 1, 44, 1], [18, 1, 45, -1], [18, 1, 55,168  -1], [18, 1, 64, 1], [18, 1, 91, 1], [18, 1, 92, -1], [18, 1, 96, -1], [18, 1, 99, 1], [19, 1], [19, 1, 28, -1, 73,169  1, 76, -1, 103, 1], [19, 1, 29, -1], [19, 1, 31, -1], [19, 1, 38, 1], [19, 1, 40, 1], [19, 1, 41, 1], [19, 1, 42,170  -1], [19, 1, 47, 1], [19, 1, 48, -1], [19, 1, 52, -1], [19, 1, 58, -1], [19, 1, 61, 1], [19, 1, 67, 1], [19, 1, 82,171  1], [19, 1, 83, -1], [19, 1, 87, -1], [19, 1, 90, 1], [19, 1, 100, 1], [19, 1, 101, -1], [19, 1, 105, -1], [19, 1,172  108, 1], [20, 1], [20, 1, 22, -1], [20, 1, 29, -1, 74, 1, 101, -1, 102, 1]]173174def constraintRows1 : List (List Int) :=175  [[20, 1, 43, -1], [20, 1, 49, -1], [20, 1, 84, -1], [20, 1, 102, -1], [21, 1], [21, 1, 30, -1, 75, 1, 100, -1, 101,176  1], [21, 1, 46, -1], [21, 1, 93, -1], [22, 1], [22, 1, 31, -1, 76, 1, 100, 1], [22, 1, 43, -1], [22, 1, 49, -1],177  [22, 1, 84, -1], [22, 1, 102, -1], [23, 1, 25, -1], [23, 1, 26, 1], [23, 1, 28, 1], [23, 1, 32, -1, 77, 1, 80, -1,178  98, -1, 99, 1], [23, 1, 32, 1], [23, 1, 34, 1], [23, 1, 35, -1], [23, 1, 37, -1], [23, 1, 50, -1], [23, 1, 51, 1],179  [23, 1, 56, -1], [23, 1, 57, 1], [23, 1, 59, 1], [23, 1, 60, -1], [23, 1, 65, 1], [23, 1, 66, -1], [23, 1, 85, -1],180  [23, 1, 86, 1], [23, 1, 88, 1], [23, 1, 89, -1], [23, 1, 103, -1], [23, 1, 104, 1], [23, 1, 106, 1], [23, 1, 107,181  -1], [24, 1, 27, 1], [24, 1, 33, -1, 78, 1, 81, -2, 97, -1, 98, 1], [24, 1, 33, 1], [24, 1, 36, -1], [24, 1, 53,182  -1], [24, 1, 54, 1], [24, 1, 62, 1], [24, 1, 63, -1], [24, 1, 94, -1], [24, 1, 95, 1], [24, 1, 97, 1], [24, 1, 98,183  -1], [25, 1, 26, 1], [25, 1, 28, 1], [25, 1, 32, 1], [25, 1, 34, -1, 79, 1, 80, -1, 97, 1], [25, 1, 34, 1], [25, 1,184  35, -1], [25, 1, 37, -1], [25, 1, 50, -1], [25, 1, 51, 1], [25, 1, 56, -1], [25, 1, 57, 1], [25, 1, 59, 1], [25, 1,185  60, -1], [25, 1, 65, 1], [25, 1, 66, -1], [25, 1, 85, -1], [25, 1, 86, 1], [25, 1, 88, 1], [25, 1, 89, -1], [25, 1,186  103, -1], [25, 1, 104, 1], [25, 1, 106, 1], [25, 1, 107, -1], [26, 1, 28, -1], [26, 1, 32, -1], [26, 1, 34, -1],187  [26, 1, 35, -1, 79, -1, 80, 1, 95, -1, 96, 1], [26, 1, 35, 1], [26, 1, 37, 1], [26, 1, 50, 1], [26, 1, 51, -1],188  [26, 1, 56, 1], [26, 1, 57, -1], [26, 1, 59, -1], [26, 1, 60, 1], [26, 1, 65, -1], [26, 1, 66, 1], [26, 1, 85, 1],189  [26, 1, 86, -1], [26, 1, 88, -1], [26, 1, 89, 1], [26, 1, 103, 1], [26, 1, 104, -1], [26, 1, 106, -1], [26, 1, 107,190  1], [27, 1, 33, -1], [27, 1, 36, -1, 78, -1, 81, 2, 94, -1, 95, 1], [27, 1, 36, 1], [27, 1, 53, 1], [27, 1, 54,191  -1], [27, 1, 62, -1], [27, 1, 63, 1], [27, 1, 94, 1], [27, 1, 95, -1], [27, 1, 97, -1], [27, 1, 98, 1], [28, 1, 32,192  -1], [28, 1, 34, -1], [28, 1, 35, 1], [28, 1, 37, -1, 77, -1, 80, 1, 94, 1], [28, 1, 37, 1], [28, 1, 50, 1], [28,193  1, 51, -1], [28, 1, 56, 1], [28, 1, 57, -1], [28, 1, 59, -1], [28, 1, 60, 1], [28, 1, 65, -1], [28, 1, 66, 1], [28,194  1, 85, 1], [28, 1, 86, -1], [28, 1, 88, -1], [28, 1, 89, 1], [28, 1, 103, 1], [28, 1, 104, -1], [28, 1, 106, -1],195  [28, 1, 107, 1], [29, 1], [29, 1, 31, -1], [29, 1, 38, -1, 79, 1, 92, -1, 93, 1], [29, 1, 38, 1], [29, 1, 40, 1],196  [29, 1, 41, 1], [29, 1, 42, -1], [29, 1, 47, 1], [29, 1, 48, -1], [29, 1, 52, -1], [29, 1, 58, -1], [29, 1, 61, 1],197  [29, 1, 67, 1], [29, 1, 82, 1], [29, 1, 83, -1], [29, 1, 87, -1], [29, 1, 90, 1], [29, 1, 100, 1], [29, 1, 101,198  -1], [29, 1, 105, -1], [29, 1, 108, 1], [30, 1], [30, 1, 39, -1, 78, 1, 91, -1, 92, 1], [30, 1, 39, 1], [30, 1, 44,199  1], [30, 1, 45, -1], [30, 1, 55, -1], [30, 1, 64, 1], [30, 1, 91, 1], [30, 1, 92, -1], [30, 1, 96, -1], [30, 1, 99,200  1], [31, 1], [31, 1, 38, 1], [31, 1, 40, -1, 77, 1, 91, 1], [31, 1, 40, 1], [31, 1, 41, 1], [31, 1, 42, -1], [31,201  1, 47, 1], [31, 1, 48, -1], [31, 1, 52, -1], [31, 1, 58, -1], [31, 1, 61, 1], [31, 1, 67, 1], [31, 1, 82, 1], [31,202  1, 83, -1], [31, 1, 87, -1], [31, 1, 90, 1], [31, 1, 100, 1], [31, 1, 101, -1], [31, 1, 105, -1], [31, 1, 108, 1],203  [32, 1, 34, -1], [32, 1, 35, 1], [32, 1, 37, 1], [32, 1, 50, 1], [32, 1, 51, -1], [32, 1, 56, 1], [32, 1, 57, -1],204  [32, 1, 59, -1], [32, 1, 60, 1], [32, 1, 65, -1], [32, 1, 66, 1], [32, 1, 73, -1, 76, 1, 89, -1, 90, 1], [32, 1,205  85, 1], [32, 1, 86, -1], [32, 1, 88, -1], [32, 1, 89, 1], [32, 1, 103, 1], [32, 1, 104, -1], [32, 1, 106, -1], [32,206  1, 107, 1], [33, 1, 36, 1], [33, 1, 53, 1], [33, 1, 54, -1], [33, 1, 62, -1], [33, 1, 63, 1], [33, 1, 72, -1, 75,207  1, 88, -1, 89, 1], [33, 1, 94, 1], [33, 1, 95, -1], [33, 1, 97, -1], [33, 1, 98, 1], [34, 1, 35, 1], [34, 1, 37,208  1], [34, 1, 50, 1], [34, 1, 51, -1], [34, 1, 56, 1], [34, 1, 57, -1], [34, 1, 59, -1], [34, 1, 60, 1], [34, 1, 65,209  -1], [34, 1, 66, 1], [34, 1, 71, -1, 74, 1, 88, 1], [34, 1, 85, 1], [34, 1, 86, -1], [34, 1, 88, -1], [34, 1, 89,210  1], [34, 1, 103, 1], [34, 1, 104, -1], [34, 1, 106, -1], [34, 1, 107, 1], [35, 1, 37, -1], [35, 1, 50, -1], [35, 1,211  51, 1], [35, 1, 56, -1], [35, 1, 57, 1], [35, 1, 59, 1], [35, 1, 60, -1], [35, 1, 65, 1], [35, 1, 66, -1], [35, 1,212  70, -1, 73, 1, 86, -1, 87, 1], [35, 1, 85, -1], [35, 1, 86, 1], [35, 1, 88, 1], [35, 1, 89, -1], [35, 1, 103, -1],213  [35, 1, 104, 1], [35, 1, 106, 1], [35, 1, 107, -1], [36, 1, 53, -1], [36, 1, 54, 1], [36, 1, 62, 1], [36, 1, 63,214  -1], [36, 1, 69, -1, 72, 1, 85, -1, 86, 1], [36, 1, 94, -1], [36, 1, 95, 1], [36, 1, 97, 1], [36, 1, 98, -1], [37,215  1, 50, -1]]216217def constraintRows2 : List (List Int) :=218  [[37, 1, 51, 1], [37, 1, 56, -1], [37, 1, 57, 1], [37, 1, 59, 1], [37, 1, 60, -1], [37, 1, 65, 1], [37, 1, 66, -1],219  [37, 1, 68, -1, 71, 1, 85, 1], [37, 1, 85, -1], [37, 1, 86, 1], [37, 1, 88, 1], [37, 1, 89, -1], [37, 1, 103, -1],220  [37, 1, 104, 1], [37, 1, 106, 1], [37, 1, 107, -1], [38, 1], [38, 1, 40, -1], [38, 1, 41, -1], [38, 1, 42, 1], [38,221  1, 47, -1], [38, 1, 48, 1], [38, 1, 52, 1], [38, 1, 58, 1], [38, 1, 61, -1], [38, 1, 67, -1], [38, 1, 70, 1, 83,222  -1, 84, 1], [38, 1, 82, -1], [38, 1, 83, 1], [38, 1, 87, 1], [38, 1, 90, -1], [38, 1, 100, -1], [38, 1, 101, 1],223  [38, 1, 105, 1], [38, 1, 108, -1], [39, 1], [39, 1, 44, -1], [39, 1, 45, 1], [39, 1, 55, 1], [39, 1, 64, -1], [39,224  1, 69, 1, 82, -1, 83, 1], [39, 1, 91, -1], [39, 1, 92, 1], [39, 1, 96, 1], [39, 1, 99, -1], [40, 1], [40, 1, 41,225  -1], [40, 1, 42, 1], [40, 1, 47, -1], [40, 1, 48, 1], [40, 1, 52, 1], [40, 1, 58, 1], [40, 1, 61, -1], [40, 1, 67,226  -1], [40, 1, 68, 1, 82, 1], [40, 1, 82, -1], [40, 1, 83, 1], [40, 1, 87, 1], [40, 1, 90, -1], [40, 1, 100, -1],227  [40, 1, 101, 1], [40, 1, 105, 1], [40, 1, 108, -1], [41, 1], [41, 1, 42, 1], [41, 1, 47, -1], [41, 1, 48, 1], [41,228  1, 50, -1, 82, 1, 85, -1, 109, 1, 110, -1], [41, 1, 52, 1], [41, 1, 58, 1], [41, 1, 61, -1], [41, 1, 67, -1], [41,229  1, 82, -1], [41, 1, 83, 1], [41, 1, 87, 1], [41, 1, 90, -1], [41, 1, 100, -1], [41, 1, 101, 1], [41, 1, 105, 1],230  [41, 1, 108, -1], [42, 1], [42, 1, 47, 1], [42, 1, 48, -1], [42, 1, 51, -1, 83, 1, 86, -1, 110, 1, 111, -1], [42,231  1, 52, -1], [42, 1, 58, -1], [42, 1, 61, 1], [42, 1, 67, 1], [42, 1, 82, 1], [42, 1, 83, -1], [42, 1, 87, -1], [42,232  1, 90, 1], [42, 1, 100, 1], [42, 1, 101, -1], [42, 1, 105, -1], [42, 1, 108, 1], [43, 1], [43, 1, 49, -1], [43, 1,233  52, -1, 84, 1, 87, -1, 111, 1], [43, 1, 84, -1], [43, 1, 102, -1], [44, 1], [44, 1, 45, 1], [44, 1, 53, -1, 85, 1,234  88, -1, 112, 1, 113, -1], [44, 1, 55, 1], [44, 1, 64, -1], [44, 1, 91, -1], [44, 1, 92, 1], [44, 1, 96, 1], [44, 1,235  99, -1], [45, 1], [45, 1, 54, -1, 86, 1, 89, -1, 113, 1, 114, -1], [45, 1, 55, -1], [45, 1, 64, 1], [45, 1, 91, 1],236  [45, 1, 92, -1], [45, 1, 96, -1], [45, 1, 99, 1], [46, 1], [46, 1, 55, -1, 87, 1, 90, -1, 114, 1], [46, 1, 93, -1],237  [47, 1], [47, 1, 48, 1], [47, 1, 52, 1], [47, 1, 56, -1, 88, 1, 115, 1, 116, -1], [47, 1, 58, 1], [47, 1, 61, -1],238  [47, 1, 67, -1], [47, 1, 82, -1], [47, 1, 83, 1], [47, 1, 87, 1], [47, 1, 90, -1], [47, 1, 100, -1], [47, 1, 101,239  1], [47, 1, 105, 1], [47, 1, 108, -1], [48, 1], [48, 1, 52, -1], [48, 1, 57, -1, 89, 1, 116, 1, 117, -1], [48, 1,240  58, -1], [48, 1, 61, 1], [48, 1, 67, 1], [48, 1, 82, 1], [48, 1, 83, -1], [48, 1, 87, -1], [48, 1, 90, 1], [48, 1,241  100, 1], [48, 1, 101, -1], [48, 1, 105, -1], [48, 1, 108, 1], [49, 1], [49, 1, 58, -1, 90, 1, 117, 1], [49, 1, 84,242  -1], [49, 1, 102, -1], [50, 1, 51, 1], [50, 1, 56, -1], [50, 1, 57, 1], [50, 1, 59, -1, 91, 1, 94, -1, 118, 1, 119,243  -1], [50, 1, 59, 1], [50, 1, 60, -1], [50, 1, 65, 1], [50, 1, 66, -1], [50, 1, 85, -1], [50, 1, 86, 1], [50, 1, 88,244  1], [50, 1, 89, -1], [50, 1, 103, -1], [50, 1, 104, 1], [50, 1, 106, 1], [50, 1, 107, -1], [51, 1, 56, 1], [51, 1,245  57, -1], [51, 1, 59, -1], [51, 1, 60, -1, 92, 1, 95, -1, 119, 1, 120, -1], [51, 1, 60, 1], [51, 1, 65, -1], [51, 1,246  66, 1], [51, 1, 85, 1], [51, 1, 86, -1], [51, 1, 88, -1], [51, 1, 89, 1], [51, 1, 103, 1], [51, 1, 104, -1], [51,247  1, 106, -1], [51, 1, 107, 1], [52, 1], [52, 1, 58, -1], [52, 1, 61, -1, 93, 1, 96, -1, 120, 1], [52, 1, 61, 1],248  [52, 1, 67, 1], [52, 1, 82, 1], [52, 1, 83, -1], [52, 1, 87, -1], [52, 1, 90, 1], [52, 1, 100, 1], [52, 1, 101,249  -1], [52, 1, 105, -1], [52, 1, 108, 1], [53, 1, 54, 1], [53, 1, 62, -1, 94, 1, 97, -1, 121, 1, 122, -2], [53, 1,250  62, 1], [53, 1, 63, -1], [53, 1, 94, -1], [53, 1, 95, 1], [53, 1, 97, 1], [53, 1, 98, -1], [54, 1, 62, -1], [54, 1,251  63, -1, 95, 1, 98, -1, 121, -1, 122, 2], [54, 1, 63, 1], [54, 1, 94, 1], [54, 1, 95, -1], [54, 1, 97, -1], [54, 1,252  98, 1], [55, 1], [55, 1, 64, -1, 96, 1, 99, -1, 121, 1], [55, 1, 64, 1], [55, 1, 91, 1], [55, 1, 92, -1], [55, 1,253  96, -1], [55, 1, 99, 1], [56, 1, 57, 1], [56, 1, 59, 1], [56, 1, 60, -1], [56, 1, 65, -1, 97, 1, 119, -1, 120, 1],254  [56, 1, 65, 1], [56, 1, 66, -1], [56, 1, 85, -1], [56, 1, 86, 1], [56, 1, 88, 1], [56, 1, 89, -1], [56, 1, 103,255  -1], [56, 1, 104, 1], [56, 1, 106, 1], [56, 1, 107, -1], [57, 1, 59, -1], [57, 1, 60, 1], [57, 1, 65, -1], [57, 1,256  66, -1, 98, 1, 118, -1, 119, 1], [57, 1, 66, 1], [57, 1, 85, 1], [57, 1, 86, -1], [57, 1, 88, -1], [57, 1, 89, 1],257  [57, 1, 103, 1], [57, 1, 104, -1], [57, 1, 106, -1], [57, 1, 107, 1], [58, 1], [58, 1, 61, 1], [58, 1, 67, -1, 99,258  1, 118, 1], [58, 1, 67, 1], [58, 1, 82, 1], [58, 1, 83, -1], [58, 1, 87, -1], [58, 1, 90, 1], [58, 1, 100, 1]]259260def constraintRows3 : List (List Int) :=261  [[58, 1, 101, -1], [58, 1, 105, -1], [58, 1, 108, 1], [59, 1, 60, 1], [59, 1, 65, -1], [59, 1, 66, 1], [59, 1, 85,262  1], [59, 1, 86, -1], [59, 1, 88, -1], [59, 1, 89, 1], [59, 1, 100, 1, 103, -1, 116, -1, 117, 1], [59, 1, 103, 1],263  [59, 1, 104, -1], [59, 1, 106, -1], [59, 1, 107, 1], [60, 1, 65, 1], [60, 1, 66, -1], [60, 1, 85, -1], [60, 1, 86,264  1], [60, 1, 88, 1], [60, 1, 89, -1], [60, 1, 101, 1, 104, -1, 115, -1, 116, 1], [60, 1, 103, -1], [60, 1, 104, 1],265  [60, 1, 106, 1], [60, 1, 107, -1], [61, 1], [61, 1, 67, -1], [61, 1, 82, -1], [61, 1, 83, 1], [61, 1, 87, 1], [61,266  1, 90, -1], [61, 1, 100, -1], [61, 1, 101, 1], [61, 1, 102, 1, 105, -1, 115, 1], [61, 1, 105, 1], [61, 1, 108, -1],267  [62, 1, 63, 1], [62, 1, 94, 1], [62, 1, 95, -1], [62, 1, 97, -1], [62, 1, 98, 1], [62, 1, 103, 1, 106, -1, 113, -1,268  114, 1], [63, 1, 94, -1], [63, 1, 95, 1], [63, 1, 97, 1], [63, 1, 98, -1], [63, 1, 104, 1, 107, -1, 112, -1, 113,269  1], [64, 1], [64, 1, 91, -1], [64, 1, 92, 1], [64, 1, 96, 1], [64, 1, 99, -1], [64, 1, 105, 1, 108, -1, 112, 1],270  [65, 1, 66, 1], [65, 1, 85, 1], [65, 1, 86, -1], [65, 1, 88, -1], [65, 1, 89, 1], [65, 1, 103, 1], [65, 1, 104,271  -1], [65, 1, 106, -1], [65, 1, 106, 1, 110, -1, 111, 1], [65, 1, 107, 1], [66, 1, 85, -1], [66, 1, 86, 1], [66, 1,272  88, 1], [66, 1, 89, -1], [66, 1, 103, -1], [66, 1, 104, 1], [66, 1, 106, 1], [66, 1, 107, -1], [66, 1, 107, 1, 109,273  -1, 110, 1], [67, 1], [67, 1, 82, -1], [67, 1, 83, 1], [67, 1, 87, 1], [67, 1, 90, -1], [67, 1, 100, -1], [67, 1,274  101, 1], [67, 1, 105, 1], [67, 1, 108, -1], [67, 1, 108, 1, 109, 1], [68, 1], [68, 1, 70, -1], [68, 1, 74, -1],275  [68, 1, 76, -1], [68, 1, 109, -1], [68, 1, 111, -1], [68, 1, 115, -1], [68, 1, 117, -1], [69, 1], [69, 1, 75, -1],276  [69, 1, 77, -1], [69, 1, 79, -1], [69, 1, 112, -1], [69, 1, 114, -1], [69, 1, 118, -1], [69, 1, 120, -1], [70, 1],277  [70, 1, 74, -1], [70, 1, 76, -1], [70, 1, 109, -1], [70, 1, 111, -1], [70, 1, 115, -1], [70, 1, 117, -1], [71, 1,278  73, -1], [71, 1, 110, -1], [71, 1, 116, -1], [72, 1, 80, -1], [72, 1, 113, -1], [72, 1, 119, -1], [73, 1, 110, -1],279  [73, 1, 116, -1], [74, 1], [74, 1, 76, -1], [74, 1, 109, -1], [74, 1, 111, -1], [74, 1, 115, -1], [74, 1, 117, -1],280  [75, 1], [75, 1, 77, -1], [75, 1, 79, -1], [75, 1, 112, -1], [75, 1, 114, -1], [75, 1, 118, -1], [75, 1, 120, -1],281  [76, 1], [76, 1, 109, -1], [76, 1, 111, -1], [76, 1, 115, -1], [76, 1, 117, -1], [77, 1], [77, 1, 79, -1], [77, 1,282  112, -1], [77, 1, 114, -1], [77, 1, 118, -1], [77, 1, 120, -1], [78, 1], [78, 1, 121, -1], [79, 1], [79, 1, 112,283  -1], [79, 1, 114, -1], [79, 1, 118, -1], [79, 1, 120, -1], [80, 1, 113, -1], [80, 1, 119, -1], [81, 2, 122, -2],284  [82, 1], [82, 1, 83, 1], [82, 1, 87, 1], [82, 1, 90, -1], [82, 1, 100, -1], [82, 1, 101, 1], [82, 1, 105, 1], [82,285  1, 108, -1], [83, 1], [83, 1, 87, -1], [83, 1, 90, 1], [83, 1, 100, 1], [83, 1, 101, -1], [83, 1, 105, -1], [83, 1,286  108, 1], [84, 1], [84, 1, 102, -1], [85, 1, 86, 1], [85, 1, 88, 1], [85, 1, 89, -1], [85, 1, 103, -1], [85, 1, 104,287  1], [85, 1, 106, 1], [85, 1, 107, -1], [86, 1, 88, -1], [86, 1, 89, 1], [86, 1, 103, 1], [86, 1, 104, -1], [86, 1,288  106, -1], [86, 1, 107, 1], [87, 1], [87, 1, 90, 1], [87, 1, 100, 1], [87, 1, 101, -1], [87, 1, 105, -1], [87, 1,289  108, 1], [88, 1, 89, 1], [88, 1, 103, 1], [88, 1, 104, -1], [88, 1, 106, -1], [88, 1, 107, 1], [89, 1, 103, -1],290  [89, 1, 104, 1], [89, 1, 106, 1], [89, 1, 107, -1], [90, 1], [90, 1, 100, -1], [90, 1, 101, 1], [90, 1, 105, 1],291  [90, 1, 108, -1], [91, 1], [91, 1, 92, 1], [91, 1, 96, 1], [91, 1, 99, -1], [92, 1], [92, 1, 96, -1], [92, 1, 99,292  1], [93, 1], [94, 1, 95, 1], [94, 1, 97, 1], [94, 1, 98, -1], [95, 1, 97, -1], [95, 1, 98, 1], [96, 1], [96, 1, 99,293  1], [97, 1, 98, 1], [99, 1], [100, 1], [100, 1, 101, 1], [100, 1, 105, 1], [100, 1, 108, -1], [101, 1], [101, 1,294  105, -1], [101, 1, 108, 1], [102, 1], [103, 1, 104, 1], [103, 1, 106, 1], [103, 1, 107, -1], [104, 1, 106, -1],295  [104, 1, 107, 1], [105, 1], [105, 1, 108, 1], [106, 1, 107, 1], [108, 1], [109, 1], [109, 1, 111, -1], [109, 1,296  115, -1], [109, 1, 117, -1], [110, 1, 116, -1], [111, 1], [111, 1, 115, -1], [111, 1, 117, -1], [112, 1], [112, 1,297  114, -1], [112, 1, 118, -1], [112, 1, 120, -1], [113, 1, 119, -1], [114, 1], [114, 1, 118, -1], [114, 1, 120, -1],298  [115, 1], [115, 1, 117, -1], [117, 1], [118, 1], [118, 1, 120, -1], [120, 1], [121, 1]]299300def constraintRows : List (List Int) := constraintRows0 ++ constraintRows1 ++ constraintRows2 ++ constraintRows3301302/-- A constraint row applied to a vector. -/303def rowDot (r v : List Int) : Int :=304  (r.foldl (fun (s : Int × Option Int) x =>305    match s.2 with306    | none => (s.1, some x)307    | some a => (s.1 + x * lget v a.toNat, none)) (0, none)).1308309/-- 27:C2, 27:X3 — the two admissible vectors satisfy every one of the `1 023` constraint rows (python's `13 338` rows310distinct up to a scalar; that the range-1 translation-, gauge- and hypercubic-invariant quadratic actions at `L = 4` form311exactly a two-dimensional space is the rank `121` of the rows, python's check A5), Maxwell's plaquette action satisfies312them too, and it is their difference: `2 · Maxwell = B − A`. -/313theorem admissible_two :314    constraintRows.length = 1023 ∧ admissibleA.length = 123 ∧ admissibleB.length = 123 ∧ maxwellForm.length = 123 ∧315    constraintRows.all (fun r => rowDot r admissibleA == 0) = true ∧316    constraintRows.all (fun r => rowDot r admissibleB == 0) = true ∧317    constraintRows.all (fun r => rowDot r maxwellForm == 0) = true ∧318    maxwellForm.map (fun c => 2 * c) = List.zipWith (fun b a => b - a) admissibleB admissibleA ∧319    admissibleA ≠ admissibleB := by320  decide +kernel321322/-! ## The colour sector over `𝔽₄` (27:C7, X7) -/323324/-- `𝔽₄ = 𝔽₂[w]`, `w² = w + 1`: the four elements `0, 1, w, w²`. -/325inductive F4 where326  | z | o | w | w2327  deriving DecidableEq, Repr328329namespace F4330331def add : F4 → F4 → F4332  | z, z => z | z, o => o | z, w => w | z, w2 => w2333  | o, z => o | o, o => z | o, w => w2 | o, w2 => w334  | w, z => w | w, o => w2 | w, w => z | w, w2 => o335  | w2, z => w2 | w2, o => w | w2, w => o | w2, w2 => z336337def mul : F4 → F4 → F4338  | z, z => z | z, o => z | z, w => z | z, w2 => z339  | o, z => z | o, o => o | o, w => w | o, w2 => w2340  | w, z => z | w, o => w | w, w => w2 | w, w2 => o341  | w2, z => z | w2, o => w2 | w2, w => o | w2, w2 => w342343/-- Frobenius `x ↦ x²`, the conjugation of `𝔽₄` over `𝔽₂`. -/344def conj : F4 → F4345  | z => z | o => o | w => w2 | w2 => w346347instance : Add F4 := ⟨add⟩348instance : Mul F4 := ⟨mul⟩349350/-- A `3 × 3` matrix as its nine entries in reading order. -/351abbrev M := List F4352353/-- The entry of a list of `𝔽₄` values, `0` past its end. -/354def fget : List F4 → Nat → F4355  | [], _ => z356  | x :: _, 0 => x357  | _ :: l, n + 1 => fget l n358359def at' (A : M) (i j : Nat) : F4 := fget A (3 * i + j)360361def mm (A B : M) : M := (List.range 9).map (fun k =>362  at' A (k / 3) 0 * at' B 0 (k % 3) + at' A (k / 3) 1 * at' B 1 (k % 3) + at' A (k / 3) 2 * at' B 2 (k % 3))363364def dg (A : M) : M := (List.range 9).map (fun k => conj (at' A (k % 3) (k / 3)))365366def det (A : M) : F4 :=367  at' A 0 0 * (at' A 1 1 * at' A 2 2 + at' A 1 2 * at' A 2 1) + at' A 0 1 * (at' A 1 0 * at' A 2 2 + at' A 1 2 * at' A 2 0) +368    at' A 0 2 * (at' A 1 0 * at' A 2 1 + at' A 1 1 * at' A 2 0)369370def one : M := [o, z, z, z, o, z, z, z, o]371372def scal (x : F4) : M := [x, z, z, z, x, z, z, z, x]373374end F4375376open F4 in377/-- 27:C7, 27:X7 — the scalar centre of `SU(3, 2)` over `𝔽₄`: the scalars `x I` with `x x̄ = 1` and `x³ = 1` are the three378cube roots of unity `1, w, w²` (`ℤ₃`, colour triality), `0` is not one, and each commutes with `U₁` and `U₂`; that the379centre is no larger is the ledger file's check E1 (all `216²` products). -/380theorem su3_centre :381    ([o, w, w2].all (fun x => x * conj x == o && x * x * x == o)) = true ∧382    (z * conj z == o) = false ∧ [o, w, w2].length = 3 ∧ 2 + 1 = 3 ∧383    ([o, w, w2].all (fun x => mm (scal x) [z, z, o, z, o, z, o, z, z] == mm [z, z, o, z, o, z, o, z, z] (scal x) &&384      mm (scal x) [z, z, o, z, w, z, w2, z, z] == mm [z, z, o, z, w, z, w2, z, z] (scal x))) = true := by385  decide386387open F4 in388/-- 27:C7, 27:X7, 27:X1 — the gluon self-coupling over `𝔽₄`: the two elements `U₁ = [[0,0,1],[0,1,0],[1,0,0]]` and389`U₂ = [[0,0,1],[0,w,0],[w²,0,0]]` of `SU(3, 2)` (`U†U = I`, `det U = 1`) do not commute, their commutator plaquette390`U₁U₂U₁⁻¹U₂⁻¹ = diag(w², 1, w) ≠ I`, while the abelian control `D₁ = diag(1, w, w²)`, `D₂ = diag(w, 1, w²)` returns `I`. -/391theorem gluon_commutator :392    let U₁ : M := [z, z, o, z, o, z, o, z, z]393    let U₂ : M := [z, z, o, z, w, z, w2, z, z]394    let D₁ : M := [o, z, z, z, w, z, z, z, w2]395    let D₂ : M := [w, z, z, z, o, z, z, z, w2]396    mm (dg U₁) U₁ = one ∧ mm (dg U₂) U₂ = one ∧ det U₁ = o ∧ det U₂ = o ∧397    mm U₁ U₂ ≠ mm U₂ U₁ ∧398    mm (mm U₁ U₂) (mm (dg U₁) (dg U₂)) = [w2, z, z, z, o, z, z, z, w] ∧399    mm (mm U₁ U₂) (mm (dg U₁) (dg U₂)) ≠ one ∧400    mm (mm D₁ D₂) (mm (dg D₁) (dg D₂)) = one := by401  decide402403/-! ## The strong-CP angle: Hermitian mass matrices over `𝔽_p[√−3]` (27:X11, P9) -/404405/-- The Hermitian matrix with diagonal `(d₀, d₁, d₂)` in the shell and upper entries `u₀₁, u₀₂, u₁₂`. -/406def herm {p : Nat} [Pos p] {ν : Shell p} (d₀ d₁ d₂ : Shell p) (u₀₁ u₀₂ u₁₂ : Ext p ν) : M3 p ν :=407  ⟨Ext.ofShell d₀, u₀₁, u₀₂, Ext.conj u₀₁, Ext.ofShell d₁, u₁₂, Ext.conj u₀₂, Ext.conj u₁₂, Ext.ofShell d₂⟩408409/-- `ν = −3` on `𝔽₁₇` and on `𝔽₅₃` (`14 + 3 = 0`, `50 + 3 = 0`). -/410abbrev nu17 : Shell 17 := 14411abbrev nu53 : Shell 53 := 50412413/-- The textured up and down mass matrices and the circulant, over `𝔽₁₇[√−3]`: `M_u = herm (3, 7, 11) (1 + i, 2 + 3i, 4 + i)`,414`M_d = herm (2, 5, 13) (3 + 2i, 1 + 4i, 5 + 2i)`, `M_c = herm (7, 7, 7) (b, b̄, b)` with `b = 2 + i` (the circulant's determinant415`(7 − 5)(7 + 1)(7 + 4) = 176`, nonzero on both shells; at `a = 5` it would vanish). -/416def mu17 : M3 17 nu17 := herm 3 7 11 ⟨1, 1⟩ ⟨2, 3⟩ ⟨4, 1⟩417def md17 : M3 17 nu17 := herm 2 5 13 ⟨3, 2⟩ ⟨1, 4⟩ ⟨5, 2⟩418def mc17 : M3 17 nu17 := herm 7 7 7 ⟨2, 1⟩ ⟨2, 16⟩ ⟨2, 1⟩419/-- The same three matrices over `𝔽₅₃[√−3]`. -/420def mu53 : M3 53 nu53 := herm 3 7 11 ⟨1, 1⟩ ⟨2, 3⟩ ⟨4, 1⟩421def md53 : M3 53 nu53 := herm 2 5 13 ⟨3, 2⟩ ⟨1, 4⟩ ⟨5, 2⟩422def mc53 : M3 53 nu53 := herm 7 7 7 ⟨2, 1⟩ ⟨2, 52⟩ ⟨2, 1⟩423424/-- 27:X11 — over `𝔽₁₇[√−3]` and `𝔽₅₃[√−3]`: the textured up and down mass matrices and the circulant are Hermitian425(`M† = M` entrywise), their determinants are nonzero and lie in the shell with `det (M_u M_d)` (`arg det = 0`, the strong-CP426angle vanishes), and `[M_u, M_d] ≠ 0` (no flavour symmetry forces the two to be simultaneously diagonal). -/427theorem ckm_free :428    ents (dag mu17) = ents mu17 ∧ ents (dag md17) = ents md17 ∧ ents (dag mc17) = ents mc17 ∧429    (det mu17).im = 0 ∧ (det md17).im = 0 ∧ (det mc17).im = 0 ∧ (det (mmul mu17 md17)).im = 0 ∧430    (det mu17).re ≠ 0 ∧ (det md17).re ≠ 0 ∧ (det mc17).re ≠ 0 ∧431    ents (mmul mu17 md17) ≠ ents (mmul md17 mu17) ∧432    ents (dag mu53) = ents mu53 ∧ ents (dag md53) = ents md53 ∧ ents (dag mc53) = ents mc53 ∧433    (det mu53).im = 0 ∧ (det md53).im = 0 ∧ (det mc53).im = 0 ∧ (det (mmul mu53 md53)).im = 0 ∧434    (det mu53).re ≠ 0 ∧ (det md53).re ≠ 0 ∧ (det mc53).re ≠ 0 ∧435    ents (mmul mu53 md53) ≠ ents (mmul md53 mu53) ∧436    nu17 + 3 = 0 ∧ nu53 + 3 = 0 := by437  decide +kernel438439440end FRC.Interactions441