SemanticBridge.lean

1 import FiniteFourier
2 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
3 import Mathlib.LinearAlgebra.Matrix.ConjTranspose
4 import Mathlib.Tactic.Ring
5 
6 set_option autoImplicit false
7 set_option maxRecDepth 100000
8 set_option maxHeartbeats 2000000
9 
10 open scoped BigOperators Matrix
11 
12 namespace Komorebi.QuantumArithmetic
13 
14 /-- The exact coordinate arithmetic is interpreted in the ordinary complex numbers. -/
15 noncomputable def interpret (x : Cyclo12) : ℂ :=
16   ⟨(x.a : ℝ) + (x.b : ℝ) * Real.sqrt 3,
17    (x.c : ℝ) + (x.d : ℝ) * Real.sqrt 3⟩
18 
19 @[simp] theorem interpret_zero : interpret cZero = 0 := by
20   apply Complex.ext <;> simp [interpret, cZero]
21 
22 @[simp] theorem interpret_one : interpret cOne = 1 := by
23   apply Complex.ext <;> simp [interpret, cOne]
24 
25 @[simp] theorem interpret_rat (r : ℚ) : interpret (cRat r) = (r : ℂ) := by
26   apply Complex.ext <;> simp [interpret, cRat]
27 
28 @[simp] theorem interpret_add (x y : Cyclo12) :
29     interpret (cAdd x y) = interpret x + interpret y := by
30   apply Complex.ext <;> simp [interpret, cAdd] <;> ring
31 
32 @[simp] theorem interpret_mul (x y : Cyclo12) :
33     interpret (cMul x y) = interpret x * interpret y := by
34   apply Complex.ext <;> simp [interpret, cMul, Complex.mul_re, Complex.mul_im] <;>
35     ring_nf <;> norm_num [Real.sq_sqrt]
36 
37 @[simp] theorem interpret_conj (x : Cyclo12) :
38     interpret (cConj x) = star (interpret x) := by
39   apply Complex.ext <;> simp [interpret, cConj]
40   ring
41 
42 @[simp] theorem interpret_pow (x : Cyclo12) (n : Nat) :
43     interpret (cPow x n) = interpret x ^ n := by
44   induction n with
45   | zero => simp [cPow]
46   | succ n ih => simp [cPow, ih, pow_succ]
47 
48 @[simp] theorem interpret_sum (xs : List Cyclo12) :
49     interpret (cSum xs) = (xs.map interpret).sum := by
50   induction xs with
51   | nil => simp [cSum]
52   | cons x xs ih => simp [cSum, ih]
53 
54 @[simp] theorem interpret_kSum (f : Index → Cyclo12) :
55     interpret (kSum f) = ∑ i, interpret (f i) := by
56   simp only [kSum, interpret_sum, List.map_ofFn, List.sum_ofFn]
57   rfl
58 
59 noncomputable def complexMatrix (A : KMatrix) : Matrix Index Index ℂ :=
60   fun i j => interpret (A i j)
61 
62 noncomputable def complexVector (v : KVector) : Index → ℂ :=
63   fun i => interpret (v i)
64 
65 @[simp] theorem complexMatrix_mul (A B : KMatrix) :
66     complexMatrix (kMatMul A B) = complexMatrix A * complexMatrix B := by
67   ext i j
68   simp [complexMatrix, kMatMul, Matrix.mul_apply]
69 
70 @[simp] theorem complexMatrix_adjoint (A : KMatrix) :
71     complexMatrix (kAdjoint A) = (complexMatrix A)ᴴ := by
72   ext i j
73   simp [complexMatrix, kAdjoint, Matrix.conjTranspose_apply]
74 
75 @[simp] theorem complexMatrix_identity :
76     complexMatrix kIdentity = 1 := by
77   ext i j
78   by_cases h : i = j <;> simp [complexMatrix, kIdentity, h, Matrix.one_apply]
79 
80 @[simp] theorem complexVector_mul (A : KMatrix) (v : KVector) :
81     complexVector (kMatVec A v) = (complexMatrix A).mulVec (complexVector v) := by
82   ext i
83   simp [complexVector, complexMatrix, kMatVec, Matrix.mulVec, dotProduct]
84 
85 noncomputable def F : Matrix Index Index ℂ := complexMatrix exactFourier
86 noncomputable def P : Matrix Index Index ℂ := complexMatrix exactProjector
87 noncomputable def D : Matrix Index Index ℂ :=
88   Matrix.diagonal (fun i => if Nat.gcd i.val 12 = 1 then 1 else 0)
89 noncomputable def psi : Index → ℂ := complexVector exactPsi
90 noncomputable def chi : Index → ℂ := complexVector exactChi
91 noncomputable def unitState : Index → ℂ := complexVector exactUnitState
92 
93 /-- Actual complex unitarity, not an assertion only about the coordinate checker. -/
94 theorem fourier_unitary_left : Fᴴ * F = 1 := by
95   have h : kMatMul (kAdjoint exactFourier) exactFourier = kIdentity :=
96     funext (fun i => funext (normalized_fourier_left i))
97   simpa [F] using congrArg complexMatrix h
98 
99 theorem fourier_unitary_right : F * Fᴴ = 1 := by
100   have h : kMatMul exactFourier (kAdjoint exactFourier) = kIdentity :=
101     funext (fun i => funext (normalized_fourier_right i))
102   simpa [F] using congrArg complexMatrix h
103 
104 theorem projector_transport : F * D * Fᴴ = P := by
105   ext i j
106   have h := congrArg interpret (exact_projector_transport i j)
107   simp only [selectedKernel, interpret_kSum] at h
108   rw [Matrix.mul_apply]
109   simpa [D, P, F, complexMatrix, Matrix.mul_diagonal, Matrix.conjTranspose_apply,
110     apply_ite interpret, mul_ite] using h
111 
112 theorem state_preparation : F.mulVec unitState = psi := by
113   have h : kMatVec exactFourier exactUnitState = exactPsi :=
114     funext exact_state_preparation
115   simpa [F, unitState, psi] using congrArg complexVector h
116 
117 theorem state_recovery : Fᴴ.mulVec psi = unitState := by
118   have h : kMatVec (kAdjoint exactFourier) exactPsi = exactUnitState :=
119     funext exact_state_recovery
120   simpa [F, unitState, psi] using congrArg complexVector h
121 
122 @[simp] theorem interpret_normSq (z : Cyclo12) :
123     interpret (kNormSq z) = (Complex.normSq (interpret z) : ℂ) := by
124   simp only [kNormSq, interpret_mul, interpret_conj]
125   exact Complex.normSq_eq_conj_mul_self.symm
126 
127 noncomputable def totalProbability (v : Index → ℂ) : ℝ :=
128   ∑ i, Complex.normSq (v i)
129 
130 noncomputable def coprimeProbability (v : Index → ℂ) : ℝ :=
131   ∑ i, if Nat.gcd i.val 12 = 1 then Complex.normSq (v i) else 0
132 
133 @[simp] theorem interpret_mass (v : KVector) :
134     interpret (kMass v) = (totalProbability (complexVector v) : ℂ) := by
135   simp [kMass, totalProbability, complexVector]
136 
137 @[simp] theorem interpret_coprimeMass (v : KVector) :
138     interpret (kCoprimeMass v) = (coprimeProbability (complexVector v) : ℂ) := by
139   simp only [kCoprimeMass, interpret_kSum, coprimeProbability, Complex.ofReal_sum]
140   apply Finset.sum_congr rfl
141   intro i hi
142   by_cases h : Nat.gcd i.val 12 = 1 <;>
143     simp [h, complexVector]
144 
145 theorem psi_normalized : totalProbability psi = 1 := by
146   have h := congrArg interpret exact_psi_normalized
147   simpa [psi] using congrArg Complex.re h
148 
149 theorem chi_normalized : totalProbability chi = 1 := by
150   have h := congrArg interpret exact_chi_normalized
151   simpa [chi] using congrArg Complex.re h
152 
153 theorem unitState_normalized : totalProbability unitState = 1 := by
154   have h := congrArg interpret exact_unit_normalized
155   simpa [unitState] using congrArg Complex.re h
156 
157 theorem same_initial_probabilities (i : Index) :
158     Complex.normSq (psi i) = Complex.normSq (chi i) := by
159   have h := congrArg interpret (exact_same_initial_probabilities i)
160   simpa [psi, chi, complexVector] using congrArg Complex.re h
161 
162 theorem states_orthogonal : ∑ i, star (psi i) * chi i = 0 := by
163   have h := congrArg interpret exact_orthogonal_states
164   simpa [psi, chi, complexVector] using h
165 
166 theorem signed_state_recovers_arithmetic :
167     coprimeProbability (Fᴴ.mulVec psi) = 1 := by
168   have h := congrArg interpret exact_coprime_mass_psi
169   simpa [F, psi] using congrArg Complex.re h
170 
171 theorem unsigned_state_erases_arithmetic :
172     coprimeProbability (Fᴴ.mulVec chi) = 0 := by
173   have h := congrArg interpret exact_coprime_mass_chi
174   simpa [F, chi] using congrArg Complex.re h
175 
176 theorem projector_fixes_psi : P.mulVec psi = psi := by
177   have h : kMatVec exactProjector exactPsi = exactPsi :=
178     funext exact_projector_fixes_psi
179   simpa [P, psi] using congrArg complexVector h
180 
181 theorem projector_kills_chi : P.mulVec chi = 0 := by
182   have h : kMatVec exactProjector exactChi = fun _ => cZero :=
183     funext exact_projector_kills_chi
184   have hh := congrArg complexVector h
185   rw [complexVector_mul] at hh
186   change P.mulVec chi = complexVector (fun _ => cZero) at hh
187   rw [hh]
188   funext i
189   exact interpret_zero
190 
191 end Komorebi.QuantumArithmetic

Back to source controls