Theme/Fractional.lean — FrcCore

1import FrcCore.Theme.Fourier23/-!4# FrcCore.Theme.Fractional — the projector algebra of the fractional family (the fourier theme)56The second file of the fourier theme (one theme; the 800-line limit of decision Q03 forces the file), opened for the7revised 6-fourier of 8 October 2026 (`6-fourier-20260716/reports/blueprint-20261008.md`, task T02). Every projector8`Π_ℓ = 4⁻¹ Σ_m i^{−ℓm} F^m` is a combination `c₀ I + c₁ F + c₂ J + c₃ F J` (`Theme/Fourier.lean`), and the product of9two combinations is the cyclic convolution of their coefficients (`comb_mul`). So the algebra of the projectors is four10coefficient identities per product, decided by the kernel through the normaliser `RE.sound` with the two relations11`w² = −1` (`w = i⁻¹ = −i`) and `4 q = 1` (`q = 4⁻¹ = −κ`), and the orthogonality `Π_ℓ Π_m = 0` for `ℓ ≠ m` is the12geometric sum `1 + x + x² + x³ = 0` of the nontrivial fourth root `x = i^{m−ℓ}`: `Π_ℓ Π_m = [ℓ = m] Π_ℓ`,13`Σ_ℓ Π_ℓ = I`, `F Π_ℓ = i^ℓ Π_ℓ` (6:C2), and the two sums `Π₀ + Π₂ = (I + J)/2`, `Π₁ + Π₃ = (I − J)/2` (6:C5). No14axioms.15-/1617namespace FRC18namespace Shell19namespace Frame2021variable {p : Nat} [Pos p]2223/-! ## Ring identities (generated; `RE.sound`, decided by the kernel) -/2425theorem comb_add_id (a0 a1 a2 a3 b0 b1 b2 b3 I F J G : Shell p) :26    a0 * I + a1 * F + a2 * J + a3 * G + (b0 * I + b1 * F + b2 * J + b3 * G) =27      (a0 + b0) * I + (a1 + b1) * F + (a2 + b2) * J + (a3 + b3) * G :=28  RE.sound (look [a0, a1, a2, a3, b0, b1, b2, b3, I, F, J, G])29    (.add (.add (.add (.add (.mul (.var 0) (.var 8)) (.mul (.var 1) (.var 9))) (.mul (.var 2) (.var 10))) (.mul (.var 3) (.var 11))) (.add (.add (.add (.mul (.var 4) (.var 8)) (.mul (.var 5) (.var 9))) (.mul (.var 6) (.var 10))) (.mul (.var 7) (.var 11))))30    (.add (.add (.add (.mul (.add (.var 0) (.var 4)) (.var 8)) (.mul (.add (.var 1) (.var 5)) (.var 9))) (.mul (.add (.var 2) (.var 6)) (.var 10))) (.mul (.add (.var 3) (.var 7)) (.var 11))) (by decide +kernel)3132theorem comb_smul_id (c a0 a1 a2 a3 I F J G : Shell p) :33    c * (a0 * I + a1 * F + a2 * J + a3 * G) = c * a0 * I + c * a1 * F + c * a2 * J + c * a3 * G :=34  RE.sound (look [c, a0, a1, a2, a3, I, F, J, G])35    (.mul (.var 0) (.add (.add (.add (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 6))) (.mul (.var 3) (.var 7))) (.mul (.var 4) (.var 8))))36    (.add (.add (.add (.mul (.mul (.var 0) (.var 1)) (.var 5)) (.mul (.mul (.var 0) (.var 2)) (.var 6))) (.mul (.mul (.var 0) (.var 3)) (.var 7))) (.mul (.mul (.var 0) (.var 4)) (.var 8))) (by decide +kernel)3738theorem comb_zero_id (I F J G : Shell p) :39    0 * I + 0 * F + 0 * J + 0 * G = 0 :=40  RE.sound (look [I, F, J, G])41    (.add (.add (.add (.mul .zero (.var 0)) (.mul .zero (.var 1))) (.mul .zero (.var 2))) (.mul .zero (.var 3)))42    .zero (by decide +kernel)4344theorem comb_idm_id (I F J G : Shell p) :45    1 * I + 0 * F + 0 * J + 0 * G = I :=46  RE.sound (look [I, F, J, G])47    (.add (.add (.add (.mul .one (.var 0)) (.mul .zero (.var 1))) (.mul .zero (.var 2))) (.mul .zero (.var 3)))48    (.var 0) (by decide +kernel)4950theorem comb_Fmat_id (I F J G : Shell p) :51    0 * I + 1 * F + 0 * J + 0 * G = F :=52  RE.sound (look [I, F, J, G])53    (.add (.add (.add (.mul .zero (.var 0)) (.mul .one (.var 1))) (.mul .zero (.var 2))) (.mul .zero (.var 3)))54    (.var 1) (by decide +kernel)5556theorem comb_J_id (I F J G : Shell p) :57    0 * I + 0 * F + 1 * J + 0 * G = J :=58  RE.sound (look [I, F, J, G])59    (.add (.add (.add (.mul .zero (.var 0)) (.mul .zero (.var 1))) (.mul .one (.var 2))) (.mul .zero (.var 3)))60    (.var 2) (by decide +kernel)6162theorem comb_FJ_id (I F J G : Shell p) :63    0 * I + 0 * F + 0 * J + 1 * G = G :=64  RE.sound (look [I, F, J, G])65    (.add (.add (.add (.mul .zero (.var 0)) (.mul .zero (.var 1))) (.mul .zero (.var 2))) (.mul .one (.var 3)))66    (.var 3) (by decide +kernel)6768theorem even_sum_id (q w I F J G : Shell p) :69    (q + q) * I + (q + -q) * F + (q + q) * J + (q + -q) * G = (q + q) * (I + J) :=70  RE.sound (look [q, w, I, F, J, G])71    (.add (.add (.add (.mul (.add (.var 0) (.var 0)) (.var 2)) (.mul (.add (.var 0) (.neg (.var 0))) (.var 3))) (.mul (.add (.var 0) (.var 0)) (.var 4))) (.mul (.add (.var 0) (.neg (.var 0))) (.var 5)))72    (.mul (.add (.var 0) (.var 0)) (.add (.var 2) (.var 4))) (by decide +kernel)7374theorem odd_sum_id (q w I F J G : Shell p) :75    (q + q) * I + (q * w + -(q * w)) * F + (-q + -q) * J + (-(q * w) + q * w) * G = (q + q) * (I + -J) :=76  RE.sound (look [q, w, I, F, J, G])77    (.add (.add (.add (.mul (.add (.var 0) (.var 0)) (.var 2)) (.mul (.add (.mul (.var 0) (.var 1)) (.neg (.mul (.var 0) (.var 1)))) (.var 3))) (.mul (.add (.neg (.var 0)) (.neg (.var 0))) (.var 4))) (.mul (.add (.neg (.mul (.var 0) (.var 1))) (.mul (.var 0) (.var 1))) (.var 5)))78    (.mul (.add (.var 0) (.var 0)) (.add (.var 2) (.neg (.var 4)))) (by decide +kernel)7980theorem proj1_c2 (q w : Shell p) :81    q * (w * w) = -q + (w * w + 1) * (q) :=82  RE.sound (look [q, w])83    (.mul (.var 0) (.mul (.var 1) (.var 1)))84    (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.var 0))) (by decide +kernel)8586theorem proj1_c3 (q w : Shell p) :87    q * ((w * w) * w) = -(q * w) + (w * w + 1) * (q * w) :=88  RE.sound (look [q, w])89    (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))90    (.add (.neg (.mul (.var 0) (.var 1))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.mul (.var 0) (.var 1)))) (by decide +kernel)9192theorem proj2_c1 (q w : Shell p) :93    q * (w * w) = -q + (w * w + 1) * (q) :=94  RE.sound (look [q, w])95    (.mul (.var 0) (.mul (.var 1) (.var 1)))96    (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.var 0))) (by decide +kernel)9798theorem proj2_c2 (q w : Shell p) :99    q * ((w * w) * (w * w)) = q + (w * w + 1) * (q * w * w + -q) :=100  RE.sound (look [q, w])101    (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.mul (.var 1) (.var 1))))102    (.add (.var 0) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.neg (.var 0))))) (by decide +kernel)103104theorem proj2_c3 (q w : Shell p) :105    q * (((w * w) * (w * w)) * (w * w)) = -q + (w * w + 1) * (q * w * w * w * w + -(q * w * w) + q) :=106  RE.sound (look [q, w])107    (.mul (.var 0) (.mul (.mul (.mul (.var 1) (.var 1)) (.mul (.var 1) (.var 1))) (.mul (.var 1) (.var 1))))108    (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.neg (.mul (.mul (.var 0) (.var 1)) (.var 1)))) (.var 0)))) (by decide +kernel)109110theorem proj3_c1 (q w : Shell p) :111    q * ((w * w) * w) = -(q * w) + (w * w + 1) * (q * w) :=112  RE.sound (look [q, w])113    (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))114    (.add (.neg (.mul (.var 0) (.var 1))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.mul (.var 0) (.var 1)))) (by decide +kernel)115116theorem proj3_c2 (q w : Shell p) :117    q * (((w * w) * w) * ((w * w) * w)) = -q + (w * w + 1) * (q * w * w * w * w + -(q * w * w) + q) :=118  RE.sound (look [q, w])119    (.mul (.var 0) (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.mul (.mul (.var 1) (.var 1)) (.var 1))))120    (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.neg (.mul (.mul (.var 0) (.var 1)) (.var 1)))) (.var 0)))) (by decide +kernel)121122theorem proj3_c3 (q w : Shell p) :123    q * ((((w * w) * w) * ((w * w) * w)) * ((w * w) * w)) = q * w + (w * w + 1) * (q * w * w * w * w * w * w * w + -(q * w * w * w * w * w) + q * w * w * w + -(q * w)) :=124  RE.sound (look [q, w])125    (.mul (.var 0) (.mul (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.mul (.var 1) (.var 1)) (.var 1))))126    (.add (.mul (.var 0) (.var 1)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.neg (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1))) (.neg (.mul (.var 0) (.var 1)))))) (by decide +kernel)127128theorem neg_w_id (q w : Shell p) :129    -w = (w * w) * w + (w * w + 1) * (-w) :=130  RE.sound (look [q, w])131    (.neg (.var 1))132    (.add (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.neg (.var 1)))) (by decide +kernel)133134theorem self_c0 (q u : Shell p) :135    q * q + (q * u) * (q * ((u * u) * u)) + (q * (u * u)) * (q * (u * u)) + (q * ((u * u) * u)) * (q * u) = q + (u * u * u * u + -1) * ((1 + 1 + 1) * q * q) + ((1 + 1 + 1 + 1) * q + -1) * (q) :=136  RE.sound (look [q, u])137    (.add (.add (.add (.mul (.var 0) (.var 0)) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.var 0) (.mul (.var 1) (.var 1))))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 0) (.var 1))))138    (.add (.add (.var 0) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) (.mul (.mul (.add (.add .one .one) .one) (.var 0)) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.var 0))) (by decide +kernel)139140theorem self_c1 (q u : Shell p) :141    q * (q * u) + (q * u) * q + (q * (u * u)) * (q * ((u * u) * u)) + (q * ((u * u) * u)) * (q * (u * u)) = q * u + (u * u * u * u + -1) * ((1 + 1) * q * q * u) + ((1 + 1 + 1 + 1) * q + -1) * (q * u) :=142  RE.sound (look [q, u])143    (.add (.add (.add (.mul (.var 0) (.mul (.var 0) (.var 1))) (.mul (.mul (.var 0) (.var 1)) (.var 0))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 0) (.mul (.var 1) (.var 1)))))144    (.add (.add (.mul (.var 0) (.var 1)) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) (.mul (.mul (.mul (.add .one .one) (.var 0)) (.var 0)) (.var 1)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.mul (.var 0) (.var 1)))) (by decide +kernel)145146theorem self_c2 (q u : Shell p) :147    q * (q * (u * u)) + (q * u) * (q * u) + (q * (u * u)) * q + (q * ((u * u) * u)) * (q * ((u * u) * u)) = q * (u * u) + (u * u * u * u + -1) * (q * q * u * u) + ((1 + 1 + 1 + 1) * q + -1) * (q * u * u) :=148  RE.sound (look [q, u])149    (.add (.add (.add (.mul (.var 0) (.mul (.var 0) (.mul (.var 1) (.var 1)))) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1)))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.var 0))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))))150    (.add (.add (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.mul (.mul (.var 0) (.var 1)) (.var 1)))) (by decide +kernel)151152theorem self_c3 (q u : Shell p) :153    q * (q * ((u * u) * u)) + (q * u) * (q * (u * u)) + (q * (u * u)) * (q * u) + (q * ((u * u) * u)) * q = q * ((u * u) * u) + (u * u * u * u + -1) * (0) + ((1 + 1 + 1 + 1) * q + -1) * (q * u * u * u) :=154  RE.sound (look [q, u])155    (.add (.add (.add (.mul (.var 0) (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.mul (.var 1) (.var 1))))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.var 0) (.var 1)))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.var 0)))156    (.add (.add (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) .zero)) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)))) (by decide +kernel)157158theorem ne_c0 (q u v : Shell p) :159    q * q + (q * u) * (q * ((v * v) * v)) + (q * (u * u)) * (q * (v * v)) + (q * ((u * u) * u)) * (q * v) = 0 + (v * v * v * v + -1) * (-(q * q * u * u * u * v * v * v * v * v) + -(q * q * u * u * u * v) + -(q * q * u * u * v * v)) + (1 + u * ((v * v) * v) + (u * ((v * v) * v)) * (u * ((v * v) * v)) + ((u * ((v * v) * v)) * (u * ((v * v) * v))) * (u * ((v * v) * v))) * (q * q) :=160  RE.sound (look [q, u, v])161    (.add (.add (.add (.mul (.var 0) (.var 0)) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.var 0) (.mul (.var 2) (.var 2))))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 0) (.var 2))))162    (.add (.add .zero (.mul (.add (.mul (.mul (.mul (.var 2) (.var 2)) (.var 2)) (.var 2)) (.neg .one)) (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 2)) (.var 2)))))) (.mul (.add (.add (.add .one (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.var 0) (.var 0)))) (by decide +kernel)163164theorem ne_c1 (q u v : Shell p) :165    q * (q * v) + (q * u) * q + (q * (u * u)) * (q * ((v * v) * v)) + (q * ((u * u) * u)) * (q * (v * v)) = 0 + (v * v * v * v + -1) * (-(q * q * u * u * u * v * v * v * v * v * v) + -(q * q * u * u * u * v * v) + -(q * q * u * u * v * v * v) + -(q * q * u)) + (1 + u * ((v * v) * v) + (u * ((v * v) * v)) * (u * ((v * v) * v)) + ((u * ((v * v) * v)) * (u * ((v * v) * v))) * (u * ((v * v) * v))) * ((q * q) * v) :=166  RE.sound (look [q, u, v])167    (.add (.add (.add (.mul (.var 0) (.mul (.var 0) (.var 2))) (.mul (.mul (.var 0) (.var 1)) (.var 0))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.var 0) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 0) (.mul (.var 2) (.var 2)))))168    (.add (.add .zero (.mul (.add (.mul (.mul (.mul (.var 2) (.var 2)) (.var 2)) (.var 2)) (.neg .one)) (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.var 0) (.var 0)) (.var 1)))))) (.mul (.add (.add (.add .one (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.var 0) (.var 0)) (.var 2)))) (by decide +kernel)169170theorem ne_c2 (q u v : Shell p) :171    q * (q * (v * v)) + (q * u) * (q * v) + (q * (u * u)) * q + (q * ((u * u) * u)) * (q * ((v * v) * v)) = 0 + (v * v * v * v + -1) * (-(q * q * u * u * u * v * v * v * v * v * v * v) + -(q * q * u * u * u * v * v * v) + -(q * q * u * u * v * v * v * v) + -(q * q * u * u) + -(q * q * u * v)) + (1 + u * ((v * v) * v) + (u * ((v * v) * v)) * (u * ((v * v) * v)) + ((u * ((v * v) * v)) * (u * ((v * v) * v))) * (u * ((v * v) * v))) * ((q * q) * (v * v)) :=172  RE.sound (look [q, u, v])173    (.add (.add (.add (.mul (.var 0) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 2)))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.var 0))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.mul (.var 0) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))174    (.add (.add .zero (.mul (.add (.mul (.mul (.mul (.var 2) (.var 2)) (.var 2)) (.var 2)) (.neg .one)) (.add (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)))) (.neg (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 2)))))) (.mul (.add (.add (.add .one (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.var 0) (.var 0)) (.mul (.var 2) (.var 2))))) (by decide +kernel)175176theorem ne_c3 (q u v : Shell p) :177    q * (q * ((v * v) * v)) + (q * u) * (q * (v * v)) + (q * (u * u)) * (q * v) + (q * ((u * u) * u)) * q = 0 + (v * v * v * v + -1) * (-(q * q * u * u * u * v * v * v * v * v * v * v * v) + -(q * q * u * u * u * v * v * v * v) + -(q * q * u * u * v * v * v * v * v) + -(q * q * u * u * u) + -(q * q * u * u * v) + -(q * q * u * v * v)) + (1 + u * ((v * v) * v) + (u * ((v * v) * v)) * (u * ((v * v) * v)) + ((u * ((v * v) * v)) * (u * ((v * v) * v))) * (u * ((v * v) * v))) * ((q * q) * ((v * v) * v)) :=178  RE.sound (look [q, u, v])179    (.add (.add (.add (.mul (.var 0) (.mul (.var 0) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2))))) (.mul (.mul (.var 0) (.mul (.var 1) (.var 1))) (.mul (.var 0) (.var 2)))) (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))) (.var 0)))180    (.add (.add .zero (.mul (.add (.mul (.mul (.mul (.var 2) (.var 2)) (.var 2)) (.var 2)) (.neg .one)) (.add (.add (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 1)))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 1)) (.var 2)))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 0)) (.var 1)) (.var 2)) (.var 2)))))) (.mul (.add (.add (.add .one (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (.mul (.mul (.var 0) (.var 0)) (.mul (.mul (.var 2) (.var 2)) (.var 2))))) (by decide +kernel)181182theorem F_c0 (q u : Shell p) :183    0 * q + 1 * (q * ((u * u) * u)) + 0 * (q * (u * u)) + 0 * (q * u) = ((u * u) * u) * q + (u * u * u * u + -1) * (0) :=184  RE.sound (look [q, u])185    (.add (.add (.add (.mul .zero (.var 0)) (.mul .one (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))))) (.mul .zero (.mul (.var 0) (.mul (.var 1) (.var 1))))) (.mul .zero (.mul (.var 0) (.var 1))))186    (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 0)) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) .zero)) (by decide +kernel)187188theorem F_c1 (q u : Shell p) :189    0 * (q * u) + 1 * q + 0 * (q * ((u * u) * u)) + 0 * (q * (u * u)) = ((u * u) * u) * (q * u) + (u * u * u * u + -1) * (-q) :=190  RE.sound (look [q, u])191    (.add (.add (.add (.mul .zero (.mul (.var 0) (.var 1))) (.mul .one (.var 0))) (.mul .zero (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1))))) (.mul .zero (.mul (.var 0) (.mul (.var 1) (.var 1)))))192    (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.mul (.var 0) (.var 1))) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) (.neg (.var 0)))) (by decide +kernel)193194theorem F_c2 (q u : Shell p) :195    0 * (q * (u * u)) + 1 * (q * u) + 0 * q + 0 * (q * ((u * u) * u)) = ((u * u) * u) * (q * (u * u)) + (u * u * u * u + -1) * (-(q * u)) :=196  RE.sound (look [q, u])197    (.add (.add (.add (.mul .zero (.mul (.var 0) (.mul (.var 1) (.var 1)))) (.mul .one (.mul (.var 0) (.var 1)))) (.mul .zero (.var 0))) (.mul .zero (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))))198    (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.mul (.var 0) (.mul (.var 1) (.var 1)))) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) (.neg (.mul (.var 0) (.var 1))))) (by decide +kernel)199200theorem F_c3 (q u : Shell p) :201    0 * (q * ((u * u) * u)) + 1 * (q * (u * u)) + 0 * (q * u) + 0 * q = ((u * u) * u) * (q * ((u * u) * u)) + (u * u * u * u + -1) * (-(q * u * u)) :=202  RE.sound (look [q, u])203    (.add (.add (.add (.mul .zero (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))) (.mul .one (.mul (.var 0) (.mul (.var 1) (.var 1))))) (.mul .zero (.mul (.var 0) (.var 1)))) (.mul .zero (.var 0)))204    (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.mul (.var 0) (.mul (.mul (.var 1) (.var 1)) (.var 1)))) (.mul (.add (.mul (.mul (.mul (.var 1) (.var 1)) (.var 1)) (.var 1)) (.neg .one)) (.neg (.mul (.mul (.var 0) (.var 1)) (.var 1))))) (by decide +kernel)205206theorem sum_c0 (q w : Shell p) :207    q + q + q + q = 1 + ((1 + 1 + 1 + 1) * q + -1) * (1) :=208  RE.sound (look [q, w])209    (.add (.add (.add (.var 0) (.var 0)) (.var 0)) (.var 0))210    (.add .one (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)211212theorem sum_c1 (q w : Shell p) :213    q + q * w + -q + -(q * w) = 0 + ((1 + 1 + 1 + 1) * q + -1) * (0) :=214  RE.sound (look [q, w])215    (.add (.add (.add (.var 0) (.mul (.var 0) (.var 1))) (.neg (.var 0))) (.neg (.mul (.var 0) (.var 1))))216    (.add .zero (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)217218theorem sum_c2 (q w : Shell p) :219    q + -q + q + -q = 0 + ((1 + 1 + 1 + 1) * q + -1) * (0) :=220  RE.sound (look [q, w])221    (.add (.add (.add (.var 0) (.neg (.var 0))) (.var 0)) (.neg (.var 0)))222    (.add .zero (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)223224theorem sum_c3 (q w : Shell p) :225    q + -(q * w) + -q + q * w = 0 + ((1 + 1 + 1 + 1) * q + -1) * (0) :=226  RE.sound (look [q, w])227    (.add (.add (.add (.var 0) (.neg (.mul (.var 0) (.var 1)))) (.neg (.var 0))) (.mul (.var 0) (.var 1)))228    (.add .zero (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)229230theorem half_id (q : Shell p) :231    (1 + 1) * (q + q) = 1 + ((1 + 1 + 1 + 1) * q + -1) * (1) :=232  RE.sound (look [q])233    (.mul (.add .one .one) (.add (.var 0) (.var 0)))234    (.add .one (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)235236theorem frft_mul_id (v0 v1 v2 v3 P0 P1 P2 P3 Q : Shell p) :237    (v0 * P0 + v1 * P1 + v2 * P2 + v3 * P3) * Q = v0 * (P0 * Q) + v1 * (P1 * Q) + v2 * (P2 * Q) + v3 * (P3 * Q) :=238  RE.sound (look [v0, v1, v2, v3, P0, P1, P2, P3, Q])239    (.mul (.add (.add (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 5))) (.mul (.var 2) (.var 6))) (.mul (.var 3) (.var 7))) (.var 8))240    (.add (.add (.add (.mul (.var 0) (.mul (.var 4) (.var 8))) (.mul (.var 1) (.mul (.var 5) (.var 8)))) (.mul (.var 2) (.mul (.var 6) (.var 8)))) (.mul (.var 3) (.mul (.var 7) (.var 8)))) (by decide +kernel)241242theorem entry21_one (q i A B : Shell p) :243    q * 0 + (q * -i) * (i * A) + -(-q) * 0 + -(q * -i) * (i * B) = q * (A + -B) + (i * i + 1) * (-(q * A) + q * B) :=244  RE.sound (look [q, i, A, B])245    (.add (.add (.add (.mul (.var 0) .zero) (.mul (.mul (.var 0) (.neg (.var 1))) (.mul (.var 1) (.var 2)))) (.mul (.neg (.neg (.var 0))) .zero)) (.mul (.neg (.mul (.var 0) (.neg (.var 1)))) (.mul (.var 1) (.var 3))))246    (.add (.mul (.var 0) (.add (.var 2) (.neg (.var 3)))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.neg (.mul (.var 0) (.var 2))) (.mul (.var 0) (.var 3))))) (by decide +kernel)247248theorem entry21_three (q i A B : Shell p) :249    q * 0 + -(q * -i) * (i * A) + -(-q) * 0 + (q * -i) * (i * B) = -(q * (A + -B)) + (i * i + 1) * (q * A + -(q * B)) :=250  RE.sound (look [q, i, A, B])251    (.add (.add (.add (.mul (.var 0) .zero) (.mul (.neg (.mul (.var 0) (.neg (.var 1)))) (.mul (.var 1) (.var 2)))) (.mul (.neg (.neg (.var 0))) .zero)) (.mul (.mul (.var 0) (.neg (.var 1))) (.mul (.var 1) (.var 3))))252    (.add (.neg (.mul (.var 0) (.add (.var 2) (.neg (.var 3))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.var 0) (.var 2)) (.neg (.mul (.var 0) (.var 3)))))) (by decide +kernel)253254theorem entry00_zero (q i : Shell p) :255    q * 1 + q * i + q * 1 + q * i = (q + q) * (1 + i) :=256  RE.sound (look [q, i])257    (.add (.add (.add (.mul (.var 0) .one) (.mul (.var 0) (.var 1))) (.mul (.var 0) .one)) (.mul (.var 0) (.var 1)))258    (.mul (.add (.var 0) (.var 0)) (.add .one (.var 1))) (by decide +kernel)259260theorem entry00_two (q i : Shell p) :261    q * 1 + -q * i + q * 1 + -q * i = (q + q) * (1 + -i) :=262  RE.sound (look [q, i])263    (.add (.add (.add (.mul (.var 0) .one) (.mul (.neg (.var 0)) (.var 1))) (.mul (.var 0) .one)) (.mul (.neg (.var 0)) (.var 1)))264    (.mul (.add (.var 0) (.var 0)) (.add .one (.neg (.var 1)))) (by decide +kernel)265266theorem row_zero_id (q jj u i : Shell p) :267    NF0 q jj u * 0 + NF1 q jj u * i + NF2 q jj u * 0 + NF3 q jj u * i = (q + q) * (1 + -(u * u)) * i :=268  RE.sound (look [q, jj, u, i])269    (.add (.add (.add (.mul (.mul (.var 0) (.add (.add (.add .one (.var 2)) (.mul (.var 2) (.var 2))) (.mul (.mul (.var 2) (.var 2)) (.var 2)))) .zero) (.mul (.mul (.var 0) (.add (.add (.add .one (.mul (.var 1) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.var 1) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))) (.var 3))) (.mul (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2))))) .zero)) (.mul (.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))))) (.var 3)))270    (.mul (.mul (.add (.var 0) (.var 0)) (.add .one (.neg (.mul (.var 2) (.var 2))))) (.var 3)) (by decide +kernel)271272/-! ## The algebra of combinations -/273274variable {κ : Nat} {g : Shell p}275276theorem comb_add (a0 a1 a2 a3 b0 b1 b2 b3 : Shell p) (k j : Nat) :277    comb g κ a0 a1 a2 a3 k j + comb g κ b0 b1 b2 b3 k j = comb g κ (a0 + b0) (a1 + b1) (a2 + b2) (a3 + b3) k j :=278  comb_add_id a0 a1 a2 a3 b0 b1 b2 b3 _ _ _ _279280theorem comb_smul (c a0 a1 a2 a3 : Shell p) (k j : Nat) :281    c * comb g κ a0 a1 a2 a3 k j = comb g κ (c * a0) (c * a1) (c * a2) (c * a3) k j :=282  comb_smul_id c a0 a1 a2 a3 _ _ _ _283284theorem comb_zero (k j : Nat) : comb g κ 0 0 0 0 k j = 0 := comb_zero_id _ _ _ _285theorem comb_idm (k j : Nat) : comb g κ 1 0 0 0 k j = idm k j := comb_idm_id _ _ _ _286theorem comb_Fmat (k j : Nat) : comb g κ 0 1 0 0 k j = Fmat g κ k j := comb_Fmat_id _ _ _ _287theorem comb_J (k j : Nat) : comb g κ 0 0 1 0 k j = J (p - 1) k j := comb_J_id _ _ _ _288theorem comb_FJ (k j : Nat) : comb g κ 0 0 0 1 k j = FJ g κ k j := comb_FJ_id _ _ _ _289290/-! ## The constants `w = −i` and `q = −κ` -/291292theorem pow_two_mul (a : Shell p) (n : Nat) : a ^ (2 * n) = a ^ n * a ^ n := by293  rw [pow_mul, pow_mul_comm, pow_two]294295theorem pow_three_mul (a : Shell p) (n : Nat) : a ^ (3 * n) = a ^ n * a ^ n * a ^ n := by296  rw [pow_mul, pow_mul_comm, pow_succ, pow_two]297298theorem w_sq (F : Frame p κ g) : -(quarterTurn g κ) * -(quarterTurn g κ) = -1 := by299  rw [neg_mul_neg, F.quarter_turn_sq]300301theorem w_four (F : Frame p κ g) : (-(quarterTurn g κ)) ^ 4 = 1 := by302  rw [show (4 : Nat) = 2 * 2 from rfl, pow_mul, pow_two, pow_two, w_sq F, neg_mul_neg, one_mul]303304/-- `w^ℓ` is a fourth root of unity, in the form the normaliser takes. -/305theorem u_four (F : Frame p κ g) (ℓ : Nat) :306    (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ + -1 = 0 := by307  have e : ((-(quarterTurn g κ)) ^ ℓ) ^ 4 = (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ *308      (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ := by309    rw [pow_succ, pow_succ, pow_succ, pow_one]310  rw [← e, pow_mul_comm, w_four F, one_pow, add_neg]311312theorem w_pow_mod (F : Frame p κ g) (l : Nat) : (-(quarterTurn g κ)) ^ l = (-(quarterTurn g κ)) ^ (l % 4) := by313  obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 4 (by decide) l314  rw [congrArg (fun e => (-(quarterTurn g κ)) ^ e) hm, pow_add, pow_mul, w_four F, one_pow, one_mul]315316theorem minus_one_ne_one (F : Frame p κ g) : (-1 : Shell p) ≠ 1 := fun h => F.two_ne_zero (by317  rw [two_eq_one_add_one]318  calc (1 : Shell p) + 1 = 1 + -1 := by rw [h]319    _ = 0 := add_neg 1)320321theorem neg_w (F : Frame p κ g) : -(-(quarterTurn g κ)) = -(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ) :=322  red1 (neg_w_id (-(ofNat κ)) (-(quarterTurn g κ))) (hjj F)323324/-- `i = w³`: the quarter-turn is the cube of its inverse. -/325theorem quarter_eq (F : Frame p κ g) : quarterTurn g κ = -(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ) := by326  rw [← neg_w F, neg_neg]327328theorem quarter_pow (F : Frame p κ g) (ℓ : Nat) :329    quarterTurn g κ ^ ℓ = (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ :=330  (congrArg (· ^ ℓ) (quarter_eq F)).trans (by rw [mul_pow, mul_pow])331332theorem w_ne_one (F : Frame p κ g) : -(quarterTurn g κ) ≠ 1 := fun h =>333  F.minus_one_ne_one (by rw [← w_sq F, h, mul_one])334335theorem w_sq_ne_one (F : Frame p κ g) : -(quarterTurn g κ) * -(quarterTurn g κ) ≠ 1 := by336  rw [w_sq F]; exact F.minus_one_ne_one337338theorem w_cube_ne_one (F : Frame p κ g) : -(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ) ≠ 1 := fun h => by339  have hw : -(quarterTurn g κ) = -1 := by rw [← neg_neg (-(quarterTurn g κ)), neg_w F, h]340  exact F.minus_one_ne_one (by rw [← w_sq F, hw, neg_mul_neg, one_mul])341342/-- The nontrivial fourth roots: `w^r ≠ 1` for `0 < r < 4`. -/343theorem w_pow_ne_one (F : Frame p κ g) : ∀ {r : Nat}, 0 < r → r < 4 → (-(quarterTurn g κ)) ^ r ≠ 1344  | 0, h, _ => absurd h (Nat.lt_irrefl 0)345  | 1, _, _ => by rw [pow_one]; exact w_ne_one F346  | 2, _, _ => by rw [pow_two]; exact w_sq_ne_one F347  | 3, _, _ => by rw [pow_succ, pow_two]; exact w_cube_ne_one F348  | n + 4, _, h => absurd (Nat.lt_of_lt_of_le h (Nat.le_add_left 4 n)) (Nat.lt_irrefl _)349350theorem orth_index : ∀ ℓ, ℓ < 4 → ∀ m, m < 4 → ℓ ≠ m → 0 < (ℓ + 3 * m) % 4 := by decide351352/-- The geometric sum of the nontrivial fourth root `x = w^ℓ (w^m)³ = i^{m−ℓ}`, `ℓ ≠ m` below 4. -/353theorem geo_zero (F : Frame p κ g) {ℓ m : Nat} (hℓ : ℓ < 4) (hm : m < 4) (hne : ℓ ≠ m) :354    1 + (-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m) +355      (-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m) *356        ((-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m)) +357      (-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m) *358        ((-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m)) *359        ((-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m)) = 0 := by360  have ex : (-(quarterTurn g κ)) ^ ℓ * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m) =361      (-(quarterTurn g κ)) ^ (ℓ + 3 * m) := by362    rw [pow_add, pow_mul, pow_mul_comm, pow_succ, pow_two]363  have hx4 : ((-(quarterTurn g κ)) ^ (ℓ + 3 * m)) ^ 4 = 1 := by rw [pow_mul_comm, w_four F, one_pow]364  have hx1 : (-(quarterTurn g κ)) ^ (ℓ + 3 * m) ≠ 1 := by365    rw [w_pow_mod F]366    exact w_pow_ne_one F (orth_index ℓ hℓ m hm hne) (Nat.mod_lt _ (by decide))367  have h4 : (0 : Shell p) + ((-(quarterTurn g κ)) ^ (ℓ + 3 * m)) ^ 0 + ((-(quarterTurn g κ)) ^ (ℓ + 3 * m)) ^ 1 +368      ((-(quarterTurn g κ)) ^ (ℓ + 3 * m)) ^ 2 + ((-(quarterTurn g κ)) ^ (ℓ + 3 * m)) ^ 3 = 0 :=369    F.geom_sum_eq_zero 4 hx4 hx1370  rw [zero_add, pow_zero, pow_one, pow_two, pow_succ, pow_two] at h4371  rw [ex]; exact h4372373/-! ## The projectors in coefficient form -/374375/-- `Π_ℓ = q (I + u F + u² J + u³ F J)` with `u = w^ℓ`. -/376theorem proj_eq (ℓ k j : Nat) :377    proj g κ ℓ k j = comb g κ (-(ofNat κ)) (-(ofNat κ) * (-(quarterTurn g κ)) ^ ℓ)378      (-(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ))379      (-(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ)) k j := by380  show comb g κ (-(ofNat κ)) (-(ofNat κ) * (-(quarterTurn g κ)) ^ ℓ) (-(ofNat κ) * (-(quarterTurn g κ)) ^ (2 * ℓ))381    (-(ofNat κ) * (-(quarterTurn g κ)) ^ (3 * ℓ)) k j = _382  rw [pow_two_mul, pow_three_mul]383384theorem proj_zero_eq (k j : Nat) : proj g κ 0 k j = comb g κ (-(ofNat κ)) (-(ofNat κ)) (-(ofNat κ)) (-(ofNat κ)) k j := by385  rw [proj_eq, pow_zero, one_mul, one_mul, mul_one]386387theorem proj_one_eq (F : Frame p κ g) (k j : Nat) :388    proj g κ 1 k j = comb g κ (-(ofNat κ)) (-(ofNat κ) * -(quarterTurn g κ)) (-(-(ofNat κ)))389      (-(-(ofNat κ) * -(quarterTurn g κ))) k j := by390  rw [proj_eq, pow_one, red1 (proj1_c2 _ _) (hjj F), red1 (proj1_c3 _ _) (hjj F)]391392theorem proj_two_eq (F : Frame p κ g) (k j : Nat) :393    proj g κ 2 k j = comb g κ (-(ofNat κ)) (-(-(ofNat κ))) (-(ofNat κ)) (-(-(ofNat κ))) k j := by394  rw [proj_eq, pow_two, red1 (proj2_c1 _ _) (hjj F), red1 (proj2_c2 _ _) (hjj F), red1 (proj2_c3 _ _) (hjj F)]395396theorem proj_three_eq (F : Frame p κ g) (k j : Nat) :397    proj g κ 3 k j = comb g κ (-(ofNat κ)) (-(-(ofNat κ) * -(quarterTurn g κ))) (-(-(ofNat κ)))398      (-(ofNat κ) * -(quarterTurn g κ)) k j := by399  rw [proj_eq, pow_succ, pow_two, red1 (proj3_c1 _ _) (hjj F), red1 (proj3_c2 _ _) (hjj F), red1 (proj3_c3 _ _) (hjj F)]400401/-! ## The projector algebra (6:C2) -/402403theorem proj_mul_pt (ℓ m k j l : Nat) :404    proj g κ ℓ k l * proj g κ m l j =405      comb g κ (-(ofNat κ)) (-(ofNat κ) * (-(quarterTurn g κ)) ^ ℓ)406        (-(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ))407        (-(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ)) k l *408      comb g κ (-(ofNat κ)) (-(ofNat κ) * (-(quarterTurn g κ)) ^ m)409        (-(ofNat κ) * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m))410        (-(ofNat κ) * ((-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m * (-(quarterTurn g κ)) ^ m)) l j := by411  rw [proj_eq, proj_eq]412413/-- 6:C2, the idempotence: `Π_ℓ Π_ℓ = Π_ℓ`, the four coefficients `q² Σ u^a u^{r−a} = q u^r` with `u⁴ = 1`, `4q = 1`. -/414theorem proj_mul_self (F : Frame p κ g) (ℓ : Nat) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :415    sumRange (fun l => proj g κ ℓ k l * proj g κ ℓ l j) (p - 1) = proj g κ ℓ k j := by416  have hu := u_four F ℓ417  have hq := hq F418  rw [sum_congr _ (fun l _ => proj_mul_pt ℓ ℓ k j l), comb_mul F hk hj, proj_eq,419    red2 (self_c0 _ _) hu hq, red2 (self_c1 _ _) hu hq, red2 (self_c2 _ _) hu hq, red2 (self_c3 _ _) hu hq]420421/-- 6:C2, the orthogonality: `Π_ℓ Π_m = 0` for `ℓ ≠ m` below 4, each coefficient `q² v^r (1 + x + x² + x³)` with422`x = u v³` a nontrivial fourth root of unity. -/423theorem proj_mul_ne (F : Frame p κ g) {ℓ m : Nat} (hℓ : ℓ < 4) (hm : m < 4) (hne : ℓ ≠ m) {k j : Nat}424    (hk : k < p - 1) (hj : j < p - 1) :425    sumRange (fun l => proj g κ ℓ k l * proj g κ m l j) (p - 1) = 0 := by426  have hv := u_four F m427  have hx := geo_zero F hℓ hm hne428  rw [sum_congr _ (fun l _ => proj_mul_pt ℓ m k j l), comb_mul F hk hj,429    red2 (ne_c0 _ _ _) hv hx, red2 (ne_c1 _ _ _) hv hx, red2 (ne_c2 _ _ _) hv hx, red2 (ne_c3 _ _ _) hv hx]430  exact comb_zero k j431432/-- 6:C2, the resolution of the identity: `Π₀ + Π₁ + Π₂ + Π₃ = I`. -/433theorem sum_proj (F : Frame p κ g) (k j : Nat) :434    proj g κ 0 k j + proj g κ 1 k j + proj g κ 2 k j + proj g κ 3 k j = idm k j := by435  rw [proj_zero_eq, proj_one_eq F, proj_two_eq F, proj_three_eq F, comb_add, comb_add, comb_add,436    red1 (sum_c0 (-(ofNat κ)) (-(quarterTurn g κ))) (hq F), red1 (sum_c1 _ _) (hq F),437    red1 (sum_c2 (-(ofNat κ)) (-(quarterTurn g κ))) (hq F), red1 (sum_c3 _ _) (hq F)]438  exact comb_idm k j439440theorem Fmat_proj_pt (ℓ k j l : Nat) :441    Fmat g κ k l * proj g κ ℓ l j =442      comb g κ 0 1 0 0 k l *443      comb g κ (-(ofNat κ)) (-(ofNat κ) * (-(quarterTurn g κ)) ^ ℓ)444        (-(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ))445        (-(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ)) l j := by446  rw [comb_Fmat, proj_eq]447448/-- 6:C2, the eigen-relation: `F Π_ℓ = i^ℓ Π_ℓ`, the coefficients of `F Π_ℓ` the cyclic shift of `Π_ℓ`'s and449`i^ℓ = u³` with `u = w^ℓ`. -/450theorem Fmat_proj (F : Frame p κ g) (ℓ : Nat) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :451    sumRange (fun l => Fmat g κ k l * proj g κ ℓ l j) (p - 1) = quarterTurn g κ ^ ℓ * proj g κ ℓ k j := by452  have hu := u_four F ℓ453  rw [sum_congr _ (fun l _ => Fmat_proj_pt ℓ k j l), comb_mul F hk hj, quarter_pow F ℓ, proj_eq, comb_smul,454    red1 (F_c0 _ _) hu, red1 (F_c1 _ _) hu, red1 (F_c2 _ _) hu, red1 (F_c3 _ _) hu]455456/-! ## The two sums (6:C5) -/457458/-- 6:C5, the even sum: `Π₀ + Π₂ = (q + q)(I + J)`, with `q + q = 2⁻¹` (`half`). -/459theorem proj_even_sum (F : Frame p κ g) (k j : Nat) :460    proj g κ 0 k j + proj g κ 2 k j = (-(ofNat κ) + -(ofNat κ)) * (idm k j + J (p - 1) k j) := by461  rw [proj_zero_eq, proj_two_eq F, comb_add]462  exact even_sum_id (-(ofNat κ)) (-(quarterTurn g κ)) _ _ _ _463464/-- 6:C5, the odd sum: `Π₁ + Π₃ = (q + q)(I − J)`. -/465theorem proj_odd_sum (F : Frame p κ g) (k j : Nat) :466    proj g κ 1 k j + proj g κ 3 k j = (-(ofNat κ) + -(ofNat κ)) * (idm k j + -(J (p - 1) k j)) := by467  rw [proj_one_eq F, proj_three_eq F, comb_add]468  exact odd_sum_id (-(ofNat κ)) (-(quarterTurn g κ)) _ _ _ _469470/-- 6:C5, the half: `2 (q + q) = 1`, so `q + q = 2⁻¹ = −2κ`. -/471theorem half (F : Frame p κ g) : (1 + 1 : Shell p) * (-(ofNat κ) + -(ofNat κ)) = 1 :=472  red1 (half_id (-(ofNat κ))) (hq F)473474/-! ## The character sector, nonvanishing, faithfulness and the domains (T03) -/475476theorem proj_mul (F : Frame p κ g) {ℓ m : Nat} (hℓ : ℓ < 4) (hm : m < 4) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :477    sumRange (fun l => proj g κ ℓ k l * proj g κ m l j) (p - 1) = if ℓ = m then proj g κ ℓ k j else 0 :=478  match Nat.decEq ℓ m with479  | isTrue e => by rw [ite_eq_left e]; subst e; exact proj_mul_self F ℓ hk hj480  | isFalse e => by rw [ite_eq_right e]; exact proj_mul_ne F hℓ hm e hk hj481482theorem frft_mul_pt (z : Shell p) (s m k j l : Nat) :483    frft g κ z s k l * proj g κ m l j =484      (z ^ s) ^ 0 * (proj g κ 0 k l * proj g κ m l j) + (z ^ s) ^ 1 * (proj g κ 1 k l * proj g κ m l j) +485      (z ^ s) ^ 2 * (proj g κ 2 k l * proj g κ m l j) + (z ^ s) ^ 3 * (proj g κ 3 k l * proj g κ m l j) :=486  frft_mul_id _ _ _ _ _ _ _ _ _487488/-- 6:C4, 6:E6, the character sector: `F^{[s]} Π_m = (z^s)^m Π_m` on every projector, `m < 4`; the family acts on489`Π_m`'s range by the character `s ↦ z^{ms}`. -/490theorem frft_proj (F : Frame p κ g) (z : Shell p) (s : Nat) {m : Nat} (hm : m < 4) {k j : Nat} (hk : k < p - 1)491    (hj : j < p - 1) :492    sumRange (fun l => frft g κ z s k l * proj g κ m l j) (p - 1) = (z ^ s) ^ m * proj g κ m k j := by493  rw [sum_congr _ (fun l _ => frft_mul_pt z s m k j l), sum_add, sum_add, sum_add, sum_mul_left, sum_mul_left,494    sum_mul_left, sum_mul_left, proj_mul F (Nat.zero_lt_succ 3) hm hk hj, proj_mul F (by decide : (1 : Nat) < 4) hm hk hj,495    proj_mul F (by decide : (2 : Nat) < 4) hm hk hj, proj_mul F (by decide : (3 : Nat) < 4) hm hk hj]496  match m, hm with497  | 0, _ => rw [ite_eq_left rfl, ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_right (by decide),498      mul_zero, mul_zero, mul_zero, add_zero, add_zero, add_zero]499  | 1, _ => rw [ite_eq_right (by decide), ite_eq_left rfl, ite_eq_right (by decide), ite_eq_right (by decide),500      mul_zero, mul_zero, mul_zero, zero_add, add_zero, add_zero]501  | 2, _ => rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl, ite_eq_right (by decide),502      mul_zero, mul_zero, mul_zero, zero_add, zero_add, add_zero]503  | 3, _ => rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl,504      mul_zero, mul_zero, mul_zero, zero_add, zero_add, zero_add]505  | n + 4, h => exact absurd (Nat.lt_of_lt_of_le h (Nat.le_add_left 4 n)) (Nat.lt_irrefl _)506507/-! The basis entries the nonvanishing reads. -/508509theorem idm_ne {k j : Nat} (h : k ≠ j) : (idm k j : Shell p) = 0 := ite_eq_right h510theorem idm_self (k : Nat) : (idm k k : Shell p) = 1 := ite_eq_left rfl511512theorem Fmat_zero_row (g : Shell p) (κ j : Nat) : Fmat g κ 0 j = quarterTurn g κ := by513  show quarterTurn g κ * g ^ (j * 0) = _514  rw [Nat.mul_zero, pow_zero, mul_one]515516theorem FJ_zero_row (g : Shell p) (κ j : Nat) : FJ g κ 0 j = quarterTurn g κ := by517  show quarterTurn g κ * g ^ (rev (p - 1) j * 0) = _518  rw [Nat.mul_zero, pow_zero, mul_one]519520theorem J_zero_zero : (J (p - 1) 0 0 : Shell p) = 1 := ite_eq_left (FRC.Nat.zero_mod _)521522theorem J_zero_row {j : Nat} (hj0 : 0 < j) (hj : j < p - 1) : (J (p - 1) 0 j : Shell p) = 0 :=523  ite_eq_right (fun e => by524    rw [Nat.zero_add, FRC.Nat.mod_eq_of_lt hj] at e525    exact Nat.lt_irrefl 0 (e ▸ hj0))526527theorem three_lt_n (F : Frame p κ g) : 2 + 1 < p - 1 := by528  rw [F.n_eq]; exact Nat.lt_of_lt_of_le (by decide) (Nat.mul_le_mul_left 4 F.cap_pos)529530theorem J_two_one (F : Frame p κ g) : (J (p - 1) 2 1 : Shell p) = 0 :=531  ite_eq_right (fun e => by rw [FRC.Nat.mod_eq_of_lt (three_lt_n F)] at e; exact absurd e (by decide))532533theorem hii (F : Frame p κ g) : quarterTurn g κ * quarterTurn g κ + 1 = 0 := by534  rw [F.quarter_turn_sq, neg_add]535536theorem q_ne_zero (F : Frame p κ g) : -(ofNat κ) ≠ (0 : Shell p) := fun h =>537  F.one_ne_zero (by538    have e := hq F539    rw [h, mul_zero, zero_add] at e540    rw [← neg_neg (1 : Shell p), e, neg_zero])541542theorem half_ne_zero (F : Frame p κ g) : -(ofNat κ) + -(ofNat κ) ≠ (0 : Shell p) := fun h =>543  F.one_ne_zero (by rw [← half F, h, mul_zero])544545theorem quarter_ne_zero (F : Frame p κ g) : quarterTurn g κ ≠ 0 := fun h =>546  F.one_ne_zero (by rw [← neg_neg (1 : Shell p), ← F.quarter_turn_sq, h, mul_zero, neg_zero])547548theorem one_add_quarter_ne_zero (F : Frame p κ g) : 1 + quarterTurn g κ ≠ 0 := fun h =>549  F.minus_one_ne_one (by rw [← F.quarter_turn_sq, ← neg_eq_of_add_eq_zero h, neg_mul_neg, one_mul])550551theorem one_sub_quarter_ne_zero (F : Frame p κ g) : 1 + -(quarterTurn g κ) ≠ 0 := fun h => by552  have hi : quarterTurn g κ = 1 := by rw [← neg_neg (quarterTurn g κ), ← neg_eq_of_add_eq_zero h, neg_neg]553  exact F.minus_one_ne_one (by rw [← F.quarter_turn_sq, hi, one_mul])554555/-- 6:C5, the entry `(0, 0)` of the even projectors: `(Π₀)₀₀ = (q + q)(1 + i)` and `(Π₂)₀₀ = (q + q)(1 − i)`. -/556theorem even_proj_entry (F : Frame p κ g) :557    proj g κ 0 0 0 = (-(ofNat κ) + -(ofNat κ)) * (1 + quarterTurn g κ) ∧558      proj g κ 2 0 0 = (-(ofNat κ) + -(ofNat κ)) * (1 + -(quarterTurn g κ)) := by559  rw [proj_zero_eq, proj_two_eq F]560  show -(ofNat κ) * idm 0 0 + -(ofNat κ) * Fmat g κ 0 0 + -(ofNat κ) * J (p - 1) 0 0 + -(ofNat κ) * FJ g κ 0 0 = _ ∧561    -(ofNat κ) * idm 0 0 + -(-(ofNat κ)) * Fmat g κ 0 0 + -(ofNat κ) * J (p - 1) 0 0 + -(-(ofNat κ)) * FJ g κ 0 0 = _562  rw [idm_self, Fmat_zero_row, FJ_zero_row, J_zero_zero]563  exact ⟨entry00_zero _ _, entry00_two _ _⟩564565/-- 6:C5, the even projectors never vanish: `(Π₀)₀₀ ≠ 0` and `(Π₂)₀₀ ≠ 0` on every frame, since `q + q = 2⁻¹` and566`1 ± i` are nonzero. -/567theorem even_proj_ne_zero (F : Frame p κ g) : proj g κ 0 0 0 ≠ 0 ∧ proj g κ 2 0 0 ≠ 0 := by568  rw [(even_proj_entry F).1, (even_proj_entry F).2]569  exact ⟨F.mul_ne_zero (half_ne_zero F) (one_add_quarter_ne_zero F),570    F.mul_ne_zero (half_ne_zero F) (one_sub_quarter_ne_zero F)⟩571572/-- 6:C5, the odd projectors at the entry `(2, 1)`: `(Π₁)₂₁ = q (g² − g^{−2})` and `(Π₃)₂₁ = −q (g² − g^{−2})`,573with `g^{−2}` read as `g^{2 (n−1)}`. -/574theorem odd_proj_entry (F : Frame p κ g) :575    proj g κ 1 2 1 = -(ofNat κ) * (g ^ (1 * 2) + -(g ^ (rev (p - 1) 1 * 2))) ∧576      proj g κ 3 2 1 = -(-(ofNat κ) * (g ^ (1 * 2) + -(g ^ (rev (p - 1) 1 * 2)))) := by577  rw [proj_one_eq F, proj_three_eq F]578  show -(ofNat κ) * idm 2 1 + -(ofNat κ) * -(quarterTurn g κ) * Fmat g κ 2 1 + -(-(ofNat κ)) * J (p - 1) 2 1 +579      -(-(ofNat κ) * -(quarterTurn g κ)) * FJ g κ 2 1 = _ ∧580    -(ofNat κ) * idm 2 1 + -(-(ofNat κ) * -(quarterTurn g κ)) * Fmat g κ 2 1 + -(-(ofNat κ)) * J (p - 1) 2 1 +581      -(ofNat κ) * -(quarterTurn g κ) * FJ g κ 2 1 = _582  rw [idm_ne (by decide), J_two_one F]583  exact ⟨red1 (entry21_one _ _ _ _) (hii F), red1 (entry21_three _ _ _ _) (hii F)⟩584585theorem four_lt_n (F : Frame p κ g) (hκ : 2 ≤ κ) : 4 < p - 1 := by586  rw [F.n_eq]; exact Nat.lt_of_lt_of_le (by decide) (Nat.mul_le_mul_left 4 hκ)587588/-- `g² ≠ g^{−2}` for `κ ≥ 2`: otherwise `g⁴ = 1` below the order `4κ`. -/589theorem sq_ne_inv_sq (F : Frame p κ g) (hκ : 2 ≤ κ) : g ^ (1 * 2) + -(g ^ (rev (p - 1) 1 * 2)) ≠ 0 := fun h => by590  have hn := F.n_pos591  have h1 : 1 < p - 1 := Nat.lt_trans (by decide) (four_lt_n F hκ)592  have e : g ^ (1 * 2) = g ^ (rev (p - 1) 1 * 2) := by rw [eq_neg_of_add_eq_zero h, neg_neg]593  have e1 : g ^ (rev (p - 1) 1 * 2) * g ^ (1 * 2) = 1 := by594    rw [← pow_add, ← FRC.Nat.add_mul]595    exact F.pow_eq_one_of_mod (by rw [FRC.Nat.mul_mod_left' _ _ _ hn, rev_add_mod h1, Nat.zero_mul]; rfl)596  rw [← e, ← pow_add] at e1597  exact F.prim.2 4 (four_lt_n F hκ) (by decide) e1598599/-- 6:C5, the odd projectors do not vanish for `κ ≥ 2`: the entry `(2, 1)` of each is `±q (g² − g^{−2}) ≠ 0`. -/600theorem odd_proj_ne_zero (F : Frame p κ g) (hκ : 2 ≤ κ) : proj g κ 1 2 1 ≠ 0 ∧ proj g κ 3 2 1 ≠ 0 := by601  rw [(odd_proj_entry F).1, (odd_proj_entry F).2]602  have h := F.mul_ne_zero (q_ne_zero F) (sq_ne_inv_sq F hκ)603  exact ⟨h, fun e => h (by rw [← neg_neg (-(ofNat κ) * _), e, neg_zero])⟩604605/-- 6:C4, 6:D2, faithfulness: `F^{[s]} = F^{[r]}` entrywise forces `s = r` below the period, for `κ ≥ 2`. The entry606`(2, 1)` of `F^{[s]} Π₁ = z^s Π₁` reads `z^s (Π₁)₂₁` with `(Π₁)₂₁ ≠ 0`, so `z^s = z^r` and `z` has order `4κ`. -/607theorem frft_injective (F : Frame p κ g) (hκ : 2 ≤ κ) {z : Shell p} (hz : g * z = 1) {s r : Nat} (hs : s < p - 1)608    (hr : r < p - 1) (h : ∀ k j, k < p - 1 → j < p - 1 → frft g κ z s k j = frft g κ z r k j) : s = r := by609  have h2 : 2 < p - 1 := Nat.lt_trans (by decide) (four_lt_n F hκ)610  have h1 : 1 < p - 1 := Nat.lt_trans (by decide) h2611  have es := frft_proj F z s (by decide : (1 : Nat) < 4) h2 h1612  have er := frft_proj F z r (by decide : (1 : Nat) < 4) h2 h1613  have hsum : sumRange (fun l => frft g κ z s 2 l * proj g κ 1 l 1) (p - 1) =614      sumRange (fun l => frft g κ z r 2 l * proj g κ 1 l 1) (p - 1) :=615    sum_congr _ (fun l hl => by rw [h 2 l h2 hl])616  rw [es, er, pow_one, pow_one] at hsum617  have hz' : z ^ s = z ^ r :=618    (inv_frame F hz).mul_left_cancel (odd_proj_ne_zero F hκ).1619      ((mul_comm _ _).trans (hsum.trans (mul_comm _ _)))620  exact (inv_frame F hz).pow_inj hs hr hz'621622/-! The shell `p = 5` (`κ = 1`), its two frames `g = 2, 3`, decided by the kernel. -/623624theorem frame5_two : Frame 5 1 (2 : Shell 5) := ⟨rfl, Nat.zero_lt_succ 0, by decide⟩625theorem frame5_three : Frame 5 1 (3 : Shell 5) := ⟨rfl, Nat.zero_lt_succ 0, by decide⟩626627/-- 6:C4, 6:C5, 6:D2, the shell `p = 5` has exactly the two frames `g = 2` and `g = 3`. -/628theorem five_frames : ∀ g : Shell 5, IsPrimitive g 4 → g = 2 ∨ g = 3 := by decide +kernel629630/-- 6:C5, 6:C4, at `p = 5` exactly one odd projector vanishes: `Π₁ = 0 ≠ Π₃` at `g = 2`, `Π₃ = 0 ≠ Π₁` at `g = 3`;631the surviving odd projector carries the faithful character `s ↦ z^{ms}`, `m` its index. -/632theorem five_odd_proj :633    (∀ k, k < 4 → ∀ j, j < 4 → proj (2 : Shell 5) 1 1 k j = 0) ∧ proj (2 : Shell 5) 1 3 1 1 ≠ 0 ∧634    (∀ k, k < 4 → ∀ j, j < 4 → proj (3 : Shell 5) 1 3 k j = 0) ∧ proj (3 : Shell 5) 1 1 1 1 ≠ 0 ∧635    (∀ s, s < 4 → ∀ r, r < 4 → (3 : Shell 5) ^ (3 * s) = 3 ^ (3 * r) → s = r) ∧636    (∀ s, s < 4 → ∀ r, r < 4 → (2 : Shell 5) ^ (1 * s) = 2 ^ (1 * r) → s = r) := by decide +kernel637638/-- 6:C4, 6:D2, faithfulness at `p = 5` on both frames (`z = g⁻¹`: `3` for `g = 2`, `2` for `g = 3`). -/639theorem five_faithful :640    (∀ s, s < 4 → ∀ r, r < 4 → (∀ k, k < 4 → ∀ j, j < 4 → frft (2 : Shell 5) 1 3 s k j = frft (2 : Shell 5) 1 3 r k j) →641      s = r) ∧642    (∀ s, s < 4 → ∀ r, r < 4 → (∀ k, k < 4 → ∀ j, j < 4 → frft (3 : Shell 5) 1 2 s k j = frft (3 : Shell 5) 1 2 r k j) →643      s = r) := by decide +kernel644645/-! The domains (6:D1, 6:D2, 6:D7). -/646647/-- 6:D1, every `F^{[s]}` is invertible: `F^{[s]} F^{[n−s]} = I = F^{[n−s]} F^{[s]}` for `s ≤ n = p − 1`. -/648theorem frft_inverse (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {s : Nat} (hs : s ≤ p - 1) {k j : Nat}649    (hk : k < p - 1) (hj : j < p - 1) :650    sumRange (fun l => frft g κ z s k l * frft g κ z (p - 1 - s) l j) (p - 1) = idm k j ∧651      sumRange (fun l => frft g κ z (p - 1 - s) k l * frft g κ z s l j) (p - 1) = idm k j := by652  have hn : frft g κ z (p - 1) k j = idm k j := by653    have e := frft_period F hz 0 k j654    rw [Nat.zero_add] at e655    rw [e]; exact (frft_cardinal F hz k j).1656  constructor657  · rw [← frft_add F z s (p - 1 - s) hk hj, FRC.Nat.add_sub_of_le hs]; exact hn658  · rw [← frft_add F z (p - 1 - s) s hk hj, FRC.Nat.sub_add_cancel hs]; exact hn659660/-- 6:D2, the half-turn is the reversal: `F^{[s + 2κ]} = F^{[s]} J`, entrywise `F^{[s+2κ]}_{kj} = F^{[s]}_{k, rev j}`,661so the framed bases `B_{s+2κ}` and `B_s` agree as unordered bases. -/662theorem frft_half_turn (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (s : Nat) {k j : Nat} (hk : k < p - 1)663    (hj : j < p - 1) : frft g κ z (s + 2 * κ) k j = frft g κ z s k (rev (p - 1) j) := by664  rw [frft_add F z s (2 * κ) hk hj, sum_congr _ (fun l _ => by rw [(frft_cardinal F hz l j).2.2.1])]665  exact mm_X_J (frft g κ z s) hj666667/-- 6:D7, the row-0 entries of `F^{[t]}` off the site `j = 0`: `F^{[t]}_{0j} = (q + q)(1 − z^{2t}) i = (i/2)(1 − g^{−2t})`,668the same value at every `0 < j < n`. -/669theorem frft_row_zero (F : Frame p κ g) (z : Shell p) (t : Nat) {j : Nat} (hj0 : 0 < j) (hj : j < p - 1) :670    frft g κ z t 0 j = (-(ofNat κ) + -(ofNat κ)) * (1 + -(z ^ t * z ^ t)) * quarterTurn g κ := by671  rw [frft_eq F z t 0 j]672  show NF0 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * idm 0 j + NF1 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * Fmat g κ 0 j +673    NF2 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * J (p - 1) 0 j + NF3 (-(ofNat κ)) (-(quarterTurn g κ)) (z ^ t) * FJ g κ 0 j = _674  rw [idm_ne (fun (e : 0 = j) => Nat.lt_irrefl j (e ▸ hj0)), J_zero_row hj0 hj, Fmat_zero_row, FJ_zero_row]675  exact row_zero_id _ _ _ _676677/-- `t + t ≡ 0 (mod n)` below `n = 2κ + 2κ` forces `t = 0` or `t = 2κ`. -/678theorem double_mod_n (F : Frame p κ g) {t : Nat} (ht : t < p - 1) (h : (t + t) % (p - 1) = 0) : t = 0 ∨ t = 2 * κ := by679  have hn := F.n_pos680  obtain ⟨c, hc⟩ := FRC.Nat.mod_spec (p - 1) hn (t + t)681  rw [h, Nat.add_zero] at hc682  match c, hc with683  | 0, hc => exact Or.inl (match t, hc with | 0, _ => rfl | t + 1, hc => Nat.noConfusion hc)684  | 1, hc =>685    rw [Nat.mul_one, ← F.four_kappa, ← Nat.two_mul, ← Nat.two_mul] at hc686    exact Or.inr (Nat.eq_of_mul_eq_mul_left (by decide) hc)687  | c + 2, hc =>688    have : t + t < (p - 1) * (c + 2) :=689      Nat.lt_of_lt_of_le (Nat.add_lt_add ht ht) (by rw [Nat.mul_add, Nat.mul_two]; exact Nat.le_add_left _ _)690    exact absurd hc (Nat.ne_of_lt this)691692/-- 6:D7, the row-0 entries off the site are nonzero for `t ∉ {0, 2κ}` (the paper reads: `F^{[t]}` is not monomial,693`B_{s+t} ≠ B_s`, exactly `2κ` unordered bases). -/694theorem frft_row_zero_ne_zero (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {t : Nat} (ht : t < p - 1) (h0 : t ≠ 0)695    (h2 : t ≠ 2 * κ) {j : Nat} (hj0 : 0 < j) (hj : j < p - 1) : frft g κ z t 0 j ≠ 0 := by696  rw [frft_row_zero F z t hj0 hj]697  refine F.mul_ne_zero (F.mul_ne_zero (half_ne_zero F) ?_) (quarter_ne_zero F)698  intro e699  have e1 : z ^ (t + t) = 1 := by rw [pow_add, ← neg_neg (z ^ t * z ^ t), ← neg_eq_of_add_eq_zero e, neg_neg]700  match double_mod_n F ht ((inv_frame F hz).mod_eq_zero_of_pow_eq_one e1) with701  | Or.inl e0 => exact h0 e0702  | Or.inr e2 => exact h2 e2703704end Frame705end Shell706end FRC707