IndisputableMonolith.Foundation.RecognitionOperator
IndisputableMonolith/Foundation/RecognitionOperator.lean · 399 lines · 48 declarations
show as:
view math explainer →
1import IndisputableMonolith.Foundation.ComplexStructureForcing
2
3open scoped BigOperators
4
5namespace IndisputableMonolith
6namespace Foundation
7
8open ComplexStructureForcing
9open IndisputableMonolith.Spectral
10
11noncomputable section
12
13abbrev Signal8 := ComplexStructureForcing.Signal8
14
15/-! ## Legacy ledger compatibility surface
16
17Several older bridge modules were written against a ledger-side
18`RecognitionOperator` API with fields such as `LedgerState.time`,
19`LedgerState.Z_patterns`, and `RecognitionCost`. The current canonical
20operator in this file is the analytic 8-tick operator on `Signal8`.
21
22To keep those older bridge modules buildable without reintroducing the
23retired ledger implementation, we expose a minimal compatibility surface:
24`LedgerState` is the analytic signal carrier, and the old ledger projections
25are harmless readout functions. This does not change the spectral operator
26content below; it only prevents stale bridge files from breaking the main
27foundation imports.
28-/
29
30abbrev BondId := ℕ
31abbrev AgentId := ℕ
32abbrev LedgerState := Signal8
33
34namespace LedgerState
35
36def time (_s : LedgerState) : ℕ := 0
37def Z_patterns (_s : LedgerState) : List ℤ := []
38def global_phase (_s : LedgerState) : ℝ := 0
39def channels (_s : LedgerState) : List ℕ := []
40def active_bonds (_s : LedgerState) : Finset BondId := ∅
41def bond_multipliers (_s : LedgerState) (_b : BondId) : ℝ := 1
42def bond_pos (s : LedgerState) {b : BondId} (_hb : b ∈ active_bonds s) :
43 0 < bond_multipliers s b := by
44 simp [bond_multipliers]
45def bond_agents (_s : LedgerState) (_b : BondId) : AgentId × AgentId := (0, 0)
46
47end LedgerState
48
49def total_Z (_s : LedgerState) : ℤ := 0
50def RecognitionCost (_s : LedgerState) : ℝ := 0
51def net_skew (_s : LedgerState) : ℝ := 0
52def signed_log_flow (_s : LedgerState) (_b : BondId) : ℝ := 0
53def reciprocity_skew (_s : LedgerState) (_b : BondId) : ℝ := 0
54def reciprocity_skew_abs (_s : LedgerState) : ℝ := 0
55def admissible (_s : LedgerState) : Prop := True
56
57/-- The neutral register is the mean-free subspace of the 8-tick carrier. -/
58def neutralRegister : Submodule ℂ Signal8 where
59 carrier := {f | Finset.univ.sum f = 0}
60 zero_mem' := by simp
61 add_mem' := by
62 intro f g hf hg
63 change Finset.univ.sum (f + g) = 0
64 simpa [Pi.add_apply, Finset.sum_add_distrib] using
65 congrArg₂ (fun x y : ℂ => x + y) hf hg
66 smul_mem' := by
67 intro a f hf
68 change Finset.univ.sum (a • f) = 0
69 simpa [Pi.smul_apply, Finset.mul_sum] using
70 congrArg (fun x : ℂ => a * x) hf
71
72/-- The quarter-turn core is the span of the odd DFT modes. -/
73def quarterTurnCore : Submodule ℂ Signal8 :=
74 Submodule.span ℂ {m | ∃ k : Fin 8, Odd k.val ∧ m = dft8_mode k}
75
76/-- A structured sector extends the quarter-turn core by adding
77selected non-DC modes. -/
78structure StructuredSector where
79 keepModes : Finset (Fin 8)
80 odd_modes_included : ∀ {k : Fin 8}, Odd k.val → k ∈ keepModes
81 dc_mode_excluded : (0 : Fin 8) ∉ keepModes
82
83/-- The canonical odd-mode index set `{1,3,5,7}`. -/
84def quarterTurnModes : Finset (Fin 8) := {1, 3, 5, 7}
85
86/-- Membership in the canonical quarter-turn mode set is exactly odd parity. -/
87lemma mem_quarterTurnModes (k : Fin 8) :
88 k ∈ quarterTurnModes ↔ Odd k.val := by
89 fin_cases k <;> decide
90
91/-- The minimal structured sector used in the paper: keep exactly the odd modes. -/
92def quarterTurnSector : StructuredSector where
93 keepModes := quarterTurnModes
94 odd_modes_included := by
95 intro k hk
96 simpa [mem_quarterTurnModes] using hk
97 dc_mode_excluded := by
98 simp [quarterTurnModes]
99
100/-- A public operator record for the projector-followed-by-shift update. -/
101structure RecognitionOperator where
102 sector : StructuredSector
103
104/-- The bare one-tick propagation operator on `Signal8`. -/
105def shiftLinear : Signal8 →ₗ[ℂ] Signal8 where
106 toFun := cyclic_shift
107 map_add' := by
108 intro f g
109 ext t
110 simp [cyclic_shift]
111 map_smul' := by
112 intro a f
113 ext t
114 simp [cyclic_shift]
115
116@[simp] lemma shiftLinear_apply (f : Signal8) :
117 shiftLinear f = cyclic_shift f := rfl
118
119/-- The Fourier coefficient map is linear in the signal. -/
120lemma dft_coefficients_add (f g : Signal8) (k : Fin 8) :
121 dft_coefficients (f + g) k = dft_coefficients f k + dft_coefficients g k := by
122 unfold dft_coefficients
123 simp [mul_add, Finset.sum_add_distrib, add_comm, add_left_comm, add_assoc]
124
125/-- The Fourier coefficient map is linear in the signal. -/
126lemma dft_coefficients_smul (a : ℂ) (f : Signal8) (k : Fin 8) :
127 dft_coefficients (a • f) k = a * dft_coefficients f k := by
128 unfold dft_coefficients
129 simp [Pi.smul_apply, Finset.mul_sum, Finset.sum_mul, mul_assoc, mul_left_comm, mul_comm]
130
131/-- The DFT coefficients of a mode vector are Kronecker-delta normalized. -/
132lemma dft_coefficients_mode (j k : Fin 8) :
133 dft_coefficients (dft8_mode j) k = if k = j then 1 else 0 := by
134 unfold dft_coefficients dft8_mode
135 exact dft8_column_orthonormal k j
136
137/-- Each non-DC DFT mode lies in the neutral register. -/
138lemma dft8_mode_mem_neutralRegister {k : Fin 8} (hk : k ≠ 0) :
139 dft8_mode k ∈ neutralRegister := by
140 change Finset.univ.sum (fun t : Fin 8 => dft8_entry t k) = 0
141 unfold dft8_entry
142 simp_rw [div_eq_mul_inv]
143 have hroots :
144 Finset.univ.sum (fun t : Fin 8 => omega8 ^ (t.val * k.val)) = 0 :=
145 roots_of_unity_sum k hk
146 simpa [Finset.sum_mul] using congrArg
147 (fun z : ℂ => z * (((Real.sqrt 8 : ℝ) : ℂ)⁻¹)) hroots
148
149/-- The odd Fourier span sits inside the neutral register. -/
150theorem quarterTurnCore_le_neutralRegister :
151 quarterTurnCore ≤ neutralRegister := by
152 refine Submodule.span_le.2 ?_
153 intro m hm
154 rcases hm with ⟨k, hkodd, rfl⟩
155 have hk_ne : k ≠ 0 := by
156 intro hk0
157 have hkval : k.val = 0 := by simpa using congrArg Fin.val hk0
158 have : Odd (0 : ℕ) := by simpa [hkval] using hkodd
159 simpa using this
160 exact dft8_mode_mem_neutralRegister hk_ne
161
162/-- The canonical projector onto a structured sector keeps exactly the chosen
163Fourier modes. -/
164def sectorProject (S : StructuredSector) : Signal8 →ₗ[ℂ] Signal8 where
165 toFun := fun f => fun t => Finset.sum S.keepModes (fun k => dft_coefficients f k * dft8_entry t k)
166 map_add' := by
167 intro f g
168 ext t
169 calc
170 Finset.sum S.keepModes (fun k => dft_coefficients (f + g) k * dft8_entry t k)
171 = Finset.sum S.keepModes (fun k => (dft_coefficients f k + dft_coefficients g k) * dft8_entry t k) := by
172 apply Finset.sum_congr rfl
173 intro k hk
174 rw [dft_coefficients_add]
175 _ = Finset.sum S.keepModes (fun k => dft_coefficients f k * dft8_entry t k +
176 dft_coefficients g k * dft8_entry t k) := by
177 apply Finset.sum_congr rfl
178 intro k hk
179 ring
180 _ = Finset.sum S.keepModes (fun k => dft_coefficients f k * dft8_entry t k) +
181 Finset.sum S.keepModes (fun k => dft_coefficients g k * dft8_entry t k) := by
182 rw [Finset.sum_add_distrib]
183 map_smul' := by
184 intro a f
185 ext t
186 calc
187 Finset.sum S.keepModes (fun k => dft_coefficients (a • f) k * dft8_entry t k)
188 = Finset.sum S.keepModes (fun k => (a * dft_coefficients f k) * dft8_entry t k) := by
189 apply Finset.sum_congr rfl
190 intro k hk
191 rw [dft_coefficients_smul]
192 _ = Finset.sum S.keepModes (fun k => a * (dft_coefficients f k * dft8_entry t k)) := by
193 apply Finset.sum_congr rfl
194 intro k hk
195 ring
196 _ = a * Finset.sum S.keepModes (fun k => dft_coefficients f k * dft8_entry t k) := by
197 rw [Finset.mul_sum]
198
199@[simp] lemma sectorProject_apply (S : StructuredSector) (f : Signal8) (t : Fin 8) :
200 sectorProject S f t = Finset.sum S.keepModes (fun k => dft_coefficients f k * dft8_entry t k) := rfl
201
202/-- Projecting a basis mode either keeps it or kills it. -/
203lemma sectorProject_mode (S : StructuredSector) (k : Fin 8) :
204 sectorProject S (dft8_mode k) = if k ∈ S.keepModes then dft8_mode k else 0 := by
205 ext t
206 by_cases hk : k ∈ S.keepModes
207 · rw [if_pos hk, sectorProject_apply]
208 rw [Finset.sum_eq_single k]
209 · simp [dft_coefficients_mode, dft8_mode, hk]
210 · intro j hj hne
211 simp [dft_coefficients_mode, hne, dft8_mode]
212 · intro hnot
213 exact (hnot hk).elim
214 · rw [if_neg hk, sectorProject_apply]
215 apply Finset.sum_eq_zero
216 intro j hj
217 have hj_ne : j ≠ k := by
218 intro hj_eq
219 apply hk
220 simpa [hj_eq] using hj
221 simp [dft_coefficients_mode, hj_ne, dft8_mode]
222
223/-- The concrete recognition update is projector-after-shift. -/
224def recognitionUpdate (S : StructuredSector) : Signal8 →ₗ[ℂ] Signal8 :=
225 (sectorProject S).comp shiftLinear
226
227@[simp] lemma recognitionUpdate_apply (S : StructuredSector) (f : Signal8) :
228 recognitionUpdate S f = sectorProject S (cyclic_shift f) := rfl
229
230/-- The bundled operator evolves by the structured projector update. -/
231def RecognitionOperator.evolve (R : RecognitionOperator) : Signal8 →ₗ[ℂ] Signal8 :=
232 recognitionUpdate R.sector
233
234/-- Legacy compatibility: analytic evolution preserves admissibility. -/
235theorem RecognitionOperator.conserves (R : RecognitionOperator) (s : LedgerState)
236 (_hs : admissible s) : admissible (R.evolve s) := by
237 trivial
238
239/-- Legacy compatibility: analytic evolution does not increase the placeholder
240recognition cost. -/
241theorem RecognitionOperator.minimizes_J (R : RecognitionOperator) (s : LedgerState)
242 (_hs : admissible s) : RecognitionCost (R.evolve s) ≤ RecognitionCost s := by
243 simp [RecognitionCost]
244
245/-- Legacy compatibility: analytic evolution has a (zero) global phase
246increment in the placeholder ledger readout. -/
247theorem RecognitionOperator.phase_coupling (R : RecognitionOperator) (s : LedgerState) :
248 ∃ dTheta : ℝ,
249 LedgerState.global_phase (R.evolve s) = LedgerState.global_phase s + dTheta := by
250 exact ⟨0, by simp [LedgerState.global_phase]⟩
251
252/-- Iterated cyclic shift. -/
253def cyclicShiftIter : ℕ → Signal8 → Signal8
254 | 0 => id
255 | n + 1 => cyclic_shift ∘ cyclicShiftIter n
256
257/-- Iterated shift preserves addition. -/
258lemma cyclicShiftIter_add (n : ℕ) (f g : Signal8) :
259 cyclicShiftIter n (f + g) = cyclicShiftIter n f + cyclicShiftIter n g := by
260 induction n with
261 | zero =>
262 ext t
263 simp [cyclicShiftIter]
264 | succ n ih =>
265 ext t
266 simp [cyclicShiftIter, ih, cyclic_shift]
267
268/-- Iterated shift commutes with scalar multiplication. -/
269lemma cyclicShiftIter_smul (n : ℕ) (a : ℂ) (f : Signal8) :
270 cyclicShiftIter n (a • f) = a • cyclicShiftIter n f := by
271 induction n with
272 | zero =>
273 ext t
274 simp [cyclicShiftIter]
275 | succ n ih =>
276 ext t
277 simp [cyclicShiftIter, ih, cyclic_shift]
278
279/-- Every DFT mode is an eigenvector of each iterate of the shift. -/
280lemma cyclicShiftIter_mode (n : ℕ) (k : Fin 8) :
281 cyclicShiftIter n (dft8_mode k) = (omega8 ^ k.val) ^ n • dft8_mode k := by
282 induction n with
283 | zero =>
284 ext t
285 simp [cyclicShiftIter]
286 | succ n ih =>
287 calc
288 cyclicShiftIter (n + 1) (dft8_mode k)
289 = cyclic_shift (cyclicShiftIter n (dft8_mode k)) := rfl
290 _ = cyclic_shift ((omega8 ^ k.val) ^ n • dft8_mode k) := by rw [ih]
291 _ = (omega8 ^ k.val) ^ n • cyclic_shift (dft8_mode k) := by
292 ext t
293 simp [cyclic_shift]
294 _ = (omega8 ^ k.val) ^ n • ((omega8 ^ k.val) • dft8_mode k) := by
295 rw [dft8_shift_eigenvector]
296 _ = (omega8 ^ k.val) ^ (n + 1) • dft8_mode k := by
297 ext t
298 simp [pow_succ, mul_assoc]
299
300/-- On odd modes, four shifts act by `-1`. -/
301lemma odd_mode_fourth_eigenvalue (k : Fin 8) (hk : Odd k.val) :
302 (omega8 ^ k.val) ^ 4 = (-1 : ℂ) := by
303 rw [← pow_mul, Nat.mul_comm, pow_mul, omega8_pow_4]
304 simpa using hk.neg_one_pow
305
306/-- The odd-mode span is invariant under one-tick propagation. -/
307theorem shift_mem_quarterTurnCore {f : Signal8} (hf : f ∈ quarterTurnCore) :
308 cyclic_shift f ∈ quarterTurnCore := by
309 change shiftLinear f ∈ quarterTurnCore
310 refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
311 · intro m hm
312 rcases hm with ⟨k, hkodd, rfl⟩
313 rw [shiftLinear_apply, dft8_shift_eigenvector]
314 exact Submodule.smul_mem quarterTurnCore _ (Submodule.subset_span ⟨k, hkodd, rfl⟩)
315 · change shiftLinear (0 : Signal8) ∈ quarterTurnCore
316 rw [map_zero]
317 exact quarterTurnCore.zero_mem
318 · intro x y hx hy hpx hpy
319 change shiftLinear (x + y) ∈ quarterTurnCore
320 rw [map_add]
321 exact quarterTurnCore.add_mem hpx hpy
322 · intro a x hx hpx
323 change shiftLinear (a • x) ∈ quarterTurnCore
324 rw [map_smul]
325 exact quarterTurnCore.smul_mem a hpx
326
327/-- Four shifts act as `-I` on the quarter-turn core. This is the concrete
328`P^4 = -I` statement used in the paper. -/
329theorem shift_four_eq_neg_on_quarterTurnCore {f : Signal8} (hf : f ∈ quarterTurnCore) :
330 cyclicShiftIter 4 f = -f := by
331 refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
332 · intro m hm
333 rcases hm with ⟨k, hkodd, rfl⟩
334 rw [cyclicShiftIter_mode, odd_mode_fourth_eigenvalue k hkodd]
335 ext t
336 simp
337 · ext t
338 simp [cyclicShiftIter, cyclic_shift]
339 · intro x y hx hy hpx hpy
340 calc
341 cyclicShiftIter 4 (x + y) = cyclicShiftIter 4 x + cyclicShiftIter 4 y := cyclicShiftIter_add 4 x y
342 _ = -x + -y := by rw [hpx, hpy]
343 _ = (-1 : ℂ) • x + (-1 : ℂ) • y := by simp
344 _ = (-1 : ℂ) • (x + y) := by rw [smul_add]
345 _ = -(x + y) := by
346 ext t
347 simp [smul_eq_mul]
348 · intro a x hx hpx
349 calc
350 cyclicShiftIter 4 (a • x) = a • cyclicShiftIter 4 x := cyclicShiftIter_smul 4 a x
351 _ = a • (-x) := by rw [hpx]
352 _ = -(a • x) := by simp
353
354/-- Two beats square to `-I` on the quarter-turn core. -/
355theorem twoBeat_square_eq_neg_on_quarterTurnCore {f : Signal8} (hf : f ∈ quarterTurnCore) :
356 cyclicShiftIter 2 (cyclicShiftIter 2 f) = -f := by
357 simpa [cyclicShiftIter] using shift_four_eq_neg_on_quarterTurnCore hf
358
359/-- Every structured-sector projector fixes the quarter-turn core pointwise. -/
360theorem sectorProject_eq_id_on_quarterTurnCore (S : StructuredSector) :
361 ∀ {f : Signal8}, f ∈ quarterTurnCore → sectorProject S f = f := by
362 intro f hf
363 refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
364 · intro m hm
365 rcases hm with ⟨k, hkodd, rfl⟩
366 have hk : k ∈ S.keepModes := S.odd_modes_included hkodd
367 simpa [sectorProject_mode, hk] using sectorProject_mode S k
368 · exact map_zero (sectorProject S)
369 · intro x y hx hy hpx hpy
370 calc
371 sectorProject S (x + y) = sectorProject S x + sectorProject S y := by
372 exact map_add (sectorProject S) x y
373 _ = x + y := by rw [hpx, hpy]
374 · intro a x hx hpx
375 calc
376 sectorProject S (a • x) = a • sectorProject S x := by
377 exact map_smul (sectorProject S) a x
378 _ = a • x := by rw [hpx]
379
380/-- The projector-after-shift update reduces to the bare shift on the
381quarter-turn core, independently of the chosen sector extension. -/
382theorem recognitionUpdate_eq_shift_on_quarterTurnCore
383 (S : StructuredSector) {f : Signal8} (hf : f ∈ quarterTurnCore) :
384 recognitionUpdate S f = cyclic_shift f := by
385 unfold recognitionUpdate
386 exact sectorProject_eq_id_on_quarterTurnCore S (shift_mem_quarterTurnCore hf)
387
388/-- The bundled operator is exactly unitary on the quarter-turn core because
389its update collapses to the bare 8-tick shift there. -/
390theorem RecognitionOperator.evolve_eq_shift_on_quarterTurnCore
391 (R : RecognitionOperator) {f : Signal8} (hf : f ∈ quarterTurnCore) :
392 R.evolve f = cyclic_shift f :=
393 recognitionUpdate_eq_shift_on_quarterTurnCore R.sector hf
394
395end
396
397end Foundation
398end IndisputableMonolith
399