Transform.lean — FrcCore

1import FrcCore.Series2import FrcCore.Frame34/-!5# FrcCore.Transform — the shell Fourier transform on the cycle: `W`, the reversal `J`, `F = i W` (the frame theme)67The geometric sum gives the principal-root identity (2:F1, Prop. 6.1 of 2-geometry) and the entrywise inversion of the8shell Fourier matrix `W k j = g^{jk}`: `Σ_l W k l · (−g^{−lj}) = [k = j]` (2:F3, Prop. 6.3; 6:B5 in matrix form); the9reversal `rev`, `J`, and the quarter-turn transform `F = i W` with `W² = −J`, `F² = J`, `J² = I` and `W J = J W` (6:B5,106:B7). Split from `Sum.lean` by the ledger migration (task LM25), every name unchanged, so that the fourier theme takes11the transform without the orbits (gate G10). Since task LM36 it also holds the sum over the nonzero residues reindexed by12the drive (`sum_units_eq_sum_pow`, from `Sum.lean`) and the frame `frame13` (from `Instances.lean`), names unchanged,13so that the horizon theme takes them without the orbits. No axioms.14-/1516namespace FRC17namespace Shell1819variable {p : Nat} [Pos p]2021namespace Frame22variable {κ : Nat} {g : Shell p}2324/-- `Σ_{l<n} x^l = 0` when `x^n = 1` and `x ≠ 1` (the field has no zero divisors). -/25theorem geom_sum_eq_zero (F : Frame p κ g) {x : Shell p} (n : Nat) (hn : x ^ n = 1) (hx : x ≠ 1) :26    sumRange (fun l => x ^ l) n = 0 := by27  have h := geom_sum_mul x n28  rw [hn, add_neg] at h29  match F.mul_eq_zero h with30  | .inl e => exact e31  | .inr e => exact absurd (by32      calc x = x + 0 := (add_zero x).symm33        _ = x + (-1 + 1) := by rw [neg_add]34        _ = (x + -1) + 1 := (add_assoc _ _ _).symm35        _ = 1 := by rw [e, zero_add]) hx3637/-- 6:B6 — the normalization constant read in the field: `n = p − 1 ≡ −1`. -/38theorem ofNat_n (F : Frame p κ g) : (ofNat (p - 1) : Shell p) = -1 := by39  apply ext40  rw [val_ofNat, val_neg, val_one, FRC.Nat.mod_eq_of_lt F.one_lt_p,41    FRC.Nat.mod_eq_of_lt (Nat.sub_lt Pos.pos (Nat.zero_lt_succ 0))]4243/-- 2:F1 (Prop. 6.1), 26:B5, 26:H3 — `g` is a principal root of unity: `g^n = 1`, `Σ_{j<n} (g^k)^j = 0` for44`0 < k < n`, and `n = p − 1` reads as `−1` in the shell. -/45theorem principal_root (F : Frame p κ g) (k : Nat) (hk0 : 0 < k) (hk : k < p - 1) :46    g ^ (p - 1) = 1 ∧ sumRange (fun j => (g ^ k) ^ j) (p - 1) = 0 ∧ (ofNat (p - 1) : Shell p) = -1 := by47  refine ⟨F.pow_n, ?_, F.ofNat_n⟩48  apply F.geom_sum_eq_zero49  · rw [pow_mul_comm, F.pow_n, one_pow]50  · exact F.prim.2 k hk hk05152/-- `g^{k + (n − j)} = 1` exactly when `k = j`, for `k, j < n`. -/53theorem pow_shift_eq_one_iff (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :54    g ^ (k + (p - 1 - j)) = 1 ↔ k = j := by55  have hn := F.n_pos56  have hjn : p - 1 - j + j = p - 1 := FRC.Nat.sub_add_cancel (Nat.le_of_lt hj)57  constructor58  · intro h59    have hm := F.mod_eq_zero_of_pow_eq_one h60    match Nat.lt_or_ge k j with61    | .inl hlt =>62      have hlt' : k + (p - 1 - j) < p - 1 := by63        have := Nat.add_lt_add_right hlt (p - 1 - j)64        rw [Nat.add_comm j, hjn] at this65        exact this66      rw [FRC.Nat.mod_eq_of_lt hlt'] at hm67      have hpos : 0 < p - 1 - j := by68        refine Nat.lt_of_add_lt_add_right (n := j) ?_69        rw [Nat.zero_add, hjn]; exact hj70      exact absurd hm (Nat.ne_of_gt (Nat.lt_of_lt_of_le hpos (Nat.le_add_left _ _)))71    | .inr hge =>72      have e : k + (p - 1 - j) = (p - 1) * 1 + (k - j) := by73        rw [Nat.mul_one]74        calc k + (p - 1 - j) = (j + (k - j)) + (p - 1 - j) := by rw [FRC.Nat.add_sub_of_le hge]75          _ = (p - 1 - j + j) + (k - j) := by76              rw [Nat.add_comm j (k - j), Nat.add_assoc, Nat.add_comm (k - j), Nat.add_comm j (p - 1 - j)]77          _ = p - 1 + (k - j) := by rw [hjn]78      rw [e, FRC.Nat.add_mul_mod_self_left _ _ _ hn,79        FRC.Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.sub_le k j) hk)] at hm80      have := FRC.Nat.add_sub_of_le hge81      rw [hm, Nat.add_zero] at this82      exact this.symm83  · intro e84    rw [e, FRC.Nat.add_sub_of_le (Nat.le_of_lt hj), F.pow_n]8586/-- 2:F3 (Prop. 6.3), 6:B5, 26:H3 — the inversion of the shell Fourier matrix, entrywise: with87`W k j = g^{jk}` and `W' l j = −g^{(n−j)l}` (`= −g^{−lj}`), `Σ_{l<n} W k l · W' l j = [k = j]`. The matrix `g^{jk}` on the88full cycle `n = p − 1` is both the longitudinal character table (26:B3) and the additive transform on the shell (26:H3). -/89theorem dft_inverse (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :90    sumRange (fun l => g ^ (l * k) * -(g ^ ((p - 1 - j) * l))) (p - 1) = if k = j then 1 else 0 := by91  have hsum : sumRange (fun l => g ^ (l * k) * -(g ^ ((p - 1 - j) * l))) (p - 1)92      = -(sumRange (fun l => (g ^ (k + (p - 1 - j))) ^ l) (p - 1)) := by93    rw [← sum_neg]94    apply sum_congr95    intro l _96    rw [← mul_neg, ← pow_add, ← pow_mul, Nat.mul_comm l k, ← FRC.Nat.add_mul]97  rw [hsum]98  exact match Nat.decEq k j with99    | .isTrue e => by100        rw [ite_eq_left e]101        have h1 : g ^ (k + (p - 1 - j)) = 1 := (F.pow_shift_eq_one_iff hk hj).2 e102        have : sumRange (fun l => (g ^ (k + (p - 1 - j))) ^ l) (p - 1) = ofNat (p - 1) * 1 := by103          rw [← sum_const]; apply sum_congr; intro l _; rw [h1, one_pow]104        rw [this, F.ofNat_n, mul_one, neg_neg]105    | .isFalse e => by106        rw [ite_eq_right e]107        have h1 : g ^ (k + (p - 1 - j)) ≠ 1 := fun h => e ((F.pow_shift_eq_one_iff hk hj).1 h)108        rw [F.geom_sum_eq_zero _ (by rw [pow_mul_comm, F.pow_n, one_pow]) h1, neg_zero]109110/-- `g^{k + j} = 1` exactly when `(k + j) % n = 0`, i.e. `j` is the reversal `−k` of `k` (`k, j < n`). -/111theorem pow_add_eq_one_iff (F : Frame p κ g) (k j : Nat) : g ^ (k + j) = 1 ↔ (k + j) % (p - 1) = 0 :=112  ⟨F.mod_eq_zero_of_pow_eq_one, F.pow_eq_one_of_mod⟩113114/-- 6:B5 (the shell Fourier matrix squares to the reversal, entrywise): with `W k j = g^{jk}` and115`J k j = [(k + j) % n = 0]`, `Σ_{l<n} W k l · W l j = −J k j` on every shell (`n = p − 1 ≡ −1`). -/116theorem W_sq (F : Frame p κ g) (k j : Nat) :117    sumRange (fun l => g ^ (l * k) * g ^ (j * l)) (p - 1)118      = -(if (k + j) % (p - 1) = 0 then 1 else 0) := by119  have hsum : sumRange (fun l => g ^ (l * k) * g ^ (j * l)) (p - 1)120      = sumRange (fun l => (g ^ (k + j)) ^ l) (p - 1) := by121    apply sum_congr; intro l _122    rw [← pow_add, ← pow_mul, Nat.mul_comm l k, ← FRC.Nat.add_mul]123  rw [hsum]124  exact match Nat.decEq ((k + j) % (p - 1)) 0 with125    | .isTrue e => by126        rw [ite_eq_left e]127        have h1 : g ^ (k + j) = 1 := F.pow_eq_one_of_mod e128        have : sumRange (fun l => (g ^ (k + j)) ^ l) (p - 1) = ofNat (p - 1) * 1 := by129          rw [← sum_const]; apply sum_congr; intro l _; rw [h1, one_pow]130        rw [this, F.ofNat_n, mul_one]131    | .isFalse e => by132        rw [ite_eq_right e, neg_zero]133        exact F.geom_sum_eq_zero _ (by rw [pow_mul_comm, F.pow_n, one_pow]) (fun h => e (F.mod_eq_zero_of_pow_eq_one h))134135/-! ### The reversal, the Fourier matrix `W`, the quarter-turn transform `F = i·W` (6:B5, B7) -/136137/-- The reversal `rev n k = (n − k) % n`: the index `l` with `(k + l) % n = 0`. -/138def rev (n k : Nat) : Nat := (n - k) % n139140theorem rev_lt {n : Nat} (hn : 0 < n) (k : Nat) : rev n k < n := Nat.mod_lt _ hn141142theorem rev_zero (n : Nat) (hn : 0 < n) : rev n 0 = 0 := by143  unfold rev; rw [Nat.sub_zero]; exact FRC.Nat.mod_self n hn144145theorem rev_of_pos {n k : Nat} (hk : k < n) (hk0 : 0 < k) : rev n k = n - k := by146  unfold rev; exact FRC.Nat.mod_eq_of_lt (Nat.sub_lt (Nat.lt_of_lt_of_le hk0 (Nat.le_of_lt hk)) hk0)147148theorem rev_add_mod {n k : Nat} (hk : k < n) : (rev n k + k) % n = 0 := by149  have hn : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le k) hk150  exact match Nat.decEq k 0 with151    | isTrue e => by rw [e, rev_zero n hn]; rfl152    | isFalse e => by153        rw [rev_of_pos hk (Nat.pos_of_ne_zero e), FRC.Nat.sub_add_cancel (Nat.le_of_lt hk)]154        exact FRC.Nat.mod_self n hn155156theorem rev_rev {n k : Nat} (hk : k < n) : rev n (rev n k) = k := by157  have hn : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le k) hk158  exact match Nat.decEq k 0 with159    | isTrue e => by rw [e, rev_zero n hn, rev_zero n hn]160    | isFalse e => by161        have hk0 := Nat.pos_of_ne_zero e162        rw [rev_of_pos hk hk0]163        have hnk : n - k < n := Nat.sub_lt (Nat.lt_of_lt_of_le hk0 (Nat.le_of_lt hk)) hk0164        have hnk0 : 0 < n - k := by165          refine Nat.lt_of_add_lt_add_right (n := k) ?_166          rw [Nat.zero_add, FRC.Nat.sub_add_cancel (Nat.le_of_lt hk)]; exact hk167        rw [rev_of_pos hnk hnk0]168        calc n - (n - k) = (n - k + k) - (n - k) := by rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hk)]169          _ = k := FRC.Nat.add_sub_cancel_left _ _170171/-- `(k + l) % n = 0` exactly when `l` is the reversal of `k` (`k, l < n`). -/172theorem add_mod_eq_zero_iff {n k l : Nat} (hk : k < n) (hl : l < n) : (k + l) % n = 0 ↔ l = rev n k := by173  have hn : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le k) hk174  constructor175  · intro h176    exact match Nat.decEq k 0 with177      | isTrue e => by178          rw [e, Nat.zero_add, FRC.Nat.mod_eq_of_lt hl] at h179          rw [e, rev_zero n hn, h]180      | isFalse e => by181          have hk0 := Nat.pos_of_ne_zero e182          rw [rev_of_pos hk hk0]183          exact match Nat.lt_or_ge l (n - k) with184            | Or.inl hlt => by185                have : k + l < n := by186                  have := Nat.add_lt_add_left hlt k187                  rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt hk)] at this; exact this188                rw [FRC.Nat.mod_eq_of_lt this] at h189                exact absurd h (Nat.ne_of_gt (Nat.lt_of_lt_of_le hk0 (Nat.le_add_right k l)))190            | Or.inr hge => by191                have e1 : k + l = n * 1 + (l - (n - k)) := by192                  rw [Nat.mul_one]193                  calc k + l = k + ((n - k) + (l - (n - k))) := by rw [FRC.Nat.add_sub_of_le hge]194                    _ = (k + (n - k)) + (l - (n - k)) := (Nat.add_assoc _ _ _).symm195                    _ = n + (l - (n - k)) := by rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt hk)]196                rw [e1, FRC.Nat.add_mul_mod_self_left _ _ _ hn,197                  FRC.Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt (Nat.sub_le _ _) hl)] at h198                have := FRC.Nat.add_sub_of_le hge199                rw [h, Nat.add_zero] at this200                exact this.symm201  · intro e; rw [e, Nat.add_comm]; exact rev_add_mod hk202203/-- The shell Fourier matrix, `W k j = g^{jk}` (6:B5's convention). -/204def W (g : Shell p) (k j : Nat) : Shell p := g ^ (j * k)205206/-- The reversal matrix `J k j = [(k + j) % n = 0]`. -/207def J (n k j : Nat) : Shell p := if (k + j) % n = 0 then 1 else 0208209/-- The quarter-turn transform `F = i·W`, `i = −g^κ`. -/210def Fmat (g : Shell p) (κ k j : Nat) : Shell p := quarterTurn g κ * W g k j211212theorem J_eq {n k l : Nat} (hk : k < n) (hl : l < n) :213    (J n k l : Shell p) = (if l = rev n k then (1 : Shell p) else 0) := by214  unfold J215  exact match Nat.decEq l (rev n k) with216    | isTrue e => by rw [ite_eq_left e, ite_eq_left ((add_mod_eq_zero_iff hk hl).2 e)]217    | isFalse e => by rw [ite_eq_right e, ite_eq_right (fun h => e ((add_mod_eq_zero_iff hk hl).1 h))]218219/-- 6:B5 (`W² = −J`, entrywise), in the matrix notation. -/220theorem W_sq' (F : Frame p κ g) (k j : Nat) :221    sumRange (fun l => W g k l * W g l j) (p - 1) = -(J (p - 1) k j) := F.W_sq k j222223/-- 6:B5, 6:B7 (`J² = 1`, entrywise): the reversal is an involution, so `F⁴ = J² = 1`. -/224theorem J_sq (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :225    sumRange (fun l => (J (p - 1) k l : Shell p) * J (p - 1) l j) (p - 1) = (if k = j then (1 : Shell p) else 0) := by226  have hn := F.n_pos227  have hr : rev (p - 1) k < p - 1 := rev_lt hn k228  rw [sum_eq_single hr (fun l hl hne => by rw [J_eq hk hl, ite_eq_right hne, zero_mul])]229  rw [J_eq hk hr, ite_eq_left rfl, one_mul, J_eq hr hj, rev_rev hk]230  exact match Nat.decEq k j with231    | isTrue e => by rw [ite_eq_left e, ite_eq_left e.symm]232    | isFalse e => by rw [ite_eq_right e, ite_eq_right (fun h => e h.symm)]233234/-- 6:B5, 6:B7 (`F² = J`, entrywise): the quarter-turn transform squares to the reversal. -/235theorem F_sq (F : Frame p κ g) (k j : Nat) :236    sumRange (fun l => Fmat g κ k l * Fmat g κ l j) (p - 1) = J (p - 1) k j := by237  have e : ∀ l, Fmat g κ k l * Fmat g κ l j = (quarterTurn g κ * quarterTurn g κ) * (W g k l * W g l j) := by238    intro l; unfold Fmat239    rw [mul_assoc, mul_left_comm (W g k l), ← mul_assoc]240  rw [sum_congr _ (fun l _ => e l), sum_mul_left, F.W_sq' k j, F.quarter_turn_sq, ← neg_mul, one_mul, neg_neg]241242/-- 6:B7 (`W J = J W`, entrywise). -/243theorem W_J_comm (F : Frame p κ g) {k j : Nat} (hk : k < p - 1) (hj : j < p - 1) :244    sumRange (fun l => W g k l * J (p - 1) l j) (p - 1) = sumRange (fun l => J (p - 1) k l * W g l j) (p - 1) := by245  have hn := F.n_pos246  have hrj : rev (p - 1) j < p - 1 := rev_lt hn j247  have hrk : rev (p - 1) k < p - 1 := rev_lt hn k248  rw [sum_eq_single hrj (fun l hl hne => by249        rw [J_eq hl hj, ite_eq_right (fun e => hne (by rw [e, rev_rev hl])), mul_zero])]250  rw [sum_eq_single hrk (fun l hl hne => by rw [J_eq hk hl, ite_eq_right hne, zero_mul])]251  rw [J_eq hrj hj, ite_eq_left (rev_rev hj).symm, mul_one, J_eq hk hrk, ite_eq_left rfl, one_mul]252  unfold W253  -- both are the inverse of g^{jk}254  apply inv_unique (y := g ^ (j * k))255  · rw [← pow_add, ← FRC.Nat.add_mul, F.pow_mod, ← FRC.Nat.mod_mul_mod _ _ _ hn, rev_add_mod hj, Nat.zero_mul,256      FRC.Nat.zero_mod, pow_zero]257  · rw [← pow_add, ← Nat.left_distrib, F.pow_mod, ← FRC.Nat.mul_mod_mod _ _ _ hn, rev_add_mod hk, Nat.mul_zero,258      FRC.Nat.zero_mod, pow_zero]259260/-- The sum over the nonzero residues equals the sum over the powers of the drive: `x = g^m` reindexes. -/261theorem sum_units_eq_sum_pow (F : Frame p κ g) (f : Shell p → Shell p) :262    sumRange (fun l => f (ofNat (l + 1))) (p - 1) = sumRange (fun m => f (g ^ m)) (p - 1) := by263  have hn : p = (p - 1) + 1 := (FRC.Nat.sub_add_cancel Pos.pos).symm264  have hpos : ∀ m, 1 ≤ (g ^ m).val := fun m =>265    Nat.pos_of_ne_zero (fun h0 => F.pow_ne_zero m (ext (by rw [h0, val_zero])))266  have hlt : ∀ m, m < p - 1 → (g ^ m).val - 1 < p - 1 := fun m _ => by267    have h1 : (g ^ m).val - 1 + 1 = (g ^ m).val := FRC.Nat.sub_add_cancel (hpos m)268    have h2 : (g ^ m).val < (p - 1) + 1 := hn ▸ (g ^ m).lt269    rw [← h1] at h2270    exact Nat.lt_of_succ_lt_succ h2271  have hinj : ∀ i j, i < p - 1 → j < p - 1 → (g ^ i).val - 1 = (g ^ j).val - 1 → i = j := fun i j hi hj h => by272    apply F.pow_inj hi hj273    apply ext274    rw [← FRC.Nat.sub_add_cancel (hpos i), ← FRC.Nat.sub_add_cancel (hpos j), h]275  have := sum_perm (fun l => f (ofNat (l + 1))) (fun m => (g ^ m).val - 1) (p - 1) hlt hinj276  rw [← this]277  apply sum_congr278  intro m _279  show f (ofNat ((g ^ m).val - 1 + 1)) = f (g ^ m)280  rw [FRC.Nat.sub_add_cancel (hpos m), ofNat_val]281282end Frame283284/-- 00:C1, 20:B10 on `𝔽₁₃`: the frame `(τ; 0, 1, 2)` of capacity `3` — `2` is primitive (decided). Moved here from285`Instances.lean` under its name (task LM36), so that the horizon theme takes it without the orbits. -/286theorem frame13 : Frame 13 3 (2 : Shell 13) := ⟨rfl, Nat.zero_lt_succ 2, by decide⟩287288end Shell289end FRC290