QuantumStateBridge.lean

1 module
2 public import KnillLaflammeNecessity
3 import all KnillLaflammeNecessity
4 import all KnillLaflammeSufficiency
5 public import Mathlib.Tactic
6 /-! Author: Komorebi P. Paper VII fifth block.
7 State-space versus operator-space exact correction: polarization and normalization.
8 -/
9 public section
10 set_option autoImplicit false
11 set_option backward.isDefEq.respectTransparency false
12 set_option backward.isDefEq.respectTransparency.types false
13 set_option linter.unusedSectionVars false
14 namespace KomorebiPaperVII.KnillLaflamme
15 open scoped BigOperators ComplexOrder
16 open Matrix
17 variable {n : Type*} [Fintype n] [DecidableEq n]
18 
19 def pure (x : n → ℂ) : Matrix n n ℂ := Matrix.vecMulVec x (star x)
20 
21 theorem outer_polarization (x y : n → ℂ) :
22     (4 : ℂ) • Matrix.vecMulVec x (star y) =
23       pure (x+y) - pure (x-y) + Complex.I • (pure (x+Complex.I • y) - pure (x-Complex.I • y)) := by
24   ext i j
25   simp [pure, Matrix.vecMulVec, star_add, star_sub]
26   ring_nf
27   simp [Complex.I_sq]
28   ring
29 
30 theorem linearMap_eq_of_pure (f g : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ)
31     (h : ∀ x, f (pure x)=g (pure x)) : f=g := by
32   have outer (x y : n → ℂ) : f (Matrix.vecMulVec x (star y))=g (Matrix.vecMulVec x (star y)) := by
33     apply (smul_right_injective (M := Matrix n n ℂ) (by norm_num : (4 : ℂ) ≠ 0))
34     change (4 : ℂ) • f (Matrix.vecMulVec x (star y)) = (4 : ℂ) • g (Matrix.vecMulVec x (star y))
35     rw [← map_smul, ← map_smul, outer_polarization]
36     simp only [map_add, map_sub, map_smul, h]
37   have single (i j : n) (c : ℂ) : f (Matrix.single i j c)=g (Matrix.single i j c) := by
38     have hh := outer (Pi.single i c) (Pi.single j 1)
39     have hs : Matrix.vecMulVec (Pi.single i c) (star (Pi.single j (1 : ℂ))) = Matrix.single i j c := by
40       ext a b
41       by_cases ha : i=a <;> by_cases hb : j=b <;>
42         simp [Matrix.vecMulVec, Pi.single_apply, ha, hb, eq_comm]
43     rwa [hs] at hh
44   ext rho i j
45   have heq : f rho=g rho := by
46     conv_lhs => rw [Matrix.matrix_eq_sum_single rho]
47     conv_rhs => rw [Matrix.matrix_eq_sum_single rho]
48     simp only [map_sum, single]
49   exact congrArg (fun M : Matrix n n ℂ => M i j) heq
50 
51 
52 /-- Finite Kraus sums as an actual complex-linear map. -/
53 def noiseLinear {I : Type*} [Fintype I] (E : I → Matrix n n ℂ) :
54     Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ where
55   toFun := noise E
56   map_add' x y := by simp [noise, mul_add, add_mul, Finset.sum_add_distrib]
57   map_smul' c x := by simp [noise, Finset.smul_sum]
58 
59 def sandwichLinear (P : Matrix n n ℂ) : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ where
60   toFun := fun rho => P*rho*star P
61   map_add' x y := by simp [mul_add, add_mul]
62   map_smul' c x := by simp
63 
64 theorem sandwich_pure (P : Matrix n n ℂ) (x : n → ℂ) :
65     sandwichLinear P (pure x)=pure (P *ᵥ x) := by
66   simp only [sandwichLinear, LinearMap.coe_mk, AddHom.coe_mk, pure, Matrix.mul_vecMulVec, Matrix.vecMulVec_mul, star_mulVec]
67   rfl
68 
69 /-- Normalization is removed by linearity, including the zero positive matrix. -/
70 theorem fixes_positive_of_density (P : Matrix n n ℂ)
71     (L : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ)
72     (hfix : ∀ rho : Matrix n n ℂ, rho.PosSemidef → Matrix.trace rho=1 → P*rho*P=rho → L rho=rho)
73     (rho : Matrix n n ℂ) (hpos : rho.PosSemidef) (hsupport : P*rho*P=rho) : L rho=rho := by
74   by_cases hz : rho=0
75   · simp [hz]
76   have htr : Matrix.trace rho ≠ 0 := (hpos.trace_eq_zero_iff).not.mpr hz
77   have hreal : ((Matrix.trace rho).re : ℂ)=Matrix.trace rho := by
78     apply Complex.ext
79     · simp
80     · simpa using (RCLike.nonneg_iff.mp hpos.trace_nonneg).2.symm
81   have ht : (Matrix.trace rho).re ≠ 0 := by
82     intro hh
83     apply htr
84     rw [← hreal, hh, Complex.ofReal_zero]
85   have hc : (((Matrix.trace rho).re)⁻¹ : ℂ) ≠ 0 := by exact_mod_cast inv_ne_zero ht
86   let c : ℂ := ((Matrix.trace rho).re)⁻¹
87   have hcpos : 0 ≤ c := by
88     change 0 ≤ (((Matrix.trace rho).re)⁻¹ : ℂ)
89     exact_mod_cast inv_nonneg.mpr (RCLike.nonneg_iff.mp hpos.trace_nonneg).1
90   have hct : Matrix.trace (c • rho)=1 := by
91     rw [Matrix.trace_smul, ← hreal]
92     change (((Matrix.trace rho).re)⁻¹ : ℂ) * ((Matrix.trace rho).re : ℂ) = 1
93     exact_mod_cast inv_mul_cancel₀ ht
94   have hcs : P*(c • rho)*P=c • rho := by simp [hsupport]
95   have hh := hfix (c • rho) (hpos.smul hcpos) hct hcs
96   rw [map_smul] at hh
97   exact smul_right_injective (M := Matrix n n ℂ) hc hh
98 
99 /-- Agreement on normalized code density matrices implies agreement on every code operator. -/
100 theorem fixes_operators_of_density (P : Matrix n n ℂ) (hP : IsStarProjection P)
101     (L : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ)
102     (hfix : ∀ rho : Matrix n n ℂ, rho.PosSemidef → Matrix.trace rho=1 → P*rho*P=rho → L rho=rho)
103     (rho : Matrix n n ℂ) (hsupport : P*rho*P=rho) : L rho=rho := by
104   have heq : L.comp (sandwichLinear P)=sandwichLinear P := by
105     apply linearMap_eq_of_pure
106     intro x
107     change L (sandwichLinear P (pure x)) = sandwichLinear P (pure x)
108     apply fixes_positive_of_density P L hfix
109     · rw [sandwich_pure]
110       exact Matrix.posSemidef_vecMulVec_self_star _
111     · change P*(P*pure x*star P)*P=P*pure x*star P
112       rw [hP.isSelfAdjoint.star_eq]
113       simp only [← mul_assoc, hP.isIdempotentElem.eq]
114       rw [mul_assoc (P*pure x), hP.isIdempotentElem.eq]
115   have hh := congrArg (fun f : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ => f rho) heq
116   simpa [sandwichLinear, hP.isSelfAdjoint.star_eq, hsupport] using hh
117 
118 /-- Physical density-state correctness and code-operator correctness are equivalent. -/
119 theorem density_corrects_iff_operators {I J : Type*} [Fintype I] [Fintype J]
120     (P : Matrix n n ℂ) (hP : IsStarProjection P)
121     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ) :
122     (∀ rho : Matrix n n ℂ, rho.PosSemidef → Matrix.trace rho=1 → P*rho*P=rho →
123       noise R (noise E rho)=rho) ↔
124     (∀ rho : Matrix n n ℂ, P*rho*P=rho → noise R (noise E rho)=rho) := by
125   constructor
126   · intro hh rho hs
127     exact fixes_operators_of_density P hP ((noiseLinear R).comp (noiseLinear E)) hh rho hs
128   · intro hh rho _ _ hs
129     exact hh rho hs
130 
131 
132 def StateCorrectable {I : Type*} [Fintype I] (P : Matrix n n ℂ) (E : I → Matrix n n ℂ) : Prop :=
133   ∃ m : ℕ, ∃ R : Fin m → Matrix n n ℂ,
134     (∑ r, star (R r)*R r)=1 ∧
135     ∀ rho : Matrix n n ℂ, rho.PosSemidef → Matrix.trace rho=1 → P*rho*P=rho →
136       noise R (noise E rho)=rho
137 
138 /-- The physical-state formulation of the full finite channel criterion. -/
139 theorem state_correctable_iff_gram {I : Type*} [Fintype I] [DecidableEq I]
140     (P : Matrix n n ℂ) (hP : IsStarProjection P) (E : I → Matrix n n ℂ)
141     (hE : (∑ a, star (E a)*E a)=1) :
142     StateCorrectable P E ↔ ∃ C : Matrix I I ℂ, C.PosSemidef ∧
143       ∀ a b, P*star (E a)*E b*P=C a b • P := by
144   rw [← correctable_iff_gram P hP E hE]
145   constructor
146   · rintro ⟨m,R,hR,hcorrect⟩
147     exact ⟨m,R,hR,(density_corrects_iff_operators P hP E R).mp hcorrect⟩
148   · rintro ⟨m,R,hR,hcorrect⟩
149     exact ⟨m,R,hR,(density_corrects_iff_operators P hP E R).mpr hcorrect⟩
150 
151 open scoped Kronecker
152 
153 def amplifiedNoise {I J : Type*} [Fintype I] [Fintype J] [DecidableEq J]
154     (E : I → Matrix n n ℂ) (rho : Matrix (J × n) (J × n) ℂ) : Matrix (J × n) (J × n) ℂ :=
155   noise (fun a => (1 : Matrix J J ℂ) ⊗ₖ E a) rho
156 
157 theorem amplifiedNoise_block {I J : Type*} [Fintype I] [Fintype J] [DecidableEq J]
158     (E : I → Matrix n n ℂ) (rho : Matrix (J × n) (J × n) ℂ) (i j : J) (u v : n) :
159     amplifiedNoise E rho (i,u) (j,v) = noise E (fun a b => rho (i,a) (j,b)) u v := by
160   simp [amplifiedNoise, noise, Matrix.sum_apply, Matrix.mul_apply, Matrix.star_apply,
161     Matrix.kroneckerMap_apply, Fintype.sum_prod_type, Matrix.one_apply, apply_ite]
162 
163 /-- Exact correction persists for arbitrary finite reference systems, including entangled states. -/
164 theorem recovery_with_reference {I J A : Type*} [Fintype I] [Fintype J] [Fintype A] [DecidableEq A]
165     (P : Matrix n n ℂ) (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ)
166     (hcorrect : ∀ rho, P*rho*P=rho → noise R (noise E rho)=rho)
167     (rho : Matrix (A × n) (A × n) ℂ)
168     (hs : ((1 : Matrix A A ℂ) ⊗ₖ P)*rho*((1 : Matrix A A ℂ) ⊗ₖ P)=rho) :
169     amplifiedNoise R (amplifiedNoise E rho)=rho := by
170   have hblock (i j : A) :
171       P*(Matrix.of fun a b => rho (i,a) (j,b))*P=(Matrix.of fun a b => rho (i,a) (j,b)) := by
172     ext u v
173     have hh := congrArg (fun M : Matrix (A × n) (A × n) ℂ => M (i,u) (j,v)) hs
174     simpa [Matrix.mul_apply, Matrix.kroneckerMap_apply, Fintype.sum_prod_type, Matrix.one_apply] using hh
175   ext ⟨i,u⟩ ⟨j,v⟩
176   rw [amplifiedNoise_block]
177   have hin : (fun a b => amplifiedNoise E rho (i,a) (j,b)) =
178       noise E (fun a b => rho (i,a) (j,b)) := by
179     ext a b
180     exact amplifiedNoise_block E rho i j a b
181   rw [hin]
182   exact congrArg (fun M : Matrix n n ℂ => M u v) (hcorrect _ (hblock i j))
183 
184 end KomorebiPaperVII.KnillLaflamme
185 
186 /-! Complete declaration-level trust audit. -/
187 #print axioms KomorebiPaperVII.KnillLaflamme.outer_polarization
188 #print axioms KomorebiPaperVII.KnillLaflamme.linearMap_eq_of_pure
189 #print axioms KomorebiPaperVII.KnillLaflamme.sandwich_pure
190 #print axioms KomorebiPaperVII.KnillLaflamme.fixes_positive_of_density
191 #print axioms KomorebiPaperVII.KnillLaflamme.fixes_operators_of_density
192 #print axioms KomorebiPaperVII.KnillLaflamme.density_corrects_iff_operators
193 #print axioms KomorebiPaperVII.KnillLaflamme.state_correctable_iff_gram
194 #print axioms KomorebiPaperVII.KnillLaflamme.amplifiedNoise_block
195 #print axioms KomorebiPaperVII.KnillLaflamme.recovery_with_reference

Back to source controls