Theme/Heisenberg.lean — FrcCore

1import FrcCore.Theme.Rotations2import FrcCore.Theme.Dichotomy34/-!5# FrcCore.Theme.Heisenberg — the character sector and the cardinal Heisenberg covariance (the fourier theme)67The sixth file of the fourier theme (6-fourier's blueprint of 8 October 2026, task T07). On the range of `Π₁` the8family acts by the meridian character, `F^{[s]} Π₁ = z^s Π₁` (`frft_proj`), so `F^{[s]} T_v = T_v S_{−s}` for9`T_v(x) = x v`, and the rotation `R_s` carries the same character on its eigenline `(1, −i)` (6:E6). The shift10`(σ v)_k = v_{k−1}` and the modulation `D₁ = diag(g^k)` are intertwined by the cardinal skeleton: `F σ = D₁ F`,11`F D₁ = σ⁻¹ F`, `J σ = σ⁻¹ J`, `F J σ = D₁⁻¹ F J`, the quarter-rotation `σ ↦ D₁ ↦ σ⁻¹ ↦ D₁⁻¹` (6:E7); and12`F^{[s]} = Σ_r c_r(s) F^r` with `c_r(s) = ¼ Σ_ℓ (g^{rκ−s})^ℓ` is `frft_eq` of `Theme/Fourier.lean` with its13coefficients written as geometric sums. No axioms.14-/1516namespace FRC17namespace Shell18namespace Frame1920variable {p : Nat} [Pos p]2122/-! ## Ring identities (generated; `RE.sound`, decided by the kernel) -/2324theorem shift_id (i A B : Shell p) :25    i * (A * B) = B * (i * A) :=26  RE.sound (look [i, A, B])27    (.mul (.var 0) (.mul (.var 1) (.var 2)))28    (.mul (.var 2) (.mul (.var 0) (.var 1))) (by decide +kernel)2930theorem modul_id (i A B : Shell p) :31    (i * A) * B = 1 * (i * (A * B)) :=32  RE.sound (look [i, A, B])33    (.mul (.mul (.var 0) (.var 1)) (.var 2))34    (.mul .one (.mul (.var 0) (.mul (.var 1) (.var 2)))) (by decide +kernel)3536theorem assoc4_id (Z A B C : Shell p) :37    (Z * A) * (B * C) = (Z * C) * (A * B) :=38  RE.sound (look [Z, A, B, C])39    (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))40    (.mul (.mul (.var 0) (.var 3)) (.mul (.var 1) (.var 2))) (by decide +kernel)4142theorem coeff1_id (q i u : Shell p) :43    q * (1 + -i * u + -(u * u) + -(-i * ((u * u) * u))) = q * (1 + u * -i + (u * -i) * (u * -i) + ((u * -i) * (u * -i)) * (u * -i)) + (i * i + 1) * (q * i * u * u * u + -(q * u * u)) :=44  RE.sound (look [q, i, u])45    (.mul (.var 0) (.add (.add (.add .one (.mul (.neg (.var 1)) (.var 2))) (.neg (.mul (.var 2) (.var 2)))) (.neg (.mul (.neg (.var 1)) (.mul (.mul (.var 2) (.var 2)) (.var 2))))))46    (.add (.mul (.var 0) (.add (.add (.add .one (.mul (.var 2) (.neg (.var 1)))) (.mul (.mul (.var 2) (.neg (.var 1))) (.mul (.var 2) (.neg (.var 1))))) (.mul (.mul (.mul (.var 2) (.neg (.var 1))) (.mul (.var 2) (.neg (.var 1)))) (.mul (.var 2) (.neg (.var 1)))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2)) (.neg (.mul (.mul (.var 0) (.var 2)) (.var 2)))))) (by decide +kernel)4748theorem coeff2_id (q i u : Shell p) :49    q * (1 + -u + u * u + -((u * u) * u)) = q * (1 + u * (-i * -i) + (u * (-i * -i)) * (u * (-i * -i)) + ((u * (-i * -i)) * (u * (-i * -i))) * (u * (-i * -i))) + (i * i + 1) * (-(q * i * i * i * i * u * u * u) + q * i * i * u * u * u + -(q * i * i * u * u) + -(q * u * u * u) + q * u * u + -(q * u)) :=50  RE.sound (look [q, i, u])51    (.mul (.var 0) (.add (.add (.add .one (.neg (.var 2))) (.mul (.var 2) (.var 2))) (.neg (.mul (.mul (.var 2) (.var 2)) (.var 2)))))52    (.add (.mul (.var 0) (.add (.add (.add .one (.mul (.var 2) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.mul (.mul (.var 2) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.var 2) (.mul (.neg (.var 1)) (.neg (.var 1)))))) (.mul (.mul (.mul (.var 2) (.mul (.neg (.var 1)) (.neg (.var 1)))) (.mul (.var 2) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.mul (.var 2) (.mul (.neg (.var 1)) (.neg (.var 1))))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.add (.add (.neg (.mul (.mul (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2))) (.mul (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 2)) (.var 2)) (.var 2))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 2)) (.var 2)))) (.neg (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.var 2)))) (.mul (.mul (.var 0) (.var 2)) (.var 2))) (.neg (.mul (.var 0) (.var 2)))))) (by decide +kernel)5354theorem coeff3_id (q i u : Shell p) :55    q * (1 + -(-i * u) + -(u * u) + -i * ((u * u) * u)) = q * (1 + u * ((-i * -i) * -i) + (u * ((-i * -i) * -i)) * (u * ((-i * -i) * -i)) + ((u * ((-i * -i) * -i)) * (u * ((-i * -i) * -i))) * (u * ((-i * -i) * -i))) + (i * i + 1) * (q * i * i * i * i * i * i * i * u * u * u + -(q * i * i * i * i * i * u * u * u) + -(q * i * i * i * i * u * u) + q * i * i * i * u * u * u + q * i * i * u * u + -(q * i * u * u * u) + q * i * u + -(q * u * u)) :=56  RE.sound (look [q, i, u])57    (.mul (.var 0) (.add (.add (.add .one (.neg (.mul (.neg (.var 1)) (.var 2)))) (.neg (.mul (.var 2) (.var 2)))) (.mul (.neg (.var 1)) (.mul (.mul (.var 2) (.var 2)) (.var 2)))))58    (.add (.mul (.var 0) (.add (.add (.add .one (.mul (.var 2) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))) (.mul (.mul (.var 2) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.var 2) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))))) (.mul (.mul (.mul (.var 2) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1)))) (.mul (.var 2) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))) (.mul (.var 2) (.mul (.mul (.neg (.var 1)) (.neg (.var 1))) (.neg (.var 1))))))) (.mul (.add (.mul (.var 1) (.var 1)) .one) (.add (.add (.add (.add (.add (.add (.add (.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)) (.neg (.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)))) (.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))) (.neg (.mul (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.var 2)) (.var 2)))) (.mul (.mul (.var 0) (.var 1)) (.var 2))) (.neg (.mul (.mul (.var 0) (.var 2)) (.var 2)))))) (by decide +kernel)5960theorem eigenline_a_id (i c d : Shell p) :61    c * 1 + -(d * -i) = (c + i * d) * 1 :=62  RE.sound (look [i, c, d])63    (.add (.mul (.var 1) .one) (.neg (.mul (.var 2) (.neg (.var 0)))))64    (.mul (.add (.var 1) (.mul (.var 0) (.var 2))) .one) (by decide +kernel)6566theorem eigenline_b_id (i c d : Shell p) :67    d * 1 + c * -i = (c + i * d) * -i + (i * i + 1) * (d) :=68  RE.sound (look [i, c, d])69    (.add (.mul (.var 2) .one) (.mul (.var 1) (.neg (.var 0))))70    (.add (.mul (.add (.var 1) (.mul (.var 0) (.var 2))) (.neg (.var 0))) (.mul (.add (.mul (.var 0) (.var 0)) .one) (.var 2))) (by decide +kernel)7172variable {κ : Nat} {g : Shell p}7374/-! ## The common character sector (6:E6) -/7576/-- 6:E6, the intertwiner: `F^{[s]} T_v = T_v S_{−s}` with `v` a column of `Π₁` and `T_v(x) = x v`, `S_{−s} x = z^s x`. -/77theorem frft_intertwine (F : Frame p κ g) (z : Shell p) (s : Nat) (x : Shell p) {k j : Nat} (hk : k < p - 1)78    (hj : j < p - 1) :79    sumRange (fun l => frft g κ z s k l * (x * proj g κ 1 l j)) (p - 1) = x * (z ^ s * proj g κ 1 k j) := by80  rw [sum_congr _ (fun l _ => mul_left_comm (frft g κ z s k l) x (proj g κ 1 l j)), sum_mul_left,81    frft_proj F z s (by decide : (1 : Nat) < 4) hk hj, pow_one]8283/-- 6:E6, the eigenline: `R_s (1, −i)ᵀ = z_s (1, −i)ᵀ`. -/84theorem rot_eigenline (F : Frame p κ g) (z : Shell p) (s : Nat) :85    cs g κ z s * 1 + -(ds g κ z s * -(quarterTurn g κ)) = z ^ s * 1 ∧86      ds g κ z s * 1 + cs g κ z s * -(quarterTurn g κ) = z ^ s * -(quarterTurn g κ) :=87  ⟨by rw [eigenline_a_id, (rot_eq F z s).1], by rw [red1 (eigenline_b_id _ _ _) (hii F), (rot_eq F z s).1]⟩8889/-! ## The shift and the modulation -/9091/-- The shift `(σ v)_k = v_{k−1}`: `σ_{kj} = [j + 1 ≡ k]`. -/92def shift (p : Nat) [Pos p] (k j : Nat) : Shell p := if (j + 1) % (p - 1) = k then 1 else 09394/-- Its inverse `(σ⁻¹ v)_k = v_{k+1}`: `σ⁻¹_{kj} = [k + 1 ≡ j]`. -/95def shiftInv (p : Nat) [Pos p] (k j : Nat) : Shell p := if (k + 1) % (p - 1) = j then 1 else 09697/-- The modulation `D₁ = diag(g^k)`; `D₁⁻¹ = diag(z^k)` is `modul z`. -/98def modul (g : Shell p) (k j : Nat) : Shell p := if k = j then g ^ k else 099100theorem shift_single (F : Frame p κ g) (X : Nat → Nat → Shell p) (k j : Nat) :101    sumRange (fun l => X k l * shift p l j) (p - 1) = X k ((j + 1) % (p - 1)) := by102  rw [sum_eq_single (FRC.Nat.mod_lt' _ F.n_pos) (fun l _ hne => by103    show X k l * (if (j + 1) % (p - 1) = l then 1 else 0) = 0104    rw [ite_eq_right (fun e => hne e.symm), mul_zero])]105  show X k ((j + 1) % (p - 1)) * (if (j + 1) % (p - 1) = (j + 1) % (p - 1) then 1 else 0) = _106  rw [ite_eq_left rfl, mul_one]107108theorem shiftInv_single (F : Frame p κ g) (X : Nat → Nat → Shell p) (k j : Nat) :109    sumRange (fun l => shiftInv p k l * X l j) (p - 1) = X ((k + 1) % (p - 1)) j := by110  rw [sum_eq_single (FRC.Nat.mod_lt' _ F.n_pos) (fun l _ hne => by111    show (if (k + 1) % (p - 1) = l then 1 else 0) * X l j = 0112    rw [ite_eq_right (fun e => hne e.symm), zero_mul])]113  show (if (k + 1) % (p - 1) = (k + 1) % (p - 1) then 1 else 0) * X ((k + 1) % (p - 1)) j = _114  rw [ite_eq_left rfl, one_mul]115116theorem modul_left (a : Shell p) (X : Nat → Nat → Shell p) {k : Nat} (hk : k < p - 1) (j : Nat) :117    sumRange (fun l => modul a k l * X l j) (p - 1) = a ^ k * X k j := by118  rw [sum_eq_single hk (fun l _ hne => by119    show (if k = l then a ^ k else 0) * X l j = 0120    rw [ite_eq_right (fun e => hne e.symm), zero_mul])]121  show (if k = k then a ^ k else 0) * X k j = _122  rw [ite_eq_left rfl]123124theorem modul_right (a : Shell p) (X : Nat → Nat → Shell p) (k : Nat) {j : Nat} (hj : j < p - 1) :125    sumRange (fun l => X k l * modul a l j) (p - 1) = X k j * a ^ j := by126  rw [sum_eq_single hj (fun l _ hne => by127    show X k l * (if l = j then a ^ l else 0) = 0128    rw [ite_eq_right hne, mul_zero])]129  show X k j * (if j = j then a ^ j else 0) = _130  rw [ite_eq_left rfl]131132theorem add_n_mod (F : Frame p κ g) {x : Nat} (hx : x < p - 1) : (x + (p - 1)) % (p - 1) = x := by133  have e := FRC.Nat.add_mul_mod_self_left x 1 (p - 1) F.n_pos134  rw [Nat.mul_one] at e135  rw [Nat.add_comm, e, FRC.Nat.mod_eq_of_lt hx]136137theorem succ_pred_mod (F : Frame p κ g) {k : Nat} (hk : k < p - 1) : ((k + (p - 1 - 1)) % (p - 1) + 1) % (p - 1) = k := by138  rw [FRC.Nat.mod_add_mod _ _ _ F.n_pos, Nat.add_assoc, FRC.Nat.sub_add_cancel F.n_pos, add_n_mod F hk]139140theorem pred_succ_mod (F : Frame p κ g) {l : Nat} (hl : l < p - 1) : ((l + 1) % (p - 1) + (p - 1 - 1)) % (p - 1) = l := by141  rw [FRC.Nat.mod_add_mod _ _ _ F.n_pos, Nat.add_assoc, Nat.add_comm 1 (p - 1 - 1), FRC.Nat.sub_add_cancel F.n_pos,142    add_n_mod F hl]143144/-- `g^{((j+1) mod n) k} = g^{jk} g^k`. -/145theorem pow_succ_mod (F : Frame p κ g) (j k : Nat) : g ^ ((j + 1) % (p - 1) * k) = g ^ (j * k) * g ^ k := by146  rw [F.pow_mod, FRC.Nat.mod_mul_mod _ _ _ F.n_pos, ← F.pow_mod, Nat.add_mul, Nat.one_mul, pow_add]147148/-- 6:E7, `F σ = D₁ F`: the transform turns the shift into the modulation. -/149theorem Fmat_shift (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (_hj : j < p - 1) :150    sumRange (fun l => Fmat g κ k l * shift p l j) (p - 1) = sumRange (fun l => modul g k l * Fmat g κ l j) (p - 1) := by151  rw [shift_single F, modul_left g (Fmat g κ) hk j]152  show quarterTurn g κ * g ^ ((j + 1) % (p - 1) * k) = g ^ k * (quarterTurn g κ * g ^ (j * k))153  rw [pow_succ_mod F]; exact shift_id _ _ _154155/-- `g^{j ((k+1) mod n)} = g^{jk} g^j`. -/156theorem pow_mod_succ (F : Frame p κ g) (j k : Nat) : g ^ (j * ((k + 1) % (p - 1))) = g ^ (j * k) * g ^ j := by157  rw [F.pow_mod, FRC.Nat.mul_mod_mod _ _ _ F.n_pos, ← F.pow_mod, Nat.mul_add, Nat.mul_one, pow_add]158159/-- 6:E7, `F D₁ = σ⁻¹ F`: the transform turns the modulation into the inverse shift. -/160theorem Fmat_modul (F : Frame p κ g) {k j : Nat} (_hk : k < p - 1) (hj : j < p - 1) :161    sumRange (fun l => Fmat g κ k l * modul g l j) (p - 1) = sumRange (fun l => shiftInv p k l * Fmat g κ l j) (p - 1) := by162  rw [modul_right g (Fmat g κ) k hj, shiftInv_single F]163  show quarterTurn g κ * g ^ (j * k) * g ^ j = quarterTurn g κ * g ^ (j * ((k + 1) % (p - 1)))164  rw [pow_mod_succ F]; exact (modul_id _ _ _).trans (one_mul _)165166theorem ite_iff {c1 c2 : Prop} [Decidable c1] [Decidable c2] (h : c1 ↔ c2) :167    (if c1 then (1 : Shell p) else 0) = if c2 then 1 else 0 :=168  match Decidable.em c1 with169  | Or.inl e => by rw [ite_eq_left e, ite_eq_left (h.1 e)]170  | Or.inr e => by rw [ite_eq_right e, ite_eq_right (fun e2 => e (h.2 e2))]171172/-- 6:E7, `J σ = σ⁻¹ J`: the reversal conjugates the shift to its inverse. -/173theorem J_shift (F : Frame p κ g) {k j : Nat} (_hk : k < p - 1) (_hj : j < p - 1) :174    sumRange (fun l => (J (p - 1) k l : Shell p) * shift p l j) (p - 1) =175      sumRange (fun l => shiftInv p k l * J (p - 1) l j) (p - 1) := by176  have hn := F.n_pos177  rw [shift_single F (fun k l => (J (p - 1) k l : Shell p)), shiftInv_single F (fun l j => (J (p - 1) l j : Shell p))]178  show (if (k + (j + 1) % (p - 1)) % (p - 1) = 0 then (1 : Shell p) else 0) =179    if ((k + 1) % (p - 1) + j) % (p - 1) = 0 then 1 else 0180  apply ite_iff181  rw [FRC.Nat.add_mod_mod _ _ _ hn, FRC.Nat.mod_add_mod _ _ _ hn, ← Nat.add_assoc, Nat.add_right_comm k j 1]182183/-- 6:E7, `σ σ⁻¹ = I = σ⁻¹ σ` on the cycle: `shiftInv` is the inverse shift. -/184theorem shift_inverse (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :185    sumRange (fun l => shift p k l * shiftInv p l j) (p - 1) = idm k j ∧186      sumRange (fun l => shiftInv p k l * shift p l j) (p - 1) = idm k j := by187  have hn := F.n_pos188  constructor189  · rw [sum_eq_single (l₀ := (k + (p - 1 - 1)) % (p - 1)) (FRC.Nat.mod_lt' _ hn) (fun l hl hne => by190      show (if (l + 1) % (p - 1) = k then (1 : Shell p) else 0) * shiftInv p l j = 0191      rw [ite_eq_right (fun e => hne (by rw [← pred_succ_mod F hl, e])), zero_mul])]192    show (if ((k + (p - 1 - 1)) % (p - 1) + 1) % (p - 1) = k then (1 : Shell p) else 0) *193      (if ((k + (p - 1 - 1)) % (p - 1) + 1) % (p - 1) = j then (1 : Shell p) else 0) = idm k j194    rw [succ_pred_mod F hk, ite_eq_left rfl, one_mul]195    rfl196  · rw [shiftInv_single F (fun k l => shift p k l) k j]197    show (if (j + 1) % (p - 1) = (k + 1) % (p - 1) then (1 : Shell p) else 0) = idm k j198    exact ite_iff ⟨fun e => (shift_inj F (one_lt_n F) j k hj hk (by rw [Nat.add_comm 1 j, Nat.add_comm 1 k]; exact e)).symm,199      fun e => by rw [e]⟩200201/-- `g^{(−a) k} g^{a k} = 1` for `a < n`, with `−a = rev a`. -/202theorem pow_rev_mul (F : Frame p κ g) {a : Nat} (ha : a < p - 1) (k : Nat) :203    g ^ (rev (p - 1) a * k) * g ^ (a * k) = 1 := by204  rw [← pow_add, ← FRC.Nat.add_mul, F.pow_mod, ← FRC.Nat.mod_mul_mod _ _ _ F.n_pos, rev_add_mod ha, Nat.zero_mul,205    FRC.Nat.zero_mod, pow_zero]206207/-- 6:E7, `F J σ = D₁⁻¹ F J`: the inverse transform turns the shift into the inverse modulation. -/208theorem FJ_shift (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :209    sumRange (fun l => FJ g κ k l * shift p l j) (p - 1) = sumRange (fun l => modul z k l * FJ g κ l j) (p - 1) := by210  have hn := F.n_pos211  rw [shift_single F, modul_left z (FJ g κ) hk j]212  show quarterTurn g κ * g ^ (rev (p - 1) ((j + 1) % (p - 1)) * k) = z ^ k * (quarterTurn g κ * g ^ (rev (p - 1) j * k))213  have e : g ^ (rev (p - 1) ((j + 1) % (p - 1)) * k) = z ^ k * g ^ (rev (p - 1) j * k) := by214    apply inv_unique (y := g ^ ((j + 1) % (p - 1) * k))215    · exact pow_rev_mul F (FRC.Nat.mod_lt' _ hn) k216    · rw [pow_succ_mod F, assoc4_id, ← mul_pow, mul_comm z g, hz, one_pow, one_mul, pow_rev_mul F hj]217  rw [e]; exact mul_left_comm _ _ _218219/-- 6:E7, the quarter-rotation of the Heisenberg pair: `F σ = D₁ F`, `F D₁ = σ⁻¹ F`, `J σ = σ⁻¹ J`, `FJ σ = D₁⁻¹ FJ`. -/220theorem heisenberg (F : Frame p κ g) {z : Shell p} (hz : g * z = 1) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :221    sumRange (fun l => Fmat g κ k l * shift p l j) (p - 1) = sumRange (fun l => modul g k l * Fmat g κ l j) (p - 1) ∧222    sumRange (fun l => Fmat g κ k l * modul g l j) (p - 1) = sumRange (fun l => shiftInv p k l * Fmat g κ l j) (p - 1) ∧223    sumRange (fun l => (J (p - 1) k l : Shell p) * shift p l j) (p - 1) =224      sumRange (fun l => shiftInv p k l * J (p - 1) l j) (p - 1) ∧225    sumRange (fun l => FJ g κ k l * shift p l j) (p - 1) = sumRange (fun l => modul z k l * FJ g κ l j) (p - 1) :=226  ⟨Fmat_shift F hk hj, Fmat_modul F hk hj, J_shift F hk hj, FJ_shift F hz hk hj⟩227228/-! ## The expansion `F^{[s]} = Σ_r c_r(s) F^r` -/229230/-- 6:E7, the coefficients of `frft_eq` are the geometric sums `c_r(s) = ¼ Σ_{ℓ<4} (u w^r)^ℓ`, `u = z^s`, `w = g^κ = −i`:231`c_r(s) = ¼ Σ_ℓ (g^{rκ−s})^ℓ`. -/232theorem frft_coeff (F : Frame p κ g) (u : Shell p) :233    NF0 (-(ofNat κ)) (-(quarterTurn g κ)) u = -(ofNat κ) * (1 + u + u * u + u * u * u) ∧234    NF1 (-(ofNat κ)) (-(quarterTurn g κ)) u =235      -(ofNat κ) * (1 + u * -(quarterTurn g κ) + u * -(quarterTurn g κ) * (u * -(quarterTurn g κ)) +236        u * -(quarterTurn g κ) * (u * -(quarterTurn g κ)) * (u * -(quarterTurn g κ))) ∧237    NF2 (-(ofNat κ)) (-(quarterTurn g κ)) u =238      -(ofNat κ) * (1 + u * (-(quarterTurn g κ) * -(quarterTurn g κ)) +239        u * (-(quarterTurn g κ) * -(quarterTurn g κ)) * (u * (-(quarterTurn g κ) * -(quarterTurn g κ))) +240        u * (-(quarterTurn g κ) * -(quarterTurn g κ)) * (u * (-(quarterTurn g κ) * -(quarterTurn g κ))) *241          (u * (-(quarterTurn g κ) * -(quarterTurn g κ)))) ∧242    NF3 (-(ofNat κ)) (-(quarterTurn g κ)) u =243      -(ofNat κ) * (1 + u * (-(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ)) +244        u * (-(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ)) *245          (u * (-(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ))) +246        u * (-(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ)) *247          (u * (-(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ))) *248          (u * (-(quarterTurn g κ) * -(quarterTurn g κ) * -(quarterTurn g κ)))) :=249  ⟨rfl, red1 (coeff1_id _ _ _) (hii F), red1 (coeff2_id _ _ _) (hii F), red1 (coeff3_id _ _ _) (hii F)⟩250251/-- 6:E7, `g^κ = −w = −i`: the coefficient base of `frft_coeff` is `u w^r = z^s (g^κ)^r = g^{rκ − s}`. -/252theorem w_eq_pow_kappa : -(quarterTurn g κ) = g ^ κ := neg_neg _253254end Frame255end Shell256end FRC257