III.18 The precise finite channel statement
On this page · Permalink · Source line 1
Let \(\mathcal H={\mathbb 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
The input channel normalization is the actual matrix identity
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.
III.18.1 Necessary and sufficient conditions
On this page · Permalink · Source line 12
Under the stated normalization, the following equivalence is proved:
The statement applies throughout the code space. The formalization separately proves equivalence with correction of 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.
III.18.2 Including degenerate cases
On this page · Permalink · Source line 30
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 \({\operatorname{Tr}} P\).
For an unnormalized error family, the correct statement is generally
not unconditional equality to \(\rho\). Normalization forces \({\operatorname{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.
III.19 From Gram data to an actual total recovery
On this page · Permalink · Source line 41
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
Define the transformed errors by an actual finite sum,
The formal module proves the identities
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.
III.19.1 Null directions are removed by proof
On this page · Permalink · Source line 59
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 DiagonalErrors.zero_weight_error. The normalized syndrome operators are defined only on
Consequently no inverse square root at a null eigenvalue is needed. Lean proves
The previous block's recovery is now instantiated from these derived syndromes, rather than from an assumed orthogonal error family.
III.19.2 A channel on the whole ambient space
On this page · Permalink · Source line 70
Put \(Q=I-\sum_{r\in A_+}V_rV_r^*\). The recovery is
The complement is an orthogonal projector and
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.
Finally the checked calculation gives \(\mathcal R\mathcal N_E(\rho)=\sum_r\lambda_r\rho={\operatorname{Tr}}(C)\rho\). Under normalization of the input channel and \(P\ne0\), summing the diagonal Gram identities gives \({\operatorname{Tr}}(C)P=P\), hence \({\operatorname{Tr}} C=1\). The proof for the zero code does not use this cancellation.
III.20 Deriving the Gram matrix from recovery
On this page · Permalink · Source line 85
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
For every ambient matrix \(\rho\), correction on the code implies
This equality on all matrices follows by applying correction to the sandwich supported on the code, \(P\rho P\), using the projector identities.
III.20.1 Rank-one rigidity of the corrected channel
On this page · Permalink · Source line 96
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
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.
Applied to the corrected Kraus family, this yields scalars \(z_{ra}\) with
The essential declarations are rank_one_gram_rigidity, kraus_rank_one_rigidity and corrected_kraus_family. No rank-one Choi characterization is inserted as an axiom or as the desired conclusion in hypothesis form.
III.20.2 Trace-preserving recovery supplies the original Gram data
On this page · Permalink · Source line 109
Let \(Z_{ra}=z_{ra}\). The recovery normalization gives
Thus \(C=Z^*Z\) is positive semidefinite and satisfies the required compressed identities. The theorem gram_of_recovery implements this calculation with the original error and recovery matrices.
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.
III.21 Density matrices, all operators, and finite references
On this page · Permalink · Source line 124
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.
III.21.1 Normalization is not an extra assumption
On this page · Permalink · Source line 127
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
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.
III.21.2 Complex polarization reaches the whole operator space
On this page · Permalink · Source line 134
Write \(q(x)=xx^*\). The module proves the exact identity
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.
The result 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.
III.21.3 An arbitrary finite reference system
On this page · Permalink · Source line 144
For any finite reference index set \(A\), the amplified channel is defined using the actual Kronecker Kraus operators,
Its reference blocks are proved equal to the original channel applied blockwise. If
then every reference block is code supported. Applying the checked correction theorem for operators to those blocks gives
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.
The declaration 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.
III.22 Coherent combinations and normalization
On this page · Permalink · Source line 164
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.
III.22.1 Cross terms for the original errors
On this page · Permalink · Source line 167
For arbitrary positive Gram data, the same recovery satisfies
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.
For \(E(c)=\sum_a c_aE_a\), finite-sum expansion gives
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.
III.22.2 Every normalized channel in the same span
On this page · Permalink · Source line 182
Suppose \(F_j=\sum_a c_{ja}E_a\) and \(\sum_jF_j^*F_j=I\). The decoder is 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
This is Data.recovery_span_channel, a quantified statement over arbitrary finite \(F\) families and their complex coefficients.
III.22.3 The equivalence for unnormalized error families
On this page · Permalink · Source line 189
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
Then error_family_correctable_iff_gram proves that this condition is equivalent to the existence of \(C\succeq0\) satisfying the Gram identities. Sufficiency chooses \(t={\operatorname{Tr}} C\). Necessity constructs \(C\) from the scaled rank-one rigidity argument.
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.
III.23 Exact examples, trust audit, and remaining work
On this page · Permalink · Source line 201
III.23.1 Singular, nonorthogonal errors are accepted
On this page · Permalink · Source line 202
On a qubit with full code \(P=I\), take
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.
III.23.2 A genuine channel can still be uncorrectable
On this page · Permalink · Source line 210
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.