Theme/Exclusivity.lean — FrcCore

1import FrcCore.Theme.Spectra23/-!4# FrcCore.Theme.Exclusivity — cardinal exclusivity: no intermediate conjugate of the shift is monomial (the fourier theme)56The eighth file of the fourier theme (6-fourier's blueprint of 8 October 2026, task T09). With `F^{[s]} = Σ_r c_r F^r`7(`frft_eq`) and `F^{[−s]} = F^{[n−s]} = Σ_r c'_r F^r`, the entry `(0, j)` of `F^{[s]} σ F^{[−s]}` off the three sites8`j ∈ {n−1, 0, 1}` is `i [(c₀ + c₂)(c'₃ x + c'₁ x⁻¹) + (c₁ + c₃)(c'₀ + c'₂)]` with `x = g^j`: row 0 of `F^{[s]} σ` is9`(c₀ + c₂) δ_{n−1} + (c₁ + c₃) i`, the last row of `F^{[−s]}` is `i (c'₁ x⁻¹ + c'₃ x)` off the sites, and its column10sums are `c'₀ + c'₂` by the geometric sum. So `x` times the entry is a quadratic in `x` with leading coefficient11`i (c₀ + c₂) c'₃`, nonzero for `s ∉ {0, κ, 2κ, 3κ}` (`c₀ + c₂ = ½ (1 + z_s²)` vanishes only at `z_s = ±i`; `c'₃` is a12geometric sum of a nontrivial root), and a quadratic has at most two roots: the row vanishes at no three distinct indices13off the sites (6:E8; the paper counts at least `4κ − 5` nonzero entries from this, a count not stated here). No axioms.14-/1516namespace FRC17namespace Shell18namespace Frame1920variable {p : Nat} [Pos p]2122/-! ## Ring identities (generated; `RE.sound`, decided by the kernel) -/2324theorem quad_diff_id (a b c x1 x2 : Shell p) :25    a * (x1 * x1) + b * x1 + c + -(a * (x2 * x2) + b * x2 + c) = (x1 + -x2) * (a * (x1 + x2) + b) :=26  RE.sound (look [a, b, c, x1, x2])27    (.add (.add (.add (.mul (.var 0) (.mul (.var 3) (.var 3))) (.mul (.var 1) (.var 3))) (.var 2)) (.neg (.add (.add (.mul (.var 0) (.mul (.var 4) (.var 4))) (.mul (.var 1) (.var 4))) (.var 2))))28    (.mul (.add (.var 3) (.neg (.var 4))) (.add (.mul (.var 0) (.add (.var 3) (.var 4))) (.var 1))) (by decide +kernel)2930theorem quad_lin_id (a b x1 x2 x3 : Shell p) :31    a * (x1 + x2) + b + -(a * (x1 + x3) + b) = a * (x2 + -x3) :=32  RE.sound (look [a, b, x1, x2, x3])33    (.add (.add (.mul (.var 0) (.add (.var 2) (.var 3))) (.var 1)) (.neg (.add (.mul (.var 0) (.add (.var 2) (.var 4))) (.var 1))))34    (.mul (.var 0) (.add (.var 3) (.neg (.var 4)))) (by decide +kernel)3536theorem row_quad_id (i s0 s1 d0 d1 d3 Z G : Shell p) :37    G * (s0 * ((d1 * i) * Z + (d3 * i) * G) + (s1 * i) * d0) = i * ((s0 * d3) * (G * G) + (s1 * d0) * G + s0 * d1) + (Z * G + -1) * (i * s0 * d1) :=38  RE.sound (look [i, s0, s1, d0, d1, d3, Z, G])39    (.mul (.var 7) (.add (.mul (.var 1) (.add (.mul (.mul (.var 4) (.var 0)) (.var 6)) (.mul (.mul (.var 5) (.var 0)) (.var 7)))) (.mul (.mul (.var 2) (.var 0)) (.var 3))))40    (.add (.mul (.var 0) (.add (.add (.mul (.mul (.var 1) (.var 5)) (.mul (.var 7) (.var 7))) (.mul (.mul (.var 2) (.var 3)) (.var 7))) (.mul (.var 1) (.var 4)))) (.mul (.add (.mul (.var 6) (.var 7)) (.neg .one)) (.mul (.mul (.var 0) (.var 1)) (.var 4)))) (by decide +kernel)4142/-- 6:E8, `c₀ + c₂ = ½ (1 + u²)`, `u = z^s`, i.e. `½ (1 + g^{−2s})`. -/43theorem even_coeff_id (q jj u : Shell p) :44    NF0 q jj u + NF2 q jj u = (q + q) * (1 + u * u) :=45  RE.sound (look [q, jj, u])46    (.add (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))))47    (.mul (.add (.var 0) (.var 0)) (.add .one (.mul (.var 2) (.var 2)))) (by decide +kernel)4849theorem odd_coeff_id (q jj u : Shell p) :50    NF3 q jj u = q * (1 + u * ((jj * jj) * jj) + (u * ((jj * jj) * jj)) * (u * ((jj * jj) * jj)) + ((u * ((jj * jj) * jj)) * (u * ((jj * jj) * jj))) * (u * ((jj * jj) * jj))) + (jj * jj + 1) * (-(q * jj * jj * jj * jj * jj * jj * jj * u * u * u) + q * jj * jj * jj * jj * jj * u * u * u + -(q * jj * jj * jj * jj * u * u) + -(q * jj * jj * jj * u * u * u) + q * jj * jj * u * u + q * jj * u * u * u + -(q * jj * u) + -(q * u * u)) :=51  RE.sound (look [q, jj, u])52    (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.var 1) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))53    (.add (.mul (.var 0) (.add (.add (.add .one (.mul (.var 2) (.mul (.mul (.var 1) (.var 1)) (.var 1)))) (.mul (.mul (.var 2) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 2) (.mul (.mul (.var 1) (.var 1)) (.var 1))))) (.mul (.mul (.mul (.var 2) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 2) (.mul (.mul (.var 1) (.var 1)) (.var 1)))) (.mul (.var 2) (.mul (.mul (.var 1) (.var 1)) (.var 1)))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.add (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2))) (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)))) (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 2)) (.var 2))) (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.var 0) (.var 1)) (.var 2)))) (.neg (.mul (.mul (.var 0) (.var 2)) (.var 2)))))) (by decide +kernel)5455theorem geom4_id (y : Shell p) :56    (y + -1) * (1 + y + y * y + (y * y) * y) = ((y * y) * y) * y + -1 :=57  RE.sound (look [y])58    (.mul (.add (.var 0) (.neg .one)) (.add (.add (.add .one (.var 0)) (.mul (.var 0) (.var 0))) (.mul (.mul (.var 0) (.var 0)) (.var 0))))59    (.add (.mul (.mul (.mul (.var 0) (.var 0)) (.var 0)) (.var 0)) (.neg .one)) (by decide +kernel)6061theorem row_comb_id (c0 c1 c2 c3 i d : Shell p) :62    c0 * d + c1 * i + c2 * d + c3 * i = (c0 + c2) * d + ((c1 + c3) * i) :=63  RE.sound (look [c0, c1, c2, c3, i, d])64    (.add (.add (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 4))) (.mul (.var 2) (.var 5))) (.mul (.var 3) (.var 4)))65    (.add (.mul (.add (.var 0) (.var 2)) (.var 5)) (.mul (.add (.var 1) (.var 3)) (.var 4))) (by decide +kernel)6667theorem last_row_id (d0 d1 d2 d3 i Z G : Shell p) :68    d0 * 0 + d1 * (i * Z) + d2 * 0 + d3 * (i * G) = (d1 * i) * Z + (d3 * i) * G :=69  RE.sound (look [d0, d1, d2, d3, i, Z, G])70    (.add (.add (.add (.mul (.var 0) .zero) (.mul (.var 1) (.mul (.var 4) (.var 5)))) (.mul (.var 2) .zero)) (.mul (.var 3) (.mul (.var 4) (.var 6))))71    (.add (.mul (.mul (.var 1) (.var 4)) (.var 5)) (.mul (.mul (.var 3) (.var 4)) (.var 6))) (by decide +kernel)7273theorem col_sum_id (d0 d1 d2 d3 i : Shell p) :74    d0 * 1 + d1 * 0 + d2 * 1 + d3 * 0 = d0 + d2 :=75  RE.sound (look [d0, d1, d2, d3, i])76    (.add (.add (.add (.mul (.var 0) .one) (.mul (.var 1) .zero)) (.mul (.var 2) .one)) (.mul (.var 3) .zero))77    (.add (.var 0) (.var 2)) (by decide +kernel)7879variable {κ : Nat} {g : Shell p}8081/-! ## A quadratic has at most two roots -/8283/-- Three distinct roots of `a x² + b x + c` force `a = 0`. -/84theorem quad_roots (F : Frame p κ g) {a b c x1 x2 x3 : Shell p} (ha : a ≠ 0)85    (h1 : a * (x1 * x1) + b * x1 + c = 0) (h2 : a * (x2 * x2) + b * x2 + c = 0)86    (h3 : a * (x3 * x3) + b * x3 + c = 0) (d12 : x1 ≠ x2) (d13 : x1 ≠ x3) (d23 : x2 ≠ x3) : False := by87  have ne : ∀ {u v : Shell p}, u ≠ v → u + -v ≠ 0 := fun {u v} h e =>88    h (by rw [eq_neg_of_add_eq_zero e, neg_neg])89  have lin : ∀ {y : Shell p}, a * (y * y) + b * y + c = 0 → x1 ≠ y → a * (x1 + y) + b = 0 := fun {y} hy hne => by90    have e : (x1 + -y) * (a * (x1 + y) + b) = 0 := by rw [← quad_diff_id, h1, hy, neg_zero, add_zero]91    match F.mul_eq_zero e with92    | Or.inl e1 => exact absurd e1 (ne hne)93    | Or.inr e2 => exact e294  have e : a * (x2 + -x3) = 0 := by rw [← quad_lin_id, lin h2 d12, lin h3 d13, neg_zero, add_zero]95  match F.mul_eq_zero e with96  | Or.inl e1 => exact ha e197  | Or.inr e2 => exact ne d23 e29899/-! ## The last row of `F^{[−s]}` and its column sums -/100101theorem last_lt (F : Frame p κ g) : p - 1 - 1 < p - 1 := Nat.sub_lt F.n_pos (Nat.zero_lt_succ 0)102103theorem last_pos (F : Frame p κ g) : 0 < p - 1 - 1 := FRC.Nat.le_sub_of_add_le (one_lt_n F)104105/-- `F_{n−1, j} = i z^j`: the last row of `F` is the conjugate's. -/106theorem Fmat_last (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (j : Nat) :107    Fmat g κ (p - 1 - 1) j = quarterTurn g κ * z ^ j := by108  show quarterTurn g κ * g ^ (j * (p - 1 - 1)) = _109  congr 1110  apply inv_unique (y := g ^ j)111  · rw [← pow_add, ← Nat.mul_succ, Nat.succ_eq_add_one, FRC.Nat.sub_add_cancel F.n_pos, pow_mul, pow_mul_comm, F.pow_n,112      one_pow]113  · rw [← mul_pow, mul_comm, hz, one_pow]114115/-- `(FJ)_{n−1, j} = i g^j`. -/116theorem FJ_last (F : Frame p κ g) {j : Nat} (hj : j < p - 1) : FJ g κ (p - 1 - 1) j = quarterTurn g κ * g ^ j := by117  show quarterTurn g κ * g ^ (rev (p - 1) j * (p - 1 - 1)) = _118  congr 1119  apply inv_unique (y := g ^ rev (p - 1) j)120  · rw [← pow_add, ← Nat.mul_succ, Nat.succ_eq_add_one, FRC.Nat.sub_add_cancel F.n_pos, pow_mul, pow_mul_comm, F.pow_n,121      one_pow]122  · have e := pow_rev_mul F hj 1123    rw [Nat.mul_one, Nat.mul_one, mul_comm] at e124    exact e125126/-- `J_{n−1, j} = 0` off `j = 1`. -/127theorem J_last (F : Frame p κ g) {j : Nat} (hj : j < p - 1) (hj1 : j ≠ 1) : (J (p - 1) (p - 1 - 1) j : Shell p) = 0 := by128  show (if (p - 1 - 1 + j) % (p - 1) = 0 then (1 : Shell p) else 0) = 0129  apply ite_eq_right130  intro e131  have hn := F.n_pos132  match j, hj, hj1 with133  | 0, _, _ =>134    rw [Nat.add_zero, FRC.Nat.mod_eq_of_lt (last_lt F)] at e135    exact Nat.lt_irrefl 0 (e ▸ last_pos F)136  | 1, _, h1 => exact h1 rfl137  | m + 2, hj, _ =>138    have e2 := FRC.Nat.add_mul_mod_self_left (m + 1) 1 (p - 1) hn139    rw [Nat.mul_one] at e2140    change (p - 1 - 1 + (m + 1 + 1)) % (p - 1) = 0 at e141    rw [Nat.add_left_comm, FRC.Nat.sub_add_cancel hn, Nat.add_comm, e2, FRC.Nat.mod_eq_of_lt (Nat.lt_of_succ_lt hj)] at e142    exact Nat.noConfusion e143144theorem sum_idm_col {j : Nat} (hj : j < p - 1) : sumRange (fun l => (idm l j : Shell p)) (p - 1) = 1 := by145  rw [sum_eq_single hj (fun l _ hne => idm_ne hne), idm_self]146147theorem sum_J_col {j : Nat} (hj : j < p - 1) : sumRange (fun l => (J (p - 1) l j : Shell p)) (p - 1) = 1 := by148  rw [sum_congr _ (fun l _ => by149    show (if (l + j) % (p - 1) = 0 then (1 : Shell p) else 0) = (J (p - 1) j l : Shell p) * 1150    rw [mul_one, Nat.add_comm]; rfl)]151  exact @mm_J_X p _ (fun _ _ => (1 : Shell p)) j 0 hj152153theorem sum_F_col (F : Frame p κ g) {j : Nat} (hj0 : 0 < j) (hj : j < p - 1) :154    sumRange (fun l => Fmat g κ l j) (p - 1) = 0 := by155  show sumRange (fun l => quarterTurn g κ * g ^ (j * l)) (p - 1) = 0156  rw [sum_congr _ (fun l _ => by rw [pow_mul]), sum_mul_left,157    F.geom_sum_eq_zero _ (by rw [pow_mul_comm, F.pow_n, one_pow]) (F.prim.2 j hj hj0), mul_zero]158159theorem sum_FJ_col (F : Frame p κ g) {j : Nat} (hj0 : 0 < j) (hj : j < p - 1) :160    sumRange (fun l => FJ g κ l j) (p - 1) = 0 := by161  have hn := F.n_pos162  have hr : rev (p - 1) j = p - 1 - j := rev_of_pos hj hj0163  have hr0 : 0 < rev (p - 1) j := by rw [hr]; exact FRC.Nat.le_sub_of_add_le (by rw [Nat.add_comm]; exact hj)164  show sumRange (fun l => quarterTurn g κ * g ^ (rev (p - 1) j * l)) (p - 1) = 0165  rw [sum_congr _ (fun l _ => by rw [pow_mul]), sum_mul_left,166    F.geom_sum_eq_zero _ (by rw [pow_mul_comm, F.pow_n, one_pow]) (F.prim.2 _ (rev_lt hn j) hr0), mul_zero]167168/-- The column sums of `F^{[t]} = Σ_r c_r F^r` off `j = 0`: `c₀ + c₂`. -/169theorem frft_col_sum (F : Frame p κ g) (z : Shell p) (t : Nat) {j : Nat} (hj0 : 0 < j) (hj : j < p - 1) :170    sumRange (fun l => frft g κ z t l j) (p - 1) =171      NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) := by172  rw [sum_congr _ (fun l _ => frft_eq F z t l j)]173  show sumRange (fun l => NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * idm l j +174    NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * Fmat g κ l j + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * J (p - 1) l j +175    NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * FJ g κ l j) (p - 1) = _176  rw [sum_add, sum_add, sum_add, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left, sum_idm_col hj, sum_J_col hj,177    sum_F_col F hj0 hj, sum_FJ_col F hj0 hj]178  exact col_sum_id _ _ _ _ (quarterTurn g κ)179180/-- The last-row entry of `F^{[t]}` off `j ∈ {1, n−1}`: `i (c₁ z^j + c₃ g^j)`. -/181theorem frft_last (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (t : Nat) {j : Nat} (hj : j < p - 1) (hj1 : j ≠ 1)182    (hjn : j ≠ p - 1 - 1) :183    frft g κ z t (p - 1 - 1) j =184      NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * quarterTurn g κ * z ^ j +185        NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * quarterTurn g κ * g ^ j := by186  rw [frft_eq F z t]187  show NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * idm (p - 1 - 1) j +188    NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * Fmat g κ (p - 1 - 1) j +189    NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * J (p - 1) (p - 1 - 1) j +190    NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * FJ g κ (p - 1 - 1) j = _191  rw [idm_ne (fun e => hjn e.symm), J_last F hj hj1, Fmat_last F hz, FJ_last F hj]192  exact last_row_id _ _ _ _ _ _ _193194/-! ## Row 0 of `F^{[s]} σ` -/195196theorem succ_mod_zero (F : Frame p κ g) {l : Nat} (hl : l < p - 1) : (l + 1) % (p - 1) = 0 ↔ l = p - 1 - 1 := by197  constructor198  · intro h199    match Nat.lt_or_ge (l + 1) (p - 1) with200    | Or.inl hlt => rw [FRC.Nat.mod_eq_of_lt hlt] at h; exact Nat.noConfusion h201    | Or.inr hge =>202      have e : l + 1 = p - 1 := Nat.le_antisymm hl hge203      rw [← e, FRC.Nat.add_sub_cancel]204  · intro e205    rw [e, FRC.Nat.sub_add_cancel F.n_pos]206    exact FRC.Nat.mod_self _ F.n_pos207208/-- Row 0 of `F^{[s]} σ`: `(F^{[s]} σ)_{0l} = F^{[s]}_{0, l+1} = (c₀ + c₂) [l = n−1] + (c₁ + c₃) i`. -/209theorem row_shift (F : Frame p κ g) (z : Shell p) (s : Nat) {l : Nat} (hl : l < p - 1) :210    frft g κ z s 0 ((l + 1) % (p - 1)) =211      (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) * idm l (p - 1 - 1) +212        (NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) * quarterTurn g κ := by213  rw [frft_eq F z s]214  show NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) * idm 0 ((l + 1) % (p - 1)) +215    NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) * Fmat g κ 0 ((l + 1) % (p - 1)) +216    NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) * J (p - 1) 0 ((l + 1) % (p - 1)) +217    NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) * FJ g κ 0 ((l + 1) % (p - 1)) = _218  have e1 : (idm 0 ((l + 1) % (p - 1)) : Shell p) = idm l (p - 1 - 1) :=219    ite_iff (Iff.trans ⟨Eq.symm, Eq.symm⟩ (succ_mod_zero F hl))220  have e2 : (J (p - 1) 0 ((l + 1) % (p - 1)) : Shell p) = idm l (p - 1 - 1) := by221    show (if (0 + (l + 1) % (p - 1)) % (p - 1) = 0 then (1 : Shell p) else 0) = _222    rw [Nat.zero_add, FRC.Nat.mod_mod _ _ F.n_pos]223    exact ite_iff (succ_mod_zero F hl)224  rw [e1, e2, Fmat_zero_row, FJ_zero_row]225  exact row_comb_id _ _ _ _ _ _226227/-- 6:E8, the entry `(0, j)` of `F^{[s]} σ F^{[−s]}` off the three sites `j ∈ {0, 1, n−1}`, with `F^{[−s]} = F^{[n−s]}`228(`n − s` the natural difference, so `s ≤ n` is the reading): `i [(c₀ + c₂)(c'₁ z^j + c'₃ g^j) + (c₁ + c₃)(c'₀ + c'₂)]`. -/229theorem row_entry (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (s : Nat) {j : Nat} (hj : j < p - 1) (hj0 : j ≠ 0)230    (hj1 : j ≠ 1) (hjn : j ≠ p - 1 - 1) :231    mmul (mmul (frft g κ z s) (shift p) (p - 1)) (frft g κ z (p - 1 - s)) (p - 1) 0 j =232      (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) *233          (NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) * quarterTurn g κ * z ^ j +234            NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) * quarterTurn g κ * g ^ j) +235        (NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) * quarterTurn g κ *236          (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s))) := by237  have hj0' : 0 < j := Nat.pos_of_ne_zero hj0238  show sumRange (fun l => mmul (frft g κ z s) (shift p) (p - 1) 0 l * frft g κ z (p - 1 - s) l j) (p - 1) = _239  rw [sum_congr _ (fun l hl => by240    rw [show mmul (frft g κ z s) (shift p) (p - 1) 0 l = frft g κ z s 0 ((l + 1) % (p - 1)) from241      shift_single F (frft g κ z s) 0 l, row_shift F z s hl, right_distrib,242      mul_assoc (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s))])]243  rw [sum_add, sum_mul_left, sum_mul_left, sum_eq_single (last_lt F) (fun l _ hne => by rw [idm_ne hne, zero_mul]),244    idm_self, one_mul, frft_last F hz _ hj hj1 hjn, frft_col_sum F z _ hj0' hj]245246/-! ## The coefficients off the cardinal indices -/247248theorem three_kappa_lt (F : Frame p κ g) : 3 * κ < p - 1 := by249  rw [F.n_eq]; exact FRC.Nat.mul_lt_mul_of_lt_of_pos (by decide) F.cap_pos250251theorem kappa_lt_n (F : Frame p κ g) : κ < p - 1 := by252  rw [F.n_eq]253  have := FRC.Nat.mul_lt_mul_of_lt_of_pos (by decide : 1 < 4) F.cap_pos254  rw [Nat.one_mul] at this255  exact this256257/-- 6:E8, `c₀ + c₂ = ½ (1 + z_s²)` (`even_coeff_id`) is nonzero off `s ∈ {κ, 3κ}`, where `z_s = ±i`. -/258theorem even_coeff_ne_zero (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {s : Nat} (hs : s < p - 1) (h1 : s ≠ κ)259    (h3 : s ≠ 3 * κ) :260    NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) ≠ 0 := by261  rw [even_coeff_id]262  refine F.mul_ne_zero (half_ne_zero F) (fun e => ?_)263  have e2 : z ^ s * z ^ s = -1 := (neg_eq_of_add_eq_zero e).symm264  have hzk := inv_pow_kappa F hz265  match (sqrt_neg_one F (z ^ s)).1 e2 with266  | Or.inl e3 => exact h1 ((inv_frame F hz).pow_inj hs (kappa_lt_n F) (by rw [e3, hzk]))267  | Or.inr e3 => exact h3 ((inv_frame F hz).pow_inj hs (three_kappa_lt F) (by268      rw [e3, pow_mul, pow_mul_comm, hzk, pow_succ, pow_two, F.quarter_turn_sq, neg_one_mul]))269270/-- `4t ≡ 0 (mod 4κ)` below `4κ` forces `t ∈ {0, κ, 2κ, 3κ}`. -/271theorem quad_mod_n (F : Frame p κ g) {t : Nat} (ht : t < p - 1) (h : (4 * t) % (p - 1) = 0) :272    t = 0 ∨ t = κ ∨ t = 2 * κ ∨ t = 3 * κ := by273  obtain ⟨c, hc⟩ := FRC.Nat.mod_spec (p - 1) F.n_pos (4 * t)274  rw [h, Nat.add_zero, F.n_eq, Nat.mul_assoc] at hc275  have e : t = κ * c := Nat.eq_of_mul_eq_mul_left (by decide) hc276  have hc4 : c < 4 := by277    rw [F.n_eq, e] at ht278    have ht' : κ * c < κ * 4 := by rw [Nat.mul_comm κ 4]; exact ht279    match Nat.lt_or_ge c 4 with280    | Or.inl h => exact h281    | Or.inr h => exact absurd (Nat.lt_of_lt_of_le ht' (Nat.mul_le_mul_left κ h)) (Nat.lt_irrefl _)282  match c, hc4, e with283  | 0, _, e => exact Or.inl (by rw [e, Nat.mul_zero])284  | 1, _, e => exact Or.inr (Or.inl (by rw [e, Nat.mul_one]))285  | 2, _, e => exact Or.inr (Or.inr (Or.inl (by rw [e, Nat.mul_comm])))286  | 3, _, e => exact Or.inr (Or.inr (Or.inr (by rw [e, Nat.mul_comm])))287  | c + 4, hc4, _ => exact absurd (Nat.lt_of_lt_of_le hc4 (Nat.le_add_left 4 c)) (Nat.lt_irrefl _)288289/-- `z^{n−s} = g^s`: the conjugate family's base at `−s`. -/290theorem pow_sub_eq (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {s : Nat} (hs : s ≤ p - 1) :291    z ^ (p - 1 - s) = g ^ s := by292  apply inv_unique (y := z ^ s)293  · rw [← pow_add, FRC.Nat.sub_add_cancel hs, inv_pow_n F hz]294  · rw [← mul_pow, hz, one_pow]295296/-- 6:E8, `c'₃ = c₃(−s) = ¼ Σ_ℓ y^ℓ` with `y = g^s i = g^{s + 3κ}`, nonzero off the cardinal indices: `y ≠ 1` (else297`s = κ`) and `y⁴ = g^{4s} ≠ 1` (else `κ ∣ s`); with `even_coeff_ne_zero`, the leading coefficient `i (c₀ + c₂) c'₃ ≠ 0`. -/298theorem odd_coeff_ne_zero (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {s : Nat} (hs : s < p - 1) (h0 : s ≠ 0)299    (h1 : s ≠ κ) (h2 : s ≠ 2 * κ) (h3 : s ≠ 3 * κ) :300    NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) ≠ 0 := by301  rw [red1 (odd_coeff_id _ _ _) (hjj F), ← neg_w F, neg_neg, pow_sub_eq F hz (Nat.le_of_lt hs)]302  refine F.mul_ne_zero (q_ne_zero F) (fun e => ?_)303  have hy1 : g ^ s * quarterTurn g κ ≠ 1 := fun e1 => h1 (F.pow_inj hs (kappa_lt_n F) (inv_unique (y := quarterTurn g κ) e1 (by304        show g ^ κ * -(g ^ κ) = 1305        rw [← mul_neg, ← pow_two, F.quarter_turn_order.1, neg_neg])))306  have hy4 : g ^ s * quarterTurn g κ * (g ^ s * quarterTurn g κ) * (g ^ s * quarterTurn g κ) * (g ^ s * quarterTurn g κ) ≠ 1 :=307    fun e4 => by308      have e5 : g ^ (4 * s) = 1 := by309        rw [show (4 : Nat) = 2 * 2 from rfl, Nat.mul_assoc, pow_mul, pow_two, pow_mul, pow_two, ← e4]310        rw [show g ^ s * quarterTurn g κ * (g ^ s * quarterTurn g κ) * (g ^ s * quarterTurn g κ) * (g ^ s * quarterTurn g κ) =311          (g ^ s * g ^ s) * (g ^ s * g ^ s) * (quarterTurn g κ * quarterTurn g κ * (quarterTurn g κ * quarterTurn g κ)) from312          RE.sound (look [g ^ s, quarterTurn g κ]) (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (.mul (.var 0) (.var 1))) (.mul (.var 0) (.var 1)))313            (.mul (.mul (.mul (.var 0) (.var 0)) (.mul (.var 0) (.var 0))) (.mul (.mul (.var 1) (.var 1)) (.mul (.var 1) (.var 1)))) (by decide +kernel),314          F.quarter_turn_sq, neg_mul_neg, one_mul, mul_one, mul_pow, mul_pow]315      match quad_mod_n F hs (F.mod_eq_zero_of_pow_eq_one e5) with316      | Or.inl e => exact h0 e317      | Or.inr (Or.inl e) => exact h1 e318      | Or.inr (Or.inr (Or.inl e)) => exact h2 e319      | Or.inr (Or.inr (Or.inr e)) => exact h3 e320  have e6 : (g ^ s * quarterTurn g κ + -1) * (1 + g ^ s * quarterTurn g κ + g ^ s * quarterTurn g κ * (g ^ s * quarterTurn g κ) +321      g ^ s * quarterTurn g κ * (g ^ s * quarterTurn g κ) * (g ^ s * quarterTurn g κ)) = 0 := by rw [e, mul_zero]322  rw [geom4_id] at e6323  exact hy4 (by rw [eq_neg_of_add_eq_zero e6, neg_neg])324325/-! ## Cardinal exclusivity (6:E8) -/326327/-- 6:E8, cardinal exclusivity: for `s ∉ {0, κ, 2κ, 3κ}` the row `0` of `F^{[s]} σ F^{[−s]}` vanishes at no three328distinct indices off the sites `{0, 1, n−1}`: `x = g^j` times the entry is a quadratic in `x` with leading coefficient329`i (c₀ + c₂) c'₃ ≠ 0` (the paper counts: at least `4κ − 5` nonzero entries, so the conjugate is not monomial). -/330theorem exclusivity (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {s : Nat} (hs : s < p - 1) (h0 : s ≠ 0)331    (h1 : s ≠ κ) (h2 : s ≠ 2 * κ) (h3 : s ≠ 3 * κ) {j1 j2 j3 : Nat}332    (hj1 : j1 < p - 1) (hj2 : j2 < p - 1) (hj3 : j3 < p - 1)333    (o1 : j1 ≠ 0 ∧ j1 ≠ 1 ∧ j1 ≠ p - 1 - 1) (o2 : j2 ≠ 0 ∧ j2 ≠ 1 ∧ j2 ≠ p - 1 - 1)334    (o3 : j3 ≠ 0 ∧ j3 ≠ 1 ∧ j3 ≠ p - 1 - 1) (d12 : j1 ≠ j2) (d13 : j1 ≠ j3) (d23 : j2 ≠ j3) :335    ¬(mmul (mmul (frft g κ z s) (shift p) (p - 1)) (frft g κ z (p - 1 - s)) (p - 1) 0 j1 = 0 ∧336      mmul (mmul (frft g κ z s) (shift p) (p - 1)) (frft g κ z (p - 1 - s)) (p - 1) 0 j2 = 0 ∧337      mmul (mmul (frft g κ z s) (shift p) (p - 1)) (frft g κ z (p - 1 - s)) (p - 1) 0 j3 = 0) := by338  intro ⟨e1, e2, e3⟩339  have quad : ∀ {j : Nat}, j < p - 1 → j ≠ 0 → j ≠ 1 → j ≠ p - 1 - 1 →340      mmul (mmul (frft g κ z s) (shift p) (p - 1)) (frft g κ z (p - 1 - s)) (p - 1) 0 j = 0 →341      (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) *342          NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) * (g ^ j * g ^ j) +343        (NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) *344          (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s))) *345          g ^ j +346        (NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s) + NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ s)) *347          NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ (p - 1 - s)) = 0 := fun {j} hj hj0 hj1 hjn e => by348    rw [row_entry F hz s hj hj0 hj1 hjn] at e349    have e' := congrArg (fun x => g ^ j * x) e350    rw [mul_zero, row_quad_id, show z ^ j * g ^ j = 1 by rw [← mul_pow, mul_comm, hz, one_pow], add_neg, zero_mul,351      add_zero] at e'352    match F.mul_eq_zero e' with353    | Or.inl e0 => exact absurd e0 (quarter_ne_zero F)354    | Or.inr e0 => exact e0355  have ha := F.mul_ne_zero (even_coeff_ne_zero F hz hs h1 h3) (odd_coeff_ne_zero F hz hs h0 h1 h2 h3)356  exact quad_roots F ha (quad hj1 o1.1 o1.2.1 o1.2.2 e1) (quad hj2 o2.1 o2.2.1 o2.2.2 e2) (quad hj3 o3.1 o3.2.1 o3.2.2 e3)357    (fun e => d12 (F.pow_inj hj1 hj2 e)) (fun e => d13 (F.pow_inj hj1 hj3 e)) (fun e => d23 (F.pow_inj hj2 hj3 e))358359end Frame360end Shell361end FRC362