Empirical/QM: syndrome collapse — the three-qubit code corrects a continuum of errors #
Category: 3-Local. QM-validity layer.
QEC/ErrorDiscretization.lean proves an arbitrary error is a ℂ-combination of four discrete
ones. QEC/ThreeQubit.lean proves each of those four is corrected. Nothing joined them: four
point-checks plus a decomposition is not yet an error-correction claim, because a superposition
of error branches is not obviously reducible to a single branch.
This file supplies the missing half — syndrome collapse — and states the resulting theorem:
the three-qubit code corrects every error in span ℂ {I, X₁, X₂, X₃}, a continuum, not four
points.
The mechanism #
The four errored codewords have disjoint supports in the computational basis:
ψ_L = a|000⟩ + b|111⟩, X₁ψ_L = a|100⟩ + b|011⟩,
X₂ψ_L = a|010⟩ + b|101⟩, X₃ψ_L = a|001⟩ + b|110⟩.
That disjointness is the concrete form of syndrome-distinctness (three_qubit_syndromes_distinct):
the four branches are simultaneous stabiliser eigenvectors with distinct (Z₁Z₂, Z₂Z₃) eigenvalue
pairs, and distinct eigenvalues force orthogonality. Here it is available directly, so the
orthogonality is proved by computation rather than through the spectral theorem.
Orthogonality is what makes the syndrome measurement work: the corrupted state
E ψ_L = Σₖ cₖ · (Eₖ ψ_L) is a superposition of four mutually orthogonal branches, so
measuring (Z₁Z₂, Z₂Z₃) projects onto exactly one of them, with the overlap picking out exactly
that branch's coefficient — and each branch is corrected by re-applying its own Xₖ.
What this file proves #
X1_logical/X2_logical/X3_logical— the three errored codewords in closed form.errored_pairwise_orthogonal— all six pairwise inner products vanish, for everya, b.spanError_logical— an arbitraryE ∈ span {I, X₁, X₂, X₃}sendsψ_Lto the corresponding combination of the four branches.branch_overlap_*— the collapse step: the overlap ofE ψ_Lwith branchkis exactlycₖ · ⟪branch k, branch k⟫. The syndrome measurement reads offcₖand nothing else; the other three branches contribute nothing.- ★
three_qubit_corrects_span_error— the capstone, bundling all four ingredients: decomposition, orthogonality, branch extraction, and branch-wise recovery. The code corrects an arbitrary error in the span, so today's discretization result is load-bearing rather than decorative.
Scope #
Still the bit-flip span {I, X₁, X₂, X₃} — the three-qubit code's actual correctable set.
Extending to all four Paulis per qubit needs the concatenated Shor 9-qubit code, which remains
open on 512-dimensional infrastructure. Superseded 2026-08-13: the concatenated Shor-9 code
landed (QEC/ShorNine.lean, Q5/E1) — {X, Z, XZ} corrected at every one of the nine positions
via the block-Kronecker combinator, no 512-dimensional entry-wise work. The collapse half at
nine qubits (this module's syndrome-projection argument re-established on the concatenated
stabilisers) is not restated there; it remains the natural next brick if the QEC ladder continues
(Q16 metrology is the consumer). What is closed here is the gap within the three-qubit story:
four corrected errors plus discretization genuinely imply a corrected continuum.
References #
QEC/ThreeQubit.lean (logical, X1/X2/X3, bitflip_recovers,
three_qubit_syndromes_distinct, three_qubit_syndrome_eigenstates);
QEC/ErrorDiscretization.lean (pauli_decomposition, pauli_span_top);
specs/BACKLOG.md (Shor-9 / concatenation, DONE — QEC/ShorNine.lean); specs/future-work.md.
Shor 1995; Nielsen–Chuang §10.1–10.2.
The four errored codewords in closed form #
Orthogonality of the branches #
The four error branches are mutually orthogonal, for every logical amplitude pair.
This is the concrete form of syndrome-distinctness: the branches occupy disjoint sets of
computational basis states ({000,111}, {100,011}, {010,101}, {001,110}), which is why the
stabiliser eigenvalue pairs can tell them apart. Orthogonality is what makes the syndrome
measurement project onto a single branch rather than smear across several.
An arbitrary error in the span, and the collapse #
An arbitrary element of span ℂ {I, X₁, X₂, X₃} — the three-qubit code's correctable set —
with coefficient vector c.
Equations
- CSD.Empirical.QM.QEC.spanError c = c 0 • 1 + c 1 • CSD.Empirical.QM.QEC.X1 + c 2 • CSD.Empirical.QM.QEC.X2 + c 3 • CSD.Empirical.QM.QEC.X3
Instances For
The corrupted codeword is the matching combination of the four branches.
The collapse step, branch 1. The overlap of the corrupted codeword with branch X₁ψ_L
is exactly c₁ · ⟪X₁ψ_L, X₁ψ_L⟫ — the other three branches contribute nothing, so the syndrome
measurement reads off c₁ and only c₁.
The collapse step, branch 2.
The collapse step, branch 3.
The capstone #
★ The three-qubit code corrects an arbitrary error in span ℂ {I, X₁, X₂, X₃} — a
continuum of errors, not four discrete ones.
All four ingredients, bundled:
- Decomposition — the corrupted codeword is the matching combination of four branches.
- Orthogonality — the branches are mutually orthogonal, so the syndrome measurement projects onto exactly one of them (this is syndrome-distinctness made concrete: disjoint supports).
- Extraction — the overlap with branch
kis exactlycₖtimes that branch's norm; the measurement reads off one coefficient and is blind to the rest. - Recovery — re-applying
Xₖon branchkrestoresψ_Lexactly, since eachXₖis self-inverse.
Together with pauli_decomposition this is what makes error correction a claim about all
errors of the correctable type rather than about a finite list.