The ancilla ladder: how a single fault propagates, and why the cat state is needed

Category: 1-Mathlib (CSD-free). BACKLOG #95, split out of #62 (c2).

SyndromeExtraction.lean (#94) built syndrome extraction as a circuit and left one thing open in its header: the ancilla is one unverified block, so nothing bounds how far a single ancilla fault spreads into the data. This file proves what that costs, and what the cat state buys, in the Heisenberg picture Clifford.lean already supports.

The mechanism, and the two architectures

A CNOT ladder that measures a weight-w check can be wired two ways:

• shared target — all w data qubits are controls onto one ancilla qubit. Cheap, and it is what #94's gadget does;
• cat state — w ancilla qubits, each the target of one CNOT, prepared in |0…0⟩ + |1…1⟩ so the parity of their measurements is the check value. Expensive, and it is what fault-tolerant syndrome extraction actually uses.

cnotGate_conj_pauliOp says a CNOT propagates X from control to target and Z from target to control. So the dangerous direction for a data→ancilla ladder is a Z fault on the ancilla, and the two architectures differ exactly there — which is the content below.

What is proved

• laddGate anc L — the ladder with controls L and shared target anc, built from cnotGate, with ★ cnotGate_laddGate_comm (the CNOTs commute: same target, controls off the target) and ★ laddGate_involutive;
• ★★★ laddGate_conj_pauliOp — the ladder's Heisenberg action: it conjugates every Pauli to a Pauli with no phase, with the X and Z label maps xLadd, zLadd given as explicit folds of cnotFlip. This is Clifford.lean's one-gate theorem telescoped along the ladder, by induction;
• ★ zLadd_apply_target — the invariant that makes the computation work: the ladder never changes the target's own Z bit;
• ★★★ zLadd_bitAt_target_apply — the shared-target cost: a single Z fault on the shared ancilla comes out as a Z on the ancilla and on every control in the ladder. With ★★★ dataSupport_zLadd_bitAt_target and ★★ card_dataSupport_zLadd_bitAt_target, the data-side support is exactly the control list, of size L.length: one fault, w data errors;
• ★★ zLadd_singleton_apply and ★★ card_dataSupport_zLadd_singleton — the cat-state cost: with one control per ancilla qubit the same fault reaches exactly one data qubit. The contrast is the whole justification for the cat state;
• IsCat, catVerify — the cat labels (the constant strings) and the pairwise-agreement verification, with ★ catVerify_eq_zero_iff (verification passes exactly on cat labels) and ★★ not_isCat_add_bitAt / ★★ catVerify_ne_zero_of_single_flip — a single bit-flip during preparation is flagged, for every register of at least two qubits.

Together: a single ancilla fault either lands on one data qubit (cat architecture) or is caught by verification — and with the shared ancilla of #94 it lands on w of them, which for a weight-4 check is past what a distance-3 code can correct.

Honest scope

⚠️ No fault model, no probabilities, no threshold. "One fault" here means one Pauli inserted at one place, and the conclusions are support statements about where it comes out. Nothing here counts fault locations, assigns them probabilities, or proves any threshold; that is #96 and #97.

⚠️ The cat state is not prepared here. IsCat describes the labels a cat state is supported on and catVerify is the parity check on them; no preparation circuit is built, no superposition is constructed, and the X-basis measurement whose parity gives the check value is not assembled. So this file proves the propagation and flagging content of "verified ancilla", not a verified-ancilla gadget.

⚠️ Z faults on the ancilla only. That is the dangerous direction for a data→ancilla ladder, and it is the one the architectures differ on; X faults on the ancilla propagate away from the data (xLadd moves control bits into the target) and faults on the data are not the ancilla's business. No claim is made about a general fault at a general location.

⚠️ Weight is not correctability. card_dataSupport_zLadd_bitAt_target says the induced data error has weight L.length; that a weight-4 error is not corrected by a distance-3 code is not proved here — what follows is only that the distance-3 guarantee does not apply to it. The weight-1 case is the one the corpus's recovery theorems cover.

⚠️ One register, one check. The data and the ancilla live in the same Fin n register and one ladder is analysed; nothing composes rounds, interleaves gates, or tracks a second check.

⚠️ No Steane instance is built here. The theorems are stated for an arbitrary control list, so a Hamming row's weight-4 support is one of their instances, but the embedding of seven data qubits and an ancilla block into a single register is not written down and no Steane-specific number is proved in this file.

References

Mathlib/QuantumInfo/Clifford.lean (cnotGate_conj_pauliOp, cnotFlip); Mathlib/QuantumInfo/SyndromeExtraction.lean (#94, whose unverified ancilla this prices); specs/BACKLOG.md #95, #94, #96, #97, #62; specs/future-work.md.

Single-bit labels

def QuantumInfo.bitAt {n : ℕ} (j : Fin n) : Fin n → Fin 2

The label with a single bit set — one Pauli on one qubit.

Equations

• QuantumInfo.bitAt j i = if i = j then 1 else 0

@[simp]

theorem QuantumInfo.bitAt_self {n : ℕ} (j : Fin n) : bitAt j j = 1

theorem QuantumInfo.bitAt_of_ne {n : ℕ} {i j : Fin n} (h : i ≠ j) : bitAt j i = 0

The ladder

noncomputable def QuantumInfo.laddGate {n : ℕ} (anc : Fin n) : List (Fin n) → QReg n → QReg n

The ancilla ladder: a CNOT from each control in L into the shared target anc.

Equations

• QuantumInfo.laddGate anc [] x✝ = x✝
• QuantumInfo.laddGate anc (d :: L) x✝ = QuantumInfo.cnotGate d anc (QuantumInfo.laddGate anc L x✝)

@[simp]

theorem QuantumInfo.laddGate_nil {n : ℕ} (anc : Fin n) (ψ : QReg n) : laddGate anc [] ψ = ψ

@[simp]

theorem QuantumInfo.laddGate_cons {n : ℕ} (anc d : Fin n) (L : List (Fin n)) (ψ : QReg n) : laddGate anc (d :: L) ψ = cnotGate d anc (laddGate anc L ψ)

def QuantumInfo.xLadd {n : ℕ} (anc : Fin n) : List (Fin n) → (Fin n → Fin 2) → Fin n → Fin 2

The X label map of the ladder: each control's bit is added into the target.

Equations

• QuantumInfo.xLadd anc [] x✝ = x✝
• QuantumInfo.xLadd anc (d :: L) x✝ = QuantumInfo.cnotFlip d anc (QuantumInfo.xLadd anc L x✝)

def QuantumInfo.zLadd {n : ℕ} (anc : Fin n) : List (Fin n) → (Fin n → Fin 2) → Fin n → Fin 2

The Z label map of the ladder: the target's bit is added into each control. This is the direction that costs.

Equations

• QuantumInfo.zLadd anc [] x✝ = x✝
• QuantumInfo.zLadd anc (d :: L) x✝ = QuantumInfo.cnotFlip anc d (QuantumInfo.zLadd anc L x✝)

@[simp]

theorem QuantumInfo.zLadd_nil {n : ℕ} (anc : Fin n) (b : Fin n → Fin 2) : zLadd anc [] b = b

@[simp]

theorem QuantumInfo.zLadd_cons {n : ℕ} (anc d : Fin n) (L : List (Fin n)) (b : Fin n → Fin 2) : zLadd anc (d :: L) b = cnotFlip anc d (zLadd anc L b)

The ladder's CNOTs commute

theorem QuantumInfo.cnotFlip_comm_of_target {n : ℕ} {d₁ d₂ anc : Fin n} (h₁ : d₁ ≠ anc) (h₂ : d₂ ≠ anc) (z : Fin n → Fin 2) : cnotFlip d₂ anc (cnotFlip d₁ anc z) = cnotFlip d₁ anc (cnotFlip d₂ anc z)

Two CNOTs with the same target and controls off it commute, at the label level.

theorem QuantumInfo.cnotGate_laddGate_comm {n : ℕ} (anc : Fin n) (L : List (Fin n)) (hL : ∀ d ∈ L, d ≠ anc) {d : Fin n} (hd : d ≠ anc) (ψ : QReg n) : cnotGate d anc (laddGate anc L ψ) = laddGate anc L (cnotGate d anc ψ)

★ A single CNOT of the ladder commutes with the rest of it.

theorem QuantumInfo.laddGate_involutive {n : ℕ} (anc : Fin n) (L : List (Fin n)) (hL : ∀ d ∈ L, d ≠ anc) (ψ : QReg n) : laddGate anc L (laddGate anc L ψ) = ψ

★ The ladder is self-inverse.

The ladder's Heisenberg action

theorem QuantumInfo.laddGate_conj_pauliOp {n : ℕ} (anc : Fin n) (L : List (Fin n)) : (∀ d ∈ L, d ≠ anc) → ∀ (a b : Fin n → Fin 2) (ψ : QReg n), laddGate anc L (pauliOp a b (laddGate anc L ψ)) = pauliOp (xLadd anc L a) (zLadd anc L b) ψ

★★★ The ladder conjugates every Pauli to a Pauli, with no phase, and the label maps are the folds xLadd, zLadd. Clifford.lean's one-gate theorem, telescoped along the ladder.

What one Z fault on the shared ancilla costs

theorem QuantumInfo.zLadd_apply_target {n : ℕ} (anc : Fin n) (L : List (Fin n)) (hL : ∀ d ∈ L, d ≠ anc) (b : Fin n → Fin 2) : zLadd anc L b anc = b anc

★ The ladder never changes the target's own Z bit. The invariant behind every computation below.

theorem QuantumInfo.zLadd_bitAt_target_apply {n : ℕ} (anc : Fin n) (L : List (Fin n)) (hL : ∀ d ∈ L, d ≠ anc) (hnd : L.Nodup) (i : Fin n) : zLadd anc L (bitAt anc) i = if i = anc then 1 else if i ∈ L then 1 else 0

★★★ The shared-target cost. A single Z fault on the shared ancilla comes out of the ladder as a Z on the ancilla and on every control: with w controls, one fault becomes w data errors.

def QuantumInfo.dataSupport {n : ℕ} (anc : Fin n) (b : Fin n → Fin 2) : Finset (Fin n)

The data-side support of the propagated fault: the qubits other than the ancilla that carry a Z.

Equations

• QuantumInfo.dataSupport anc b = {i : Fin n | i ≠ anc ∧ b i = 1}

theorem QuantumInfo.dataSupport_zLadd_bitAt_target {n : ℕ} (anc : Fin n) (L : List (Fin n)) (hL : ∀ d ∈ L, d ≠ anc) (hnd : L.Nodup) : dataSupport anc (zLadd anc L (bitAt anc)) = L.toFinset

★★★ The data-side support is exactly the control list.

theorem QuantumInfo.card_dataSupport_zLadd_bitAt_target {n : ℕ} (anc : Fin n) (L : List (Fin n)) (hL : ∀ d ∈ L, d ≠ anc) (hnd : L.Nodup) : (dataSupport anc (zLadd anc L (bitAt anc))).card = L.length

★★ One fault, w data errors, where w is the weight of the check the ladder measures.

What the cat architecture costs instead

theorem QuantumInfo.zLadd_singleton_apply {n : ℕ} {anc d : Fin n} (h : d ≠ anc) (i : Fin n) : zLadd anc [d] (bitAt anc) i = if i = anc then 1 else if i = d then 1 else 0

★★ The cat-state cost. With one control per ancilla qubit the same fault reaches the ancilla and exactly one data qubit.

theorem QuantumInfo.card_dataSupport_zLadd_singleton {n : ℕ} {anc d : Fin n} (h : d ≠ anc) : (dataSupport anc (zLadd anc [d] (bitAt anc))).card = 1

★★ One fault, one data error — the contrast that justifies the cat state.

The cat labels and their verification

def QuantumInfo.IsCat {n : ℕ} (z : Fin n → Fin 2) : Prop

The labels a cat state is supported on: the constant strings.

Equations

• QuantumInfo.IsCat z = ∀ (i j : Fin n), z i = z j

theorem QuantumInfo.isCat_const {n : ℕ} (v : Fin 2) : IsCat fun (x : Fin n) => v

def QuantumInfo.catVerify {n : ℕ} [NeZero n] (z : Fin n → Fin 2) : Fin n → Fin 2

The verification measurement: the pairwise agreement of the ancilla bits, as a label. It vanishes exactly on the cat labels.

Equations

• QuantumInfo.catVerify z i = z i + z 0

theorem QuantumInfo.catVerify_eq_zero_iff {n : ℕ} [NeZero n] (z : Fin n → Fin 2) : catVerify z = 0 ↔ IsCat z

★ Verification passes exactly on the cat labels.

theorem QuantumInfo.not_isCat_add_bitAt {n : ℕ} {z : Fin n → Fin 2} (hz : IsCat z) {j i : Fin n} (hij : i ≠ j) : ¬IsCat (z + bitAt j)

★★ A single bit-flip takes a cat label off the cat set — on any register of at least two qubits.

theorem QuantumInfo.catVerify_ne_zero_of_single_flip {n : ℕ} [NeZero n] {z : Fin n → Fin 2} (hz : IsCat z) {j i : Fin n} (hij : i ≠ j) : catVerify (z + bitAt j) ≠ 0

★★ So a single preparation bit-flip is flagged. The verification measurement is nonzero on it, which is the content of "verified ancilla": one fault inside the preparation either lands on one data qubit or is caught.