Syndrome extraction as a circuit

Category: 1-Mathlib. Matrix algebra only; nothing here mentions CSD or a particular code. BACKLOG #94, split out of #62 (c1).

The corpus measures a syndrome as a projective measurement on the data register (Empirical/QM/QEC/SyndromeRecovery.lean). A circuit-level fault-tolerance argument needs it as a circuit: an ancilla block prepared in 0, a ladder of transversal CNOTs from data to ancilla, and a measurement of the ancilla. This file builds that gadget and proves what it does when nothing fails.

The whole construction is one observation: a CNOT ladder from data to ancilla is a permutation of basis labels, (z, a) ↦ (z, a + H z) for the check map H, so it is permMat of TransversalClifford.lean — no amplitudes to track, and the circuit's action on the computational basis is a relabelling.

What is proved

• extractPerm H, extractMat H — the label permutation and its matrix, with extractPerm_involutive, extractMat_conjTranspose, extractMat_mul_self and ★ extractMat_mem_unitaryGroup: the gadget is a self-inverse unitary, exactly as a CNOT ladder is. Only H z + H z = 0 is needed — characteristic two, nothing else;
• ancInit — the ancilla preparation z ↦ (z, 0), an isometry (ancInit_conjTranspose_mul);
• ancProj s — the projector reading the ancilla block as s, and synProj H s the projector on the data onto {z | H z = s}; both are Hermitian idempotents summing to 1 (sum_ancProj, sum_synProj);
• ★★ extractMat_mul_ancInit_apply — extraction tags the data with its syndrome: the circuit sends the basis state z with a fresh ancilla to (z, H z), and that single matrix-entry computation is the content of the gadget;
• ★★★ ancProj_mul_extractMat_mul_ancInit — extraction returns the syndrome: reading the ancilla as s after extraction is the same operator as projecting the data onto the syndrome-s subspace. The circuit implements the projective measurement the corpus had been assuming;
• ★★★ extractMat_mul_ancInit_mul_synProj_zero and ★★★ extractMat_conj_codeState — extraction leaves a code state alone: on the syndrome-0 subspace the circuit acts as the identity, ancilla included, so for any operator supported on the code the extracted state is the input with a fresh ancilla and nothing else;
• ★★ ancProj_zero_mul_extractMat_conj_codeState — and the syndrome-0 outcome is then certain: the extracted code state is already in that branch;
• ★ ancProj_mul_extractMat_mul_ancInit_of_ne — a syndrome the data does not have has zero amplitude, which is the statement that the measurement is not merely consistent but exhaustive.

Honest scope

⚠️ No faults are modelled. Every theorem here is about the gadget when nothing fails: this is the fault-free extraction circuit, and the faulty version — a fault in the ladder or in the ancilla — is BACKLOG #95 (the verified ancilla) and #96 (the extended rectangle). Nothing here says the gadget is fault-tolerant; it says what it computes.

⚠️ The ancilla is one unverified block. ancInit prepares the all-zero ancilla and the gadget reads it; no cat-state preparation, no verification step, and therefore no protection against a single ancilla fault spreading to the data. That is exactly what #95 is for.

⚠️ One check map, measured once. H is a single map to the syndrome labels, applied once; nothing here iterates extraction, interleaves it with gates, or composes rounds. Repeated extraction with faults is #96's extended rectangle.

⚠️ X-type only, as a relabelling. The construction works because the ladder permutes computational-basis labels. A Z-type check is the same statement in the conjugate basis and is not derived here; combining both bases for a CSS code is further work.

⚠️ No decoder. The syndrome is produced, not interpreted: nothing here maps a syndrome to a correction, and the recovery maps of the corpus are not re-derived or connected.

References

Mathlib/QuantumInfo/TransversalClifford.lean (permMat); Empirical/QM/QEC/SyndromeRecovery.lean (the projective-measurement form this replaces with a circuit); specs/BACKLOG.md #94, #95, #96, #62; specs/future-work.md.

The extraction gadget

def QuantumInfo.extractPerm {α : Type u_1} {β : Type u_2} [AddCommGroup β] (H : α → β) (p : α × β) : α × β

The label permutation a CNOT ladder performs: the data is untouched and the ancilla block is shifted by the data's check value.

Equations

• QuantumInfo.extractPerm H p = (p.1, p.2 + H p.1)

@[simp]

theorem QuantumInfo.extractPerm_fst {α : Type u_1} {β : Type u_2} [AddCommGroup β] (H : α → β) (p : α × β) : (extractPerm H p).1 = p.1

@[simp]

theorem QuantumInfo.extractPerm_snd {α : Type u_1} {β : Type u_2} [AddCommGroup β] (H : α → β) (p : α × β) : (extractPerm H p).2 = p.2 + H p.1

theorem QuantumInfo.extractPerm_involutive {α : Type u_1} {β : Type u_2} [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) : Function.Involutive (extractPerm H)

The ladder is an involution — the only arithmetic the gadget needs is characteristic two.

noncomputable def QuantumInfo.extractMat {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup β] (H : α → β) : Matrix (α × β) (α × β) ℂ

The extraction circuit: the transversal CNOT ladder from data to ancilla, as the matrix of its basis relabelling.

Equations

• QuantumInfo.extractMat H = QuantumInfo.permMat (QuantumInfo.extractPerm H)

