The transversal CNOT across two Steane blocks, and a fault at one of its locations

Category: 3-Local (Empirical, QM twin). BACKLOG #62 (f), the two-block half of the transversal gate set.

SteaneFaultyGate.lean (#62 (a), (b)) treats gadgets on one block: the transversal X̄, Z̄ and Hadamard. The remaining Clifford generator acts on two blocks: CNOT on the q-th qubit of each, for all seven q. In the computational basis that gadget is a permutation of the labels, (u, v) ↦ (u, u + v), and the whole content of its transversality is that the Steane code is linear: adding a codeword of the coset of x to the coset of y lands in the coset of x + y.

• pairEnc — the two-block encoder steaneEnc ⊗ steaneEnc, as a blockKron over two blocks (#86's layer), with pairEnc_conjTranspose_mul;
• cosetAmp, steaneEnc_eq_cosetAmp — the encoder's amplitudes as coset counts, and ★★ cosetAmp_shift / ★★ steaneEnc_mul_shift: the coset shift, the linearity of the code in the form the gadget needs;
• cnotPerm, cnotT — the transversal CNOT as the permutation matrix of (u, v) ↦ (u, u + v), with cnotT_conjTranspose, cnotT_mul_self (it is its own inverse) and cnotT_mem_unitaryGroup; cnotL is the logical CNOT, the same permutation on two bits;
• ★★★ cnotT_mul_pairEnc — the transversal CNOT IS the logical CNOT: CNOT^{⊗7} · (V ⊗ V) = (V ⊗ V) · CNOT, in the Schrödinger picture, so ★★ cnotT_conj_pairEnc_code gives the ideal gadget's action on an encoded pair of qubits;
• pairFam, ★★ encoderKL_pairFam, ★★ exists_pair_recovery — one recovery channel for the two blocks, from Knill–Laflamme in encoder form (#86): the family is one single-qubit Pauli per block, and the condition composes over the blocks because steaneEnc_pauli_pair holds in each;
• ★★★ steane_faultyCNOT_recovery — a faulty transversal CNOT is corrected: one bad location (an arbitrary unitary on the two qubits of one CNOT, in product form) leaves the recovery returning the ideal output, the logical CNOT applied to the encoded pair.

Honest scope

⚠️ The fault at a location is taken in product form A ⊗ B (an arbitrary single-qubit operator on each of the two qubits of that CNOT). Products span the operators on two qubits, and recovery_apply_lin_comb is exactly the tool that lifts the statement to sums, but the general non-product fault is not stated: it would need a pair-register view of the two-block labels, which this file does not build.

⚠️ The recovery is the Knill–Laflamme channel of the two-block code, not two independent per-block recoveries; nothing here says the two blocks can be corrected separately (they can, but that needs a tensor product of channels, which the corpus does not have).

⚠️ Faults in the recovery gadget — extended rectangles — are still BACKLOG #62 (c), and the simulation theorem #62 (d).

References: A. Steane, PRL 77 (1996); M. Nielsen, I. Chuang, Quantum Computation and Quantum Information §10.4.2 (CSS codes and transversal gates); P. Aliferis, D. Gottesman, J. Preskill, Quantum Inf. Comput. 6 (2006); Empirical/QM/QEC/SteaneConcat.lean (#86); specs/BACKLOG.md #62 (f); specs/steane-plan.md.

The two-block encoder

noncomputable def CSD.Empirical.QM.QEC.Steane.pairEnc : Matrix (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 2) ℂ

The encoder of a pair of Steane blocks: steaneEnc on each, as a tensor over two blocks.

Equations

• CSD.Empirical.QM.QEC.Steane.pairEnc = QuantumInfo.blockKron fun (x : Fin 2) => CSD.Empirical.QM.QEC.Steane.steaneEnc

theorem CSD.Empirical.QM.QEC.Steane.pairEnc_conjTranspose_mul : pairEnc.conjTranspose * pairEnc = 1

theorem CSD.Empirical.QM.QEC.Steane.pairEnc_apply (z : Fin 2 → Fin 7 → Fin 2) (c : Fin 2 → Fin 2) : pairEnc z c = steaneEnc (z 0) (c 0) * steaneEnc (z 1) (c 1)

The encoder's amplitudes are coset counts

def CSD.Empirical.QM.QEC.Steane.constVec (y : Fin 2) : Fin 7 → Fin 2

The constant label: 0 for the code itself, the all-ones vector for the other coset.

Equations

• CSD.Empirical.QM.QEC.Steane.constVec y x✝ = y

theorem CSD.Empirical.QM.QEC.Steane.constVec_zero : constVec 0 = 0

theorem CSD.Empirical.QM.QEC.Steane.constVec_one : constVec 1 = allOnes

theorem CSD.Empirical.QM.QEC.Steane.constVec_add (x y : Fin 2) : constVec (x + y) = constVec x + constVec y

noncomputable def CSD.Empirical.QM.QEC.Steane.cosetAmp (y : Fin 2) (z : Fin 7 → Fin 2) : ℂ

How many row-space representatives put z in the coset labelled y.

Equations

• CSD.Empirical.QM.QEC.Steane.cosetAmp y z = ∑ c : Fin 3 → Fin 2, if z = CSD.Empirical.QM.QEC.Steane.rowComb c + CSD.Empirical.QM.QEC.Steane.constVec y then 1 else 0

theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_eq_cosetAmp (z : Fin 7 → Fin 2) (y : Fin 2) : steaneEnc z y = (↑√8)⁻¹ * cosetAmp y z

The encoder's entries are the coset counts, normalised: the logical states are the uniform superpositions over the code and its coset.

theorem CSD.Empirical.QM.QEC.Steane.cosetAmp_shift {u : Fin 7 → Fin 2} {x : Fin 2} {c₀ : Fin 3 → Fin 2} (hu : u = rowComb c₀ + constVec x) (v : Fin 7 → Fin 2) (y : Fin 2) : cosetAmp y (u + v) = cosetAmp (x + y) v

★★ The coset shift. If u lies in the coset labelled x, adding u carries the coset labelled y onto the coset labelled x + y: the code is linear, which is the whole reason a transversal CNOT is a logical CNOT.

theorem CSD.Empirical.QM.QEC.Steane.steaneEnc_mul_shift (u v : Fin 7 → Fin 2) (x y : Fin 2) : steaneEnc u x * steaneEnc (u + v) y = steaneEnc u x * steaneEnc v (x + y)

★★ The product form the gadget consumes: on the support of the coset of x, shifting by u relabels y as x + y.

The transversal CNOT

def CSD.Empirical.QM.QEC.Steane.cnotPerm (z : Fin 2 → Fin 7 → Fin 2) : Fin 2 → Fin 7 → Fin 2

The label permutation of the transversal CNOT: the control block is unchanged, the target block is added the control, qubit by qubit.

Equations

• CSD.Empirical.QM.QEC.Steane.cnotPerm z = ![z 0, z 0 + z 1]

theorem CSD.Empirical.QM.QEC.Steane.cnotPerm_involutive : Function.Involutive cnotPerm

def CSD.Empirical.QM.QEC.Steane.cnotPermL (c : Fin 2 → Fin 2) : Fin 2 → Fin 2

The logical CNOT, the same permutation on two bits.

Equations

• CSD.Empirical.QM.QEC.Steane.cnotPermL c = ![c 0, c 0 + c 1]

theorem CSD.Empirical.QM.QEC.Steane.cnotPermL_involutive : Function.Involutive cnotPermL

noncomputable def CSD.Empirical.QM.QEC.Steane.cnotT : Matrix (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 7 → Fin 2) ℂ

The transversal CNOT on two blocks: CNOT between the q-th qubits, for every q — the permutation matrix of cnotPerm.

Equations

• CSD.Empirical.QM.QEC.Steane.cnotT = QuantumInfo.permMat CSD.Empirical.QM.QEC.Steane.cnotPerm

noncomputable def CSD.Empirical.QM.QEC.Steane.cnotL : Matrix (Fin 2 → Fin 2) (Fin 2 → Fin 2) ℂ

The logical CNOT on the two encoded qubits.

Equations

• CSD.Empirical.QM.QEC.Steane.cnotL = QuantumInfo.permMat CSD.Empirical.QM.QEC.Steane.cnotPermL

theorem CSD.Empirical.QM.QEC.Steane.cnotT_conjTranspose : cnotT.conjTranspose = cnotT

theorem CSD.Empirical.QM.QEC.Steane.cnotT_mul_self : cnotT * cnotT = 1

theorem CSD.Empirical.QM.QEC.Steane.cnotT_mem_unitaryGroup : cnotT ∈ Matrix.unitaryGroup (Fin 2 → Fin 7 → Fin 2) ℂ

theorem CSD.Empirical.QM.QEC.Steane.cnotL_conjTranspose : cnotL.conjTranspose = cnotL

theorem CSD.Empirical.QM.QEC.Steane.cnotL_mul_self : cnotL * cnotL = 1

theorem CSD.Empirical.QM.QEC.Steane.cnotT_mul_pairEnc : cnotT * pairEnc = pairEnc * cnotL

★★★ The transversal CNOT is the logical CNOT. Conjugating the pair encoder by the gadget is the logical gate on the two encoded qubits — the Schrödinger-picture statement, with the coset shift as the only input.

theorem CSD.Empirical.QM.QEC.Steane.cnotT_conj_pairEnc_code (ρ : Matrix (Fin 2 → Fin 2) (Fin 2 → Fin 2) ℂ) : cnotT * (pairEnc * ρ * pairEnc.conjTranspose) * cnotT.conjTranspose = pairEnc * (cnotL * ρ * cnotL.conjTranspose) * pairEnc.conjTranspose

★★ The ideal gadget on an encoded pair: the logical CNOT, conjugated into the code.

The two-block recovery

noncomputable def CSD.Empirical.QM.QEC.Steane.pairFam (g : Fin 2 → SingleErr) : Matrix (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 7 → Fin 2) ℂ

The error family of the pair: one single-qubit Pauli in each block.

Equations

• CSD.Empirical.QM.QEC.Steane.pairFam g = QuantumInfo.blockKron fun (b : Fin 2) => QuantumInfo.pauliMat (CSD.Empirical.QM.QEC.Steane.errA (g b)) (CSD.Empirical.QM.QEC.Steane.errB (g b))

theorem CSD.Empirical.QM.QEC.Steane.encoderKL_pairFam : QuantumInfo.EncoderKL pairEnc pairFam

★★ Knill–Laflamme in encoder form for the pair: it composes over the blocks, because it holds in each (steaneEnc_pauli_pair).

theorem CSD.Empirical.QM.QEC.Steane.exists_pair_recovery : ∃ (c : Matrix (Fin 2 → SingleErr) (Fin 2 → SingleErr) ℂ) (R : QuantumInfo.Channel (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 7 → Fin 2) (Option (Fin 2 → SingleErr))), ∀ (ρ : Matrix (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 7 → Fin 2) ℂ), ρ = pairEnc * pairEnc.conjTranspose * ρ * (pairEnc * pairEnc.conjTranspose) → ∀ (g h : Fin 2 → SingleErr), R.apply (pairFam g * ρ * (pairFam h).conjTranspose) = c h g • ρ

★★ One recovery channel for the two blocks.

A fault at one location of the gadget

noncomputable def CSD.Empirical.QM.QEC.Steane.pairFault (q : Fin 7) (A B : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 7 → Fin 2) ℂ

A product fault on the two qubits of the q-th CNOT: an arbitrary single-qubit operator on each block's q-th qubit.

Equations

• CSD.Empirical.QM.QEC.Steane.pairFault q A B = QuantumInfo.blockKron ![QuantumInfo.Controlled.gateOf q A, QuantumInfo.Controlled.gateOf q B]

theorem CSD.Empirical.QM.QEC.Steane.pairFault_eq_sum (q : Fin 7) (A B : Matrix (Fin 2) (Fin 2) ℂ) : pairFault q A B = ∑ g : Fin 2 → SingleErr, (∏ b : Fin (Nat.succ 1), ![singleCoeff q A, singleCoeff q B] b (g b)) • pairFam g

The fault is a combination of the family: the Paulis span the operators of a qubit (gateOf_eq_sum_pauliMat) and the tensor over blocks is multilinear.

A faulty transversal CNOT is corrected

theorem CSD.Empirical.QM.QEC.Steane.pairFault_conjTranspose_mul {q : Fin 7} {A B : Matrix (Fin 2) (Fin 2) ℂ} (hA : A ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hB : B ∈ Matrix.unitaryGroup (Fin 2) ℂ) : (pairFault q A B).conjTranspose * pairFault q A B = 1

theorem CSD.Empirical.QM.QEC.Steane.trace_pairEnc_conj (ρ : Matrix (Fin 2 → Fin 2) (Fin 2 → Fin 2) ℂ) : (pairEnc * ρ * pairEnc.conjTranspose).trace = ρ.trace

theorem CSD.Empirical.QM.QEC.Steane.trace_cnotL_conj (ρ : Matrix (Fin 2 → Fin 2) (Fin 2 → Fin 2) ℂ) : (cnotL * ρ * cnotL.conjTranspose).trace = ρ.trace

theorem CSD.Empirical.QM.QEC.Steane.steane_faultyCNOT_recovery : ∃ (R : QuantumInfo.Channel (Fin 2 → Fin 7 → Fin 2) (Fin 2 → Fin 7 → Fin 2) (Option (Fin 2 → SingleErr))), ∀ (ρ : Matrix (Fin 2 → Fin 2) (Fin 2 → Fin 2) ℂ) (q : Fin 7) (A B : Matrix (Fin 2) (Fin 2) ℂ), A ∈ Matrix.unitaryGroup (Fin 2) ℂ → B ∈ Matrix.unitaryGroup (Fin 2) ℂ → ρ.trace ≠ 0 → R.apply (pairFault q A B * (cnotT * (pairEnc * ρ * pairEnc.conjTranspose) * cnotT.conjTranspose) * (pairFault q A B).conjTranspose) = pairEnc * (cnotL * ρ * cnotL.conjTranspose) * pairEnc.conjTranspose

★★★ A faulty transversal CNOT is corrected. The gadget is CNOT between the q-th qubits of the two blocks for every q — the logical CNOT, by cnotT_mul_pairEnc — and one of its seven locations is faulty, the fault an arbitrary unitary on each of that location's two qubits. One channel returns the ideal output: the logical CNOT applied to the encoded pair.