Theme/Dichotomy.lean — FrcCore

1import FrcCore.Theme.Lifts23/-!4# FrcCore.Theme.Dichotomy — the multiplicity dichotomy in trace form (the fourier theme)56The fourth file of the fourier theme (6-fourier's blueprint of 8 October 2026, task T05). With the Gauss sum7`G = Σ_k g^{k²}` over the cycle and its conjugate `Ḡ = Σ_k z^{k²}` (`z = g⁻¹`), the traces of the cardinal powers are8`Tr I = n = −1`, `Tr F = i G`, `Tr F² = Tr J = 2`, `Tr F³ = Tr FJ = i Ḡ`, and the trace of a projector is9`Tr Π_ℓ = q Σ_r w^{ℓr} Tr F^r` (`q = 4⁻¹`, `w = i⁻¹`). The product `G Ḡ = −2` comes from the substitution10`k = l + d` and the geometric sum. When `G = ε (1 + i)` with `ε = ±1` (the sign of the Gauss sum, the paper's import A3,11decided by the kernel on the six shells of its table), the conjugate sum is `Ḡ = −ε (1 − i)` (the conjugate law12`ε(g⁻¹) = −ε(g)`) and the four traces are `(κ, κ, κ+1, κ−1)` for `ε = 1` and `(κ+1, κ−1, κ, κ)` for `ε = −1`, read in13the field (6:C7). No axioms.14-/1516namespace FRC17namespace Shell18namespace Frame1920variable {p : Nat} [Pos p]2122/-! ## Ring identities (generated; `RE.sound`, decided by the kernel) -/2324theorem gauss_pt_id (A B D E : Shell p) :25    ((A * B) * (B * D)) * E = D * (B * B) + (A * E + -1) * ((D * B) * B) :=26  RE.sound (look [A, B, D, E])27    (.mul (.mul (.mul (.var 0) (.var 1)) (.mul (.var 1) (.var 2))) (.var 3))28    (.add (.mul (.var 2) (.mul (.var 1) (.var 1))) (.mul (.add (.mul (.var 0) (.var 3)) (.neg .one)) (.mul (.mul (.var 2) (.var 1)) (.var 1)))) (by decide +kernel)2930theorem one_add_i_mul (i : Shell p) :31    (1 + i) * (1 + -i) = 1 + 1 + (i * i + 1) * (-1) :=32  RE.sound (look [i])33    (.mul (.add .one (.var 0)) (.add .one (.neg (.var 0))))34    (.add (.add .one .one) (.mul (.add (.mul (.var 0) (.var 0)) .one) (.neg .one))) (by decide +kernel)3536theorem conj_sign_id (e i : Shell p) :37    (e * (1 + i)) * -(e * (1 + -i)) = -(1 + 1) + (e * e + -1) * -(1 + 1) + (i * i + 1) * (e * e) :=38  RE.sound (look [e, i])39    (.mul (.mul (.var 0) (.add .one (.var 1))) (.neg (.mul (.var 0) (.add .one (.neg (.var 1))))))40    (.add (.add (.neg (.add .one .one)) (.mul (.add (.mul (.var 0) (.var 0)) (.neg .one)) (.neg (.add .one .one)))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.mul (.var 0) (.var 0)))) (by decide +kernel)4142theorem tuple_plus_0 (q i : Shell p) :43    q * -1 + (q * 1) * (i * (1 * (1 + i))) + (q * (1 * 1)) * (1 + 1) + (q * ((1 * 1) * 1)) * (i * -(1 * (1 + -i))) = -q + (i * i + 1) * ((1 + 1) * q) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=44  RE.sound (look [q, i])45    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) .one) (.mul (.var 1) (.mul .one (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul .one .one)) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul .one .one) .one)) (.mul (.var 1) (.neg (.mul .one (.add .one (.neg (.var 1))))))))46    (.add (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.mul (.add .one .one) (.var 0)))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)4748theorem tuple_plus_1 (q i : Shell p) :49    q * -1 + (q * -i) * (i * (1 * (1 + i))) + (q * (-i * -i)) * (1 + 1) + (q * ((-i * -i) * -i)) * (i * -(1 * (1 + -i))) = -q + (i * i + 1) * (-(q * i * i * i) + q * i * i) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=50  RE.sound (look [q, i])51    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) (.neg (.var 1))) (.mul (.var 1) (.mul .one (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.var 1) (.neg (.mul .one (.add .one (.neg (.var 1))))))))52    (.add (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.neg (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1))) (.mul (.mul (.var 0) (.var 1)) (.var 1))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)5354theorem tuple_plus_2 (q i : Shell p) :55    q * -1 + (q * (-i * -i)) * (i * (1 * (1 + i))) + (q * ((-i * -i) * (-i * -i))) * (1 + 1) + (q * (((-i * -i) * (-i * -i)) * (-i * -i))) * (i * -(1 * (1 + -i))) = -q + 1 + (i * i + 1) * (q * i * i * i * i * i * i + -(q * i * i * i * i * i) + -(q * i * i * i * i) + q * i * i * i + (1 + 1 + 1 + 1) * q * i * i + -((1 + 1 + 1 + 1) * q)) + ((1 + 1 + 1 + 1) * q + -1) * (1) :=56  RE.sound (look [q, i])57    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.var 1) (.mul .one (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.mul (.var 1) (.neg (.mul .one (.add .one (.neg (.var 1))))))))58    (.add (.add (.add (.neg (.var 0)) .one) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.add (.add (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.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)))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1))) (.mul (.mul (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.var 1)) (.var 1))) (.neg (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)5960theorem tuple_plus_3 (q i : Shell p) :61    q * -1 + (q * ((-i * -i) * -i)) * (i * (1 * (1 + i))) + (q * (((-i * -i) * -i) * ((-i * -i) * -i))) * (1 + 1) + (q * ((((-i * -i) * -i) * ((-i * -i) * -i)) * ((-i * -i) * -i))) * (i * -(1 * (1 + -i))) = -q + -1 + (i * i + 1) * (-(q * i * i * i * i * i * i * i * i * i) + q * i * i * i * i * i * i * i * i + q * i * i * i * i * i * i * i + -(q * i * i * i * i * i * i) + -(q * i * i * i * i * i) + (1 + 1 + 1) * q * i * i * i * i + -((1 + 1 + 1 + 1) * q * i * i) + (1 + 1 + 1 + 1) * q) + ((1 + 1 + 1 + 1) * q + -1) * (-1) :=62  RE.sound (look [q, i])63    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.var 1) (.mul .one (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))) (.mul (.var 1) (.neg (.mul .one (.add .one (.neg (.var 1))))))))64    (.add (.add (.add (.neg (.var 0)) (.neg .one)) (.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 (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.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 1))) (.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 (.mul (.var 0) (.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 (.mul (.mul (.add (.add .one .one) .one) (.var 0)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.neg (.mul (.mul (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.var 1)) (.var 1)))) (.mul (.add (.add (.add .one .one) .one) .one) (.var 0))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.neg .one))) (by decide +kernel)6566theorem tuple_minus_0 (q i : Shell p) :67    q * -1 + (q * 1) * (i * (-1 * (1 + i))) + (q * (1 * 1)) * (1 + 1) + (q * ((1 * 1) * 1)) * (i * -(-1 * (1 + -i))) = -q + 1 + (i * i + 1) * (-((1 + 1) * q)) + ((1 + 1 + 1 + 1) * q + -1) * (1) :=68  RE.sound (look [q, i])69    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) .one) (.mul (.var 1) (.mul (.neg .one) (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul .one .one)) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul .one .one) .one)) (.mul (.var 1) (.neg (.mul (.neg .one) (.add .one (.neg (.var 1))))))))70    (.add (.add (.add (.neg (.var 0)) .one) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.neg (.mul (.add .one .one) (.var 0))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .one)) (by decide +kernel)7172theorem tuple_minus_1 (q i : Shell p) :73    q * -1 + (q * -i) * (i * (-1 * (1 + i))) + (q * (-i * -i)) * (1 + 1) + (q * ((-i * -i) * -i)) * (i * -(-1 * (1 + -i))) = -q + -1 + (i * i + 1) * (q * i * i * i + -(q * i * i) + (1 + 1 + 1 + 1) * q) + ((1 + 1 + 1 + 1) * q + -1) * (-1) :=74  RE.sound (look [q, i])75    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) (.neg (.var 1))) (.mul (.var 1) (.mul (.neg .one) (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.var 1) (.neg (.mul (.neg .one) (.add .one (.neg (.var 1))))))))76    (.add (.add (.add (.neg (.var 0)) (.neg .one)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.neg (.mul (.mul (.var 0) (.var 1)) (.var 1)))) (.mul (.add (.add (.add .one .one) .one) .one) (.var 0))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) (.neg .one))) (by decide +kernel)7778theorem tuple_minus_2 (q i : Shell p) :79    q * -1 + (q * (-i * -i)) * (i * (-1 * (1 + i))) + (q * ((-i * -i) * (-i * -i))) * (1 + 1) + (q * (((-i * -i) * (-i * -i)) * (-i * -i))) * (i * -(-1 * (1 + -i))) = -q + (i * i + 1) * (-(q * i * i * i * i * i * i) + q * i * i * i * i * i + q * i * i * i * i + -(q * i * i * i)) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=80  RE.sound (look [q, i])81    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.var 1) (.mul (.neg .one) (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.mul (.var 1) (.neg (.mul (.neg .one) (.add .one (.neg (.var 1))))))))82    (.add (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.neg (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)8384theorem tuple_minus_3 (q i : Shell p) :85    q * -1 + (q * ((-i * -i) * -i)) * (i * (-1 * (1 + i))) + (q * (((-i * -i) * -i) * ((-i * -i) * -i))) * (1 + 1) + (q * ((((-i * -i) * -i) * ((-i * -i) * -i)) * ((-i * -i) * -i))) * (i * -(-1 * (1 + -i))) = -q + (i * i + 1) * (q * i * i * i * i * i * i * i * i * i + -(q * i * i * i * i * i * i * i * i) + -(q * i * i * i * i * i * i * i) + q * i * i * i * i * i * i + q * i * i * i * i * i + q * i * i * i * i) + ((1 + 1 + 1 + 1) * q + -1) * (0) :=86  RE.sound (look [q, i])87    (.add (.add (.add (.mul (.var 0) (.neg .one)) (.mul (.mul (.var 0) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.var 1) (.mul (.neg .one) (.add .one (.var 1)))))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))) (.add .one .one))) (.mul (.mul (.var 0) (.mul (.mul (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))) (.mul (.var 1) (.neg (.mul (.neg .one) (.add .one (.neg (.var 1))))))))88    (.add (.add (.neg (.var 0)) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.add (.add (.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 1)) (.var 1)) (.neg (.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 1)))) (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)))) (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 1))) (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1))))) (.mul (.add (.mul (.add (.add (.add .one .one) .one) .one) (.var 0)) (.neg .one)) .zero)) (by decide +kernel)8990variable {κ : Nat} {g : Shell p}9192/-- The quadratic Gauss sum over the cycle, `G = Σ_{k<n} g^{k²}`; `Tr W = G`. -/93def gauss (g : Shell p) (n : Nat) : Shell p := sumRange (fun k => g ^ (k * k)) n9495/-! ## The traces of the four basis matrices -/9697theorem trace_comb (c0 c1 c2 c3 : Shell p) :98    sumRange (fun k => comb g κ c0 c1 c2 c3 k k) (p - 1) =99      c0 * trace (idm : Nat → Nat → Shell p) (p - 1) + c1 * trace (Fmat g κ) (p - 1) +100        c2 * trace (J (p - 1) : Nat → Nat → Shell p) (p - 1) + c3 * trace (FJ g κ) (p - 1) := by101  show sumRange (fun k => c0 * idm k k + c1 * Fmat g κ k k + c2 * J (p - 1) k k + c3 * FJ g κ k k) (p - 1) =102    c0 * sumRange (fun k => idm k k) (p - 1) + c1 * sumRange (fun k => Fmat g κ k k) (p - 1) +103      c2 * sumRange (fun k => J (p - 1) k k) (p - 1) + c3 * sumRange (fun k => FJ g κ k k) (p - 1)104  rw [sum_add, sum_add, sum_add, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left]105106theorem trace_idm (F : Frame p κ g) : trace (idm : Nat → Nat → Shell p) (p - 1) = -1 := by107  show sumRange (fun k => idm k k) (p - 1) = -1108  rw [sum_congr _ (fun k _ => idm_self k), sum_const, mul_one, F.ofNat_n]109110theorem trace_Fmat : trace (Fmat g κ) (p - 1) = quarterTurn g κ * gauss g (p - 1) :=111  sum_mul_left (fun k => g ^ (k * k)) (quarterTurn g κ) (p - 1)112113theorem J_diag (F : Frame p κ g) {k : Nat} (hk : k < p - 1) : (J (p - 1) k k : Shell p) = idm k 0 + idm k (2 * κ) := by114  show (if (k + k) % (p - 1) = 0 then (1 : Shell p) else 0) = (if k = 0 then 1 else 0) + (if k = 2 * κ then 1 else 0)115  match Nat.decEq ((k + k) % (p - 1)) 0 with116  | isTrue h =>117    rw [ite_eq_left h]118    match double_mod_n F hk h with119    | Or.inl e =>120      rw [ite_eq_left e, ite_eq_right (fun e2 => absurd F.two_kappa_pos (by rw [← e2, e]; exact Nat.lt_irrefl 0)), add_zero]121    | Or.inr e =>122      rw [ite_eq_right (fun e0 => absurd F.two_kappa_pos (by rw [← e, e0]; exact Nat.lt_irrefl 0)), ite_eq_left e, zero_add]123  | isFalse h =>124    rw [ite_eq_right h, ite_eq_right (fun e => h (by rw [e]; exact FRC.Nat.zero_mod _)),125      ite_eq_right (fun e => h (by rw [e, F.four_kappa]; exact FRC.Nat.mod_self _ F.n_pos)), add_zero]126127/-- `Tr J = 2`: the reversal fixes the two sites `0` and `2κ`. -/128theorem trace_J (F : Frame p κ g) : trace (J (p - 1) : Nat → Nat → Shell p) (p - 1) = 1 + 1 := by129  show sumRange (fun k => (J (p - 1) k k : Shell p)) (p - 1) = 1 + 1130  rw [sum_congr _ (fun k hk => J_diag F hk), sum_add, sum_eq_single F.n_pos (fun l _ hne => idm_ne hne),131    sum_eq_single F.two_kappa_lt (fun l _ hne => idm_ne hne), idm_self, idm_self]132133/-- `g^{(−k) k} = z^{k²}`: the reversed exponent is the conjugate's. -/134theorem W_rev_diag (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {k : Nat} (hk : k < p - 1) :135    g ^ (rev (p - 1) k * k) = z ^ (k * k) := by136  have hn := F.n_pos137  apply inv_unique (y := g ^ (k * k))138  · rw [← pow_add, ← FRC.Nat.add_mul, F.pow_mod, ← FRC.Nat.mod_mul_mod _ _ _ hn, rev_add_mod hk, Nat.zero_mul,139      FRC.Nat.zero_mod, pow_zero]140  · rw [← mul_pow, mul_comm, hz, one_pow]141142theorem trace_FJ (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) :143    trace (FJ g κ) (p - 1) = quarterTurn g κ * gauss z (p - 1) := by144  show sumRange (fun k => quarterTurn g κ * g ^ (rev (p - 1) k * k)) (p - 1) =145    quarterTurn g κ * sumRange (fun k => z ^ (k * k)) (p - 1)146  rw [sum_congr _ (fun k hk => by rw [W_rev_diag F hz hk])]147  exact sum_mul_left _ _ _148149/-- 6:C7, the traces of the cardinal powers: `Tr I = −1`, `Tr F = i G`, `Tr F² = Tr J = 2`, `Tr F³ = Tr FJ = i Ḡ`. -/150theorem trace_powers (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) :151    trace (idm : Nat → Nat → Shell p) (p - 1) = -1 ∧ trace (Fmat g κ) (p - 1) = quarterTurn g κ * gauss g (p - 1) ∧152      trace (J (p - 1) : Nat → Nat → Shell p) (p - 1) = 1 + 1 ∧153      trace (FJ g κ) (p - 1) = quarterTurn g κ * gauss z (p - 1) :=154  ⟨trace_idm F, trace_Fmat, trace_J F, trace_FJ F hz⟩155156/-- 6:C7, the trace of a projector in trace form: `Tr Π_ℓ = q (Tr I + u Tr F + u² Tr J + u³ Tr FJ)`, `u = w^ℓ`, i.e.157`Tr Π_ℓ = ¼ Σ_r i^{−ℓr} Tr F^r`. -/158theorem trace_proj (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) (ℓ : Nat) :159    trace (proj g κ ℓ) (p - 1) =160      -(ofNat κ) * -1 + -(ofNat κ) * (-(quarterTurn g κ)) ^ ℓ * (quarterTurn g κ * gauss g (p - 1)) +161        -(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ) * (1 + 1) +162        -(ofNat κ) * ((-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ * (-(quarterTurn g κ)) ^ ℓ) *163          (quarterTurn g κ * gauss z (p - 1)) := by164  show sumRange (fun k => proj g κ ℓ k k) (p - 1) = _165  rw [sum_congr _ (fun k _ => proj_eq ℓ k k), trace_comb, trace_idm F, trace_Fmat, trace_J F, trace_FJ F hz]166167/-! ## `G Ḡ = −2` -/168169/-- The sums commute. -/170theorem sum_swap (f : Nat → Nat → Shell p) (n : Nat) : ∀ m : Nat,171    sumRange (fun l => sumRange (fun d => f l d) n) m = sumRange (fun d => sumRange (fun l => f l d) m) n172  | 0 => (sum_zero n (fun _ _ => rfl)).symm173  | m + 1 => by174    show sumRange (fun l => sumRange (fun d => f l d) n) m + sumRange (fun d => f m d) n =175      sumRange (fun d => sumRange (fun l => f l d) m + f m d) n176    rw [sum_swap f n m, ← sum_add]177178/-- The shift `d ↦ (l + d) % n` is injective on the cycle. -/179theorem shift_inj (F : Frame p κ g) {l : Nat} (hl : l < p - 1) (i j : Nat) (hi : i < p - 1) (hj : j < p - 1)180    (h : (l + i) % (p - 1) = (l + j) % (p - 1)) : i = j := by181  have hn := F.n_pos182  have key : ∀ i, i < p - 1 → i = (rev (p - 1) l + (l + i) % (p - 1)) % (p - 1) := fun i hi => by183    rw [FRC.Nat.add_mod_mod _ _ _ hn, ← Nat.add_assoc, ← FRC.Nat.mod_add_mod _ _ _ hn, rev_add_mod hl, Nat.zero_add,184      FRC.Nat.mod_eq_of_lt hi]185  rw [key i hi, key j hj, h]186187/-- The term of the double sum after the substitution `k = l + d`: `g^{(l+d)²} z^{l²} = g^{d²} (g^{2d})^l`. -/188theorem gauss_pt {z : Shell p} (hz : g * z = 1) (l d : Nat) :189    g ^ ((l + d) * (l + d)) * z ^ (l * l) = g ^ (d * d) * (g ^ (d + d)) ^ l := by190  have hAE : g ^ (l * l) * z ^ (l * l) + -1 = 0 := by rw [← mul_pow, hz, one_pow, add_neg]191  rw [Nat.add_mul, pow_add g (l * (l + d)), Nat.mul_add, Nat.mul_add, pow_add g (l * l), pow_add g (d * l),192    ← pow_mul g (d + d) l, Nat.add_mul d d l, pow_add g (d * l), Nat.mul_comm l d]193  exact red1 (gauss_pt_id _ _ _ _) hAE194195/-- The inner geometric sum: `Σ_{l<n} (g^{2d})^l` is `−1` at `d ∈ {0, 2κ}` and `0` elsewhere. -/196theorem gauss_inner (F : Frame p κ g) {d : Nat} (hd : d < p - 1) :197    g ^ (d * d) * sumRange (fun l => (g ^ (d + d)) ^ l) (p - 1) = -(idm d 0 + idm d (2 * κ)) := by198  match Nat.decEq ((d + d) % (p - 1)) 0 with199  | isTrue h =>200    have h1 : g ^ (d + d) = 1 := F.pow_eq_one_of_mod h201    have hs : sumRange (fun l => (g ^ (d + d)) ^ l) (p - 1) = -1 := by202      rw [sum_congr _ (fun l _ => by rw [h1, one_pow]), sum_const, mul_one, F.ofNat_n]203    rw [hs]204    match double_mod_n F hd h with205    | Or.inl e =>206      rw [e, idm_self, idm_ne (fun e2 => absurd F.two_kappa_pos (by rw [← e2]; exact Nat.lt_irrefl 0)), add_zero,207        Nat.mul_zero, pow_zero, one_mul]208    | Or.inr e =>209      rw [e, idm_ne (fun e0 => absurd F.two_kappa_pos (by rw [e0]; exact Nat.lt_irrefl 0)), idm_self, zero_add,210        pow_mul, F.half_period, pow_mul, pow_two, neg_mul_neg, one_mul, one_pow, one_mul]211  | isFalse h =>212    rw [F.geom_sum_eq_zero _ (by rw [pow_mul_comm, F.pow_n, one_pow]) (fun e => h (F.mod_eq_zero_of_pow_eq_one e)),213      mul_zero, idm_ne (fun e => h (by rw [e]; exact FRC.Nat.zero_mod _)),214      idm_ne (fun e => h (by rw [e, F.four_kappa]; exact FRC.Nat.mod_self _ F.n_pos)), add_zero, neg_zero]215216/-- 6:C7, `G Ḡ = −2`: the substitution `k = l + d` and the geometric sum over `l`. -/217theorem gauss_mul (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) :218    gauss g (p - 1) * gauss z (p - 1) = -(1 + 1) := by219  have hn := F.n_pos220  show sumRange (fun k => g ^ (k * k)) (p - 1) * sumRange (fun l => z ^ (l * l)) (p - 1) = -(1 + 1)221  rw [← sum_mul_left]222  rw [sum_congr _ (fun l hl => by223    show sumRange (fun k => g ^ (k * k)) (p - 1) * z ^ (l * l) =224      sumRange (fun d => g ^ (d * d) * (g ^ (d + d)) ^ l) (p - 1)225    rw [← sum_mul_right, ← sum_perm (fun k => g ^ (k * k) * z ^ (l * l)) (fun d => (l + d) % (p - 1)) (p - 1)226      (fun d _ => FRC.Nat.mod_lt' _ hn) (shift_inj F hl)]227    exact sum_congr _ (fun d _ => by228      show g ^ ((l + d) % (p - 1) * ((l + d) % (p - 1))) * z ^ (l * l) = g ^ (d * d) * (g ^ (d + d)) ^ l229      rw [F.pow_mod ((l + d) % (p - 1) * ((l + d) % (p - 1))), FRC.Nat.mod_mul_mod _ _ _ hn,230        FRC.Nat.mul_mod_mod _ _ _ hn, ← F.pow_mod, gauss_pt hz l d]))]231  rw [sum_swap (fun l d => g ^ (d * d) * (g ^ (d + d)) ^ l) (p - 1) (p - 1)]232  rw [sum_congr _ (fun d hd => by rw [sum_mul_left, gauss_inner F hd]), sum_neg, sum_add,233    sum_eq_single F.n_pos (fun l _ hne => idm_ne hne), sum_eq_single F.two_kappa_lt (fun l _ hne => idm_ne hne),234    idm_self, idm_self]235236/-! ## The sign and the two tuples (6:C7) -/237238/-- `G ≠ 0`, since `G Ḡ = −2`. -/239theorem gauss_ne_zero (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) : gauss g (p - 1) ≠ 0 := fun h =>240  F.two_ne_zero (by241    have e := gauss_mul F hz242    rw [h, zero_mul] at e243    rw [two_eq_one_add_one (p := p), ← neg_neg (1 + 1 : Shell p), ← e, neg_zero])244245/-- 6:C7, the conjugate law: when `G = ε (1 + i)` with `ε² = 1`, the conjugate frame's Gauss sum is246`Ḡ = −ε (1 − i)`, i.e. `ε(g⁻¹) = −ε(g)`. -/247theorem gauss_conj (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {ε : Shell p} (hε : ε * ε = 1)248    (hG : gauss g (p - 1) = ε * (1 + quarterTurn g κ)) :249    gauss z (p - 1) = -(ε * (1 + -(quarterTurn g κ))) := by250  apply F.mul_left_cancel (gauss_ne_zero F hz)251  rw [gauss_mul F hz, hG, conj_sign_id, hε, add_neg, zero_mul, add_zero, hii F, zero_mul, add_zero]252253theorem sign_sq {ε : Shell p} (h : ε = 1 ∨ ε = -1) : ε * ε = 1 := by254  match h with255  | Or.inl e => rw [e, one_mul]256  | Or.inr e => rw [e, neg_mul_neg, one_mul]257258/-- 6:C7, the dichotomy: under `G = ε (1 + i)` the traces of the projectors are `(κ, κ, κ+1, κ−1)` for `ε = 1` and259`(κ+1, κ−1, κ, κ)` for `ε = −1`, read in the field. -/260theorem trace_tuples (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {ε : Shell p} (hε : ε = 1 ∨ ε = -1)261    (hG : gauss g (p - 1) = ε * (1 + quarterTurn g κ)) :262    (ε = 1 ∧ trace (proj g κ 0) (p - 1) = ofNat κ ∧ trace (proj g κ 1) (p - 1) = ofNat κ ∧263        trace (proj g κ 2) (p - 1) = ofNat κ + 1 ∧ trace (proj g κ 3) (p - 1) = ofNat κ + -1) ∨264      (ε = -1 ∧ trace (proj g κ 0) (p - 1) = ofNat κ + 1 ∧ trace (proj g κ 1) (p - 1) = ofNat κ + -1 ∧265        trace (proj g κ 2) (p - 1) = ofNat κ ∧ trace (proj g κ 3) (p - 1) = ofNat κ) := by266  have hGb := gauss_conj F hz (sign_sq hε) hG267  have t0 := trace_proj F hz 0268  have t1 := trace_proj F hz 1269  have t2 := trace_proj F hz 2270  have t3 := trace_proj F hz 3271  rw [pow_zero, hG, hGb] at t0272  rw [pow_one, hG, hGb] at t1273  rw [pow_two, hG, hGb] at t2274  rw [pow_succ, pow_two, hG, hGb] at t3275  have hq := hq F276  have hi := hii F277  have nn : ∀ b : Shell p, -(-(ofNat κ)) + b = ofNat κ + b := fun b => by rw [neg_neg]278  match hε with279  | Or.inl e =>280    subst e281    refine Or.inl ⟨rfl, ?_, ?_, ?_, ?_⟩282    · rw [t0]; exact (red2 (tuple_plus_0 _ _) hi hq).trans (neg_neg _)283    · rw [t1]; exact (red2 (tuple_plus_1 _ _) hi hq).trans (neg_neg _)284    · rw [t2]; exact (red2 (tuple_plus_2 _ _) hi hq).trans (nn 1)285    · rw [t3]; exact (red2 (tuple_plus_3 _ _) hi hq).trans (nn (-1))286  | Or.inr e =>287    subst e288    refine Or.inr ⟨rfl, ?_, ?_, ?_, ?_⟩289    · rw [t0]; exact (red2 (tuple_minus_0 _ _) hi hq).trans (nn 1)290    · rw [t1]; exact (red2 (tuple_minus_1 _ _) hi hq).trans (nn (-1))291    · rw [t2]; exact (red2 (tuple_minus_2 _ _) hi hq).trans (neg_neg _)292    · rw [t3]; exact (red2 (tuple_minus_3 _ _) hi hq).trans (neg_neg _)293294/-! The six shells of the paper's table, decided by the kernel: the sign of the Gauss sum and the tuple of traces. -/295296theorem frame17_three : Frame 17 4 (3 : Shell 17) := ⟨rfl, Nat.zero_lt_succ 3, by decide⟩297theorem frame29_two : Frame 29 7 (2 : Shell 29) := ⟨rfl, Nat.zero_lt_succ 6, by decide⟩298theorem frame37_two : Frame 37 9 (2 : Shell 37) := ⟨rfl, Nat.zero_lt_succ 8, by decide⟩299theorem frame41_six : Frame 41 10 (6 : Shell 41) := ⟨rfl, Nat.zero_lt_succ 9, by decide⟩300301/-- 6:C7, the sign on the six shells: `G = ε (1 + i)` with `ε = −1` at `(5, 2)` and `ε = +1` at `(13, 2)`, `(17, 3)`,302`(29, 2)`, `(37, 2)`, `(41, 6)`. -/303theorem six_signs :304    gauss (2 : Shell 5) 4 = -1 * (1 + quarterTurn 2 1) ∧ gauss (2 : Shell 13) 12 = 1 * (1 + quarterTurn 2 3) ∧305    gauss (3 : Shell 17) 16 = 1 * (1 + quarterTurn 3 4) ∧ gauss (2 : Shell 29) 28 = 1 * (1 + quarterTurn 2 7) ∧306    gauss (2 : Shell 37) 36 = 1 * (1 + quarterTurn 2 9) ∧ gauss (6 : Shell 41) 40 = 1 * (1 + quarterTurn 6 10) := by307  decide +kernel308309/-- 6:C7, the tuples on the six shells: `(2, 0, 1, 1)` at `p = 5` (`ε = −1`) and `(κ, κ, κ+1, κ−1)` at the five others. -/310theorem six_tuples :311    (trace (proj (2 : Shell 5) 1 0) 4 = 2 ∧ trace (proj (2 : Shell 5) 1 1) 4 = 0 ∧312      trace (proj (2 : Shell 5) 1 2) 4 = 1 ∧ trace (proj (2 : Shell 5) 1 3) 4 = 1) ∧313    (trace (proj (2 : Shell 13) 3 0) 12 = 3 ∧ trace (proj (2 : Shell 13) 3 1) 12 = 3 ∧314      trace (proj (2 : Shell 13) 3 2) 12 = 4 ∧ trace (proj (2 : Shell 13) 3 3) 12 = 2) ∧315    (trace (proj (3 : Shell 17) 4 0) 16 = 4 ∧ trace (proj (3 : Shell 17) 4 1) 16 = 4 ∧316      trace (proj (3 : Shell 17) 4 2) 16 = 5 ∧ trace (proj (3 : Shell 17) 4 3) 16 = 3) ∧317    (trace (proj (2 : Shell 29) 7 0) 28 = 7 ∧ trace (proj (2 : Shell 29) 7 1) 28 = 7 ∧318      trace (proj (2 : Shell 29) 7 2) 28 = 8 ∧ trace (proj (2 : Shell 29) 7 3) 28 = 6) ∧319    (trace (proj (2 : Shell 37) 9 0) 36 = 9 ∧ trace (proj (2 : Shell 37) 9 1) 36 = 9 ∧320      trace (proj (2 : Shell 37) 9 2) 36 = 10 ∧ trace (proj (2 : Shell 37) 9 3) 36 = 8) ∧321    (trace (proj (6 : Shell 41) 10 0) 40 = 10 ∧ trace (proj (6 : Shell 41) 10 1) 40 = 10 ∧322      trace (proj (6 : Shell 41) 10 2) 40 = 11 ∧ trace (proj (6 : Shell 41) 10 3) 40 = 9) := by323  decide +kernel324325end Frame326end Shell327end FRC328