Sum.lean — FrcCore

1import FrcCore.Series2import FrcCore.Transform3import FrcCore.Orbit45/-!6# FrcCore.Sum — finite sums on the shell, the geometric sum, the Fourier inversion78Sums over `l < n` are defined by structural recursion (`sumRange f (n+1) = sumRange f n + f n`): no9`Finset`, no quotient, no function extensionality — a congruence lemma (`sum_congr`) replaces `funext`.10The geometric sum gives the principal-root identity (2:F1, Prop. 6.1 of 2-geometry) and the entrywise11inversion of the shell Fourier matrix `W k j = g^{jk}`: `Σ_l W k l · (−g^{−lj}) = [k = j]` (2:F3,12Prop. 6.3; 6:B5 in matrix form). No axioms.1314Since the ledger migration (task LM17) it also holds 20-rh's sums: peeling the first term, and the sum over the15nonzero residues reindexed by the drive. Since task LM22 the sums that need no frame (`sumRange` and its lemmas, the16geometric sum, the sums over lists and `sum_perm`) are in `Series.lean`, under their names; this module keeps the17frame's: the principal root, the Fourier inversion, the reversal and the eigenspaces. Since task LM25 the transform18(the principal root, the inversion, `rev`, `W`, `J`, `F` and their products) is in `Transform.lean`, names unchanged,19and since task LM36 the reindexing by the drive (`sum_units_eq_sum_pow`) is there too.20-/2122namespace FRC23namespace Shell2425variable {p : Nat} [Pos p]2627namespace Frame28variable {κ : Nat} {g : Shell p}2930/-- The shell Fourier transform of `v` at `k`: `Σ_{j<n} v_j g^{jk}`. -/31def dft (g : Shell p) (n : Nat) (v : Nat → Shell p) (k : Nat) : Shell p := sumRange (fun j => v j * g ^ (j * k)) n3233/-- The polynomial `P_v(x) = Σ_{j<n} v_j x^j`. -/34def polyEval (n : Nat) (v : Nat → Shell p) (x : Shell p) : Shell p := sumRange (fun j => v j * x ^ j) n3536/-- 2:F4 (Prop. 6.5) — the polynomial reading: `F_g(v)_k = P_v(g^k)`. -/37theorem dft_eq_polyEval (g : Shell p) (n : Nat) (v : Nat → Shell p) (k : Nat) :38    dft g n v k = polyEval n v (g ^ k) := by39  unfold dft polyEval40  apply sum_congr; intro j _41  rw [Nat.mul_comm j k, pow_mul]4243/-- The reindexing `j ↦ u·j mod n` is injective on `[0, n)` when `u` is invertible mod `n`. -/44theorem mul_mod_inj (F : Frame p κ g) {u : Nat} (hu : Coprime u (p - 1)) {i j : Nat} (hi : i < p - 1) (hj : j < p - 1)45    (h : (u * i) % (p - 1) = (u * j) % (p - 1)) : i = j := by46  have hn := F.n_pos47  match hu with48  | ⟨a, _, ha⟩ =>49    have key : ∀ i, i < p - 1 → (a * (u * i)) % (p - 1) = i := by50      intro i hi51      match FRC.Nat.mod_spec (p - 1) hn (a * u) with52      | ⟨q, hq⟩ =>53        rw [ha] at hq54        rw [← FRC.Nat.mul_assoc, hq, FRC.Nat.add_mul, Nat.one_mul, FRC.Nat.mul_assoc,55          FRC.Nat.add_mul_mod_self_left _ _ _ hn, FRC.Nat.mod_eq_of_lt hi]56    rw [← key i hi, ← key j hj, ← FRC.Nat.mul_mod_mod _ _ _ hn, h, FRC.Nat.mul_mod_mod _ _ _ hn]5758/-- 2:F5 (Prop. 6.7) — covariance under generator change: for `g' = g^u` (`u` invertible mod `n`) and59`v'_j = v_{u·j mod n}`, `F_{g'}(v')_k = F_g(v)_k`. -/60theorem dft_covariance (F : Frame p κ g) {u : Nat} (hu : Coprime u (p - 1)) (v : Nat → Shell p) (k : Nat) :61    dft (g ^ u) (p - 1) (fun j => v ((u * j) % (p - 1))) k = dft g (p - 1) v k := by62  have hn := F.n_pos63  unfold dft64  have e : ∀ j, v ((u * j) % (p - 1)) * (g ^ u) ^ (j * k) = v ((u * j) % (p - 1)) * g ^ (((u * j) % (p - 1)) * k) := by65    intro j66    rw [← pow_mul, F.pow_mod (u * (j * k)), F.pow_mod (((u * j) % (p - 1)) * k), FRC.Nat.mod_mul_mod _ _ _ hn,67      ← FRC.Nat.mul_assoc]68  rw [sum_congr _ (fun j _ => e j)]69  exact sum_perm (fun l => v l * g ^ (l * k)) (fun j => (u * j) % (p - 1)) (p - 1)70    (fun j _ => Nat.mod_lt _ hn) (fun i j hi hj h => F.mul_mod_inj hu hi hj h)7172/-! ### 6:B7 — the eigenspaces of the reversal: `V = V⁺ ⊕ V⁻`, `dim V⁺ = 2κ + 1`, `dim V⁻ = 2κ − 1` -/7374/-- `v` is symmetric under the reversal: `v (rev k) = v k` for `k < n`. -/75def Symm (n : Nat) (v : Nat → Shell p) : Prop := ∀ k, k < n → v (rev n k) = v k7677/-- `v` is antisymmetric under the reversal: `v (rev k) = −v k` for `k < n`. -/78def Antisymm (n : Nat) (v : Nat → Shell p) : Prop := ∀ k, k < n → v (rev n k) = -(v k)7980theorem rev_eq_sub {n k : Nat} (hk : k < n) (hk0 : 0 < k) : rev n k = n - k := rev_of_pos hk hk08182/-- 6:B7 — a symmetric vector is determined by its `2κ + 1` coordinates `v 0, …, v (2κ)`. -/83theorem symm_determined (F : Frame p κ g) {v w : Nat → Shell p} (hv : Symm (p - 1) v) (hw : Symm (p - 1) w)84    (h : ∀ k, k ≤ 2 * κ → v k = w k) : ∀ k, k < p - 1 → v k = w k := by85  intro k hk86  exact match Nat.lt_or_ge k (2 * κ + 1) with87    | Or.inl hlt => h k (Nat.le_of_lt_succ hlt)88    | Or.inr hge =>89      -- k > 2κ: rev k = n − k ≤ 2κ − 190      have hk0 : 0 < k := Nat.lt_of_lt_of_le (Nat.zero_lt_succ _) hge91      have hr : rev (p - 1) k ≤ 2 * κ := by92        rw [rev_eq_sub hk hk0]93        apply FRC.Nat.sub_le_of_le_add94        rw [← F.four_kappa]95        exact Nat.add_le_add_left (Nat.le_of_lt hge) _96      calc v k = v (rev (p - 1) k) := (hv k hk).symm97        _ = w (rev (p - 1) k) := h _ hr98        _ = w k := hw k hk99100/-- 6:B7 — every assignment of the `2κ + 1` coordinates extends to a symmetric vector. -/101theorem symm_extend (F : Frame p κ g) (c : Nat → Shell p) :102    ∃ v : Nat → Shell p, Symm (p - 1) v ∧ ∀ k, k ≤ 2 * κ → v k = c k := by103  refine ⟨fun k => if k ≤ 2 * κ then c k else c (rev (p - 1) k), ?_, fun k hk => by104    show (if k ≤ 2 * κ then c k else c (rev (p - 1) k)) = c k105    rw [ite_eq_left hk]⟩106  intro k hk107  show (if rev (p - 1) k ≤ 2 * κ then c (rev (p - 1) k) else c (rev (p - 1) (rev (p - 1) k)))108      = (if k ≤ 2 * κ then c k else c (rev (p - 1) k))109  rw [rev_rev hk]110  exact match Nat.decLe k (2 * κ), Nat.decLe (rev (p - 1) k) (2 * κ) with111    | isTrue h1, isTrue h2 => by112        rw [ite_eq_left h1, ite_eq_left h2]113        -- both k and n − k are ≤ 2κ: k = 0 (rev 0 = 0) or k = 2κ (rev = 2κ)114        exact match Nat.decEq k 0 with115          | isTrue e => by rw [e, rev_zero _ F.n_pos]116          | isFalse e => by117              have hk0 := Nat.pos_of_ne_zero e118              rw [rev_eq_sub hk hk0] at h2 ⊢119              -- n − k ≤ 2κ and k ≤ 2κ force k = 2κ120              have h3 : p - 1 ≤ 2 * κ + k := FRC.Nat.le_add_of_sub_le (Nat.le_of_lt hk) h2121              rw [← F.four_kappa] at h3122              have hk2 : k = 2 * κ := Nat.le_antisymm h1 (FRC.Nat.le_of_add_le_add_left h3)123              rw [hk2, ← F.four_kappa, FRC.Nat.add_sub_cancel]124    | isTrue h1, isFalse h2 => by rw [ite_eq_left h1, ite_eq_right h2]125    | isFalse h1, isTrue h2 => by rw [ite_eq_right h1, ite_eq_left h2]126    | isFalse h1, isFalse h2 => by127        rw [ite_eq_right h1, ite_eq_right h2]128        -- impossible: k > 2κ and n − k > 2κ would give n > 4κ129        exact absurd (by130          have hk0 : 0 < k := Nat.lt_of_lt_of_le (Nat.zero_lt_succ _) (Nat.lt_of_not_le h1)131          rw [rev_eq_sub hk hk0] at h2132          have a1 := Nat.lt_of_not_le h1133          have a2 := Nat.lt_of_not_le h2134          have := Nat.add_lt_add a1 a2135          rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt hk), F.four_kappa] at this136          exact this) (Nat.lt_irrefl _)137138/-- 6:B7 — an antisymmetric vector vanishes at the two fixed points of the reversal, `0` and `2κ`. -/139theorem antisymm_fixed (F : Frame p κ g) {v : Nat → Shell p} (hv : Antisymm (p - 1) v) :140    v 0 = 0 ∧ v (2 * κ) = 0 := by141  have hn := F.n_pos142  have h0 : v 0 = -(v 0) := by rw [← hv 0 hn, rev_zero _ hn]143  have h2 : v (2 * κ) = -(v (2 * κ)) := by144    rw [← hv (2 * κ) F.two_kappa_lt, rev_eq_sub F.two_kappa_lt F.two_kappa_pos, ← F.four_kappa, FRC.Nat.add_sub_cancel]145  exact ⟨F.eq_zero_of_eq_neg h0, F.eq_zero_of_eq_neg h2⟩146147/-- 6:B7 — an antisymmetric vector is determined by its `2κ − 1` coordinates `v 1, …, v (2κ − 1)`. -/148theorem antisymm_determined (F : Frame p κ g) {v w : Nat → Shell p} (hv : Antisymm (p - 1) v)149    (hw : Antisymm (p - 1) w) (h : ∀ k, 0 < k → k < 2 * κ → v k = w k) : ∀ k, k < p - 1 → v k = w k := by150  intro k hk151  exact match Nat.decEq k 0 with152    | isTrue e => by rw [e, (F.antisymm_fixed hv).1, (F.antisymm_fixed hw).1]153    | isFalse e0 => match Nat.decEq k (2 * κ) with154      | isTrue e => by rw [e, (F.antisymm_fixed hv).2, (F.antisymm_fixed hw).2]155      | isFalse e2 => match Nat.lt_or_ge k (2 * κ) with156        | Or.inl hlt => h k (Nat.pos_of_ne_zero e0) hlt157        | Or.inr hge =>158          have hgt : 2 * κ < k := Nat.lt_of_le_of_ne hge (fun e => e2 e.symm)159          have hk0 : 0 < k := Nat.lt_of_lt_of_le F.two_kappa_pos hge160          have hr1 : 0 < rev (p - 1) k := by161            rw [rev_eq_sub hk hk0]162            refine Nat.lt_of_add_lt_add_right (n := k) ?_163            rw [Nat.zero_add, FRC.Nat.sub_add_cancel (Nat.le_of_lt hk)]; exact hk164          have hr2 : rev (p - 1) k < 2 * κ := by165            rw [rev_eq_sub hk hk0]166            refine Nat.lt_of_add_lt_add_right (n := k) ?_167            rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hk), ← F.four_kappa]168            exact Nat.add_lt_add_left hgt _169          calc v k = -(-(v k)) := (neg_neg _).symm170            _ = -(v (rev (p - 1) k)) := by rw [hv k hk]171            _ = -(w (rev (p - 1) k)) := by rw [h _ hr1 hr2]172            _ = -(-(w k)) := by rw [hw k hk]173            _ = w k := neg_neg _174175/-- 6:B7 — every assignment of the `2κ − 1` inner coordinates extends to an antisymmetric vector. -/176theorem antisymm_extend (F : Frame p κ g) (c : Nat → Shell p) :177    ∃ v : Nat → Shell p, Antisymm (p - 1) v ∧ ∀ k, 0 < k → k < 2 * κ → v k = c k := by178  refine ⟨fun k => if k = 0 then 0 else if k = 2 * κ then 0 else if k < 2 * κ then c k else -(c (rev (p - 1) k)),179    ?_, fun k hk0 hk2 => by180      show (if k = 0 then 0 else if k = 2 * κ then 0 else if k < 2 * κ then c k else -(c (rev (p - 1) k))) = c k181      rw [ite_eq_right (Nat.ne_of_gt hk0), ite_eq_right (Nat.ne_of_lt hk2), ite_eq_left hk2]⟩182  intro k hk183  have hn := F.n_pos184  show (if rev (p - 1) k = 0 then 0 else if rev (p - 1) k = 2 * κ then 0 else if rev (p - 1) k < 2 * κ then c (rev (p - 1) k) else -(c (rev (p - 1) (rev (p - 1) k))))185      = -(if k = 0 then 0 else if k = 2 * κ then 0 else if k < 2 * κ then c k else -(c (rev (p - 1) k)))186  match Nat.decEq k 0 with187  | isTrue e => rw [e, rev_zero _ hn, ite_eq_left rfl, ite_eq_left rfl, neg_zero]188  | isFalse e0 =>189    have hk0 := Nat.pos_of_ne_zero e0190    have hrk : rev (p - 1) k = p - 1 - k := rev_eq_sub hk hk0191    have hr0 : rev (p - 1) k ≠ 0 := fun h => by192      rw [hrk] at h193      have := FRC.Nat.sub_add_cancel (Nat.le_of_lt hk)194      rw [h, Nat.zero_add] at this195      exact Nat.lt_irrefl _ (this ▸ hk)196    match Nat.decEq k (2 * κ) with197    | isTrue e =>198      have : rev (p - 1) k = 2 * κ := by rw [hrk, e, ← F.four_kappa, FRC.Nat.add_sub_cancel]199      rw [ite_eq_right hr0, ite_eq_left this, ite_eq_right e0, ite_eq_left e, neg_zero]200    | isFalse e2 =>201      have hr2 : rev (p - 1) k ≠ 2 * κ := fun h => e2 (by202        have := rev_rev hk203        rw [h] at this204        rw [← this, rev_eq_sub F.two_kappa_lt F.two_kappa_pos, ← F.four_kappa, FRC.Nat.add_sub_cancel])205      rw [ite_eq_right hr0, ite_eq_right hr2, ite_eq_right e0, ite_eq_right e2]206      match Nat.lt_or_ge k (2 * κ) with207      | Or.inl hlt =>208        have hge : ¬ rev (p - 1) k < 2 * κ := fun h => by209          rw [hrk] at h210          have := Nat.add_lt_add h hlt211          rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hk), F.four_kappa] at this212          exact Nat.lt_irrefl _ this213        rw [ite_eq_right hge, ite_eq_left hlt, rev_rev hk]214      | Or.inr hge =>215        have hlt' : ¬ k < 2 * κ := Nat.not_lt_of_le hge216        have hgt : 2 * κ < k := Nat.lt_of_le_of_ne hge (fun e => e2 e.symm)217        have hr : rev (p - 1) k < 2 * κ := by218          rw [hrk]219          refine Nat.lt_of_add_lt_add_right (n := k) ?_220          rw [FRC.Nat.sub_add_cancel (Nat.le_of_lt hk), ← F.four_kappa]221          exact Nat.add_lt_add_left hgt _222        rw [ite_eq_left hr, ite_eq_right hlt', neg_neg]223224/-- 6:B7 — the decomposition `V = V⁺ ⊕ V⁻`: with `h = 2⁻¹`, `v = v⁺ + v⁻` where `v⁺ k = h(v k + v (rev k))`225is symmetric and `v⁻ k = h(v k − v (rev k))` antisymmetric; the decomposition is unique. -/226theorem symm_antisymm_decomp (F : Frame p κ g) (v : Nat → Shell p) :227    ∃ vp vm : Nat → Shell p, Symm (p - 1) vp ∧ Antisymm (p - 1) vm ∧ ∀ k, k < p - 1 → v k = vp k + vm k := by228  match F.exists_inv F.two_ne_zero with229  | ⟨h, hh⟩ =>230    refine ⟨fun k => h * (v k + v (rev (p - 1) k)), fun k => h * (v k + -(v (rev (p - 1) k))), ?_, ?_, ?_⟩231    · intro k hk; show h * (v (rev (p - 1) k) + v (rev (p - 1) (rev (p - 1) k))) = h * (v k + v (rev (p - 1) k))232      rw [rev_rev hk, add_comm]233    · intro k hk; show h * (v (rev (p - 1) k) + -(v (rev (p - 1) (rev (p - 1) k)))) = -(h * (v k + -(v (rev (p - 1) k))))234      rw [rev_rev hk, mul_neg, neg_add_rev, neg_neg, add_comm]235    · intro k _236      show v k = h * (v k + v (rev (p - 1) k)) + h * (v k + -(v (rev (p - 1) k)))237      rw [← left_distrib, add_add_add_comm, add_neg, add_zero, ← two_mul', ← mul_assoc, mul_comm h, hh, one_mul]238239/-- 6:B7 — the decomposition is unique: a vector that is both symmetric and antisymmetric is zero, so the240symmetric and antisymmetric parts of `v` are determined. -/241theorem symm_antisymm_unique (F : Frame p κ g) {a b : Nat → Shell p} (ha : Symm (p - 1) a) (hb : Antisymm (p - 1) b)242    (h : ∀ k, k < p - 1 → a k + b k = 0) : ∀ k, k < p - 1 → a k = 0 ∧ b k = 0 := by243  intro k hk244  have h1 := h k hk245  have h2 := h (rev (p - 1) k) (rev_lt F.n_pos k)246  rw [ha k hk, hb k hk] at h2247  -- a k + b k = 0 and a k − b k = 0 give 2 a k = 0248  have ha0 : a k = 0 := F.no_south_pole _ (by249    rw [two_mul']250    calc a k + a k = (a k + b k) + (a k + -(b k)) := by251          rw [add_add_add_comm, add_neg, add_zero]252      _ = 0 := by rw [h1, h2, add_zero])253  refine ⟨ha0, ?_⟩254  rw [ha0, zero_add] at h1; exact h1255256end Frame257258end Shell259end FRC260