theorem QuantumInfo.extractMat_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup β] (H : α → β) (p q : α × β) : extractMat H p q = if p = extractPerm H q then 1 else 0

theorem QuantumInfo.extractMat_conjTranspose {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) : (extractMat H).conjTranspose = extractMat H

theorem QuantumInfo.extractMat_mul_self {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) : extractMat H * extractMat H = 1

theorem QuantumInfo.extractMat_mem_unitaryGroup {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) : extractMat H ∈ Matrix.unitaryGroup (α × β) ℂ

★ The gadget is unitary, as a CNOT ladder must be.

The ancilla block: preparation and readout

def QuantumInfo.ancInit {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup β] : Matrix (α × β) α ℂ

The ancilla preparation: adjoin a fresh ancilla block in the all-zero state.

Equations

• QuantumInfo.ancInit = Matrix.of fun (p : α × β) (z : α) => if p = (z, 0) then 1 else 0

theorem QuantumInfo.ancInit_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [AddCommGroup β] (p : α × β) (z : α) : ancInit p z = if p = (z, 0) then 1 else 0

theorem QuantumInfo.ancInit_conjTranspose_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] : ancInit.conjTranspose * ancInit = 1

Preparing an ancilla is an isometry.

def QuantumInfo.ancProj {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s : β) : Matrix (α × β) (α × β) ℂ

The ancilla readout: the projector onto the ancilla block reading s.

Equations

• QuantumInfo.ancProj s = Matrix.diagonal fun (p : α × β) => if p.2 = s then 1 else 0

def QuantumInfo.synProj {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (H : α → β) (s : β) : Matrix α α ℂ

The syndrome projector on the data: the projector onto {z | H z = s}, which is what the corpus's projective-measurement form of the syndrome is.

Equations

• QuantumInfo.synProj H s = Matrix.diagonal fun (z : α) => if H z = s then 1 else 0

theorem QuantumInfo.ancProj_conjTranspose {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s : β) : (ancProj s).conjTranspose = ancProj s

theorem QuantumInfo.synProj_conjTranspose {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (H : α → β) (s : β) : (synProj H s).conjTranspose = synProj H s

theorem QuantumInfo.ancProj_mul_self {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (s : β) : ancProj s * ancProj s = ancProj s

theorem QuantumInfo.synProj_mul_self {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [DecidableEq β] (H : α → β) (s : β) : synProj H s * synProj H s = synProj H s

theorem QuantumInfo.sum_ancProj {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] [DecidableEq β] : ∑ s : β, ancProj s = 1

theorem QuantumInfo.sum_synProj {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] [DecidableEq β] (H : α → β) : ∑ s : β, synProj H s = 1

What the gadget computes

theorem QuantumInfo.extractMat_mul_ancInit_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) (p : α × β) (z : α) : (extractMat H * ancInit) p z = if p = (z, H z) then 1 else 0

★★ Extraction tags the data with its syndrome. The circuit takes the basis state z with a fresh ancilla to (z, H z): one matrix entry, and the whole content of the gadget.

theorem QuantumInfo.ancProj_mul_extractMat_mul_ancInit {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) (s : β) : ancProj s * (extractMat H * ancInit) = extractMat H * ancInit * synProj H s

★★★ Extraction returns the syndrome. Reading the ancilla block as s after extraction is the same operator as projecting the data onto the syndrome-s subspace: the circuit implements the projective measurement that the corpus's SyndromeRecovery.lean form of the syndrome assumes.

theorem QuantumInfo.ancProj_mul_extractMat_mul_ancInit_of_ne {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) {s : β} (p : α × β) (z : α) (hz : H z ≠ s) : (ancProj s * (extractMat H * ancInit)) p z = 0

★ A syndrome the data does not carry gets zero amplitude. The measurement is exhaustive, not merely consistent.

theorem QuantumInfo.ancProj_zero_mul_ancInit {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] : ancProj 0 * ancInit = ancInit

The prepared ancilla is already in the 0 branch.

theorem QuantumInfo.extractMat_mul_ancInit_mul_synProj_zero {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) : extractMat H * ancInit * synProj H 0 = ancInit * synProj H 0

★★★ On the code, extraction does nothing. Restricted to the syndrome-0 subspace the circuit acts as the identity — the ancilla comes back to 0 and the data is untouched — so "extraction leaves a code state alone" is an operator identity, not a statement about a particular state.

theorem QuantumInfo.extractMat_conj_codeState {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) {ρ : Matrix α α ℂ} (hρ : synProj H 0 * ρ * synProj H 0 = ρ) : extractMat H * (ancInit * ρ * ancInit.conjTranspose) * (extractMat H).conjTranspose = ancInit * ρ * ancInit.conjTranspose

★★★ A code state is returned unchanged, ancilla included. For any operator supported on the syndrome-0 subspace, extraction conjugates it to itself with a fresh ancilla.

theorem QuantumInfo.ancProj_zero_mul_extractMat_conj_codeState {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [AddCommGroup β] {H : α → β} (hH : ∀ (z : α), H z + H z = 0) {ρ : Matrix α α ℂ} (hρ : synProj H 0 * ρ * synProj H 0 = ρ) : ancProj 0 * (extractMat H * (ancInit * ρ * ancInit.conjTranspose) * (extractMat H).conjTranspose) = extractMat H * (ancInit * ρ * ancInit.conjTranspose) * (extractMat H).conjTranspose

★★ And the syndrome-0 outcome is certain on the code.