KnillLaflammeExamples.lean

1 module
2 public import ErrorSpanRecovery
3 import all ErrorSpanRecovery
4 import all QuantumStateBridge
5 import all KnillLaflammeNecessity
6 import all KnillLaflammeSufficiency
7 public import Mathlib.Tactic
8 /-! Author: Komorebi P. Paper VII fifth block.
9 Exact regression examples for singular Gram matrices, failure of correction, and the zero code.
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 namespace KomorebiPaperVII.KnillLaflamme.Examples
16 open scoped BigOperators ComplexOrder
17 open Matrix
18 abbrev Qubit := Matrix (Fin 2) (Fin 2) ℂ
19 
20 noncomputable def redundantRow : Matrix (Fin 1) (Fin 2) ℂ := fun _ a => if a=0 then 3/5 else 4/5
21 noncomputable def redundantGram : Matrix (Fin 2) (Fin 2) ℂ := redundantRow.conjTranspose*redundantRow
22 noncomputable def redundantError (a : Fin 2) : Qubit := redundantRow 0 a • 1
23 
24 /-- Two nonorthogonal proportional errors form a normalized channel. -/
25 theorem redundant_complete : (∑ a, star (redundantError a)*redundantError a)=1 := by
26   ext i j
27   fin_cases i <;> fin_cases j <;>
28     norm_num [redundantError, redundantRow, Matrix.mul_apply, Matrix.star_apply,
29       Fin.sum_univ_two, Matrix.one_apply]
30 
31 /-- The redundant error Gram is positive semidefinite, not assumed positive definite. -/
32 theorem redundant_gram_positive : redundantGram.PosSemidef :=
33   Matrix.posSemidef_conjTranspose_mul_self redundantRow
34 
35 /-- Its actual determinant vanishes. -/
36 theorem redundant_gram_singular : Matrix.det redundantGram=0 := by
37   norm_num [redundantGram, redundantRow, Matrix.det_fin_two, Matrix.mul_apply,
38     Matrix.conjTranspose_apply]
39 
40 /-- The off-diagonal Gram entry is nonzero, so diagonal-only reasoning is insufficient. -/
41 theorem redundant_gram_off_diagonal : redundantGram 0 1=12/25 := by
42   norm_num [redundantGram, redundantRow, Matrix.mul_apply, Matrix.conjTranspose_apply]
43 
44 /-- The complete criterion actually accepts this singular, nonorthogonal example. -/
45 theorem redundant_correctable : StateCorrectable (1 : Qubit) redundantError := by
46   apply (state_correctable_iff_gram 1 (IsStarProjection.one _) redundantError redundant_complete).mpr
47   refine ⟨redundantGram, redundant_gram_positive, ?_⟩
48   intro a b
49   ext i j
50   fin_cases a <;> fin_cases b <;> fin_cases i <;> fin_cases j <;>
51     norm_num [redundantError, redundantGram, redundantRow, Matrix.mul_apply,
52       Matrix.star_apply, Matrix.conjTranspose_apply, Fin.sum_univ_two, Matrix.one_apply]
53 
54 def dephasingError (a : Fin 2) : Qubit := Matrix.single a a 1
55 
56 /-- Full dephasing is a genuine normalized channel. -/
57 theorem dephasing_complete : (∑ a, star (dephasingError a)*dephasingError a)=1 := by
58   ext i j
59   fin_cases i <;> fin_cases j <;>
60     norm_num [dephasingError, Matrix.mul_apply, Matrix.star_apply, Matrix.single_apply,
61       Fin.sum_univ_two, Matrix.one_apply]
62 
63 /-- No finite recovery channel can undo full qubit dephasing on the whole code space. -/
64 theorem dephasing_not_correctable : ¬ Correctable (1 : Qubit) dephasingError := by
65   apply not_correctable_of_nonscalar 1 (IsStarProjection.one _) dephasingError dephasing_complete 0 0
66   intro c heq
67   have h00 := congrArg (fun M : Qubit => M 0 0) heq
68   have h11 := congrArg (fun M : Qubit => M 1 1) heq
69   norm_num [dephasingError, Matrix.mul_apply, Matrix.star_apply, Matrix.single_apply,
70     Fin.sum_univ_two, Matrix.one_apply] at h00 h11
71   exact one_ne_zero (h00.trans h11.symm)
72 
73 /-- The zero-code edge case requires no density matrix to exist on that code. -/
74 theorem zero_code_correctable {n I : Type*} [Fintype n] [DecidableEq n]
75     [Fintype I] [DecidableEq I] (E : I → Matrix n n ℂ) : Correctable 0 E := by
76   refine ⟨1, fun _ => 1, ?_, ?_⟩
77   · simp
78   · intro rho hrho
79     have hz : rho=0 := by simpa using hrho.symm
80     simp [hz, noise]
81 
82 end KomorebiPaperVII.KnillLaflamme.Examples
83 
84 /-! Complete declaration-level trust audit. -/
85 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.redundant_complete
86 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.redundant_gram_positive
87 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.redundant_gram_singular
88 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.redundant_gram_off_diagonal
89 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.redundant_correctable
90 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.dephasing_complete
91 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.dephasing_not_correctable
92 #print axioms KomorebiPaperVII.KnillLaflamme.Examples.zero_code_correctable

Back to source controls