Empirical/QM: the three-qubit bit-flip code (the first QEC theorem) #
Category: 3-Local. QM-validity layer (matrix / inner-product geometry, no CSD
ontology). The smallest genuine quantum error-correcting code, and the QEC analogue of
no_cloning_two_state: a concrete, self-contained first error-correction theorem.
The code #
A logical qubit a|0⟩ + b|1⟩ is encoded as a|000⟩ + b|111⟩ on three physical qubits
(encode). The code corrects any single bit-flip (X) error:
- Stabilisers
Z₁Z₂ = Z⊗Z⊗IandZ₂Z₃ = I⊗Z⊗Zfix the codespace (stab_Z1Z2_fixes_logical,stab_Z2Z3_fixes_logical). - Errors
{I, X₁, X₂, X₃}each commute or anticommute with the stabilisers in a distinct pattern, so the errored stateE·ψ_Lis a simultaneous stabiliser eigenstate with eigenvalues = the syndrome ofE, and the four syndromes are distinct (syndrome_*). Measuring(Z₁Z₂, Z₂Z₃)therefore identifies which bit flipped. - Recovery: each
Xis self-inverse, so re-applying the identifiedXrestores the logical state (bitflip_corrects).
The proofs are pure 2×2-Pauli algebra lifted through the Kronecker mixed-product
(A⊗B)(C⊗D) = (AC)⊗(BD); the single-qubit anticommutation ZX = −XZ drives every
syndrome sign.
Source #
Shor 1995 (the 9-qubit code, of which this is the bit-flip half); the 3-qubit repetition code is the standard pedagogical entry to stabiliser QEC (Nielsen-Chuang §10.1).
The 3-qubit Hilbert space, ℂ⁸ indexed by the computational basis.
Equations
- CSD.Empirical.QM.QEC.H3 = EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)
Instances For
Single-qubit Paulis and their algebra #
The three-qubit operators (Kronecker lifts) #
M ⊗ N ⊗ P on the right-associated Fin 2 × Fin 2 × Fin 2 index.
Equations
- CSD.Empirical.QM.QEC.kron3 M N P = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) N P)
Instances For
X₁ = X ⊗ I ⊗ I.
Instances For
X₂ = I ⊗ X ⊗ I.
Instances For
X₃ = I ⊗ I ⊗ X.
Instances For
The stabiliser Z₁Z₂ = Z ⊗ Z ⊗ I.
Equations
Instances For
The stabiliser Z₂Z₃ = I ⊗ Z ⊗ Z.
Equations
Instances For
Self-inverse and the stabiliser commutations #
The encoded (logical) state and the stabiliser fixing #
The logical state a|000⟩ + b|111⟩ — the image of a|0⟩ + b|1⟩ under the encoder.
Equations
- CSD.Empirical.QM.QEC.logical a b = EuclideanSpace.single (0, 0, 0) a + EuclideanSpace.single (1, 1, 1) b
Instances For
Z₁Z₂ fixes the codespace: Z₁Z₂ · ψ_L = ψ_L.
Z₂Z₃ fixes the codespace: Z₂Z₃ · ψ_L = ψ_L.
Syndromes, recovery, and the correction theorem #
The errored codeword carries the syndrome of the error: it is a simultaneous
eigenstate of the stabilisers (Z₁Z₂, Z₂Z₃) with the eigenvalue pattern that identifies
the error. (I,X₁,X₂,X₃) give the distinct syndromes (+,+), (−,+), (−,−), (+,−).
Recovery. Each single bit-flip is self-inverse, so re-applying the identified
correction restores the logical state: Xⱼ · (Xⱼ · ψ_L) = ψ_L.
Identifiability: the four syndromes are pairwise distinct #
The syndrome of an error, as the eigenvalue sign-pair (s₁, s₂) ∈ {±1}² of the
stabilisers (Z₁Z₂, Z₂Z₃) on the errored codeword. Indexed by Fin 4 for the error set
{I, X₁, X₂, X₃}. The values I → (+,+), X₁ → (−,+), X₂ → (−,−), X₃ → (+,−) are read
off stab_*_fixes_logical / syndrome_X* (the eigenvalues live in ℂ, the scalar field of
the code space).
Equations
Instances For
Identifiability (the load-bearing QEC ingredient): the four error syndromes are
pairwise distinct. Equivalently errorSyndrome is injective on {I, X₁, X₂, X₃}. Since the
four {±1}² sign-pairs are literally distinct, measuring (Z₁Z₂, Z₂Z₃) pins down which of
the four errors occurred. This is the content that makes the stabiliser eigenvalues a usable
syndrome rather than merely an eigen-equation.
The four errored codewords are simultaneous stabiliser eigenstates carrying their
syndrome, in eigen-equation form: I is fixed ((+,+)); X₁, X₂, X₃ carry the eigenvalue
pairs (−,+), (−,−), (+,−). This is the eigenstate content underlying errorSyndrome; it
repackages stab_*_fixes_logical and syndrome_X* so that three_qubit_syndromes_distinct
(distinctness of the ±1 pairs) is the identifiability statement.
The eigenvalue sign-pair carried by three_qubit_syndrome_eigenstates for error index
k agrees with errorSyndrome k (the ±1 entries are the stabiliser eigenvalues).
The three-qubit bit-flip code corrects any single bit-flip. For the encoded state
ψ_L = a|000⟩ + b|111⟩. This capstone now bundles all three ingredients: (i) the
stabilisers Z₁Z₂, Z₂Z₃ fix the codespace; (ii) identifiability — the four errors
{I, X₁, X₂, X₃} give the distinct syndromes (+,+), (−,+), (−,−), (+,−)
(three_qubit_syndromes_distinct), so measuring (Z₁Z₂, Z₂Z₃) pins down which error
occurred (the eigen-equation form is three_qubit_syndrome_eigenstates); and (iii) each
error Xⱼ is self-inverse, so re-applying the identified error restores ψ_L.