Theme/Spectra.lean — FrcCore

1import FrcCore.Theme.Heisenberg2import FrcCore.Theme.Dichotomy34/-!5# FrcCore.Theme.Spectra — the spectra of the shift and of the family: the obstruction (the fourier theme)67The seventh file of the fourier theme (6-fourier's blueprint of 8 October 2026, task T08). Vectors on the cycle are8`Nat → Shell p` and a matrix acts by `(A v)_k = Σ_{l<n} A_{kl} v_l`. The shift `σ` has every nonzero residue as an9eigenvalue, with the geometric vector `(y^j)_j` for `b = y⁻¹` (Fermat: `y^n = 1`); an eigenvalue of `F^{[s]}` is one10of the four `(z^s)^ℓ`, since `Π_m F^{[s]} = (z^s)^m Π_m` and `v = Σ_m Π_m v` (6:E9). So no invertible `T` has11`T σ T⁻¹ = F^{[s]}` for `κ ≥ 2`: the `4κ` eigenvalues of `σ` would be eigenvalues of `F^{[s]}`, at most four, and12`no_mirror` refuses the injection of `[0, 4κ)` into `[0, 4)` (6:E5). No axioms.13-/1415namespace FRC16namespace Shell17namespace Frame1819variable {p : Nat} [Pos p]2021/-! ## Vectors and matrices on the cycle -/2223/-- `(A v)_k = Σ_{l<n} A_{kl} v_l`. -/24def act (A : Nat → Nat → Shell p) (v : Nat → Shell p) (n k : Nat) : Shell p := sumRange (fun l => A k l * v l) n2526/-- `(A B)_{kj} = Σ_{l<n} A_{kl} B_{lj}`. -/27def mmul (A B : Nat → Nat → Shell p) (n k j : Nat) : Shell p := sumRange (fun l => A k l * B l j) n2829/-- `v` is an eigenvector of `A` for the eigenvalue `lam`: nonzero on the cycle, with `A v = lam v` there. -/30def IsEigen (A : Nat → Nat → Shell p) (n : Nat) (lam : Shell p) (v : Nat → Shell p) : Prop :=31  (∃ k, k < n ∧ v k ≠ 0) ∧ ∀ k, k < n → act A v n k = lam * v k3233/-- `(A B) v = A (B v)`. -/34theorem act_mmul (A B : Nat → Nat → Shell p) (v : Nat → Shell p) (n k : Nat) :35    act (mmul A B n) v n k = act A (act B v n) n k := by36  show sumRange (fun j => sumRange (fun l => A k l * B l j) n * v j) n =37    sumRange (fun l => A k l * sumRange (fun j => B l j * v j) n) n38  rw [sum_congr _ (fun j _ => (sum_mul_right _ _ _).symm), sum_swap (fun j l => A k l * B l j * v j) n n]39  exact sum_congr _ (fun l _ => by40    rw [← sum_mul_left]41    exact sum_congr _ (fun j _ => mul_assoc _ _ _))4243theorem act_smul (A : Nat → Nat → Shell p) (v : Nat → Shell p) (c : Shell p) (n k : Nat) :44    act A (fun l => c * v l) n k = c * act A v n k := by45  show sumRange (fun l => A k l * (c * v l)) n = c * sumRange (fun l => A k l * v l) n46  rw [sum_congr _ (fun l _ => mul_left_comm _ _ _), sum_mul_left]4748theorem act_idm (v : Nat → Shell p) {n k : Nat} (hk : k < n) : act idm v n k = v k := by49  show sumRange (fun l => idm k l * v l) n = v k50  rw [sum_eq_single hk (fun l _ hne => by rw [idm_ne (fun e => hne e.symm), zero_mul]), idm_self, one_mul]5152variable {κ : Nat} {g : Shell p}5354/-! ## The shift's spectrum (6:E9) -/5556/-- `(σ v)_k = v_{k−1}`, the index `k − 1` read as `(k + (n − 1)) mod n`. -/57theorem shift_act (F : Frame p κ g) (v : Nat → Shell p) {k : Nat} (hk : k < p - 1) :58    act (shift p) v (p - 1) k = v ((k + (p - 1 - 1)) % (p - 1)) := by59  show sumRange (fun l => (if (l + 1) % (p - 1) = k then (1 : Shell p) else 0) * v l) (p - 1) = _60  rw [sum_eq_single (FRC.Nat.mod_lt' _ F.n_pos) (fun l hl hne => by61    rw [ite_eq_right (fun e => hne (by rw [← pred_succ_mod F hl, e])), zero_mul])]62  rw [ite_eq_left (succ_pred_mod F hk), one_mul]6364/-- `y^l = y^{l mod n}` for an `n`-th root of unity. -/65theorem pow_mod_of_root {y : Shell p} {n : Nat} (hn : 0 < n) (hy : y ^ n = 1) (l : Nat) : y ^ l = y ^ (l % n) := by66  obtain ⟨c, hc⟩ := FRC.Nat.mod_spec n hn l67  rw [congrArg (fun e => y ^ e) hc, pow_add, pow_mul, hy, one_pow, one_mul]6869/-- Fermat on the cycle: every unit has `y^{p−1} = 1`. -/70theorem unit_pow_n (F : Frame p κ g) {y : Shell p} (hy : y ≠ 0) : y ^ (p - 1) = 1 := by71  obtain ⟨m, _, e⟩ := F.eq_pow_of_ne_zero hy72  rw [← e, pow_mul_comm, F.pow_n, one_pow]7374/-- 6:E9, every nonzero residue `b` is an eigenvalue of the shift, with the geometric eigenvector `(y^j)_j = (b^{−j})_j`,75`b y = 1`: `(σ v)_k = y^{k−1} = b y^k`. -/76theorem shift_eigen (F : Frame p κ g) {b : Shell p} (hb : b ≠ 0) :77    ∃ y : Shell p, b * y = 1 ∧ IsEigen (shift p) (p - 1) b (fun j => y ^ j) := by78  obtain ⟨y, hy⟩ := F.exists_inv hb79  have hy0 : y ≠ 0 := fun e => F.one_ne_zero (by rw [← hy, e, mul_zero])80  have hyn := unit_pow_n F hy081  refine ⟨y, hy, ⟨0, F.n_pos, by show y ^ 0 ≠ 0; rw [pow_zero]; exact F.one_ne_zero⟩, fun k hk => ?_⟩82  rw [shift_act F _ hk]83  show y ^ ((k + (p - 1 - 1)) % (p - 1)) = b * y ^ k84  rw [← pow_mod_of_root F.n_pos hyn, pow_add, mul_comm]85  congr 186  apply inv_unique (y := y)87  · rw [← pow_succ, FRC.Nat.sub_add_cancel F.n_pos, hyn]88  · exact hy8990/-- Every nonzero `b` has the inverse `y` that `shift_eigen` names: the eigenvector is `(y^j)_j`. -/91theorem shift_eigen_exists (F : Frame p κ g) {b : Shell p} (hb : b ≠ 0) :92    ∃ v : Nat → Shell p, IsEigen (shift p) (p - 1) b v :=93  match shift_eigen F hb with94  | ⟨_, _, h⟩ => ⟨_, h⟩9596/-! ## The family's spectrum (6:E9) -/9798/-- The selection of the `m`-th term with `[m = ℓ]` factors, `m < 4`. -/99theorem four_select' (c : Nat → Shell p) (Q : Shell p) : ∀ {m : Nat}, m < 4 →100    c 0 * (if m = 0 then Q else 0) + c 1 * (if m = 1 then Q else 0) + c 2 * (if m = 2 then Q else 0) +101      c 3 * (if m = 3 then Q else 0) = c m * Q102  | 0, _ => by103    rw [ite_eq_left rfl, ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_right (by decide), mul_zero, mul_zero,104      mul_zero, add_zero, add_zero, add_zero]105  | 1, _ => by106    rw [ite_eq_right (by decide), ite_eq_left rfl, ite_eq_right (by decide), ite_eq_right (by decide), mul_zero, mul_zero,107      mul_zero, zero_add, add_zero, add_zero]108  | 2, _ => by109    rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl, ite_eq_right (by decide), mul_zero, mul_zero,110      mul_zero, zero_add, zero_add, add_zero]111  | 3, _ => by112    rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl, mul_zero, mul_zero,113      mul_zero, zero_add, zero_add, zero_add]114  | n + 4, h => absurd (Nat.lt_of_lt_of_le h (Nat.le_add_left 4 n)) (Nat.lt_irrefl _)115116theorem proj_frft_pt (z : Shell p) (s m k j l : Nat) :117    proj g κ m k l * frft g κ z s l j =118      (z ^ s) ^ 0 * (proj g κ m k l * proj g κ 0 l j) + (z ^ s) ^ 1 * (proj g κ m k l * proj g κ 1 l j) +119      (z ^ s) ^ 2 * (proj g κ m k l * proj g κ 2 l j) + (z ^ s) ^ 3 * (proj g κ m k l * proj g κ 3 l j) :=120  mul_lift_id _ _ _ _ _ _ _ _ _121122/-- `Π_m F^{[s]} = (z^s)^m Π_m`, the projector on the left. -/123theorem proj_frft (F : Frame p κ g) (z : Shell p) (s : Nat) {m : Nat} (hm : m < 4) {k j : Nat} (hk : k < p - 1)124    (hj : j < p - 1) :125    sumRange (fun l => proj g κ m k l * frft g κ z s l j) (p - 1) = (z ^ s) ^ m * proj g κ m k j := by126  rw [sum_congr _ (fun l _ => proj_frft_pt z s m k j l), sum_add, sum_add, sum_add, sum_mul_left, sum_mul_left, sum_mul_left, sum_mul_left,127    proj_mul F hm (Nat.zero_lt_succ 3) hk hj, proj_mul F hm (by decide : (1 : Nat) < 4) hk hj,128    proj_mul F hm (by decide : (2 : Nat) < 4) hk hj, proj_mul F hm (by decide : (3 : Nat) < 4) hk hj]129  exact four_select' (fun ℓ => (z ^ s) ^ ℓ) (proj g κ m k j) hm130131/-- `v = Π₀ v + Π₁ v + Π₂ v + Π₃ v` on the cycle. -/132theorem act_sum_proj (F : Frame p κ g) (v : Nat → Shell p) {k : Nat} (hk : k < p - 1) :133    act (proj g κ 0) v (p - 1) k + act (proj g κ 1) v (p - 1) k + act (proj g κ 2) v (p - 1) k +134      act (proj g κ 3) v (p - 1) k = v k := by135  show sumRange (fun l => proj g κ 0 k l * v l) (p - 1) + sumRange (fun l => proj g κ 1 k l * v l) (p - 1) +136    sumRange (fun l => proj g κ 2 k l * v l) (p - 1) + sumRange (fun l => proj g κ 3 k l * v l) (p - 1) = v k137  rw [← sum_add, ← sum_add, ← sum_add, ← act_idm v hk]138  exact sum_congr _ (fun l _ => by139    show proj g κ 0 k l * v l + proj g κ 1 k l * v l + proj g κ 2 k l * v l + proj g κ 3 k l * v l = idm k l * v l140    rw [← right_distrib, ← right_distrib, ← right_distrib, sum_proj F k l])141142/-- A sum of four that is nonzero has a nonzero term. -/143theorem four_ne_zero {a : Nat → Shell p} (h : a 0 + a 1 + a 2 + a 3 ≠ 0) : ∃ m, m < 4 ∧ a m ≠ 0 :=144  match Decidable.em (a 0 = 0), Decidable.em (a 1 = 0), Decidable.em (a 2 = 0), Decidable.em (a 3 = 0) with145  | Or.inr h0, _, _, _ => ⟨0, by decide, h0⟩146  | _, Or.inr h1, _, _ => ⟨1, by decide, h1⟩147  | _, _, Or.inr h2, _ => ⟨2, by decide, h2⟩148  | _, _, _, Or.inr h3 => ⟨3, by decide, h3⟩149  | Or.inl h0, Or.inl h1, Or.inl h2, Or.inl h3 => absurd (by rw [h0, h1, h2, h3, add_zero, add_zero, add_zero]) h150151/-- 6:E9, an eigenvalue of `F^{[s]}` is one of the four `(z^s)^ℓ`: on an eigenvector `v`, `Π_m F^{[s]} v` reads both152`lam Π_m v` and `(z^s)^m Π_m v`, and some `Π_m v` is nonzero since `v = Σ_m Π_m v`. -/153theorem frft_eigen (F : Frame p κ g) (z : Shell p) (s : Nat) {lam : Shell p} {v : Nat → Shell p}154    (h : IsEigen (frft g κ z s) (p - 1) lam v) : ∃ ℓ, ℓ < 4 ∧ lam = (z ^ s) ^ ℓ := by155  obtain ⟨⟨k, hk, hv⟩, hact⟩ := h156  have key : ∀ m, m < 4 → ∀ k, k < p - 1 → lam * act (proj g κ m) v (p - 1) k = (z ^ s) ^ m * act (proj g κ m) v (p - 1) k :=157    fun m hm k hk => by158      have e1 : act (proj g κ m) (act (frft g κ z s) v (p - 1)) (p - 1) k = lam * act (proj g κ m) v (p - 1) k := by159        rw [← act_smul]160        exact sum_congr _ (fun l hl => by rw [hact l hl])161      have e2 : act (proj g κ m) (act (frft g κ z s) v (p - 1)) (p - 1) k = (z ^ s) ^ m * act (proj g κ m) v (p - 1) k := by162        rw [← act_mmul]163        show sumRange (fun l => mmul (proj g κ m) (frft g κ z s) (p - 1) k l * v l) (p - 1) =164          (z ^ s) ^ m * sumRange (fun l => proj g κ m k l * v l) (p - 1)165        rw [← sum_mul_left]166        exact sum_congr _ (fun l hl => by167          show mmul (proj g κ m) (frft g κ z s) (p - 1) k l * v l = (z ^ s) ^ m * (proj g κ m k l * v l)168          rw [show mmul (proj g κ m) (frft g κ z s) (p - 1) k l = (z ^ s) ^ m * proj g κ m k l from169            proj_frft F z s hm hk hl, mul_assoc])170      rw [← e1, e2]171  have hsum : act (proj g κ 0) v (p - 1) k + act (proj g κ 1) v (p - 1) k + act (proj g κ 2) v (p - 1) k +172      act (proj g κ 3) v (p - 1) k ≠ 0 := by rw [act_sum_proj F v hk]; exact hv173  obtain ⟨m, hm, hne⟩ := four_ne_zero (a := fun m => act (proj g κ m) v (p - 1) k) hsum174  exact ⟨m, hm, F.mul_left_cancel hne (by rw [mul_comm, key m hm k hk, mul_comm])⟩175176/-! ## The obstruction (6:E5) -/177178/-- The least `ℓ < 4` with `P ℓ`, or `3`. -/179def find4 (P : Nat → Prop) [DecidablePred P] : Nat := if P 0 then 0 else if P 1 then 1 else if P 2 then 2 else 3180181theorem find4_lt (P : Nat → Prop) [DecidablePred P] : find4 P < 4 := by182  unfold find4183  match Decidable.em (P 0), Decidable.em (P 1), Decidable.em (P 2) with184  | Or.inl h, _, _ => rw [ite_eq_left h]; decide185  | Or.inr h, Or.inl h1, _ => rw [ite_eq_right h, ite_eq_left h1]; decide186  | Or.inr h, Or.inr h1, Or.inl h2 => rw [ite_eq_right h, ite_eq_right h1, ite_eq_left h2]; decide187  | Or.inr h, Or.inr h1, Or.inr h2 => rw [ite_eq_right h, ite_eq_right h1, ite_eq_right h2]; decide188189theorem find4_spec (P : Nat → Prop) [DecidablePred P] (h : ∃ ℓ, ℓ < 4 ∧ P ℓ) : P (find4 P) := by190  unfold find4191  match Decidable.em (P 0), Decidable.em (P 1), Decidable.em (P 2) with192  | Or.inl h0, _, _ => rw [ite_eq_left h0]; exact h0193  | Or.inr h0, Or.inl h1, _ => rw [ite_eq_right h0, ite_eq_left h1]; exact h1194  | Or.inr h0, Or.inr h1, Or.inl h2 => rw [ite_eq_right h0, ite_eq_right h1, ite_eq_left h2]; exact h2195  | Or.inr h0, Or.inr h1, Or.inr h2 =>196    rw [ite_eq_right h0, ite_eq_right h1, ite_eq_right h2]197    obtain ⟨ℓ, hℓ, hP⟩ := h198    match ℓ, hℓ, hP with199    | 0, _, hP => exact absurd hP h0200    | 1, _, hP => exact absurd hP h1201    | 2, _, hP => exact absurd hP h2202    | 3, _, hP => exact hP203    | n + 4, hℓ, _ => exact absurd (Nat.lt_of_lt_of_le hℓ (Nat.le_add_left 4 n)) (Nat.lt_irrefl _)204205/-- 6:E5, the spectral obstruction: for `κ ≥ 2` no invertible `T` (with `T' T = I`) has `T σ T' = F^{[s]}`. Every206nonzero residue is an eigenvalue of `σ`, hence of `T σ T'` on `T v`, hence one of the four `(z^s)^ℓ`: an injection of207the `4κ` residues into four indices. -/208theorem spectral_obstruction (F : Frame p κ g) (hκ : 2 ≤ κ) (z : Shell p) (s : Nat)209    (T T' : Nat → Nat → Shell p) (hinv : ∀ k j, k < p - 1 → j < p - 1 → mmul T' T (p - 1) k j = idm k j)210    (hconj : ∀ k j, k < p - 1 → j < p - 1 → mmul (mmul T (shift p) (p - 1)) T' (p - 1) k j = frft g κ z s k j) :211    False := by212  have hn := F.n_pos213  -- every power g^m is an eigenvalue of F^[s]214  have heig : ∀ m, ∃ ℓ, ℓ < 4 ∧ g ^ m = (z ^ s) ^ ℓ := fun m => by215    obtain ⟨v, ⟨k0, hk0, hv0⟩, hσ⟩ := shift_eigen_exists F (F.pow_ne_zero m)216    -- w = T v is an eigenvector of F^[s] for g^m217    have hTv : ∀ k, k < p - 1 → act T' (act T v (p - 1)) (p - 1) k = v k := fun k hk => by218      rw [← act_mmul, ← act_idm v hk]219      exact sum_congr _ (fun l hl => by rw [hinv k l hk hl])220    have hw : ∃ k, k < p - 1 ∧ act T v (p - 1) k ≠ 0 :=221      match decExistsLT (fun k => act T v (p - 1) k ≠ 0) (p - 1) with222      | isTrue e => e223      | isFalse ne => absurd (by224          rw [← hTv k0 hk0]225          exact sum_zero _ (fun l hl => by226            have e : act T v (p - 1) l = 0 := match Decidable.em (act T v (p - 1) l = 0) with227              | Or.inl e => e228              | Or.inr e => absurd ⟨l, hl, e⟩ ne229            rw [e, mul_zero])) hv0230    have hact : ∀ k, k < p - 1 → act (frft g κ z s) (act T v (p - 1)) (p - 1) k = g ^ m * act T v (p - 1) k :=231      fun k hk => by232        rw [show act (frft g κ z s) (act T v (p - 1)) (p - 1) k =233            act (mmul (mmul T (shift p) (p - 1)) T' (p - 1)) (act T v (p - 1)) (p - 1) k from234          sum_congr _ (fun l hl => by rw [hconj k l hk hl])]235        rw [act_mmul, act_mmul, ← act_smul]236        exact sum_congr _ (fun l hl => by237          show T k l * act (shift p) (act T' (act T v (p - 1)) (p - 1)) (p - 1) l = T k l * (g ^ m * v l)238          rw [← hσ l hl]239          show T k l * act (shift p) (act T' (act T v (p - 1)) (p - 1)) (p - 1) l =240            T k l * act (shift p) v (p - 1) l241          rw [shift_act F _ hl, shift_act F _ hl, hTv _ (FRC.Nat.mod_lt' _ hn)])242    exact frft_eigen F z s ⟨hw, hact⟩243  -- the injection of [0, 4κ) into [0, 4)244  have h4 : 4 < p - 1 := four_lt_n F hκ245  exact FRC.Logic.no_mirror h4 (fun m => find4 (fun ℓ => (z ^ s) ^ ℓ = g ^ m)) (fun m _ => find4_lt _) (fun m m' hm hm' e =>246    F.pow_inj hm hm' (by247      have e1 := find4_spec (fun ℓ => (z ^ s) ^ ℓ = g ^ m) (match heig m with | ⟨ℓ, hℓ, e⟩ => ⟨ℓ, hℓ, e.symm⟩)248      have e2 := find4_spec (fun ℓ => (z ^ s) ^ ℓ = g ^ m') (match heig m' with | ⟨ℓ, hℓ, e⟩ => ⟨ℓ, hℓ, e.symm⟩)249      rw [← e1, ← e2, e]))250251end Frame252end Shell253end FRC254