IndisputableMonolith.Spectral.DFT8
IndisputableMonolith/Spectral/DFT8.lean · 639 lines · 46 declarations
show as:
view math explainer →
1import Mathlib
2
3namespace IndisputableMonolith
4namespace Spectral
5
6/-!
7# Eight-Tick DFT Backbone (DFT-8)
8
9This module formalizes the 8-point Discrete Fourier Transform as the canonical
10unitary basis for the 8-tick recognition cycle.
11
12## Main Definitions
13
14- `omega8`: The primitive 8th root of unity, ω = e^{-2πi/8}
15- `dft8_entry`: Entry (t, k) of the DFT-8 matrix: ω^{tk} / √8
16- `dft8_matrix`: The full 8×8 unitary DFT matrix
17- `cyclic_shift`: The cyclic shift operator on 8-vectors
18- `dft8_mode`: The k-th DFT basis vector (column k of dft8_matrix)
19
20## Main Results
21
22- `dft8_unitary`: The DFT-8 matrix is unitary (B^H B = I)
23- `dft8_diagonalizes_shift`: DFT diagonalizes the cyclic shift operator
24- `shift_eigenvalue`: Eigenvalue of shift on mode k is ω^k
25- `dft8_neutral_subspace`: Modes k=1..7 span the neutral (mean-free) subspace
26
27## Physical Motivation
28
29The 8-tick period τ₀ = 2^D (D=3) is forced by Recognition Science axioms.
30The DFT-8 basis is the unique (up to permutation/phase) unitary basis that:
311. Diagonalizes the cyclic shift operator (time-translation symmetry)
322. Separates DC (k=0) from neutral modes (k=1..7)
333. Provides φ-lattice quantization via complex exponentials
34
35This makes DFT-8 the canonical spectral basis for the 8-tick cycle.
36-/
37
38open Complex
39
40/-- Primitive 8th root of unity: ω = e^{-2πi/8} = e^{-πi/4} -/
41noncomputable def omega8 : ℂ := Complex.exp (-Complex.I * Real.pi / 4)
42
43/-- ω^8 = 1 (periodicity) -/
44theorem omega8_pow_8 : omega8 ^ 8 = 1 := by
45 simp only [omega8]
46 rw [← Complex.exp_nat_mul]
47 have h : (8 : ℕ) * (-Complex.I * Real.pi / 4) = -(2 * Real.pi * Complex.I) := by
48 push_cast
49 ring
50 rw [h, Complex.exp_neg, Complex.exp_two_pi_mul_I, inv_one]
51
52/-- ω^4 = -1 (half-period) -/
53theorem omega8_pow_4 : omega8 ^ 4 = -1 := by
54 simp only [omega8]
55 rw [← Complex.exp_nat_mul]
56 have h : (4 : ℕ) * (-Complex.I * Real.pi / 4) = -(Real.pi * Complex.I) := by
57 push_cast
58 ring
59 rw [h, Complex.exp_neg, Complex.exp_pi_mul_I, inv_neg_one]
60
61/-- |ω| = 1 (unit modulus) -/
62theorem omega8_abs : ‖omega8‖ = 1 := by
63 have h1 : omega8 = Complex.exp ((-Real.pi / 4 : ℝ) * Complex.I) := by
64 simp only [omega8]
65 congr 1
66 simp only [Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_ofNat]
67 ring
68 rw [h1, Complex.norm_exp_ofReal_mul_I]
69
70/-- DFT-8 matrix entry at position (t, k): ω^{tk} / √8
71 t = time index (row), k = frequency index (column) -/
72noncomputable def dft8_entry (t k : Fin 8) : ℂ :=
73 omega8 ^ (t.val * k.val) / Real.sqrt 8
74
75/-- DFT entries are symmetric in their indices. -/
76lemma dft8_entry_sym (t k : Fin 8) :
77 dft8_entry t k = dft8_entry k t := by
78 unfold dft8_entry
79 simp [Nat.mul_comm]
80
81/-- The 8×8 DFT matrix as a function -/
82noncomputable def dft8_matrix : Matrix (Fin 8) (Fin 8) ℂ :=
83 fun t k => dft8_entry t k
84
85/-- The k-th DFT basis vector (column k of dft8_matrix) -/
86noncomputable def dft8_mode (k : Fin 8) : Fin 8 → ℂ :=
87 fun t => dft8_entry t k
88
89/-- Cyclic shift operator: shifts indices by 1 mod 8 -/
90def cyclic_shift (v : Fin 8 → ℂ) : Fin 8 → ℂ :=
91 fun t => v ⟨(t.val + 1) % 8, Nat.mod_lt _ (by norm_num)⟩
92
93/-- Cyclic shift as a matrix -/
94def shift_matrix : Matrix (Fin 8) (Fin 8) ℂ :=
95 fun t s => if s.val = (t.val + 1) % 8 then 1 else 0
96
97/-! ## Unitarity of DFT-8 -/
98
99/-- Helper: ω^k ≠ 1 for 0 < k < 8.
100 Proof: ω^k = exp(-I * π * k / 4), and exp(z) = 1 iff z = 2πin for some integer n.
101 The equation -k/4 = 2n has no integer solutions for 0 < k < 8. -/
102theorem omega8_pow_ne_one (k : ℕ) (hk_pos : 0 < k) (hk_lt : k < 8) :
103 omega8 ^ k ≠ 1 := by
104 simp only [omega8, ← Complex.exp_nat_mul]
105 intro h_eq_one
106 -- h_eq_one : exp(k * (-I * π / 4)) = 1
107 rw [Complex.exp_eq_one_iff] at h_eq_one
108 -- h_eq_one : ∃ n : ℤ, k * (-I * π / 4) = n * (2 * π * I)
109 obtain ⟨n, h_eq⟩ := h_eq_one
110 have hpi : (Real.pi : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr Real.pi_ne_zero
111 have hI : (Complex.I : ℂ) ≠ 0 := Complex.I_ne_zero
112 -- h_eq: (k : ℂ) * (-I * π / 4) = n * (2 * π * I)
113 -- Simplify: -k / 4 = 2n, so k = -8n
114 have h1 : -(k : ℂ) = 8 * n := by
115 have h2 : (k : ℂ) * (-Complex.I * Real.pi / 4) =
116 ↑n * (2 * Real.pi * Complex.I) := h_eq
117 field_simp [hpi, hI] at h2
118 have h3 : -(k : ℂ) = 8 * ↑n := by
119 have : -(k : ℂ) = 4 * ↑n * 2 := h2
120 ring_nf at this ⊢
121 exact this
122 exact h3
123 -- Now -k = 8n as complex numbers, need to derive contradiction
124 -- First extract to ℤ: k = -8n
125 have h2 : (k : ℤ) = -8 * n := by
126 have h1' : (k : ℂ) = -8 * ↑n := by
127 calc (k : ℂ) = -(-((k : ℂ))) := by ring
128 _ = -(8 * ↑n) := by rw [h1]
129 _ = -8 * ↑n := by ring
130 have h1'' : ((k : ℕ) : ℂ) = ((-8 * n : ℤ) : ℂ) := by
131 simp only [Int.cast_mul, Int.cast_neg, Int.cast_ofNat] at h1' ⊢
132 exact h1'
133 have : ((k : ℤ) : ℂ) = ((-8 * n : ℤ) : ℂ) := by
134 simp only [Int.cast_natCast]
135 exact h1''
136 exact Int.cast_injective this
137 -- k is a natural number with 0 < k < 8, so k ∈ {1,2,3,4,5,6,7}
138 -- -8n ∈ {..., -16, -8, 0, 8, 16, ...}
139 -- These sets are disjoint, contradiction
140 omega
141
142/-- Backward compatibility alias -/
143theorem omega8_pow_ne_one_axiom (k : ℕ) (hk_pos : 0 < k) (hk_lt : k < 8) :
144 omega8 ^ k ≠ 1 :=
145 omega8_pow_ne_one k hk_pos hk_lt
146
147/-- star(ω) = ω^(-1) for the primitive 8th root of unity.
148 Since ω = exp(-i π/4), we have conj(ω) = exp(i π/4) = ω^(-1). -/
149lemma star_omega8 : star omega8 = omega8⁻¹ := by
150 simp only [omega8, Complex.star_def]
151 rw [← Complex.exp_conj]
152 simp only [map_div₀, map_neg, map_mul, Complex.conj_I, neg_neg, Complex.conj_ofReal,
153 RCLike.conj_ofNat]
154 -- Now have: exp(I * π / 4) = exp(-I * π / 4)⁻¹
155 -- This is exp(z)⁻¹ = exp(-z)
156 rw [← Complex.exp_neg]
157 congr 1
158 ring
159
160/-- star(ω^n) = ω^(-n) for unit modulus -/
161lemma star_omega8_pow (n : ℕ) : star (omega8 ^ n) = omega8⁻¹ ^ n := by
162 rw [star_pow, star_omega8]
163
164/-- ω * ω^(-1) = 1 -/
165lemma omega8_mul_inv : omega8 * omega8⁻¹ = 1 := mul_inv_cancel₀ (by
166 simp only [omega8, ne_eq]
167 exact Complex.exp_ne_zero _)
168
169/-- |ω|² = 1, expressed as star(ω) * ω = 1 -/
170lemma star_omega8_mul_self : star omega8 * omega8 = 1 := by
171 rw [star_omega8, inv_mul_cancel₀]
172 simp only [omega8, ne_eq]
173 exact Complex.exp_ne_zero _
174
175/-- (star ω)^n * ω^n = 1 -/
176lemma star_omega8_pow_mul_self (n : ℕ) : star omega8 ^ n * omega8 ^ n = 1 := by
177 rw [← mul_pow, star_omega8_mul_self, one_pow]
178
179/-- ω^{-1} = ω^7 since ω^8 = 1 -/
180lemma omega8_inv_eq_pow7 : omega8⁻¹ = omega8 ^ 7 := by
181 have h8 : omega8 ^ 8 = 1 := omega8_pow_8
182 have h : omega8 ^ 7 * omega8 = 1 := by
183 calc
184 omega8 ^ 7 * omega8 = omega8 ^ 7 * omega8 ^ 1 := by ring
185 _ = omega8 ^ (7 + 1) := by rw [pow_add]
186 _ = omega8 ^ 8 := by norm_num
187 _ = 1 := h8
188 have hne : omega8 ≠ 0 := Complex.exp_ne_zero _
189 rw [mul_comm] at h
190 exact (eq_inv_of_mul_eq_one_right h).symm
191
192/-- star(ω^n) * ω^m = ω^(7n + m) for n, m : ℕ -/
193lemma star_omega8_pow_mul_pow (n m : ℕ) :
194 star (omega8 ^ n) * omega8 ^ m = omega8 ^ (7 * n + m) := by
195 rw [star_omega8_pow]
196 conv_lhs => rw [omega8_inv_eq_pow7]
197 rw [← pow_mul, ← pow_add]
198
199/-- Sum over star(ω^{tk}) * ω^{tk'} = sum over ω^{t(7k+k')} -/
200lemma sum_star_omega8_pow_prod (k k' : Fin 8) :
201 Finset.univ.sum (fun t : Fin 8 => star (omega8 ^ (t.val * k.val)) * omega8 ^ (t.val * k'.val)) =
202 Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * (7 * k.val + k'.val))) := by
203 congr 1
204 ext t
205 rw [star_omega8_pow_mul_pow]
206 congr 1
207 ring
208
209/-- Sum of roots of unity vanishes: ∑_{t=0}^{7} ω^{tk} = 0 for k ≠ 0 mod 8
210 Standard result from geometric series. -/
211theorem roots_of_unity_sum (k : Fin 8) (hk : k ≠ 0) :
212 Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * k.val)) = 0 := by
213 -- Let ζ = ω^k, then sum = ∑_{t=0}^{7} ζ^t
214 let zeta := omega8 ^ k.val
215 have h_sum_eq : Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * k.val))
216 = Finset.univ.sum (fun t : Fin 8 => zeta ^ t.val) := by
217 congr 1
218 ext t
219 simp only [zeta, ← pow_mul, mul_comm]
220 rw [h_sum_eq]
221 have h_zeta8 : zeta ^ 8 = 1 := by
222 show (omega8 ^ k.val) ^ 8 = 1
223 rw [← pow_mul, mul_comm]
224 simp only [pow_mul, omega8_pow_8, one_pow]
225 have h_k_pos : 0 < k.val := Nat.pos_of_ne_zero (fun h => hk (Fin.ext h))
226 have h_zeta_ne_one : zeta ≠ 1 := omega8_pow_ne_one_axiom k.val h_k_pos k.isLt
227 -- Geometric series: ∑_{t=0}^{7} ζ^t = (ζ^8 - 1) / (ζ - 1)
228 -- Since ζ^8 = 1, numerator = 0, so sum = 0
229 have h_ne : zeta - 1 ≠ 0 := sub_ne_zero.mpr h_zeta_ne_one
230 -- (∑ ζ^t) * (ζ - 1) = ζ^8 - 1 by telescoping
231 have h_geom_mul : Finset.univ.sum (fun t : Fin 8 => zeta ^ t.val) * (zeta - 1) = zeta ^ 8 - 1 := by
232 have h_expand : Finset.univ.sum (fun t : Fin 8 => zeta ^ t.val) =
233 zeta^0 + zeta^1 + zeta^2 + zeta^3 + zeta^4 + zeta^5 + zeta^6 + zeta^7 := by
234 simp only [Fin.sum_univ_eight]
235 rfl
236 rw [h_expand]
237 ring
238 rw [h_zeta8, sub_self] at h_geom_mul
239 exact (mul_eq_zero.mp h_geom_mul).resolve_right h_ne
240
241/-- Sum of all 8th roots equals 8 when k = 0 -/
242lemma roots_of_unity_sum_zero :
243 Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * 0)) = 8 := by
244 simp [Finset.sum_const]
245
246/-- star(dft8_entry t k) * dft8_entry t k' expressed in terms of omega8 -/
247lemma star_dft8_entry_mul (t k k' : Fin 8) :
248 star (dft8_entry t k) * dft8_entry t k' =
249 star (omega8 ^ (t.val * k.val)) * omega8 ^ (t.val * k'.val) / 8 := by
250 simp only [dft8_entry, star_div₀, Complex.star_def, Complex.conj_ofReal]
251 have hsqrt8 : (Real.sqrt 8 : ℂ) * Real.sqrt 8 = 8 := by
252 rw [← Complex.ofReal_mul, Real.mul_self_sqrt (by norm_num)]; norm_cast
253 field_simp
254 ring_nf
255 rw [sq, hsqrt8]
256
257/-- For k = k', star(ω^{tk}) * ω^{tk} = 1 -/
258lemma star_omega8_pow_mul_same (t k : Fin 8) :
259 star (omega8 ^ (t.val * k.val)) * omega8 ^ (t.val * k.val) = 1 := by
260 rw [star_omega8_pow, ← mul_pow, inv_mul_cancel₀]
261 · simp only [one_pow]
262 · simp only [omega8, ne_eq]
263 exact Complex.exp_ne_zero _
264
265/-- Inner product of DFT columns: ⟨column k, column k'⟩ = δ_{k,k'}
266 This is the fundamental orthonormality property of DFT. -/
267theorem dft8_column_orthonormal (k k' : Fin 8) :
268 Finset.univ.sum (fun t : Fin 8 =>
269 star (dft8_entry t k) * dft8_entry t k') =
270 if k = k' then 1 else 0 := by
271 -- Expand the sum in terms of omega8
272 have h_sum : Finset.univ.sum (fun t : Fin 8 => star (dft8_entry t k) * dft8_entry t k') =
273 Finset.univ.sum (fun t : Fin 8 => star (omega8 ^ (t.val * k.val)) *
274 omega8 ^ (t.val * k'.val) / 8) := by
275 congr 1
276 ext t
277 exact star_dft8_entry_mul t k k'
278 rw [h_sum]
279 -- Factor out the /8
280 have h_factor : Finset.univ.sum (fun t : Fin 8 => star (omega8 ^ (t.val * k.val)) *
281 omega8 ^ (t.val * k'.val) / 8) =
282 Finset.univ.sum (fun t : Fin 8 => star (omega8 ^ (t.val * k.val)) *
283 omega8 ^ (t.val * k'.val)) / 8 := by
284 rw [Finset.sum_div]
285 rw [h_factor]
286 split_ifs with heq
287 · -- Case k = k': sum of 1 = 8, divided by 8 = 1
288 subst heq
289 have h1 : Finset.univ.sum (fun t : Fin 8 => star (omega8 ^ (t.val * k.val)) *
290 omega8 ^ (t.val * k.val)) = 8 := by
291 have h_all_one : ∀ t : Fin 8, star (omega8 ^ (t.val * k.val)) * omega8 ^ (t.val * k.val) = 1 :=
292 fun t => star_omega8_pow_mul_same t k
293 simp only [h_all_one, Finset.sum_const, Finset.card_fin, nsmul_eq_mul, mul_one]; norm_cast
294 rw [h1]
295 norm_num
296 · -- Case k ≠ k': use roots_of_unity_sum
297 -- By sum_star_omega8_pow_prod: ∑_t star(ω^{tk}) * ω^{tk'} = ∑_t ω^{t(7k+k')}
298 rw [sum_star_omega8_pow_prod]
299 -- Define the frequency as a Fin 8
300 let freq := (7 * k.val + k'.val) % 8
301 have h_freq_lt : freq < 8 := Nat.mod_lt _ (by norm_num)
302 let freq_fin : Fin 8 := ⟨freq, h_freq_lt⟩
303 -- The key: freq_fin ≠ 0 when k ≠ k'
304 -- Note: 7k + k' ≡ -k + k' (mod 8), so (7k+k') % 8 = 0 iff k = k'
305 have h_freq_ne_zero : freq_fin ≠ 0 := by
306 simp only [freq_fin, freq, ne_eq, Fin.ext_iff, Fin.val_zero]
307 have hk : k.val < 8 := k.isLt
308 have hk' : k'.val < 8 := k'.isLt
309 have hne : k.val ≠ k'.val := fun h => heq (Fin.ext h)
310 omega
311 -- First show ∑_t ω^{t(7k+k')} = ∑_t ω^{t * freq}
312 have h_pow_mod : ∀ t : Fin 8, omega8 ^ (t.val * (7 * k.val + k'.val)) =
313 omega8 ^ (t.val * freq_fin.val) := by
314 intro t
315 simp only [freq_fin, freq]
316 have h8 : omega8 ^ 8 = 1 := omega8_pow_8
317 have h_eq : t.val * (7 * k.val + k'.val) % 8 = t.val * ((7 * k.val + k'.val) % 8) % 8 := by
318 conv_lhs => rw [Nat.mul_mod]
319 conv_rhs => rw [Nat.mul_mod]
320 have h_mod_lt : (7 * k.val + k'.val) % 8 < 8 := Nat.mod_lt _ (by norm_num)
321 rw [Nat.mod_eq_of_lt h_mod_lt]
322 have h_period : ∀ n m : ℕ, n % 8 = m % 8 → omega8 ^ n = omega8 ^ m := by
323 intro n m heq
324 have hn : n = 8 * (n / 8) + n % 8 := (Nat.div_add_mod n 8).symm
325 have hm : m = 8 * (m / 8) + m % 8 := (Nat.div_add_mod m 8).symm
326 rw [hn, hm, heq]
327 rw [pow_add, pow_add, pow_mul, pow_mul, h8, one_pow, one_pow]
328 apply h_period
329 exact h_eq
330 have h_sum_eq :
331 Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * (7 * k.val + k'.val))) =
332 Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * freq_fin.val)) := by
333 congr 1; ext t; exact h_pow_mod t
334 rw [h_sum_eq]
335 have h_roots := roots_of_unity_sum freq_fin h_freq_ne_zero
336 simp only [div_eq_zero_iff, h_roots, true_or]
337
338/-- DFT-8 matrix is unitary: B^H · B = I -/
339theorem dft8_unitary :
340 dft8_matrix.conjTranspose * dft8_matrix = 1 := by
341 ext i j
342 simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, Matrix.one_apply]
343 -- (B^H · B)_{i,j} = ∑_t conj(B_{t,i}) * B_{t,j} = ∑_t conj(dft8_entry t i) * dft8_entry t j
344 -- By dft8_column_orthonormal, this equals δ_{i,j}
345 convert dft8_column_orthonormal i j using 1
346
347/-- Row orthonormality: Σ_k star(B_sk) * B_tk = δ_{s,t}.
348 Follows from column orthonormality via symmetry B_tk = B_kt. -/
349theorem dft8_row_orthonormal (s t : Fin 8) :
350 Finset.univ.sum (fun k : Fin 8 => star (dft8_entry s k) * dft8_entry t k) =
351 if s = t then 1 else 0 := by
352 -- Use symmetry: B_sk = B_ks and B_tk = B_kt
353 have h_sym : ∀ k, star (dft8_entry s k) * dft8_entry t k =
354 star (dft8_entry k s) * dft8_entry k t := fun k => by
355 rw [dft8_entry_sym s k, dft8_entry_sym t k]
356 simp_rw [h_sym]
357 -- Now it's exactly column orthonormality with swapped indices
358 exact dft8_column_orthonormal s t
359
360/-! ## Shift Diagonalization -/
361
362/-- The eigenvalue of cyclic shift on mode k is ω^k -/
363noncomputable def shift_eigenvalue (k : Fin 8) : ℂ := omega8 ^ k.val
364
365/-- Helper: (t + 1) mod 8 * k ≡ (t + 1) * k mod 8 -/
366lemma mod8_mul_eq (t : Fin 8) (k : ℕ) :
367 omega8 ^ (((t.val + 1) % 8) * k) = omega8 ^ ((t.val + 1) * k) := by
368 -- Since ω^8 = 1, ω^(a mod 8 * k) = ω^(a * k mod 8) = ω^(a * k)
369 have h8 : omega8 ^ 8 = 1 := omega8_pow_8
370 cases Nat.lt_or_ge (t.val + 1) 8 with
371 | inl hlt =>
372 -- t.val + 1 < 8, so mod is identity
373 simp only [Nat.mod_eq_of_lt hlt]
374 | inr hge =>
375 -- t.val + 1 ≥ 8, but t.val < 8, so t.val + 1 ∈ [8, 8], i.e., = 8
376 have h_eq : t.val + 1 = 8 := by omega
377 simp only [h_eq, Nat.mod_self]
378 -- Need: ω^(0 * k) = ω^(8 * k)
379 simp only [zero_mul, pow_zero]
380 -- ω^(8 * k) = (ω^8)^k = 1^k = 1
381 rw [pow_mul, h8, one_pow]
382
383/-- DFT mode k is an eigenvector of cyclic shift with eigenvalue ω^k.
384 This is the key property: DFT diagonalizes the shift operator. -/
385theorem dft8_shift_eigenvector (k : Fin 8) :
386 cyclic_shift (dft8_mode k) = (omega8 ^ k.val) • (dft8_mode k) := by
387 funext t
388 simp only [cyclic_shift, dft8_mode, dft8_entry, Pi.smul_apply, smul_eq_mul]
389 -- LHS: ω^{((t+1) % 8)k} / √8, RHS: ω^k * ω^{tk} / √8
390 rw [mod8_mul_eq]
391 have h_add : (t.val + 1) * k.val = t.val * k.val + k.val := by ring
392 rw [h_add, pow_add]
393 ring
394
395/-- (S * B)_{t,j} = ω^j * B_{t,j} - the shift on column j equals ω^j times that column entry -/
396lemma shift_mul_dft8_entry (t j : Fin 8) :
397 (shift_matrix * dft8_matrix) t j = (omega8 ^ j.val) * dft8_matrix t j := by
398 -- Use dft8_shift_eigenvector directly
399 have h := dft8_shift_eigenvector j
400 have h_t := congrFun h t
401 simp only [cyclic_shift, dft8_mode, dft8_entry, Pi.smul_apply, smul_eq_mul] at h_t
402 simp only [Matrix.mul_apply, shift_matrix, dft8_matrix, dft8_entry]
403 -- Convert the sum to a single term using the shift matrix structure
404 let idx : Fin 8 := ⟨(t.val + 1) % 8, Nat.mod_lt _ (by norm_num)⟩
405 have h_fin : idx ∈ Finset.univ := Finset.mem_univ _
406 rw [Finset.sum_eq_single idx]
407 · -- Main case: s = idx
408 have hcond : idx.val = (t.val + 1) % 8 := rfl
409 simp only [hcond, ↓reduceIte, one_mul]
410 exact h_t
411 · -- Other cases: s ≠ idx
412 intro s _ hs
413 have hne : ¬(s.val = (t.val + 1) % 8) := by
414 intro heq
415 apply hs
416 ext
417 simp only [idx]
418 exact heq
419 simp only [hne, ↓reduceIte, zero_mul]
420 · intro h_not_in
421 exact absurd h_fin h_not_in
422
423/-- B^H * (S * B) at entry (i, j) equals ω^j * δ_{i,j} -/
424lemma conjTranspose_shift_mul (i j : Fin 8) :
425 (dft8_matrix.conjTranspose * (shift_matrix * dft8_matrix)) i j =
426 (omega8 ^ j.val) * (if i = j then 1 else 0) := by
427 have h_expand : (dft8_matrix.conjTranspose * (shift_matrix * dft8_matrix)) i j =
428 ∑ t, star (dft8_matrix t i) * (shift_matrix * dft8_matrix) t j := by
429 simp only [Matrix.mul_apply, Matrix.conjTranspose_apply]
430 rw [h_expand]
431 -- Use shift_mul_dft8_entry to simplify each term
432 have h_simp : ∀ t, star (dft8_matrix t i) * (shift_matrix * dft8_matrix) t j =
433 (omega8 ^ j.val) * (star (dft8_matrix t i) * dft8_matrix t j) := by
434 intro t
435 rw [shift_mul_dft8_entry]
436 ring
437 simp only [h_simp, ← Finset.mul_sum]
438 -- Now show ∑_t star(B_{t,i}) * B_{t,j} = δ_{i,j}
439 have h_ortho := dft8_column_orthonormal i j
440 simp only [dft8_matrix, h_ortho, mul_ite, mul_one, mul_zero]
441
442/-- DFT diagonalizes the shift operator:
443 B^H · S · B = diag(1, ω, ω², ..., ω⁷) -/
444theorem dft8_diagonalizes_shift :
445 dft8_matrix.conjTranspose * shift_matrix * dft8_matrix =
446 Matrix.diagonal (fun k => shift_eigenvalue k) := by
447 ext i j
448 rw [Matrix.mul_assoc]
449 rw [conjTranspose_shift_mul]
450 simp only [Matrix.diagonal, Matrix.of_apply, shift_eigenvalue]
451 split_ifs with h
452 · subst h; ring
453 · ring
454/-! ## Neutral Subspace -/
455
456/-- Mode k=0 is the constant (DC) mode -/
457lemma dft8_mode_zero_constant :
458 ∀ t : Fin 8, dft8_mode 0 t = 1 / Real.sqrt 8 := by
459 intro t
460 unfold dft8_mode dft8_entry
461 simp [mul_zero, pow_zero]
462
463/-- Modes k=1..7 are orthogonal to the constant mode (mean-free) -/
464lemma dft8_mode_neutral (k : Fin 8) (hk : k ≠ 0) :
465 Finset.univ.sum (dft8_mode k) = 0 := by
466 unfold dft8_mode dft8_entry
467 -- Sum of ω^{tk} over t = 0 for k ≠ 0 (roots of unity sum)
468 have hzero : Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * k.val)) = 0 :=
469 roots_of_unity_sum k hk
470 have hsum :
471 Finset.univ.sum (fun t : Fin 8 =>
472 omega8 ^ (t.val * k.val) * ((Real.sqrt 8 : ℝ) : ℂ)⁻¹) =
473 (Finset.univ.sum fun t : Fin 8 => omega8 ^ (t.val * k.val)) *
474 ((Real.sqrt 8 : ℝ) : ℂ)⁻¹ := by
475 simpa using
476 (Finset.sum_mul
477 (s := (Finset.univ : Finset (Fin 8)))
478 (f := fun t : Fin 8 => omega8 ^ (t.val * k.val))
479 (((Real.sqrt 8 : ℝ) : ℂ)⁻¹)).symm
480 simpa [div_eq_mul_inv, hzero] using hsum
481
482/-! ## Inverse DFT and Neutral Subspace -/
483
484/-- DFT coefficients of a vector v: c_k = ∑_t conj(mode_k(t)) · v(t) -/
485noncomputable def dft_coefficients (v : Fin 8 → ℂ) : Fin 8 → ℂ :=
486 fun k => Finset.univ.sum (fun t => star (dft8_entry t k) * v t)
487
488/-- The DC coefficient of v is (1/√8) · ∑v -/
489lemma dft_coeff_zero (v : Fin 8 → ℂ) :
490 dft_coefficients v 0 = (Finset.univ.sum v) / Real.sqrt 8 := by
491 unfold dft_coefficients dft8_entry
492 simp only [Fin.val_zero, mul_zero, pow_zero, one_div, star_inv₀]
493 -- star((√8)⁻¹) * v t = (√8)⁻¹ * v t since √8 is real
494 have hsqrt_real : (star ((Real.sqrt 8 : ℝ) : ℂ)) = ((Real.sqrt 8 : ℝ) : ℂ) := by
495 rw [Complex.star_def, Complex.conj_ofReal]
496 have h_factor : ∀ t, (star ((Real.sqrt 8 : ℝ) : ℂ))⁻¹ * v t =
497 ((Real.sqrt 8 : ℝ) : ℂ)⁻¹ * v t := by
498 intro t; rw [hsqrt_real]
499 simp only [h_factor]
500 have h_comm : ∀ t, ((Real.sqrt 8 : ℝ) : ℂ)⁻¹ * v t = v t * ((Real.sqrt 8 : ℝ) : ℂ)⁻¹ := by
501 intro t; ring
502 simp only [h_comm, ← Finset.sum_mul]
503 rfl
504
505/-- If v is neutral (∑v = 0), its DC coefficient is 0 -/
506lemma dft_coeff_zero_of_neutral (v : Fin 8 → ℂ) (hv : Finset.univ.sum v = 0) :
507 dft_coefficients v 0 = 0 := by
508 rw [dft_coeff_zero, hv, zero_div]
509
510/-- Inverse DFT expansion using matrix notation.
511 Since DFT is unitary (B^H B = I), we also have B B^H = I.
512 Thus v = B · (B^H · v) = ∑_k ⟨mode_k, v⟩ · mode_k. -/
513lemma inverse_dft_expansion (v : Fin 8 → ℂ) :
514 ∀ t, v t = Finset.univ.sum (fun k => dft_coefficients v k * dft8_entry t k) := by
515 intro t
516 simp only [dft_coefficients]
517 -- v(t) = ∑_k (∑_s conj(B_{s,k}) v(s)) B_{t,k}
518 -- Rearrange: = ∑_s v(s) (∑_k conj(B_{s,k}) B_{t,k})
519 -- = ∑_s v(s) δ_{s,t} [by row orthonormality]
520 -- = v(t)
521 have h_sum : (∑ k : Fin 8, (∑ s : Fin 8, star (dft8_entry s k) * v s) * dft8_entry t k) =
522 ∑ s : Fin 8, v s * ∑ k : Fin 8, star (dft8_entry s k) * dft8_entry t k := by
523 simp_rw [Finset.sum_mul, Finset.mul_sum]
524 rw [Finset.sum_comm]
525 congr 1
526 ext s
527 congr 1
528 ext k
529 ring
530 rw [h_sum]
531 have h_ortho : ∀ s, Finset.univ.sum (fun k => star (dft8_entry s k) * dft8_entry t k) =
532 if s = t then 1 else 0 := fun s => dft8_row_orthonormal s t
533 simp only [h_ortho]
534 simp [Finset.sum_ite_eq']
535
536/-- The 7 non-DC modes span the neutral subspace.
537 Any mean-free vector can be expressed as a linear combination of modes 1..7.
538
539 Proof: Using inverse DFT, v = ∑_k c_k · mode_k. For neutral v, c_0 = 0,
540 so v = ∑_{k≠0} c_k · mode_k is in span{mode_1, ..., mode_7}. -/
541theorem dft8_neutral_subspace :
542 ∀ v : Fin 8 → ℂ,
543 Finset.univ.sum v = 0 →
544 v ∈ Submodule.span ℂ {m | ∃ k : Fin 8, k ≠ 0 ∧ m = dft8_mode k} := by
545 intro v hv
546 -- Step 1: DC coefficient is 0 for neutral v
547 have h_c0 := dft_coeff_zero_of_neutral v hv
548 -- Step 2: Rewrite v using inverse DFT as a sum of smul'd modes
549 have h_inv := inverse_dft_expansion v
550 have h_eq : v = Finset.univ.sum (fun k => dft_coefficients v k • dft8_mode k) := by
551 ext t
552 simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, dft8_mode]
553 exact h_inv t
554 rw [h_eq]
555 -- Split sum: k=0 contributes 0, rest are in span
556 have h_zero_term : dft_coefficients v 0 • dft8_mode 0 = 0 := by simp [h_c0]
557 -- Isolate k=0 using Finset manipulation
558 have h_mem_univ : (0 : Fin 8) ∈ Finset.univ := Finset.mem_univ 0
559 rw [← Finset.insert_erase h_mem_univ, Finset.sum_insert (Finset.notMem_erase 0 Finset.univ)]
560 rw [h_zero_term, zero_add]
561 -- Sum over k ≠ 0 is in span
562 apply Submodule.sum_mem
563 intro k hk
564 have hk_ne : k ≠ 0 := Finset.ne_of_mem_erase hk
565 apply Submodule.smul_mem
566 apply Submodule.subset_span
567 exact ⟨k, hk_ne, rfl⟩
568
569/-- Legacy alias for compatibility. -/
570def dft8_neutral_subspace_hypothesis : Prop :=
571 ∀ v : Fin 8 → ℂ,
572 Finset.univ.sum v = 0 →
573 v ∈ Submodule.span ℂ {m | ∃ k : Fin 8, k ≠ 0 ∧ m = dft8_mode k}
574
575/-- The hypothesis is now a theorem. -/
576theorem dft8_neutral_subspace_hypothesis_holds : dft8_neutral_subspace_hypothesis :=
577 dft8_neutral_subspace
578
579/-! ## Uniqueness (Representation-Theoretic) -/
580
581/-- The DFT-8 basis is unique up to permutation and phase among bases that
582 diagonalize the cyclic shift operator.
583
584 This follows from the representation theory of cyclic groups:
585 - The cyclic group Z/8Z has exactly 8 one-dimensional irreducible representations
586 - The characters are χ_k(g) = ω^{kg} for k = 0, 1, ..., 7
587 - Any basis diagonalizing the shift must consist of eigenvectors
588 - The eigenvectors are unique up to scalar multiple (one-dimensional eigenspaces)
589
590 Therefore DFT-8 is the canonical choice (with standard normalization).
591 Note: This was an axiom but is not used in any proofs. Converted to hypothesis. -/
592def dft8_unique_up_to_phase_hypothesis : Prop :=
593 ∀ (B : Matrix (Fin 8) (Fin 8) ℂ),
594 -- B is unitary
595 B.conjTranspose * B = 1 →
596 -- B diagonalizes shift
597 (∃ D : Fin 8 → ℂ, B.conjTranspose * shift_matrix * B = Matrix.diagonal D) →
598 -- Then B differs from dft8_matrix only by a diagonal phase matrix
599 ∃ (phases : Fin 8 → ℂ) (perm : Equiv.Perm (Fin 8)),
600 (∀ k, ‖phases k‖ = 1) ∧
601 ∀ t k, B t k = phases k * dft8_matrix t (perm k)
602
603/-! ## Eight-Tick Basis Type -/
604
605/-- The canonical eight-tick DFT basis as a bundled structure.
606 This provides the standard basis for all 8-tick spectral operations. -/
607structure EightTickBasis where
608 /-- The 8 basis vectors (DFT modes) -/
609 modes : Fin 8 → (Fin 8 → ℂ)
610 /-- Mode 0 is the DC (constant) mode -/
611 mode_zero_dc : ∀ t, modes 0 t = 1 / Real.sqrt 8
612 /-- Modes 1..7 are neutral (mean-free) -/
613 modes_neutral : ∀ k, k ≠ 0 → Finset.univ.sum (modes k) = 0
614 /-- Modes are orthonormal -/
615 modes_orthonormal : ∀ k k',
616 Finset.univ.sum (fun t => star (modes k t) * modes k' t) =
617 if k = k' then 1 else 0
618
619/-- The standard DFT-8 basis instance -/
620noncomputable def standardDFT8Basis : EightTickBasis where
621 modes := dft8_mode
622 mode_zero_dc := dft8_mode_zero_constant
623 modes_neutral := dft8_mode_neutral
624 modes_orthonormal := dft8_column_orthonormal
625
626/-- Theorem: The standard DFT-8 basis is the unique shift-invariant basis.
627 Any other orthonormal basis that diagonalizes cyclic shift is equivalent
628 to DFT-8 up to phase and permutation.
629 Note: This was an axiom but is not used in any proofs. Converted to hypothesis. -/
630def standardDFT8Basis_canonical_hypothesis : Prop :=
631 ∀ (B : EightTickBasis),
632 (∀ k, ∃ lam : ℂ, cyclic_shift (B.modes k) = lam • B.modes k) →
633 ∃ (phases : Fin 8 → ℂ) (perm : Equiv.Perm (Fin 8)),
634 (∀ k, ‖phases k‖ = 1) ∧
635 ∀ k t, B.modes k t = phases k * standardDFT8Basis.modes (perm k) t
636
637end Spectral
638end IndisputableMonolith
639