Paper VII: Quantum Seed Calculus

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \section{The precise finite channel statement}\label{supp5:section:001}
2 Let $\mathcal H=\C^n$ be a finite coordinate space and let $P=P^*=P^2$. A matrix is code supported when $P\rho P=\rho$. For a finite family of square matrices $E_a$, put
3 \[
4 \mathcal N_E(\rho)=\sum_a E_a\rho E_a^*.
5 \]
6 The input channel normalization is the actual matrix identity
7 \[
8 \sum_a E_a^*E_a=I.
9 \]
10 A finite Kraus recovery has the form $\mathcal R(\sigma)=\sum_r R_r\sigma R_r^*$, with $\sum_rR_r^*R_r=I$. This representation, together with the checked amplification results, provides complete positivity and trace preservation on the entire ambient matrix space.
11 
12 \subsection{Necessary and sufficient conditions}
13 Under the stated normalization, the following equivalence is proved:
14 \[
15 \boxed{\begin{gathered}
16 \exists\,\mathcal R\text{ of the above finite Kraus form,}\\[-2pt]
17 \mathcal R\mathcal N_E(\rho)=\rho
18 \quad\text{for every }\rho\succeq0,\ \Tr\rho=1,\ P\rho P=\rho
19 \end{gathered}}
20 \quad\Longleftrightarrow\quad
21 \boxed{\begin{gathered}
22 \exists C\succeq0,\\
23 PE_a^*E_bP=C_{ab}P\quad\text{for all }a,b.
24 \end{gathered}}
25 \]
26 The statement applies throughout the code space. The formalization separately proves equivalence with correction of \emph{every} complex matrix supported on the code. It also proves preservation with arbitrary finite reference systems, as detailed in the discussion of density matrices and reference systems below.
27 
28 
29 
30 \subsection{Including degenerate cases}
31 The matrix $C$ need not be positive definite. The proof includes zero eigenvalues, redundant error operators, an empty set of positive eigenvalues, and the zero projector. If $P=0$, the only supported matrix is zero and no trace-one code density matrix exists. The proofs handle that case separately rather than dividing by the code rank or by $\Tr P$.
32 
33 For an unnormalized error family, the correct statement is generally
34 \[
35 \mathcal R\mathcal N_E(\rho)=\Tr(C)\rho,
36 \]
37 not unconditional equality to $\rho$. Normalization forces $\Tr C=1$ on a nonzero code. The discussion of coherent errors below treats unrestricted error families and shows when the same decoder works throughout their span.
38 
39 
40 
41 \section{From Gram data to an actual total recovery}\label{supp5:section:002}
42 Assume $C\succeq0$ and $PE_a^*E_bP=C_{ab}P$. First restrict the error operators to the code, $F_a=E_aP$. The finite Hermitian spectral theorem supplies a unitary $U$ such that
43 \[
44 U^*CU=\operatorname{diag}(\lambda_r),\qquad \lambda_r\ge0.
45 \]
46 
47 
48 Define the transformed errors by an actual finite sum,
49 \[
50 B_r=\sum_a U_{ar}F_a.
51 \]
52 The formal module proves the identities
53 \[
54 B_rP=B_r,\qquad B_r^*B_s=\delta_{rs}\lambda_rP,
55 \qquad \sum_rB_r\rho B_r^*=\sum_aF_a\rho F_a^*.
56 \]
57 For $\rho$ supported on the code, the restricted and unrestricted error sums are equal. Thus the unitary change of error coordinates preserves the actual channel on the code.
58 
59 \subsection{Null directions are removed by proof}
60 If $\lambda_r=0$, then $B_r^*B_r=0$. Positivity of the ordinary complex matrix inner product gives $B_r=0$. This is the checked declaration \path{DiagonalErrors.zero_weight_error}. The normalized syndrome operators are defined only on
61 \[
62 A_+=\{r:\lambda_r>0\},\qquad V_r=\lambda_r^{-1/2}B_r.
63 \]
64 Consequently no inverse square root at a null eigenvalue is needed. Lean proves
65 \[
66 V_rP=V_r,\qquad V_r^*V_s=\delta_{rs}P.
67 \]
68 The previous block's recovery is now instantiated from these derived syndromes, rather than from an assumed orthogonal error family.
69 
70 \subsection{A channel on the whole ambient space}
71 Put $Q=I-\sum_{r\in A_+}V_rV_r^*$. The recovery is
72 \[
73 \boxed{\mathcal R(\sigma)=\sum_{r\in A_+}V_r^*\sigma V_r+Q\sigma Q.}
74 \]
75 The complement is an orthogonal projector and
76 \[
77 \sum_{r\in A_+}V_rV_r^*+Q^*Q=I.
78 \]
79 Hence the recovery is trace preserving. Its finite Kraus form also proves positivity after amplification by the identity on every finite auxiliary space. The complement term matters: the map is defined as a channel even outside the syndrome ranges.
80 
81 Finally the checked calculation gives $\mathcal R\mathcal N_E(\rho)=\sum_r\lambda_r\rho=\Tr(C)\rho$. Under normalization of the input channel and $P\ne0$, summing the diagonal Gram identities gives $\Tr(C)P=P$, hence $\Tr C=1$. The proof for the zero code does not use this cancellation.
82 
83 
84 
85 \section{Deriving the Gram matrix from recovery}\label{supp5:section:003}
86 Suppose a finite recovery that preserves trace corrects every operator supported on the code. To derive the Knill--Laflamme condition without assuming a syndrome decomposition, the proof expands the composite channel into the finite Kraus family
87 \[
88 A_{ra}=R_rE_aP.
89 \]
90 For every ambient matrix $\rho$, correction on the code implies
91 \[
92 \sum_{r,a} A_{ra}\rho A_{ra}^*=P\rho P.
93 \]
94 This equality on all matrices follows by applying correction to the sandwich supported on the code, $P\rho P$, using the projector identities.
95 
96 \subsection{Rank-one rigidity of the corrected channel}
97 The module tests the map equality on actual matrix units and flattens each $A_{ra}$ into a row. If $X$ is the matrix of those rows and $p$ is the vector of entries of $P$, the resulting Gram identity is
98 \[
99 X^*X=\overline p\,p^{\mathsf T}.
100 \]
101 The checked rank-one Gram lemma proves that every row of $X$ is proportional to $p$. For nonzero $p$, a nonzero coordinate is selected and a test vector supported on two coordinates is placed in the null space of the Gram matrix. The implication $X^*Xv=0\Rightarrow Xv=0$ then gives the required proportionality. When $p=0$, the Gram identity forces $X=0$ directly.
102 
103 Applied to the corrected Kraus family, this yields scalars $z_{ra}$ with
104 \[
105 R_rE_aP=z_{ra}P.
106 \]
107 The essential declarations are \path{rank_one_gram_rigidity}, \path{kraus_rank_one_rigidity} and \path{corrected_kraus_family}. No rank-one Choi characterization is inserted as an axiom or as the desired conclusion in hypothesis form.
108 
109 \subsection{Trace-preserving recovery supplies the original Gram data}
110 Let $Z_{ra}=z_{ra}$. The recovery normalization gives
111 \begin{align*}
112 PE_a^*E_bP
113 &=PE_a^*\Bigl(\sum_rR_r^*R_r\Bigr)E_bP\\
114 &=\sum_r(R_rE_aP)^*(R_rE_bP)\\
115 &=\Bigl(\sum_r\overline{z_{ra}}z_{rb}\Bigr)P
116 =(Z^*Z)_{ab}P.
117 \end{align*}
118 Thus $C=Z^*Z$ is positive semidefinite and satisfies the required compressed identities. The theorem \path{gram_of_recovery} implements this calculation with the original error and recovery matrices.
119 
120 A second rigidity argument handles a nonnegative scalar multiple of the identity code map. It uses $\sqrt t\,P$ as the rank-one map generator and includes $t=0$. That argument proves necessity for unnormalized error families, which need not define channels.
121 
122 
123 
124 \section{Density matrices, all operators and finite references}\label{supp5:section:004}
125 The necessity argument is stated for all operators, so it must be connected to correction of physical density matrices. The proof establishes this connection explicitly for complex linear maps on finite matrices.
126 
127 \subsection{Normalization is not an extra assumption}
128 A nonzero positive semidefinite matrix has strictly positive real trace. If a complex-linear map fixes every normalized code density matrix, apply that hypothesis to
129 \[
130 \frac{\rho}{\Tr\rho}
131 \]
132 for each nonzero positive code-supported $\rho$. Linearity then gives equality on $\rho$ itself. The zero matrix is handled separately. The source proves that the trace is real and nonzero, then justifies cancellation of the scalar. These steps establish that normalization is valid.
133 
134 \subsection{Complex polarization reaches the whole operator space}
135 Write $q(x)=xx^*$. The module proves the exact identity
136 \[
137 4xy^*=q(x+y)-q(x-y)
138 +i\bigl(q(x+iy)-q(x-iy)\bigr).
139 \]
140 Agreement on all positive pure outer products therefore implies agreement on every outer product. Actual matrix units then span the full matrix space. Applying this argument to the sandwich by $P$ proves equality on every code-supported operator, including non-Hermitian ones.
141 
142 The result \path{density_corrects_iff_operators} establishes the equivalence for the actual composite Kraus maps. It does not replace the set of density matrices by an assumed basis of logical states.
143 
144 \subsection{An arbitrary finite reference system}
145 For any finite reference index set $A$, the amplified channel is defined using the actual Kronecker Kraus operators,
146 \[
147 \widetilde{\mathcal N}_E(\rho)
148 =\sum_a(I_A\otimes E_a)\rho(I_A\otimes E_a)^*.
149 \]
150 Its reference blocks are proved equal to the original channel applied blockwise. If
151 \[
152 (I_A\otimes P)\rho(I_A\otimes P)=\rho,
153 \]
154 then every reference block is code supported. Applying the checked correction theorem for operators to those blocks gives
155 \[
156 \boxed{\widetilde{\mathcal R}\,\widetilde{\mathcal N}_E(\rho)=\rho.}
157 \]
158 This includes entangled density matrices supported on the combined reference and code space. In fact, the identity holds for every jointly supported matrix and every finite reference dimension.
159 
160 The declaration \path{recovery_with_reference} proves the equality. The finite Kraus amplification separately establishes complete positivity of the recovery, which is needed to preserve states in the presence of a reference system.
161 
162 
163 
164 \section{Coherent combinations and normalization}\label{supp5:section:005}
165 A correction proof for only one selected Kraus presentation is weaker than a proof that one decoder works throughout the error span. The formal module connects the constructed spectral recovery back to the original error operators.
166 
167 \subsection{Cross terms for the original errors}
168 For arbitrary positive Gram data, the same recovery satisfies
169 \[
170 \boxed{\mathcal R(E_a\rho E_b^*)=C_{ba}\rho\qquad(P\rho P=\rho).}
171 \]
172 The index order $ba$ is intentional: the defining Gram relation is $PE_a^*E_bP=C_{ab}P$. The proof first derives scalar corrected Kraus composites for the constructed recovery and then uses its trace-preserving completeness to identify the original Gram entries.
173 
174 For $E(c)=\sum_a c_aE_a$, finite-sum expansion gives
175 \[
176 \mathcal R\bigl(E(c)\rho E(c)^*\bigr)
177 =\left(\sum_{a,b}c_a\overline{c_b}C_{ba}\right)\rho
178 =(c^*Cc)\rho.
179 \]
180 The formula with a double sum is the literal checked conclusion. The final notation as a quadratic form follows by renaming finite indices. It is not restricted to orthogonal errors or real coefficients.
181 
182 \subsection{Every normalized channel in the same span}
183 Suppose $F_j=\sum_a c_{ja}E_a$ and $\sum_jF_j^*F_j=I$. The decoder is \emph{not} reconstructed for the $F_j$. Summing the coherent identities gives a scalar multiple $q\rho$. Trace preservation of both the $F$ channel and the recovery forces $q=1$ on a nonzero code. The proof uses positivity of $P$ to justify cancellation of its trace and handles $P=0$ separately. Therefore
184 \[
185 \boxed{\mathcal R\Bigl(\sum_jF_j\rho F_j^*\Bigr)=\rho.}
186 \]
187 This is \path{Data.recovery_span_channel}, a quantified statement over arbitrary finite $F$ families and their complex coefficients.
188 
189 \subsection{The equivalence for unnormalized error families}
190 For arbitrary finite $E$, define exact family recovery to mean that a finite trace-preserving Kraus recovery and a single $t\ge0$ exist such that
191 \[
192 \mathcal R\mathcal N_E(\rho)=t\rho
193 \quad\text{for every code-supported }\rho.
194 \]
195 Then \path{error_family_correctable_iff_gram} proves that this condition is equivalent to the existence of $C\succeq0$ satisfying the Gram identities. Sufficiency chooses $t=\Tr C$. Necessity constructs $C$ from the scaled rank-one rigidity argument.
196 
197 The scale is essential. Zero errors can give $t=0$ and cannot be inverted to a nonzero normalized state. An input with a larger total trace is not silently declared a channel. For normalized input channels, the separate channel theorem removes the scale exactly as described in the sufficiency argument above.
198 
199 
200 
201 \section{Exact examples, trust audit and remaining work}\label{supp5:section:006}
202 \subsection{Singular, nonorthogonal errors are accepted}
203 On a qubit with full code $P=I$, take
204 \[
205 E_0=\frac35I,\qquad E_1=\frac45I,\qquad
206 C=\begin{pmatrix}9/25&12/25\\12/25&16/25\end{pmatrix}.
207 \]
208 Lean checks the channel normalization, the Gram identities, positivity of $C$, $\det C=0$, and the nonzero off-diagonal entry. It then applies the criterion for density matrices to prove correctability. The calculation is exact and uses rational complex entries.
209 
210 \subsection{A genuine channel can still be uncorrectable}
211 For full qubit dephasing, $E_0=\operatorname{diag}(1,0)$ and $E_1=\operatorname{diag}(0,1)$, the Kraus normalization is checked. But $E_0^*E_0$ cannot be a scalar multiple of $I$, as its two diagonal entries differ. Necessity therefore proves that no finite recovery channel corrects the full code space. The case of the zero code is also checked independently.
212 

Back to source controls

Back to Paper VII: Quantum Seed Calculus