QuantumPacketCore.lean

1 module
2 
3 public import Mathlib.Algebra.Star.BigOperators
4 public import Mathlib.LinearAlgebra.Matrix.Trace
5 public import Mathlib.LinearAlgebra.Matrix.ConjTranspose
6 public import Mathlib.Analysis.Normed.Algebra.Exponential
7 public import Mathlib.Tactic.NoncommRing
8 
9 /-!
10 Author: Komorebi P.
11 Paper VII, first checked block. Finite packet algebra, arbitrary finite circuit
12 length, both unitarity identities, symmetry and dephasing. No physical continuum
13 claim is encoded here. Multiplication is operator composition, NOT commutative.
14 -/
15 
16 public section
17 set_option autoImplicit false
18 namespace KomorebiPaperVII
19 open scoped BigOperators
20 
21 /-- Finite exact idempotent resolution; adjoint conditions are supplied separately. -/
22 structure PacketFamily (R I : Type*) [Ring R] [Fintype I] [DecidableEq I] where
23   proj : I → R
24   mul_proj : ∀ i j, proj i * proj j = if i = j then proj i else 0
25   sum_proj : ∑ i, proj i = 1
26 
27 namespace PacketFamily
28 section Algebra
29 variable {R I : Type*} [Ring R] [Fintype I] [DecidableEq I]
30 variable (P : PacketFamily R I)
31 
32 @[simp] theorem idempotent (i : I) : P.proj i * P.proj i = P.proj i := by
33   simp [P.mul_proj]
34 
35 /-- Target index precedes source index. -/
36 def block (U : R) (b a : I) : R := P.proj b * U * P.proj a
37 
38 theorem reconstruct (U : R) : (∑ b, ∑ a, P.block U b a) = U := by
39   simp only [block, ← Finset.mul_sum, P.sum_proj, mul_one, ← Finset.sum_mul, one_mul]
40 
41 theorem compose_blocks (U V : R) (b a : I) :
42     P.block (U * V) b a = ∑ c, P.block U b c * P.block V c a := by
43   have term (c : I) : P.block U b c * P.block V c a =
44       P.proj b * U * P.proj c * V * P.proj a := by
45     unfold block
46     calc
47       _ = P.proj b * U * (P.proj c * P.proj c) * V * P.proj a := by noncomm_ring
48       _ = _ := by rw [P.idempotent]
49   simp_rw [term]
50   simp only [← Finset.sum_mul, ← Finset.mul_sum, P.sum_proj, block, mul_assoc, one_mul]
51 
52 /-- Gates are listed from latest to earliest: [Um,...,U1]. -/
53 def circuit : List R → R
54   | [] => 1
55   | U :: Us => U * circuit Us
56 
57 /-- An explicit nested finite sum. The zero-gate case fixes the boundary packet. -/
58 def pathSum : List R → I → I → R
59   | [], b, a => P.proj b * P.proj a
60   | U :: Us, b, a => ∑ c, P.block U b c * pathSum Us c a
61 
62 /-- Theorem 4.1, all finite depths, not merely a two-gate example. -/
63 theorem circuit_path_expansion (Us : List R) (b a : I) :
64     P.block (circuit Us) b a = P.pathSum Us b a := by
65   induction Us generalizing b a with
66   | nil => simp [circuit, pathSum, block]
67   | cons U Us ih =>
68       simp only [circuit, pathSum, P.compose_blocks, ih]
69 
70 theorem circuit_reconstruction (Us : List R) :
71     (∑ b, ∑ a, P.pathSum Us b a) = circuit Us := by
72   simp_rw [← P.circuit_path_expansion]
73   exact P.reconstruct _
74 
75 /-- Algebraic part of Theorem 5.1. -/
76 theorem symmetry_no_transfer (H : R) (hH : ∀ i, H * P.proj i = P.proj i * H)
77     (b a : I) (hba : b ≠ a) : P.block H b a = 0 := by
78   simp [block, ← hH b, mul_assoc, P.mul_proj, hba]
79 
80 theorem symmetry_diagonal (H : R) (hH : ∀ i, H * P.proj i = P.proj i * H) :
81     (∑ a, P.block H a a) = H := by
82   have term (a : I) : P.block H a a = H * P.proj a := by
83     rw [block, ← hH a, mul_assoc, P.idempotent]
84   simp_rw [term]
85   rw [← Finset.mul_sum, P.sum_proj, mul_one]
86 
87 /-- The dephasing map discards only off-diagonal packet corners. -/
88 def dephase (rho : R) : R := ∑ a, P.block rho a a
89 
90 theorem dephase_idempotent (rho : R) : P.dephase (P.dephase rho) = P.dephase rho := by
91   unfold dephase block
92   simp only [Finset.mul_sum, Finset.sum_mul]
93   have term (a b : I) : P.proj a * (P.proj b * rho * P.proj b) * P.proj a =
94       if a = b then P.proj a * rho * P.proj a else 0 := by
95     by_cases hab : a = b
96     · subst b
97       simp only [ite_true]
98       calc
99         _ = (P.proj a * P.proj a) * rho * (P.proj a * P.proj a) := by noncomm_ring
100         _ = _ := by rw [P.idempotent]
101     · calc
102         _ = (P.proj a * P.proj b) * rho * (P.proj b * P.proj a) := by noncomm_ring
103         _ = _ := by simp [P.mul_proj, hab]
104   simp_rw [term]
105   simp
106 
107 end Algebra
108 
109 section Adjoint
110 variable {R I : Type*} [Ring R] [StarRing R] [Fintype I] [DecidableEq I]
111 variable (P : PacketFamily R I) (hstar : ∀ i, star (P.proj i) = P.proj i)
112 include hstar
113 
114 theorem adjoint_block (U : R) (b a : I) :
115     star (P.block U b a) = P.block (star U) a b := by
116   simp only [block, star_mul, hstar, mul_assoc]
117 
118 /-- The column identity in Theorem 4.2. Only U*U=1 is needed here. -/
119 theorem unitarity_columns (U : R) (hU : star U * U = 1) (a c : I) :
120     (∑ b, star (P.block U b a) * P.block U b c) =
121       if a = c then P.proj a else 0 := by
122   have term (b : I) : star (P.block U b a) * P.block U b c =
123       P.proj a * star U * P.proj b * U * P.proj c := by
124     rw [P.adjoint_block hstar]
125     unfold block
126     calc
127       _ = P.proj a * star U * (P.proj b * P.proj b) * U * P.proj c := by noncomm_ring
128       _ = _ := by rw [P.idempotent]
129   simp_rw [term]
130   rw [← Finset.sum_mul, ← Finset.sum_mul, ← Finset.mul_sum, P.sum_proj, mul_one]
131   rw [mul_assoc (P.proj a), hU, mul_one, P.mul_proj]
132 
133 /-- The row identity in Theorem 4.2. Only UU*=1 is needed here. -/
134 theorem unitarity_rows (U : R) (hU : U * star U = 1) (b d : I) :
135     (∑ a, P.block U b a * star (P.block U d a)) =
136       if b = d then P.proj b else 0 := by
137   have term (a : I) : P.block U b a * star (P.block U d a) =
138       P.proj b * U * P.proj a * star U * P.proj d := by
139     rw [P.adjoint_block hstar]
140     unfold block
141     calc
142       _ = P.proj b * U * (P.proj a * P.proj a) * star U * P.proj d := by noncomm_ring
143       _ = _ := by rw [P.idempotent]
144   simp_rw [term]
145   rw [← Finset.sum_mul, ← Finset.sum_mul, ← Finset.mul_sum, P.sum_proj, mul_one]
146   rw [mul_assoc (P.proj b), hU, mul_one, P.mul_proj]
147 
148 end Adjoint
149 
150 section Dynamics
151 variable {R I : Type*} [NormedRing R] [NormedAlgebra ℂ R]
152 variable [Fintype I] [DecidableEq I]
153 variable (P : PacketFamily R I)
154 
155 /-- Commutation propagates to the actual operator exponential, not an assumed flow. -/
156 theorem symmetry_exponential_commutes (H : R)
157     (hH : ∀ i, H * P.proj i = P.proj i * H) (z : ℂ) (i : I) :
158     NormedSpace.exp (z • H) * P.proj i = P.proj i * NormedSpace.exp (z • H) := by
159   have h : Commute H (P.proj i) := hH i
160   exact (h.smul_left z).exp_left.eq
161 
162 /-- Theorem 5.1 includes real-time Schrodinger evolution by z = -it. -/
163 theorem symmetry_exponential_diagonal (H : R)
164     (hH : ∀ i, H * P.proj i = P.proj i * H) (z : ℂ) :
165     (∑ a, P.block (NormedSpace.exp (z • H)) a a) = NormedSpace.exp (z • H) :=
166   P.symmetry_diagonal _ (P.symmetry_exponential_commutes H hH z)
167 
168 theorem symmetry_exponential_no_transfer (H : R)
169     (hH : ∀ i, H * P.proj i = P.proj i * H) (z : ℂ)
170     (b a : I) (hba : b ≠ a) : P.block (NormedSpace.exp (z • H)) b a = 0 :=
171   P.symmetry_no_transfer _ (P.symmetry_exponential_commutes H hH z) b a hba
172 
173 end Dynamics
174 end PacketFamily
175 
176 section Measurement
177 variable {n I : Type*} [Fintype n] [DecidableEq n] [Fintype I] [DecidableEq I]
178 variable (P : PacketFamily (Matrix n n ℂ) I)
179 
180 /-- Concrete complex-matrix specialization, with adjoint = conjugate transpose. -/
181 theorem matrix_unitarity_columns (hstar : ∀ i, (P.proj i).conjTranspose = P.proj i)
182     (U : Matrix n n ℂ) (hU : U.conjTranspose * U = 1) (a c : I) :
183     (∑ b, (P.block U b a).conjTranspose * P.block U b c) =
184       if a = c then P.proj a else 0 := by
185   exact P.unitarity_columns hstar U hU a c
186 
187 /-- The second conservation identity for finite complex matrices. -/
188 theorem matrix_unitarity_rows (hstar : ∀ i, (P.proj i).conjTranspose = P.proj i)
189     (U : Matrix n n ℂ) (hU : U * U.conjTranspose = 1) (b d : I) :
190     (∑ a, P.block U b a * (P.block U d a).conjTranspose) =
191       if b = d then P.proj b else 0 := by
192   exact P.unitarity_rows hstar U hU b d
193 
194 /-- Trace duality for dephasing, valid for all matrices, not only density matrices. -/
195 theorem dephase_trace_duality (E rho : Matrix n n ℂ) :
196     Matrix.trace (P.dephase E * rho) = Matrix.trace (E * P.dephase rho) := by
197   unfold PacketFamily.dephase PacketFamily.block
198   simp only [Finset.sum_mul, Finset.mul_sum, Matrix.trace_sum]
199   apply Finset.sum_congr rfl
200   intro a _
201   calc
202     _ = Matrix.trace ((E * P.proj a * rho) * P.proj a) := by
203       rw [show P.proj a * E * P.proj a * rho =
204         P.proj a * (E * P.proj a * rho) by noncomm_ring, Matrix.trace_mul_comm]
205     _ = _ := by congr 1; noncomm_ring
206 
207 /-- Theorem 7.1, exactly the stated block-diagonal-observable hypothesis. -/
208 theorem measurement_invariance (E rho : Matrix n n ℂ) (hE : P.dephase E = E) :
209     Matrix.trace (E * rho) = Matrix.trace (E * P.dephase rho) := by
210   rw [← hE] at ⊢
211   simpa only [P.dephase_idempotent] using dephase_trace_duality P (P.dephase E) rho
212 
213 theorem dephase_trace_preserving (rho : Matrix n n ℂ) :
214     Matrix.trace (P.dephase rho) = Matrix.trace rho := by
215   have h : P.dephase 1 = 1 := by
216     simp only [PacketFamily.dephase, PacketFamily.block, mul_one, P.idempotent, P.sum_proj]
217   simpa only [Matrix.one_mul] using (measurement_invariance P 1 rho h).symm
218 
219 end Measurement
220 
221 end KomorebiPaperVII
222 
223 /-! Exported theorem axiom audit. -/
224 #print axioms KomorebiPaperVII.PacketFamily.idempotent
225 #print axioms KomorebiPaperVII.PacketFamily.reconstruct
226 #print axioms KomorebiPaperVII.PacketFamily.compose_blocks
227 #print axioms KomorebiPaperVII.PacketFamily.circuit_path_expansion
228 #print axioms KomorebiPaperVII.PacketFamily.circuit_reconstruction
229 #print axioms KomorebiPaperVII.PacketFamily.symmetry_no_transfer
230 #print axioms KomorebiPaperVII.PacketFamily.symmetry_diagonal
231 #print axioms KomorebiPaperVII.PacketFamily.dephase_idempotent
232 #print axioms KomorebiPaperVII.PacketFamily.adjoint_block
233 #print axioms KomorebiPaperVII.PacketFamily.unitarity_columns
234 #print axioms KomorebiPaperVII.PacketFamily.unitarity_rows
235 #print axioms KomorebiPaperVII.PacketFamily.symmetry_exponential_commutes
236 #print axioms KomorebiPaperVII.PacketFamily.symmetry_exponential_diagonal
237 #print axioms KomorebiPaperVII.PacketFamily.symmetry_exponential_no_transfer
238 #print axioms KomorebiPaperVII.matrix_unitarity_columns
239 #print axioms KomorebiPaperVII.matrix_unitarity_rows
240 #print axioms KomorebiPaperVII.dephase_trace_duality
241 #print axioms KomorebiPaperVII.measurement_invariance
242 #print axioms KomorebiPaperVII.dephase_trace_preserving

Back to source controls