Empirical/QM: the three-qubit phase-flip code (Hadamard dual of the bit-flip code) #
Category: 3-Local. QM-validity layer. The phase-flip repetition code, the Hadamard
conjugate (X ↔ Z, |0/1⟩ ↔ |±⟩) of ThreeQubit.lean's bit-flip code: it corrects any
single phase (Z) error.
A logical qubit is encoded as a|+++⟩ + b|---⟩ (here |+⟩ = |0⟩+|1⟩, |−⟩ = |0⟩−|1⟩,
unnormalised — normalisation is irrelevant to correction). The stabilisers are
X₁X₂ = X⊗X⊗I and X₂X₃ = I⊗X⊗X; they fix the codespace (stab_*_fixes_logicalPF).
The errors {I, Z₁, Z₂, Z₃} each (anti)commute with the stabilisers in a distinct
pattern, so the errored codeword is a stabiliser eigenstate carrying the syndrome
(+,+),(−,+),(−,−),(+,−) (syndromePF_*); measuring (X₁X₂, X₂X₃) identifies the error,
and each Z is self-inverse so re-applying it recovers (phaseflip_recovers).
Everything reuses the bit-flip file's Pauli / Kronecker algebra; the syndrome signs are
driven by the same single-qubit anticommutation pX·pZ = −(pZ·pX).
Source #
Shor 1995 (the phase-flip half of the 9-qubit code); Nielsen-Chuang §10.1.
Phase errors and X-type stabilisers #
Z₁ = Z ⊗ I ⊗ I (a phase error on qubit 1).
Instances For
Z₂ = I ⊗ Z ⊗ I.
Instances For
Z₃ = I ⊗ I ⊗ Z.
Instances For
The stabiliser X₁X₂ = X ⊗ X ⊗ I.
Equations
Instances For
The stabiliser X₂X₃ = I ⊗ X ⊗ X.
Equations
Instances For
The logical states |+++⟩, |---⟩ and stabiliser fixing #
|+⟩⊗|+⟩⊗|+⟩ (unnormalised): the equal superposition of all basis states.
Equations
- CSD.Empirical.QM.QEC.lplus = ∑ i : Fin 2 × Fin 2 × Fin 2, EuclideanSpace.single i 1
Instances For
|−⟩⊗|−⟩⊗|−⟩ (unnormalised): the parity-signed superposition.
Equations
- CSD.Empirical.QM.QEC.lminus = ∑ i : Fin 2 × Fin 2 × Fin 2, EuclideanSpace.single i (CSD.Empirical.QM.QEC.paritySign i)
Instances For
The phase-flip logical state a|+++⟩ + b|---⟩.
Equations
Instances For
X₁X₂ fixes the codespace: X₁X₂ · ψ_L = ψ_L.
X₂X₃ fixes the codespace: X₂X₃ · ψ_L = ψ_L.
Syndromes, recovery, and the correction theorem #
The errored codeword carries the syndrome of the phase error: (I,Z₁,Z₂,Z₃) give
the distinct stabiliser-eigenvalue patterns (+,+),(−,+),(−,−),(+,−).
Recovery. Each single phase flip is self-inverse, so re-applying the identified
correction restores the logical state: Zⱼ · (Zⱼ · ψ_L) = ψ_L.
Identifiability: the four phase-error syndromes are pairwise distinct #
The phase-error syndrome, as the eigenvalue sign-pair (s₁, s₂) ∈ {±1}² of the
stabilisers (X₁X₂, X₂X₃) on the errored codeword. Indexed by Fin 4 for the error set
{I, Z₁, Z₂, Z₃}: I → (+,+), Z₁ → (−,+), Z₂ → (−,−), Z₃ → (+,−) (read off
stab_*_fixes_logicalPF / syndromePF_*). Hadamard dual of errorSyndrome.
Equations
Instances For
Identifiability (the load-bearing QEC ingredient): the four phase-error syndromes are
pairwise distinct. errorSyndromePF is injective, so measuring (X₁X₂, X₂X₃) pins down
which of {I, Z₁, Z₂, Z₃} occurred. Hadamard dual of three_qubit_syndromes_distinct.
The four errored codewords are simultaneous stabiliser eigenstates carrying their
phase-error syndrome, in eigen-equation form. Repackages stab_*_fixes_logicalPF and
syndromePF_* against errorSyndromePF.
The three-qubit phase-flip code corrects any single phase flip. Hadamard dual of
three_qubit_corrects_single_bitflip. This capstone now bundles all three ingredients:
stabiliser-fixing; identifiability — the four errors {I, Z₁, Z₂, Z₃} give the distinct
syndromes (+,+), (−,+), (−,−), (+,−) (three_qubit_phaseflip_syndromes_distinct; the
eigen-equation form is three_qubit_phaseflip_syndrome_eigenstates); and self-inverse
recovery.