ErrorSpanRecovery.lean

1 module
2 public import QuantumStateBridge
3 import all QuantumStateBridge
4 import all KnillLaflammeNecessity
5 import all KnillLaflammeSufficiency
6 import all SyndromeRecovery
7 public import Mathlib.Tactic
8 /-! Author: Komorebi P. Paper VII fifth block.
9 The same constructed recovery corrects the entire error span, not just one Kraus presentation.
10 -/
11 public section
12 set_option autoImplicit false
13 set_option backward.isDefEq.respectTransparency false
14 set_option backward.isDefEq.respectTransparency.types false
15 set_option linter.unusedSectionVars false
16 namespace KomorebiPaperVII.KnillLaflamme
17 open scoped BigOperators ComplexOrder
18 open Matrix
19 variable {n I J : Type*} [Fintype n] [DecidableEq n]
20     [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
21 
22 /-- Rank-one Kraus rigidity also applies to a nonnegative multiple of the code map. -/
23 theorem scaled_corrected_kraus_family (P : Matrix n n ℂ) (hP : IsStarProjection P)
24     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ) (t : ℝ) (ht : 0 ≤ t)
25     (hcorrect : ∀ rho, P*rho*P=rho → noise R (noise E rho)=(t : ℂ) • rho) :
26     ∃ z : J × I → ℂ, ∀ r a, R r*E a*P=z (r,a) • P := by
27   let Q : Matrix n n ℂ := (Real.sqrt t : ℂ) • P
28   have hsqrt : (Real.sqrt t : ℂ)*(Real.sqrt t : ℂ)=(t : ℂ) := by
29     exact_mod_cast Real.mul_self_sqrt ht
30   have hmap (rho : Matrix n n ℂ) :
31       noise (fun ra : J × I => R ra.1*E ra.2*P) rho=Q*rho*star Q := by
32     have hrho : P*(P*rho*P)*P=P*rho*P := by
33       simp only [← mul_assoc, hP.isIdempotentElem.eq]
34       rw [mul_assoc (P*rho), hP.isIdempotentElem.eq]
35     have heq : noise (fun ra : J × I => R ra.1*E ra.2*P) rho =
36         noise R (noise E (P*rho*P)) := by
37       simp only [noise, Fintype.sum_prod_type, star_mul, hP.isSelfAdjoint.star_eq,
38         Finset.mul_sum, Finset.sum_mul, mul_assoc]
39     rw [heq, hcorrect _ hrho]
40     simp only [Q, star_smul, hP.isSelfAdjoint.star_eq, Complex.star_def,
41       Complex.conj_ofReal, smul_mul_assoc, mul_smul_comm, smul_smul, hsqrt]
42   obtain ⟨z,hz⟩ := kraus_rank_one_rigidity (fun ra : J × I => R ra.1*E ra.2*P) Q hmap
43   refine ⟨fun ra => z ra*(Real.sqrt t : ℂ), ?_⟩
44   intro r a
45   exact (hz (r,a)).trans (smul_smul _ _ _)
46 
47 /-- The scalar-composite coefficients recover the original compressed Gram entries. -/
48 theorem compressed_gram_from_scalar (P : Matrix n n ℂ) (hP : IsStarProjection P)
49     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ)
50     (hR : (∑ r, star (R r)*R r)=1) (z : J × I → ℂ)
51     (hz : ∀ r a, R r*E a*P=z (r,a) • P) (a b : I) :
52     P*star (E a)*E b*P=(∑ r, star (z (r,a))*z (r,b)) • P := by
53   have heq : P*star (E a)*E b*P = ∑ r, star (R r*E a*P)*(R r*E b*P) := by
54     calc
55       _ = P*star (E a)*(∑ r, star (R r)*R r)*E b*P := by rw [hR, mul_one]
56       _ = _ := by
57         simp only [Finset.mul_sum, Finset.sum_mul, star_mul,
58           hP.isSelfAdjoint.star_eq, mul_assoc]
59   rw [heq]
60   simp_rw [hz, star_smul, hP.isSelfAdjoint.star_eq, smul_mul_assoc,
61     mul_smul_comm, smul_smul, hP.isIdempotentElem.eq]
62   rw [Finset.sum_smul]
63 
64 /-- Trace preservation of the actual normalized Kraus sum. -/
65 theorem noise_preserves_trace (E : I → Matrix n n ℂ)
66     (hE : (∑ a, star (E a)*E a)=1) (rho : Matrix n n ℂ) :
67     Matrix.trace (noise E rho)=Matrix.trace rho := by
68   rw [noise, Matrix.trace_sum]
69   have cyclic (a : I) : Matrix.trace (E a*rho*star (E a)) =
70       Matrix.trace ((star (E a)*E a)*rho) := by
71     rw [Matrix.trace_mul_comm, Matrix.mul_assoc]
72   simp_rw [cyclic]
73   rw [← Matrix.trace_sum, ← Finset.sum_mul, hE, Matrix.one_mul]
74 
75 namespace Data
76 variable (K : Data n I)
77 
78 /-- Scalar corrected Kraus operators for arbitrary Gram data, including zero trace. -/
79 theorem recovery_scalar_composites :
80     ∃ z : (Option K.diagonal.Active) × I → ℂ,
81       ∀ r a, K.diagonal.syndromes.recoveryKraus r*K.error a*K.code=z (r,a) • K.code := by
82   have hreal : ((Matrix.trace K.gramMatrix).re : ℂ)=Matrix.trace K.gramMatrix := by
83     exact Complex.ext rfl (by simpa using (RCLike.nonneg_iff.mp K.gram_positive.trace_nonneg).2.symm)
84   apply scaled_corrected_kraus_family K.code K.code_projection K.error
85     K.diagonal.syndromes.recoveryKraus (Matrix.trace K.gramMatrix).re
86     (RCLike.nonneg_iff.mp K.gram_positive.trace_nonneg).1
87   intro rho hrho
88   change (∑ r, K.diagonal.syndromes.recoveryKraus r*noise K.error rho*
89     star (K.diagonal.syndromes.recoveryKraus r)) = _
90   rw [← K.diagonal.syndromes.decoder_eq_kraus, hreal]
91   exact K.recovery_noise_scaled rho hrho
92 
93 /-- Cross terms for the original, not necessarily orthogonal or normalized, errors. -/
94 theorem recovery_cross_error (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho) (a b : I) :
95     K.diagonal.syndromes.decoder (K.error a*rho*star (K.error b)) = K.gramMatrix b a • rho := by
96   by_cases hp : K.code=0
97   · have hz : rho=0 := by simpa [hp] using hrho.symm
98     simp [hz, KomorebiPaperVII.Recovery.OrthogonalSyndromes.decoder]
99   · obtain ⟨z,hz⟩ := K.recovery_scalar_composites
100     have hcoeff : (∑ r, z (r,a)*star (z (r,b)))=K.gramMatrix b a := by
101       apply smul_left_injective ℂ hp
102       change (∑ r, z (r,a)*star (z (r,b))) • K.code=K.gramMatrix b a • K.code
103       rw [← K.gram b a, compressed_gram_from_scalar K.code K.code_projection K.error
104         K.diagonal.syndromes.recoveryKraus K.recovery_complete z hz b a]
105       simp only [mul_comm]
106     rw [K.diagonal.syndromes.decoder_eq_kraus]
107     change noise K.diagonal.syndromes.recoveryKraus (K.error a*rho*star (K.error b)) = _
108     rw [recovery_cross_from_scalar K.code K.code_projection K.error
109       K.diagonal.syndromes.recoveryKraus z hz rho hrho a b, hcoeff]
110 
111 /-- One decoder corrects every coherent combination, with its exact Gram weight. -/
112 theorem recovery_error_superposition (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho)
113     (c : I → ℂ) :
114     K.diagonal.syndromes.decoder ((∑ a, c a • K.error a)*rho*star (∑ b, c b • K.error b)) =
115       (∑ a, ∑ b, c a*star (c b)*K.gramMatrix b a) • rho := by
116   have heq : (∑ a, c a • K.error a)*rho*star (∑ b, c b • K.error b) =
117       ∑ a, ∑ b, (c a*star (c b)) • (K.error a*rho*star (K.error b)) := by
118     rw [star_sum]
119     simp only [star_smul]
120     rw [Finset.sum_mul, Finset.sum_mul]
121     simp only [Finset.mul_sum]
122     apply Finset.sum_congr rfl
123     intro a _
124     apply Finset.sum_congr rfl
125     intro b _
126     simp only [smul_mul_assoc, mul_smul_comm, smul_smul]
127     rw [mul_comm]
128   rw [heq]
129   change K.diagonal.syndromes.decoderLinear (∑ a, ∑ b, (c a*star (c b)) •
130     (K.error a*rho*star (K.error b))) = _
131   simp only [map_sum, map_smul]
132   change (∑ a, ∑ b, (c a*star (c b)) • K.diagonal.syndromes.decoder
133     (K.error a*rho*star (K.error b))) = _
134   simp_rw [K.recovery_cross_error rho hrho]
135   simp only [smul_smul, Finset.sum_smul]
136 
137 /-- The same recovery corrects every normalized channel whose errors lie in the original span. -/
138 theorem recovery_span_channel (F : J → Matrix n n ℂ) (c : J → I → ℂ)
139     (hc : ∀ j, F j=∑ a, c j a • K.error a)
140     (hF : (∑ j, star (F j)*F j)=1)
141     (rho : Matrix n n ℂ) (hrho : K.code*rho*K.code=rho) :
142     K.diagonal.syndromes.decoder (noise F rho)=rho := by
143   let q : ℂ := ∑ j, ∑ a, ∑ b, c j a*star (c j b)*K.gramMatrix b a
144   have hscaled (rho : Matrix n n ℂ) (hs : K.code*rho*K.code=rho) :
145       K.diagonal.syndromes.decoder (noise F rho)=q • rho := by
146     change K.diagonal.syndromes.decoderLinear (∑ j, F j*rho*star (F j)) = _
147     rw [map_sum]
148     change (∑ j, K.diagonal.syndromes.decoder (F j*rho*star (F j))) = _
149     simp_rw [hc, K.recovery_error_superposition rho hs]
150     rw [← Finset.sum_smul]
151   rw [hscaled rho hrho]
152   by_cases hp : K.code=0
153   · have hz : rho=0 := by simpa [hp] using hrho.symm
154     simp [hz]
155   · have hpos : K.code.PosSemidef := by
156       have hx := Matrix.posSemidef_conjTranspose_mul_self K.code
157       change (star K.code*K.code).PosSemidef at hx
158       rw [K.code_projection.isSelfAdjoint.star_eq, K.code_projection.isIdempotentElem.eq] at hx
159       exact hx
160     have ht : Matrix.trace K.code ≠ 0 := (hpos.trace_eq_zero_iff).not.mpr hp
161     have hs : K.code*K.code*K.code=K.code := by simp only [K.code_projection.isIdempotentElem.eq]
162     have hh := congrArg Matrix.trace (hscaled K.code hs)
163     rw [K.recovery_preserves_trace, noise_preserves_trace F hF, Matrix.trace_smul] at hh
164     have hq : q=1 := mul_right_cancel₀ ht (by simpa using hh.symm)
165     rw [hq, one_smul]
166 
167 end Data
168 
169 /-- For an unnormalized error family, exact recovery has a code-independent nonnegative scale. -/
170 def ErrorFamilyCorrectable (P : Matrix n n ℂ) (E : I → Matrix n n ℂ) : Prop :=
171   ∃ m : ℕ, ∃ R : Fin m → Matrix n n ℂ, (∑ r, star (R r)*R r)=1 ∧
172     ∃ t : ℝ, 0 ≤ t ∧ ∀ rho, P*rho*P=rho → noise R (noise E rho)=(t : ℂ) • rho
173 
174 /-- Gram necessity for arbitrary, possibly unnormalized and singular, error families. -/
175 theorem gram_of_scaled_recovery (P : Matrix n n ℂ) (hP : IsStarProjection P)
176     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ)
177     (hR : (∑ r, star (R r)*R r)=1) (t : ℝ) (ht : 0 ≤ t)
178     (hcorrect : ∀ rho, P*rho*P=rho → noise R (noise E rho)=(t : ℂ) • rho) :
179     ∃ C : Matrix I I ℂ, C.PosSemidef ∧ ∀ a b, P*star (E a)*E b*P=C a b • P := by
180   obtain ⟨z,hz⟩ := scaled_corrected_kraus_family P hP E R t ht hcorrect
181   let Z : Matrix J I ℂ := fun r a => z (r,a)
182   refine ⟨Z.conjTranspose*Z, Matrix.posSemidef_conjTranspose_mul_self Z, ?_⟩
183   intro a b
184   simpa [Z, Matrix.mul_apply, Matrix.conjTranspose_apply] using
185     compressed_gram_from_scalar P hP E R hR z hz a b
186 
187 /-- Full finite error-family criterion, with normalization made explicit rather than assumed. -/
188 theorem error_family_correctable_iff_gram (P : Matrix n n ℂ) (hP : IsStarProjection P)
189     (E : I → Matrix n n ℂ) :
190     ErrorFamilyCorrectable P E ↔ ∃ C : Matrix I I ℂ, C.PosSemidef ∧
191       ∀ a b, P*star (E a)*E b*P=C a b • P := by
192   constructor
193   · rintro ⟨m,R,hR,t,ht,hcorrect⟩
194     exact gram_of_scaled_recovery P hP E R hR t ht hcorrect
195   · rintro ⟨C,hC,hgram⟩
196     let K : Data n I := ⟨P,hP,E,C,hC,hgram⟩
197     let e := Fintype.equivFin (Option K.diagonal.Active)
198     let R := K.diagonal.syndromes.recoveryKraus
199     refine ⟨Fintype.card (Option K.diagonal.Active), fun r => R (e.symm r), ?_,
200       (Matrix.trace C).re, (RCLike.nonneg_iff.mp hC.trace_nonneg).1, ?_⟩
201     · exact (e.symm.sum_comp (fun a => star (R a)*R a)).trans K.recovery_complete
202     · intro rho hrho
203       change (∑ r, R (e.symm r)*noise E rho*star (R (e.symm r))) = _
204       rw [e.symm.sum_comp (fun a => R a*noise E rho*star (R a))]
205       have hreal : ((Matrix.trace C).re : ℂ)=Matrix.trace C := by
206         exact Complex.ext rfl (by simpa using (RCLike.nonneg_iff.mp hC.trace_nonneg).2.symm)
207       rw [hreal]
208       exact (K.diagonal.syndromes.decoder_eq_kraus (noise E rho)).symm.trans
209         (K.recovery_noise_scaled rho hrho)
210 
211 end KomorebiPaperVII.KnillLaflamme
212 
213 /-! Complete declaration-level trust audit. -/
214 #print axioms KomorebiPaperVII.KnillLaflamme.scaled_corrected_kraus_family
215 #print axioms KomorebiPaperVII.KnillLaflamme.compressed_gram_from_scalar
216 #print axioms KomorebiPaperVII.KnillLaflamme.noise_preserves_trace
217 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_scalar_composites
218 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_cross_error
219 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_error_superposition
220 #print axioms KomorebiPaperVII.KnillLaflamme.Data.recovery_span_channel
221 #print axioms KomorebiPaperVII.KnillLaflamme.gram_of_scaled_recovery
222 #print axioms KomorebiPaperVII.KnillLaflamme.error_family_correctable_iff_gram

Back to source controls