Documentation

CsdLean4.Empirical.QM.QEC.SteaneSyndromeCircuit

Empirical/QM: the Steane code's syndrome extraction, as a circuit #

Category: 3-Local. QM-validity layer (matrix algebra, no CSD content). BACKLOG #94, the instance; the generic gadget is Mathlib/QuantumInfo/SyndromeExtraction.lean.

Steane.lean has the X-syndrome as a function on error patterns, syndrome e = fun i => bdot (hammingRow i) e, and uses it to prove the distance-3 mechanism. This file runs the generic extraction gadget at that check map, so the syndrome the corpus reasons with is the one a CNOT ladder into a three-qubit ancilla block actually produces.

What is proved #

Honest scope #

⚠️ No faults, and therefore no fault tolerance. Every statement is about the gadget running correctly. A fault in the CNOT ladder, or in the ancilla, is BACKLOG #95 and #96; nothing here says this gadget is fault-tolerant, only what it computes when it works.

⚠️ One unverified ancilla block. The ancilla is prepared in the all-zero state and read; there is no cat state, no verification, and so no bound on a single ancilla fault spreading into the data. That is #95's subject.

⚠️ X-checks only. The Steane code is CSS and its Z-checks are the same statement in the conjugate basis; that half is not done here, and nothing combines the two bases.

⚠️ The syndrome is produced, not decoded. Nothing here maps a syndrome to a correction: the recovery maps of SteaneRecovery.lean and SteaneArbitrary.lean are neither re-derived nor connected to this circuit.

⚠️ The register is the error-pattern basis. The data index is Fin 7 → Fin 2, i.e. the computational basis of seven qubits; this is the same labelling Steane.lean uses, and no claim is made about the encoded logical state beyond its membership in the syndrome-0 subspace.

References #

Mathlib/QuantumInfo/SyndromeExtraction.lean (the generic gadget); Empirical/QM/QEC/Steane.lean (syndrome, steane_syndrome_single_ne_zero, steane_syndrome_single_injective); Empirical/QM/QEC/SyndromeRecovery.lean (the projective-measurement form); specs/BACKLOG.md #94, #95, #96, #62; specs/future-work.md.

The Steane check map in characteristic two #

source
theorem CSD.Empirical.QM.QEC.Steane.steane_syndrome_add_self (z : Fin 7 → Fin 2) :
syndrome z + syndrome z = 0

★ The only arithmetic the gadget needs. The syndrome lands in Fin 3 → Fin 2, where every element is its own inverse.

source
theorem CSD.Empirical.QM.QEC.Steane.syndrome_add (e f : Fin 7 → Fin 2) :
syndrome (e + f) = syndrome e + syndrome f

The syndrome is additive, because bdot is.

The extraction circuit #

source
noncomputable def CSD.Empirical.QM.QEC.Steane.steaneExtract :
Matrix ((Fin 7 → Fin 2) × (Fin 3 → Fin 2)) ((Fin 7 → Fin 2) × (Fin 3 → Fin 2)) ℂ

The Steane X-syndrome extraction circuit: the CNOT ladder from the seven data qubits into a three-qubit ancilla block, as the matrix of its basis relabelling.

Equations
Instances For
    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneExtract_mem_unitaryGroup :
    steaneExtract ∈ Matrix.unitaryGroup ((Fin 7 → Fin 2) × (Fin 3 → Fin 2)) ℂ

    ★ The circuit is unitary.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneExtract_mul_self :
    steaneExtract * steaneExtract = 1
    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneExtract_tags_syndrome (p : (Fin 7 → Fin 2) × (Fin 3 → Fin 2)) (z : Fin 7 → Fin 2) :
    (steaneExtract * QuantumInfo.ancInit) p z = if p = (z, syndrome z) then 1 else 0

    ★★ The ancilla ends up holding the Hamming syndrome.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneExtract_reads_syndrome (s : Fin 3 → Fin 2) :
    QuantumInfo.ancProj s * (steaneExtract * QuantumInfo.ancInit) = steaneExtract * QuantumInfo.ancInit * QuantumInfo.synProj syndrome s

    ★★★ Reading the ancilla is projecting the data onto the syndrome subspace. The circuit implements the projective syndrome measurement the corpus reasons with, as an operator identity.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneExtract_code_state {ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ} (hρ : QuantumInfo.synProj syndrome 0 * ρ * QuantumInfo.synProj syndrome 0 = ρ) :
    steaneExtract * (QuantumInfo.ancInit * ρ * QuantumInfo.ancInit.conjTranspose) * steaneExtract.conjTranspose = QuantumInfo.ancInit * ρ * QuantumInfo.ancInit.conjTranspose

    ★★★ A Steane code state is returned unchanged, ancilla included.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steaneExtract_code_state_syndrome_zero {ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ} (hρ : QuantumInfo.synProj syndrome 0 * ρ * QuantumInfo.synProj syndrome 0 = ρ) :
    QuantumInfo.ancProj 0 * (steaneExtract * (QuantumInfo.ancInit * ρ * QuantumInfo.ancInit.conjTranspose) * steaneExtract.conjTranspose) = steaneExtract * (QuantumInfo.ancInit * ρ * QuantumInfo.ancInit.conjTranspose) * steaneExtract.conjTranspose

    ★★ And the all-zero syndrome is certain on the code.

    The distance-3 mechanism, read off the ancilla #

    source
    theorem CSD.Empirical.QM.QEC.Steane.steane_extract_detects_single (z : Fin 7 → Fin 2) (j : Fin 7) :
    syndrome (z + unitErr j) ≠ syndrome z

    ★★ A single-qubit error changes what the ancilla reads. The circuit form of steane_syndrome_single_ne_zero: extraction detects every single-qubit X error.

    source
    theorem CSD.Empirical.QM.QEC.Steane.steane_extract_names_single (z : Fin 7 → Fin 2) (j j' : Fin 7) (h : syndrome (z + unitErr j) = syndrome (z + unitErr j')) :
    j = j'

    ★★ Distinct single-qubit errors read differently, so the ancilla block names the faulty qubit. The circuit form of steane_syndrome_single_injective.