IndisputableMonolith.Foundation.CoupledRecognitionCores
IndisputableMonolith/Foundation/CoupledRecognitionCores.lean · 627 lines · 61 declarations
show as:
view math explainer →
1import Mathlib
2
3open scoped BigOperators
4
5namespace IndisputableMonolith
6namespace Foundation
7namespace CoupledRecognitionCores
8
9noncomputable section
10
11/-- The local quarter-turn core is modeled as a ququart carrier. -/
12abbrev QuquartState := Fin 4 → ℂ
13
14/-- The standard basis ket `|m⟩`. -/
15def basisKet (m : Fin 4) : QuquartState :=
16 fun n => if n = m then 1 else 0
17
18/-- Previous index modulo `4`; this realizes the shift convention
19`X|m⟩ = |m+1 mod 4⟩`. -/
20def prev4 (m : Fin 4) : Fin 4 :=
21 ⟨(m.val + 3) % 4, by omega⟩
22
23/-- Addition modulo `4`. -/
24def add4 (a b : Fin 4) : Fin 4 :=
25 ⟨(a.val + b.val) % 4, by omega⟩
26
27/-- Subtraction modulo `4`. -/
28def sub4 (a b : Fin 4) : Fin 4 :=
29 ⟨(a.val + (4 - b.val)) % 4, by omega⟩
30
31/-- Mod-4 subtraction undoes mod-4 addition. -/
32theorem sub4_add4_cancel_core (a s : Fin 4) :
33 sub4 (add4 a s) a = s := by
34 fin_cases a <;> fin_cases s <;> rfl
35
36/-- Mod-4 addition undoes mod-4 subtraction. -/
37theorem add4_sub4_cancel_core (m a : Fin 4) :
38 add4 a (sub4 m a) = m := by
39 fin_cases m <;> fin_cases a <;> rfl
40
41/-- For fixed `s`, the left addend is recoverable from `add4 a s`. -/
42theorem add4_eq_add4_iff_left_core (a a' s : Fin 4) :
43 add4 a s = add4 a' s ↔ a = a' := by
44 fin_cases a <;> fin_cases a' <;> fin_cases s <;> decide
45
46/-- The canonical ququart shift operator `X`. -/
47def ququartX : QuquartState →ₗ[ℂ] QuquartState where
48 toFun := fun ψ m => ψ (prev4 m)
49 map_add' := by
50 intro ψ χ
51 ext m
52 simp [prev4]
53 map_smul' := by
54 intro a ψ
55 ext m
56 simp [prev4]
57
58/-- The canonical ququart phase operator `Z`. -/
59def ququartZ : QuquartState →ₗ[ℂ] QuquartState where
60 toFun := fun ψ m => Complex.I ^ m.val * ψ m
61 map_add' := by
62 intro ψ χ
63 ext m
64 simp
65 ring
66 map_smul' := by
67 intro a ψ
68 ext m
69 simp
70 ring
71
72/-- `X|m⟩ = |m+1 mod 4⟩`. -/
73theorem ququartX_basisKet (m : Fin 4) :
74 ququartX (basisKet m) = basisKet (add4 1 m) := by
75 ext n
76 fin_cases n <;> fin_cases m <;> simp [ququartX, basisKet, prev4, add4]
77
78/-- `Z|m⟩ = i^m |m⟩`. -/
79theorem ququartZ_basisKet (m : Fin 4) :
80 ququartZ (basisKet m) = (Complex.I ^ m.val) • basisKet m := by
81 ext n
82 by_cases h : n = m
83 · simp [basisKet, ququartZ, h]
84 · simp [basisKet, ququartZ, h]
85
86/-- Pointwise Weyl relation `ZX ψ = i XZ ψ`. -/
87lemma ququartWeyl_relation_apply (ψ : QuquartState) :
88 ququartZ (ququartX ψ) = (Complex.I : ℂ) • ququartX (ququartZ ψ) := by
89 ext m
90 fin_cases m
91 · simp [ququartZ, ququartX, prev4]
92 symm
93 have hI : Complex.I * Complex.I = (-1 : ℂ) := by
94 have h := Complex.I_sq; rw [sq] at h; exact h
95 calc
96 -(Complex.I * (Complex.I * ψ 3)) = -((Complex.I * Complex.I) * ψ 3) := by ring
97 _ = -((-1) * ψ 3) := by rw [hI]
98 _ = ψ 3 := by ring
99 · simp [ququartZ, ququartX, prev4]
100 · simp [ququartZ, ququartX, prev4]
101 have hI : Complex.I * Complex.I = (-1 : ℂ) := by
102 have h := Complex.I_sq; rw [sq] at h; exact h
103 calc
104 -ψ 1 = (-1 : ℂ) * ψ 1 := by ring
105 _ = (Complex.I * Complex.I) * ψ 1 := by rw [hI]
106 _ = Complex.I * (Complex.I * ψ 1) := by ring
107 · simp [ququartZ, ququartX, prev4, Complex.I_sq]
108
109/-- The ququart Weyl relation `ZX = iXZ`. -/
110theorem ququartWeyl_relation :
111 ququartZ.comp ququartX = (Complex.I : ℂ) • (ququartX.comp ququartZ) := by
112 apply LinearMap.ext
113 intro ψ
114 exact ququartWeyl_relation_apply ψ
115
116/-- The finite-site configuration space of coupled ququart cores. -/
117abbrev CoupledCoreIndex (N : ℕ) := Fin N → Fin 4
118
119/-- The concrete Hilbert carrier of `N` coupled recognition cores. -/
120abbrev CoupledCoreSpace (N : ℕ) := CoupledCoreIndex N → ℂ
121
122/-- The dimension of the coupled-core index space is exactly `4^N`. -/
123theorem coupledCoreIndex_card (N : ℕ) :
124 Fintype.card (CoupledCoreIndex N) = 4 ^ N := by
125 simp [CoupledCoreIndex]
126
127/-- The phase character appearing in the tensor-Weyl monomial. -/
128def phaseCharacter {N : ℕ} (b s : CoupledCoreIndex N) : ℂ :=
129 Finset.univ.prod fun x : Fin N => Complex.I ^ ((b x).val * (s x).val)
130
131/-- Shift a coupled-core configuration by a finite ququart displacement. -/
132def shiftedConfig {N : ℕ} (a s : CoupledCoreIndex N) : CoupledCoreIndex N :=
133 fun x => sub4 (s x) (a x)
134
135/-- Add a coupled-core displacement to a configuration. -/
136def addedConfig {N : ℕ} (a s : CoupledCoreIndex N) : CoupledCoreIndex N :=
137 fun x => add4 (a x) (s x)
138
139/-- Zero phase character. -/
140lemma phaseCharacter_zero {N : ℕ} (s : CoupledCoreIndex N) :
141 phaseCharacter 0 s = 1 := by
142 simp [phaseCharacter]
143
144/-- Zero displacement leaves a coupled-core configuration unchanged. -/
145lemma shiftedConfig_zero {N : ℕ} (s : CoupledCoreIndex N) :
146 shiftedConfig 0 s = s := by
147 funext x
148 apply Fin.ext
149 simp [shiftedConfig, sub4]
150
151/-- Shifting after adding the same displacement returns the original configuration. -/
152theorem shiftedConfig_addedConfig {N : ℕ} (a s : CoupledCoreIndex N) :
153 shiftedConfig a (addedConfig a s) = s := by
154 funext x
155 exact sub4_add4_cancel_core (a x) (s x)
156
157/-- Adding after shifting the same displacement returns the original configuration. -/
158theorem addedConfig_shiftedConfig {N : ℕ} (a s : CoupledCoreIndex N) :
159 addedConfig a (shiftedConfig a s) = s := by
160 funext x
161 exact add4_sub4_cancel_core (s x) (a x)
162
163/-- For fixed `s`, the displacement label is recoverable from `addedConfig a s`. -/
164theorem addedConfig_eq_addedConfig_iff_left {N : ℕ}
165 (a a' s : CoupledCoreIndex N) :
166 addedConfig a s = addedConfig a' s ↔ a = a' := by
167 constructor
168 · intro h
169 funext x
170 exact (add4_eq_add4_iff_left_core (a x) (a' x) (s x)).mp (congrArg (fun f => f x) h)
171 · intro h
172 subst h
173 rfl
174
175/-- The tensor-Weyl monomial on the concrete coupled-core carrier. -/
176def tensorWeylMonomial {N : ℕ} (a b : CoupledCoreIndex N) :
177 CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N where
178 toFun := fun ψ s => phaseCharacter b s * ψ (shiftedConfig a s)
179 map_add' := by
180 intro ψ χ
181 ext s
182 simp [phaseCharacter]
183 ring
184 map_smul' := by
185 intro z ψ
186 ext s
187 simp [phaseCharacter]
188 ring
189
190/-- The trivial Weyl monomial is the identity. -/
191theorem tensorWeylMonomial_zero_zero {N : ℕ} :
192 tensorWeylMonomial (N := N) 0 0 = LinearMap.id := by
193 ext ψ s
194 simp [tensorWeylMonomial, phaseCharacter_zero, shiftedConfig_zero]
195
196/-- Standard basis ket for the coupled-core carrier. -/
197def coupledBasisKet {N : ℕ} (s : CoupledCoreIndex N) : CoupledCoreSpace N :=
198 fun t => if t = s then 1 else 0
199
200/-- The coupled standard basis is orthonormal for the explicit finite sum. -/
201theorem coupledBasisKet_orthonormal {N : ℕ} (s t : CoupledCoreIndex N) :
202 ∑ u : CoupledCoreIndex N, star (coupledBasisKet s u) * coupledBasisKet t u =
203 if s = t then 1 else 0 := by
204 by_cases h : s = t
205 · subst h
206 rw [show (∑ u : CoupledCoreIndex N, star (coupledBasisKet s u) * coupledBasisKet s u) =
207 ∑ u : CoupledCoreIndex N, coupledBasisKet s u by
208 apply Finset.sum_congr rfl
209 intro u hu
210 simp [coupledBasisKet]]
211 rw [Finset.sum_eq_single s]
212 · simp [coupledBasisKet]
213 · intro u hu hne
214 simp [coupledBasisKet, hne]
215 · intro hnot
216 exact absurd (Finset.mem_univ s) hnot
217 · rw [if_neg h]
218 apply Finset.sum_eq_zero
219 intro u hu
220 by_cases hs : u = s <;> by_cases ht : u = t
221 · subst hs; subst ht; contradiction
222 · subst hs
223 simp [coupledBasisKet, h]
224 · subst ht
225 simp [coupledBasisKet, hs]
226 · simp [coupledBasisKet, hs, ht]
227
228/-- The tensor-Weyl monomial sends a coupled basis ket to a phased shifted basis ket. -/
229theorem tensorWeylMonomial_basisKet {N : ℕ} (a b s : CoupledCoreIndex N) :
230 tensorWeylMonomial a b (coupledBasisKet s) =
231 (phaseCharacter b (addedConfig a s)) • coupledBasisKet (addedConfig a s) := by
232 ext t
233 by_cases ht : t = addedConfig a s
234 · subst ht
235 simp [tensorWeylMonomial, coupledBasisKet, shiftedConfig_addedConfig]
236 · have hshift : shiftedConfig a t ≠ s := by
237 intro hEq
238 apply ht
239 calc
240 t = addedConfig a (shiftedConfig a t) := by symm; exact addedConfig_shiftedConfig a t
241 _ = addedConfig a s := by rw [hEq]
242 simp [tensorWeylMonomial, coupledBasisKet, hshift, ht]
243
244/-- The local ququart Weyl monomial `X^a Z^b` written directly on the
245single-core carrier. -/
246def localWeylMonomial (a b : Fin 4) : QuquartState →ₗ[ℂ] QuquartState where
247 toFun := fun ψ s => Complex.I ^ (b.val * s.val) * ψ (sub4 s a)
248 map_add' := by
249 intro ψ χ
250 ext s
251 simp
252 ring
253 map_smul' := by
254 intro z ψ
255 ext s
256 simp
257 ring
258
259/-- Hilbert-Schmidt-style pairing on single-core operators in the standard
260ququart basis. -/
261def localOperatorInner (A B : QuquartState →ₗ[ℂ] QuquartState) : ℂ :=
262 ∑ s : Fin 4, ∑ t : Fin 4, star (A (basisKet s) t) * B (basisKet s) t
263
264/-- The standard ququart basis is orthonormal for the explicit finite sum. -/
265theorem basisKet_orthonormal (m n : Fin 4) :
266 ∑ t : Fin 4, star (basisKet m t) * basisKet n t = if m = n then 1 else 0 := by
267 fin_cases m <;> fin_cases n <;> simp [basisKet]
268
269/-- Mod-4 subtraction undoes mod-4 addition. -/
270theorem sub4_add4_cancel (a s : Fin 4) :
271 sub4 (add4 a s) a = s := by
272 fin_cases a <;> fin_cases s <;> rfl
273
274/-- Mod-4 addition undoes mod-4 subtraction. -/
275theorem add4_sub4_cancel (m a : Fin 4) :
276 add4 a (sub4 m a) = m := by
277 fin_cases m <;> fin_cases a <;> rfl
278
279/-- The local Weyl monomial sends a basis ket to a phased basis ket. -/
280theorem localWeylMonomial_basisKet (a b s : Fin 4) :
281 localWeylMonomial a b (basisKet s) =
282 (Complex.I ^ (b.val * (add4 a s).val)) • basisKet (add4 a s) := by
283 ext m
284 by_cases hm : m = add4 a s
285 · subst hm
286 simp [localWeylMonomial, basisKet, sub4_add4_cancel_core]
287 · have hsub : sub4 m a ≠ s := by
288 intro hEq
289 apply hm
290 calc
291 m = add4 a (sub4 m a) := by symm; exact add4_sub4_cancel_core m a
292 _ = add4 a s := by rw [hEq]
293 simp [localWeylMonomial, basisKet, hm, hsub]
294
295/-- For fixed `s`, the shift label `a` is recoverable from `add4 a s`. -/
296theorem add4_eq_add4_iff_left (a a' s : Fin 4) :
297 add4 a s = add4 a' s ↔ a = a' := by
298 exact add4_eq_add4_iff_left_core a a' s
299
300/-- Powers of `i` have unit modulus. -/
301lemma I_pow_star_mul_self (n : ℕ) :
302 star (Complex.I ^ n) * Complex.I ^ n = 1 := by
303 have hnorm : Complex.normSq (Complex.I ^ n) = 1 := by
304 simp [Complex.normSq_I]
305 have hconj : ((Complex.normSq (Complex.I ^ n) : ℂ) =
306 star (Complex.I ^ n) * Complex.I ^ n) := by
307 simpa using (Complex.normSq_eq_conj_mul_self (z := Complex.I ^ n))
308 rw [hnorm] at hconj
309 exact hconj.symm
310
311/-- Powers of `-i` factor through powers of `-1` and `i`. -/
312lemma neg_I_pow (n : ℕ) :
313 (-Complex.I) ^ n = (-1 : ℂ) ^ n * Complex.I ^ n := by
314 rw [show (-Complex.I) = (-1 : ℂ) * Complex.I by ring, mul_pow]
315
316lemma I_pow_five : Complex.I ^ 5 = Complex.I := by
317 simpa using (Complex.I_pow_eq_pow_mod 5)
318
319/-- Inner product of two scaled basis kets. -/
320lemma scaled_basisKet_inner (c d : ℂ) (m n : Fin 4) :
321 ∑ t : Fin 4, star ((c • basisKet m) t) * ((d • basisKet n) t) =
322 star c * d * (if m = n then 1 else 0) := by
323 calc
324 ∑ t : Fin 4, star ((c • basisKet m) t) * ((d • basisKet n) t)
325 = ∑ t : Fin 4, star c * d * (star (basisKet m t) * basisKet n t) := by
326 apply Finset.sum_congr rfl
327 intro t ht
328 simp [Pi.smul_apply]
329 ring
330 _ = star c * d * ∑ t : Fin 4, star (basisKet m t) * basisKet n t := by
331 rw [← Finset.mul_sum]
332 _ = star c * d * (if m = n then 1 else 0) := by
333 rw [basisKet_orthonormal]
334
335/-- Each local Weyl monomial has Hilbert-Schmidt norm squared `4`. -/
336theorem localWeylMonomial_self_inner (a b : Fin 4) :
337 localOperatorInner (localWeylMonomial a b) (localWeylMonomial a b) = 4 := by
338 unfold localOperatorInner
339 have hs : ∀ s : Fin 4,
340 ∑ t : Fin 4,
341 star ((localWeylMonomial a b (basisKet s)) t) *
342 (localWeylMonomial a b (basisKet s)) t = 1 := by
343 intro s
344 have hphase : (-Complex.I) ^ (b.val * (add4 a s).val) *
345 Complex.I ^ (b.val * (add4 a s).val) = 1 := by
346 simpa using I_pow_star_mul_self (b.val * (add4 a s).val)
347 have hinner :=
348 scaled_basisKet_inner
349 (Complex.I ^ (b.val * (add4 a s).val))
350 (Complex.I ^ (b.val * (add4 a s).val))
351 (add4 a s) (add4 a s)
352 calc
353 ∑ t : Fin 4,
354 star ((localWeylMonomial a b (basisKet s)) t) *
355 (localWeylMonomial a b (basisKet s)) t
356 = (-Complex.I) ^ (b.val * (add4 a s).val) *
357 Complex.I ^ (b.val * (add4 a s).val) := by
358 simpa [localWeylMonomial_basisKet] using hinner
359 _ = 1 := hphase
360 rw [Fin.sum_univ_four]
361 rw [hs 0, hs 1, hs 2, hs 3]
362 norm_num
363
364/-- Distinct shift labels force Hilbert-Schmidt orthogonality. -/
365theorem localWeylMonomial_shift_orthogonal {a a' : Fin 4} (h : a ≠ a') (b b' : Fin 4) :
366 localOperatorInner (localWeylMonomial a b) (localWeylMonomial a' b') = 0 := by
367 unfold localOperatorInner
368 apply Finset.sum_eq_zero
369 intro s hs
370 rw [localWeylMonomial_basisKet, localWeylMonomial_basisKet]
371 have hidx : add4 a s ≠ add4 a' s := by
372 intro hEq
373 exact h ((add4_eq_add4_iff_left a a' s).mp hEq)
374 have hinner :=
375 scaled_basisKet_inner
376 (Complex.I ^ (b.val * (add4 a s).val))
377 (Complex.I ^ (b'.val * (add4 a' s).val))
378 (add4 a s) (add4 a' s)
379 simpa [localWeylMonomial_basisKet, hidx] using hinner
380
381set_option maxHeartbeats 800000
382/-- Equal shifts but distinct phase labels are orthogonal in the one-core Weyl family. -/
383theorem localWeylMonomial_phase_orthogonal (a : Fin 4) {b b' : Fin 4} (h : b ≠ b') :
384 localOperatorInner (localWeylMonomial a b) (localWeylMonomial a b') = 0 := by
385 unfold localOperatorInner
386 have hs : ∀ s : Fin 4,
387 ∑ t : Fin 4,
388 star ((localWeylMonomial a b (basisKet s)) t) *
389 (localWeylMonomial a b' (basisKet s)) t =
390 (-Complex.I) ^ (b.val * (add4 a s).val) *
391 Complex.I ^ (b'.val * (add4 a s).val) := by
392 intro s
393 have hinner :=
394 scaled_basisKet_inner
395 (Complex.I ^ (b.val * (add4 a s).val))
396 (Complex.I ^ (b'.val * (add4 a s).val))
397 (add4 a s) (add4 a s)
398 simpa [localWeylMonomial_basisKet] using hinner
399 rw [Fin.sum_univ_four]
400 rw [hs 0, hs 1, hs 2, hs 3]
401 fin_cases a <;> fin_cases b <;> fin_cases b' <;>
402 simp at h <;>
403 simp [add4, neg_I_pow, Complex.I_pow_eq_pow_mod] <;>
404 ring_nf <;> simp [I_pow_five]
405set_option maxHeartbeats 200000
406
407/-- Full local orthogonality for distinct one-core Weyl labels. -/
408theorem localWeylMonomial_orthogonal_of_ne {a b a' b' : Fin 4}
409 (h : (a, b) ≠ (a', b')) :
410 localOperatorInner (localWeylMonomial a b) (localWeylMonomial a' b') = 0 := by
411 by_cases ha : a = a'
412 · subst ha
413 apply localWeylMonomial_phase_orthogonal
414 intro hb
415 apply h
416 simp [hb]
417 · exact localWeylMonomial_shift_orthogonal ha b b'
418
419/-- The local Weyl family has the expected cardinality `16`. -/
420theorem localWeylFamily_card :
421 Fintype.card (Fin 4 × Fin 4) = 16 := by decide
422
423/-- Inner product of two scaled coupled basis kets. -/
424lemma scaled_coupledBasisKet_inner {N : ℕ} (c d : ℂ)
425 (m n : CoupledCoreIndex N) :
426 ∑ t : CoupledCoreIndex N, star ((c • coupledBasisKet m) t) * ((d • coupledBasisKet n) t) =
427 star c * d * (if m = n then 1 else 0) := by
428 calc
429 ∑ t : CoupledCoreIndex N, star ((c • coupledBasisKet m) t) * ((d • coupledBasisKet n) t)
430 = ∑ t : CoupledCoreIndex N,
431 star c * d * (star (coupledBasisKet m t) * coupledBasisKet n t) := by
432 apply Finset.sum_congr rfl
433 intro t ht
434 simp [Pi.smul_apply]
435 ring
436 _ = star c * d * ∑ t : CoupledCoreIndex N,
437 star (coupledBasisKet m t) * coupledBasisKet n t := by
438 rw [← Finset.mul_sum]
439 _ = star c * d * (if m = n then 1 else 0) := by
440 rw [coupledBasisKet_orthonormal]
441
442/-- Distinct tensor-Weyl displacement labels send the same coupled basis state
443to orthogonal outputs. -/
444theorem tensorWeylMonomial_basis_image_orthogonal {N : ℕ}
445 {a a' : CoupledCoreIndex N} (h : a ≠ a') (b b' : CoupledCoreIndex N)
446 (s : CoupledCoreIndex N) :
447 ∑ t : CoupledCoreIndex N,
448 star ((tensorWeylMonomial a b (coupledBasisKet s)) t) *
449 (tensorWeylMonomial a' b' (coupledBasisKet s)) t = 0 := by
450 rw [tensorWeylMonomial_basisKet, tensorWeylMonomial_basisKet]
451 have hidx : addedConfig a s ≠ addedConfig a' s := by
452 intro hEq
453 exact h ((addedConfig_eq_addedConfig_iff_left a a' s).mp hEq)
454 have hinner :=
455 scaled_coupledBasisKet_inner
456 (phaseCharacter b (addedConfig a s))
457 (phaseCharacter b' (addedConfig a' s))
458 (addedConfig a s) (addedConfig a' s)
459 simpa [hidx] using hinner
460
461/-- Hilbert-Schmidt-style pairing on coupled-core operators. -/
462def coupledOperatorInner {N : ℕ}
463 (A B : CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N) : ℂ :=
464 ∑ s : CoupledCoreIndex N, ∑ t : CoupledCoreIndex N,
465 star (A (coupledBasisKet s) t) * B (coupledBasisKet s) t
466
467/-- The coupled phase character has unit modulus. -/
468lemma phaseCharacter_star_mul_self {N : ℕ} (b s : CoupledCoreIndex N) :
469 star (phaseCharacter b s) * phaseCharacter b s = 1 := by
470 have hnorm : Complex.normSq (phaseCharacter b s) = 1 := by
471 unfold phaseCharacter
472 rw [map_prod Complex.normSq]
473 apply Finset.prod_eq_one
474 intro x hx
475 simp [Complex.normSq_I]
476 have hconj := Complex.normSq_eq_conj_mul_self (z := phaseCharacter b s)
477 rw [hnorm] at hconj
478 exact hconj.symm
479
480/-- A tensor-Weyl monomial has Hilbert-Schmidt norm squared equal to the
481dimension of the coupled-core carrier. -/
482theorem tensorWeylMonomial_self_inner {N : ℕ} (a b : CoupledCoreIndex N) :
483 coupledOperatorInner (tensorWeylMonomial a b) (tensorWeylMonomial a b) =
484 Fintype.card (CoupledCoreIndex N) := by
485 unfold coupledOperatorInner
486 have hs : ∀ s : CoupledCoreIndex N,
487 ∑ t : CoupledCoreIndex N,
488 star ((tensorWeylMonomial a b (coupledBasisKet s)) t) *
489 (tensorWeylMonomial a b (coupledBasisKet s)) t = 1 := by
490 intro s
491 let c := phaseCharacter b (addedConfig a s)
492 let m := addedConfig a s
493 have hinner := scaled_coupledBasisKet_inner c c m m
494 rw [if_pos rfl, mul_one] at hinner
495 calc
496 ∑ t : CoupledCoreIndex N,
497 star ((tensorWeylMonomial a b (coupledBasisKet s)) t) *
498 (tensorWeylMonomial a b (coupledBasisKet s)) t
499 = ∑ t : CoupledCoreIndex N,
500 star ((c • coupledBasisKet m) t) * ((c • coupledBasisKet m) t) := by
501 rw [tensorWeylMonomial_basisKet]
502 _ = star c * c := hinner
503 _ = 1 := phaseCharacter_star_mul_self b (addedConfig a s)
504 calc
505 ∑ s : CoupledCoreIndex N, ∑ t : CoupledCoreIndex N,
506 star ((tensorWeylMonomial a b (coupledBasisKet s)) t) *
507 (tensorWeylMonomial a b (coupledBasisKet s)) t
508 = ∑ _s : CoupledCoreIndex N, (1 : ℂ) := by
509 apply Finset.sum_congr rfl; intro s _; exact hs s
510 _ = Fintype.card (CoupledCoreIndex N) := by
511 rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]
512
513/-- Distinct coupled tensor-Weyl displacement labels are orthogonal in the
514Hilbert-Schmidt pairing. -/
515theorem tensorWeylMonomial_shift_orthogonal {N : ℕ}
516 {a a' : CoupledCoreIndex N} (h : a ≠ a') (b b' : CoupledCoreIndex N) :
517 coupledOperatorInner (tensorWeylMonomial a b) (tensorWeylMonomial a' b') = 0 := by
518 unfold coupledOperatorInner
519 apply Finset.sum_eq_zero
520 intro s hs
521 exact tensorWeylMonomial_basis_image_orthogonal h b b' s
522
523/-- Enumeration of the coupled-core basis by a finite index. -/
524def coupledCoreEquivFin (N : ℕ) :
525 CoupledCoreIndex N ≃ Fin (Fintype.card (CoupledCoreIndex N)) :=
526 Fintype.equivFin (CoupledCoreIndex N)
527
528/-- Zero-pad a finite-dimensional state into a coupled-core carrier. -/
529def embedState {d N : ℕ} (_h : d ≤ Fintype.card (CoupledCoreIndex N)) :
530 (Fin d → ℂ) →ₗ[ℂ] CoupledCoreSpace N where
531 toFun := fun v s =>
532 let i := coupledCoreEquivFin N s
533 if hi : i.val < d then v ⟨i.val, hi⟩ else 0
534 map_add' := by
535 intro v w
536 ext s
537 dsimp [coupledCoreEquivFin]
538 split_ifs <;> simp
539 map_smul' := by
540 intro z v
541 ext s
542 dsimp [coupledCoreEquivFin]
543 split_ifs <;> simp
544
545/-- Restrict a coupled-core state back to the first `d` coordinates of the
546enumerated basis. -/
547def projectState {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N)) :
548 CoupledCoreSpace N →ₗ[ℂ] (Fin d → ℂ) where
549 toFun := fun ψ i => ψ ((coupledCoreEquivFin N).symm (Fin.castLE h i))
550 map_add' := by
551 intro ψ χ
552 ext i
553 rfl
554 map_smul' := by
555 intro z ψ
556 ext i
557 rfl
558
559/-- Projection recovers the original state after zero-padding. -/
560theorem projectState_embedState {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
561 (v : Fin d → ℂ) :
562 projectState h (embedState h v) = v := by
563 ext i
564 unfold projectState embedState
565 simp [coupledCoreEquivFin]
566
567/-- Zero-padding is injective. -/
568theorem embedState_injective {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N)) :
569 Function.Injective (embedState h) := by
570 intro v w hEq
571 have hproj := congrArg (projectState h) hEq
572 simpa [projectState_embedState] using hproj
573
574/-- Lift a finite-dimensional linear operator to the coupled-core carrier by
575zero-padding, acting, and projecting back. -/
576def liftOperator {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
577 (T : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ)) :
578 CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N :=
579 (embedState h).comp (T.comp (projectState h))
580
581/-- The lifted operator acts exactly like the original operator on the embedded
582subspace. -/
583theorem liftOperator_intertwines {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
584 (T : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ)) (v : Fin d → ℂ) :
585 liftOperator h T (embedState h v) = embedState h (T v) := by
586 unfold liftOperator
587 simp [projectState_embedState]
588
589/-- The obvious capacity bound: `d ≤ 4^d`. -/
590theorem self_le_four_pow_self : ∀ d : ℕ, d ≤ 4 ^ d
591 | 0 => by norm_num
592 | d + 1 =>
593 let m := 4 ^ d
594 have hm : d ≤ m := self_le_four_pow_self d
595 have hm_pos : 1 ≤ m := by
596 dsimp [m]
597 exact Nat.succ_le_of_lt (pow_pos (by norm_num) _)
598 have hstep : d + 1 ≤ m + m := by
599 omega
600 calc
601 d + 1 ≤ m + m := hstep
602 _ ≤ 4 * m := by omega
603 _ = 4 ^ (d + 1) := by
604 dsimp [m]
605 rw [pow_succ]
606 ring
607
608/-- Any finite-dimensional linear dynamics embeds exactly into a coupled-core
609carrier with enough ququart capacity. Here we use `N = d`, since `d ≤ 4^d`. -/
610theorem finite_dimensional_exact_embedding (d : ℕ)
611 (T : (Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ)) :
612 ∃ L : CoupledCoreSpace d →ₗ[ℂ] CoupledCoreSpace d,
613 ∀ v : Fin d → ℂ,
614 L (embedState (N := d) (by simpa [coupledCoreIndex_card] using self_le_four_pow_self d) v) =
615 embedState (N := d) (by simpa [coupledCoreIndex_card] using self_le_four_pow_self d) (T v) := by
616 let hcap : d ≤ Fintype.card (CoupledCoreIndex d) := by
617 simpa [coupledCoreIndex_card] using self_le_four_pow_self d
618 refine ⟨liftOperator (N := d) hcap T, ?_⟩
619 intro v
620 exact liftOperator_intertwines (N := d) hcap T v
621
622end
623
624end CoupledRecognitionCores
625end Foundation
626end IndisputableMonolith
627