Let \({\mathcal H}={\mathbb C}^3\), with nonzero code projector \(P={\operatorname{diag}}(1,1,0)\). On the code use the error family \(E_1=(3/5)P\), \(E_2=(4/5)P\), and \(E_3=0\). Its Knill–Laflamme Gram matrix is
The errors are redundant rather than three distinct syndromes. A real unitary change of error coordinates gives
Reading the drawing
The top row follows the Gram spectrum to its surviving syndrome and separate complement. A lower replacement branch makes the recovery channel total on that complement. All rank and branch labels are retained below.
Drawing labels and data 4 labels
Read the original labels as selectable text. Tables preserve grid relationships; other short labels are grouped compactly.
Gram spectrum
\((1,0,0)\)
one syndrome
\(Q=P\), rank \(2\)
unused complement
\(I-P\), rank \(1\)
- \({\left|0\right\rangle}{\left\langle2\right|}\): replacement branch
Normalize only positive eigenvalues
The positive branch has \(V_1=P\) as an isometry on the code, and syndrome support \(Q=P\). No factor \(\lambda^{-1/2}\) is formed on either zero branch: those branches vanish on the code. Treating them as extra recoverable packets would divide by zero.
The syndrome support is smaller than the ambient space. Define a total recovery with Kraus operators
It acts as the identity on operators supported on the code and sends the unused complement population into a chosen code state. The declared error map preserves the trace of code states, so recovery returns every code matrix unit, including both off-diagonal units, exactly. It need not preserve states on the unused complement.
Exceptional cases and scope
This construction assumes a nonzero code so that a complement replacement state exists. The case of a zero code is vacuous and has its own formal statement in the saved ledger. The retained exact run verifies all nine Gram compressions, the diagonalization, both null branches, total channel normalization, and all four code matrix units. It adds no Lean coverage and does not implement a numerical spectral decoder for arbitrary Gram data.
Read this as
Positive Gram support defines genuine syndrome isometries. Null branches vanish. Specifying the action on the complement makes the recovery a total channel.