KnillLaflammeNecessity.lean

1 module
2 public import KnillLaflammeSufficiency
3 import all KnillLaflammeSufficiency
4 public import Mathlib.Data.Matrix.Basis
5 public import Mathlib.Tactic
6 /-! Author: Komorebi P. Paper VII fifth block.
7 Necessity via a rank-one Gram rigidity argument on actual finite Kraus maps.
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 
18 /-- Every row of a matrix with a rank-one Gram matrix is proportional to its generator. -/
19 theorem rank_one_gram_rigidity {q J : Type*} [Fintype q] [DecidableEq q]
20     [Fintype J] [DecidableEq J] (A : Matrix J q ℂ) (p : q → ℂ)
21     (hgram : A.conjTranspose*A = Matrix.vecMulVec (star p) p) :
22     ∃ z : J → ℂ, ∀ j t, A j t = z j*p t := by
23   by_cases hp : p=0
24   · have hA : A=0 := Matrix.conjTranspose_mul_self_eq_zero.mp (by simpa [hp] using hgram)
25     exact ⟨fun _ => 0, by simp [hA]⟩
26   · obtain ⟨t,ht⟩ : ∃ t, p t ≠ 0 := Function.ne_iff.mp hp
27     refine ⟨fun j => A j t / p t, ?_⟩
28     intro j s
29     let v : q → ℂ := Pi.single s (p t) - Pi.single t (p s)
30     have hpv : p ⬝ᵥ v = 0 := by
31       simp [v, dotProduct_sub, dotProduct_single, mul_comm]
32     have hav : A *ᵥ v=0 := by
33       apply (Matrix.conjTranspose_mul_self_mulVec_eq_zero A v).mp
34       rw [hgram]
35       ext u
36       change (∑ x, star (p u) * p x * v x) = 0
37       simp_rw [mul_assoc]
38       rw [← Finset.mul_sum]
39       change star (p u) * (p ⬝ᵥ v) = 0
40       rw [hpv, mul_zero]
41     have heq : A j s*p t - A j t*p s=0 := by
42       simpa [v, Matrix.mulVec_sub, Matrix.mulVec_single, mul_comm] using congrFun hav j
43     change A j s = (A j t / p t) * p s
44     field_simp [ht]
45     linear_combination heq
46 
47 
48 variable {n I J : Type*} [Fintype n] [DecidableEq n]
49     [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
50 
51 /-- A Kraus decomposition of a rank-one operator map has proportional Kraus operators. -/
52 theorem kraus_rank_one_rigidity (A : J → Matrix n n ℂ) (P : Matrix n n ℂ)
53     (hmap : ∀ rho, noise A rho=P*rho*star P) :
54     ∃ z : J → ℂ, ∀ j, A j=z j • P := by
55   let X : Matrix J (n × n) ℂ := fun j t => A j t.1 t.2
56   let p : n × n → ℂ := fun t => P t.1 t.2
57   have hgram : X.conjTranspose*X=Matrix.vecMulVec (star p) p := by
58     ext ⟨a,b⟩ ⟨c,d⟩
59     have hh := congrArg (fun M : Matrix n n ℂ => M c a) (hmap (Matrix.single d b 1))
60     simpa [X, p, noise, Matrix.mul_apply, Matrix.conjTranspose_apply, Matrix.star_apply,
61       Matrix.single_apply, ite_and, Matrix.sum_apply, Matrix.vecMulVec, mul_comm] using hh
62   obtain ⟨z,hz⟩ := rank_one_gram_rigidity X p hgram
63   refine ⟨z, fun j => ?_⟩
64   ext a b
65   exact hz j (a,b)
66 
67 /-- Expand the corrected code map as a genuine composite Kraus family. -/
68 theorem corrected_kraus_family (P : Matrix n n ℂ) (hP : IsStarProjection P)
69     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ)
70     (hcorrect : ∀ rho, P*rho*P=rho → noise R (noise E rho)=rho) :
71     ∃ z : J × I → ℂ, ∀ r a, R r*E a*P=z (r,a) • P := by
72   have hmap (rho : Matrix n n ℂ) :
73       noise (fun ra : J × I => R ra.1*E ra.2*P) rho=P*rho*star P := by
74     have hrho : P*(P*rho*P)*P=P*rho*P := by
75       simp only [← mul_assoc, hP.isIdempotentElem.eq]
76       rw [mul_assoc (P*rho), hP.isIdempotentElem.eq]
77     have heq : noise (fun ra : J × I => R ra.1*E ra.2*P) rho =
78         noise R (noise E (P*rho*P)) := by
79       simp only [noise, Fintype.sum_prod_type, star_mul, hP.isSelfAdjoint.star_eq,
80         Finset.mul_sum, Finset.sum_mul, mul_assoc]
81     rw [heq, hcorrect _ hrho, hP.isSelfAdjoint.star_eq]
82   obtain ⟨z,hz⟩ := kraus_rank_one_rigidity (fun ra : J × I => R ra.1*E ra.2*P) P hmap
83   exact ⟨z, fun r a => hz (r,a)⟩
84 
85 /-- Necessary Knill-Laflamme Gram matrix derived from actual trace-preserving recovery. -/
86 theorem gram_of_recovery (P : Matrix n n ℂ) (hP : IsStarProjection P)
87     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ)
88     (hR : (∑ r, star (R r)*R r)=1)
89     (hcorrect : ∀ rho, P*rho*P=rho → noise R (noise E rho)=rho) :
90     ∃ C : Matrix I I ℂ, C.PosSemidef ∧
91       ∀ a b, P*star (E a)*E b*P=C a b • P := by
92   obtain ⟨z,hz⟩ := corrected_kraus_family P hP E R hcorrect
93   let Z : Matrix J I ℂ := fun r a => z (r,a)
94   refine ⟨Z.conjTranspose*Z, Matrix.posSemidef_conjTranspose_mul_self Z, ?_⟩
95   intro a b
96   have heq : P*star (E a)*E b*P = ∑ r, star (R r*E a*P)*(R r*E b*P) := by
97     calc
98       _ = P*star (E a)*(∑ r, star (R r)*R r)*E b*P := by rw [hR, mul_one]
99       _ = _ := by
100         simp only [Finset.mul_sum, Finset.sum_mul, star_mul,
101           hP.isSelfAdjoint.star_eq, mul_assoc]
102   rw [heq]
103   simp_rw [hz, star_smul, hP.isSelfAdjoint.star_eq, smul_mul_assoc,
104     mul_smul_comm, smul_smul, hP.isIdempotentElem.eq]
105   simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, Finset.sum_smul, Z]
106 
107 
108 /-- Exact correction on the code operator space by a finite trace-preserving Kraus map. -/
109 def Correctable (P : Matrix n n ℂ) (E : I → Matrix n n ℂ) : Prop :=
110   ∃ m : ℕ, ∃ R : Fin m → Matrix n n ℂ,
111     (∑ r, star (R r)*R r)=1 ∧
112     ∀ rho, P*rho*P=rho → noise R (noise E rho)=rho
113 
114 /-- Finite Knill-Laflamme necessary-and-sufficient criterion for a Kraus channel. -/
115 theorem correctable_iff_gram (P : Matrix n n ℂ) (hP : IsStarProjection P)
116     (E : I → Matrix n n ℂ) (hE : (∑ a, star (E a)*E a)=1) :
117     Correctable P E ↔ ∃ C : Matrix I I ℂ, C.PosSemidef ∧
118       ∀ a b, P*star (E a)*E b*P=C a b • P := by
119   constructor
120   · rintro ⟨m,R,hR,hcorrect⟩
121     exact gram_of_recovery P hP E R hR hcorrect
122   · rintro ⟨C,hC,hgram⟩
123     let K : Data n I := ⟨P,hP,E,C,hC,hgram⟩
124     obtain ⟨R,hR,hcorrect⟩ := K.exists_recovery hE
125     let e := Fintype.equivFin (Option K.diagonal.Active)
126     refine ⟨Fintype.card (Option K.diagonal.Active), fun r => R (e.symm r), ?_, ?_⟩
127     · exact (e.symm.sum_comp (fun a => star (R a)*R a)).trans hR
128     · intro rho hrho
129       change (∑ r, R (e.symm r)*noise E rho*star (R (e.symm r)))=rho
130       exact (e.symm.sum_comp (fun a => R a*noise E rho*star (R a))).trans (hcorrect rho hrho)
131 
132 /-- Failure of scalar Gram compression is a certified obstruction to any exact recovery. -/
133 theorem not_correctable_of_nonscalar (P : Matrix n n ℂ) (hP : IsStarProjection P)
134     (E : I → Matrix n n ℂ) (hE : (∑ a, star (E a)*E a)=1)
135     (a b : I) (hab : ∀ c : ℂ, P*star (E a)*E b*P ≠ c • P) :
136     ¬ Correctable P E := by
137   intro hc
138   obtain ⟨C,_,hgram⟩ := (correctable_iff_gram P hP E hE).mp hc
139   exact hab (C a b) (hgram a b)
140 
141 /-- Cross-error terms are scalar after the very same recovery, not a newly chosen decoder. -/
142 theorem recovery_cross_from_scalar (P : Matrix n n ℂ) (hP : IsStarProjection P)
143     (E : I → Matrix n n ℂ) (R : J → Matrix n n ℂ) (z : J × I → ℂ)
144     (hz : ∀ r a, R r*E a*P=z (r,a) • P)
145     (rho : Matrix n n ℂ) (hrho : P*rho*P=rho) (a b : I) :
146     noise R (E a*rho*star (E b)) = (∑ r, z (r,a)*star (z (r,b))) • rho := by
147   have heq (r : J) : R r*(E a*rho*star (E b))*star (R r) =
148       (R r*E a*P)*rho*star (R r*E b*P) := by
149     rw [star_mul, star_mul, hP.isSelfAdjoint.star_eq]
150     calc
151       _ = (R r*E a)*(P*rho*P)*(star (E b)*star (R r)) := by rw [hrho]; noncomm_ring
152       _ = _ := by noncomm_ring
153   simp only [noise, heq, hz, star_smul, hP.isSelfAdjoint.star_eq,
154     smul_mul_assoc, mul_smul_comm, smul_smul, hrho, Finset.sum_smul]
155   apply Finset.sum_congr rfl
156   intro r _
157   rw [mul_comm]
158 
159 end KomorebiPaperVII.KnillLaflamme
160 
161 /-! Complete declaration-level trust audit. -/
162 #print axioms KomorebiPaperVII.KnillLaflamme.rank_one_gram_rigidity
163 #print axioms KomorebiPaperVII.KnillLaflamme.kraus_rank_one_rigidity
164 #print axioms KomorebiPaperVII.KnillLaflamme.corrected_kraus_family
165 #print axioms KomorebiPaperVII.KnillLaflamme.gram_of_recovery
166 #print axioms KomorebiPaperVII.KnillLaflamme.correctable_iff_gram
167 #print axioms KomorebiPaperVII.KnillLaflamme.not_correctable_of_nonscalar
168 #print axioms KomorebiPaperVII.KnillLaflamme.recovery_cross_from_scalar

Back to source controls