T-gate injection: the magic state enacts T through Clifford gates and a measurement

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #66 and #67, the two rows of R-006 (specs/magic-plan.md, "The split").

The gate-teleportation circuit: data qubit ψ on wire 0, the magic state |A⟩ = (|0⟩ + e^{iπ/4}|1⟩)/√2 (magicState) on wire 1; CNOT with control 0 and target 1; measure the ancilla in the computational basis with outcome m; apply S^m to the data. The data qubit is then T ψ — up to the normalisation 1/√2 of the outcome and, for m = 1, the global phase e^{iπ/4}:

(S^m ⊗ ⟨m|) · CNOT · (ψ ⊗ |A⟩) = (1/√2) · e^{imπ/4} · T ψ.

• dataAnc ψ φ : QReg 2 — the product state (data, ancilla); sCorr m — the correction S^m on the data wire; injectSlice φ m ψ : QReg 1 — the unnormalised data state after the circuit with resource φ and outcome m;
• ★★ injectSlice_magicState — the injection identity (row #66): with the resource magicState, injectSlice magicState m ψ = (1/√2) e^{imπ/4} • T ψ, for both outcomes; norm_sq_injectSlice_magicState — each outcome has probability ½;
• ★ injectSlice_zMagicState — the error transfers: with the resource Z|A⟩ the circuit yields (1/√2)(−e^{iπ/4})^m • Z T ψ;
• injectionKraus φ m — the Kraus operator (S^m ⊗ ⟨m|) · CNOT · (1 ⊗ |φ⟩) as a matrix on the data qubit; injectionKraus_magicState, injectionKraus_zMagicState — their closed forms c_m • T and c'_m • Z T;
• injectionChannel : Channel — the circuit as a quantum channel on the data qubit; ★★ injectionChannel_apply — T enacted (row #67, closes R-006): Φ(ρ) = T ρ T† for every ρ, consuming one magic state;
• noisyInjectionChannel p — the same with the resource (1 − p)|A⟩⟨A| + p Z|A⟩⟨A|Z; ★ noisyInjectionChannel_apply — Φ_p(ρ) = (1 − p) T ρ T† + p Z T ρ T† Z: a Z-error on the resource becomes a Z-error on the output, the error model that distillation (#75–#78) consumes.

Honest scope

⚠️ One data qubit; the two-qubit circuit is written in the coordinate-operator model of Clifford.lean/Magic.lean (wires 0 and 1 of QReg 2). The channel is the outcome-averaged one with the classical correction applied; the measurement statistics are the ‖·‖² of the slices. Distillation of noisy magic states is BACKLOG #75–#79, Clifford+T density #68–#74.

References: D. Gottesman, I. Chuang, Nature 402 (1999) 390; S. Bravyi, A. Kitaev, PRA 71 (2005) 022316 §II; Nielsen–Chuang §10.6.2; specs/magic-plan.md; specs/BACKLOG.md #66, #67; specs/future-work.md.

The circuit

def QuantumInfo.pair (x m : Fin 2) : Fin 2 → Fin 2

The two-qubit label (x, m): data x on wire 0, ancilla m on wire 1.

Equations

• QuantumInfo.pair x m = ![x, m]

@[simp]

theorem QuantumInfo.pair_zero (x m : Fin 2) : pair x m 0 = x

@[simp]

theorem QuantumInfo.pair_one (x m : Fin 2) : pair x m 1 = m

noncomputable def QuantumInfo.dataAnc (ψ φ : QReg 1) : QReg 2

The product state ψ ⊗ φ on two qubits: data ψ on wire 0, ancilla φ on wire 1.

Equations

• QuantumInfo.dataAnc ψ φ = (WithLp.equiv 2 ((Fin 2 → Fin 2) → ℂ)).symm fun (z : Fin 2 → Fin 2) => (ψ.ofLp fun (x : Fin 1) => z 0) * φ.ofLp fun (x : Fin 1) => z 1

@[simp]

theorem QuantumInfo.dataAnc_apply (ψ φ : QReg 1) (z : Fin 2 → Fin 2) : (dataAnc ψ φ).ofLp z = (ψ.ofLp fun (x : Fin 1) => z 0) * φ.ofLp fun (x : Fin 1) => z 1

noncomputable def QuantumInfo.sCorr (m : Fin 2) (Φ : QReg 2) : QReg 2

The correction S^m on the data wire.

Equations

• QuantumInfo.sCorr m Φ = if m = 0 then Φ else QuantumInfo.sGate 0 Φ

noncomputable def QuantumInfo.injectSlice (φ : QReg 1) (m : Fin 2) (ψ : QReg 1) : QReg 1

The unnormalised data state after the injection circuit with resource φ and outcome m: (S^m ⊗ ⟨m|) · CNOT_{01} · (ψ ⊗ φ).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumInfo.injectSlice_apply (φ : QReg 1) (m : Fin 2) (ψ : QReg 1) (x : Fin 1 → Fin 2) : (injectSlice φ m ψ).ofLp x = (sCorr m (cnotGate 0 1 (dataAnc ψ φ))).ofLp (pair (x 0) m)

theorem QuantumInfo.cnotFlip_pair (x m : Fin 2) : cnotFlip 0 1 (pair x m) = pair x (m + x)

theorem QuantumInfo.fun_const_eq (x : Fin 1 → Fin 2) : (fun (x_1 : Fin 1) => x 0) = x

theorem QuantumInfo.injectSlice_apply_eq (φ : QReg 1) (m : Fin 2) (ψ : QReg 1) (x : Fin 1 → Fin 2) : (injectSlice φ m ψ).ofLp x = Complex.I ^ (↑m * ↑(x 0)) * (ψ.ofLp x * φ.ofLp fun (x_1 : Fin 1) => m + x 0)

The coordinate of the slice, before the case split on the outcome.

The injection identity

theorem QuantumInfo.conj_tPhase : (starRingEnd ℂ) tPhase = tPhaseInv

theorem QuantumInfo.norm_tPhase : ‖tPhase‖ = 1

theorem QuantumInfo.fin_two_one_add_one : 1 + 1 = 0

theorem QuantumInfo.signChar_one : signChar 1 = -1

theorem QuantumInfo.injectSlice_magicState (m : Fin 2) (ψ : QReg 1) : injectSlice magicState m ψ = ((↑√2)⁻¹ * tPhase ^ ↑m) • tGate 0 ψ

★★ The injection identity (BACKLOG #66): with the magic state as resource, the data qubit after outcome m and the correction S^m is (1/√2) e^{imπ/4} · T ψ.

theorem QuantumInfo.norm_tGate (ψ : QReg 1) : ‖tGate 0 ψ‖ = ‖ψ‖

theorem QuantumInfo.norm_sq_injectSlice_magicState (m : Fin 2) (ψ : QReg 1) : ‖injectSlice magicState m ψ‖ ^ 2 = ‖ψ‖ ^ 2 / 2

Each outcome of the injection has probability ½: ‖slice‖² = ‖ψ‖²/2.

The error transfers

noncomputable def QuantumInfo.zMagicState : QReg 1

Z|A⟩, the magic state with a phase-flip error.

Equations

• QuantumInfo.zMagicState = QuantumInfo.pauliOp 0 (QuantumInfo.unitV 0) QuantumInfo.magicState

theorem QuantumInfo.zMagicState_apply (z : Fin 1 → Fin 2) : zMagicState.ofLp z = signChar (z 0) * ((↑√2)⁻¹ * tPhase ^ ↑(z 0))

theorem QuantumInfo.injectSlice_zMagicState (m : Fin 2) (ψ : QReg 1) : injectSlice zMagicState m ψ = ((↑√2)⁻¹ * (-tPhase) ^ ↑m) • pauliOp 0 (unitV 0) (tGate 0 ψ)

★ A Z-error on the resource becomes a Z-error on the output: with Z|A⟩ the circuit yields (1/√2)(−e^{iπ/4})^m · Z T ψ.

The Kraus operators and the channel

noncomputable def QuantumInfo.tMat : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ

The T gate as a matrix on one qubit.

Equations

• QuantumInfo.tMat = Matrix.diagonal fun (z : Fin 1 → Fin 2) => QuantumInfo.tPhase ^ ↑(z 0)

def QuantumInfo.zMat : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ

The Z gate as a matrix on one qubit.

Equations

• QuantumInfo.zMat = Matrix.diagonal fun (z : Fin 1 → Fin 2) => QuantumInfo.signChar (z 0)

noncomputable def QuantumInfo.injectionKraus (φ : QReg 1) (m : Fin 2) : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ

The Kraus operator of outcome m with resource φ: the matrix of ψ ↦ injectSlice φ m ψ, i.e. (S^m ⊗ ⟨m|) · CNOT · (1 ⊗ |φ⟩).

Equations

• QuantumInfo.injectionKraus φ m = Matrix.of fun (x y : Fin 1 → Fin 2) => (QuantumInfo.injectSlice φ m (QuantumInfo.basisState y)).ofLp x

theorem QuantumInfo.tGate_basisState_apply (x y : Fin 1 → Fin 2) : (tGate 0 (basisState y)).ofLp x = tMat x y

theorem QuantumInfo.injectionKraus_magicState (m : Fin 2) : injectionKraus magicState m = ((↑√2)⁻¹ * tPhase ^ ↑m) • tMat

theorem QuantumInfo.injectionKraus_zMagicState (m : Fin 2) : injectionKraus zMagicState m = ((↑√2)⁻¹ * (-tPhase) ^ ↑m) • (zMat * tMat)

theorem QuantumInfo.tMat_conjTranspose_mul : tMat.conjTranspose * tMat = 1

theorem QuantumInfo.zMat_conjTranspose_mul : zMat.conjTranspose * zMat = 1

theorem QuantumInfo.zMat_mul_tMat_conjTranspose_mul : (zMat * tMat).conjTranspose * (zMat * tMat) = 1

theorem QuantumInfo.conjTranspose_smul_mul_smul (c : ℂ) (A B : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ) : (c • A).conjTranspose * c • B = ((starRingEnd ℂ) c * c) • (A.conjTranspose * B)

theorem QuantumInfo.smul_mul_mul_conjTranspose_smul (c : ℂ) (A ρ B : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ) : c • A * ρ * (c • B).conjTranspose = (c * (starRingEnd ℂ) c) • (A * ρ * B.conjTranspose)

theorem QuantumInfo.conj_coeff_mul (m : Fin 2) : (starRingEnd ℂ) ((↑√2)⁻¹ * tPhase ^ ↑m) * ((↑√2)⁻¹ * tPhase ^ ↑m) = 2⁻¹

theorem QuantumInfo.conj_coeff_mul' (m : Fin 2) : (starRingEnd ℂ) ((↑√2)⁻¹ * (-tPhase) ^ ↑m) * ((↑√2)⁻¹ * (-tPhase) ^ ↑m) = 2⁻¹

theorem QuantumInfo.coeff_mul_conj (m : Fin 2) : (↑√2)⁻¹ * tPhase ^ ↑m * (starRingEnd ℂ) ((↑√2)⁻¹ * tPhase ^ ↑m) = 2⁻¹

theorem QuantumInfo.coeff_mul_conj' (m : Fin 2) : (↑√2)⁻¹ * (-tPhase) ^ ↑m * (starRingEnd ℂ) ((↑√2)⁻¹ * (-tPhase) ^ ↑m) = 2⁻¹

theorem QuantumInfo.sum_kraus_magicState : ∑ m : Fin 2, (injectionKraus magicState m).conjTranspose * injectionKraus magicState m = 1

The two Kraus operators of the magic-state circuit are trace-preserving.

theorem QuantumInfo.sum_kraus_zMagicState : ∑ m : Fin 2, (injectionKraus zMagicState m).conjTranspose * injectionKraus zMagicState m = 1

theorem QuantumInfo.sum_apply_magicState (ρ : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ) : ∑ m : Fin 2, injectionKraus magicState m * ρ * (injectionKraus magicState m).conjTranspose = tMat * ρ * tMat.conjTranspose

theorem QuantumInfo.sum_apply_zMagicState (ρ : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ) : ∑ m : Fin 2, injectionKraus zMagicState m * ρ * (injectionKraus zMagicState m).conjTranspose = zMat * tMat * ρ * (zMat * tMat).conjTranspose

noncomputable def QuantumInfo.injectionChannel : Channel (Fin 1 → Fin 2) (Fin 1 → Fin 2) (Fin 2)

The injection channel on the data qubit: Kraus operators (S^m ⊗ ⟨m|) · CNOT · (1 ⊗ |A⟩), m = 0, 1.

Equations

• QuantumInfo.injectionChannel = { kraus := QuantumInfo.injectionKraus QuantumInfo.magicState, tp := QuantumInfo.sum_kraus_magicState }

theorem QuantumInfo.injectionChannel_apply (ρ : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ) : injectionChannel.apply ρ = tMat * ρ * tMat.conjTranspose

★★ T enacted by injection (BACKLOG #67, closes R-006): the outcome-averaged, corrected channel of the gate-teleportation circuit with one magic state is exactly ρ ↦ T ρ T†.

noncomputable def QuantumInfo.noisyInjectionChannel (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : Channel (Fin 1 → Fin 2) (Fin 1 → Fin 2) (Fin 2 × Bool)

The noisy injection channel: the resource is (1 − p)|A⟩⟨A| + p Z|A⟩⟨A|Z, so the Kraus operators are √(1 − p) times those of |A⟩ and √p times those of Z|A⟩.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumInfo.noisyInjectionChannel_apply {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (ρ : Matrix (Fin 1 → Fin 2) (Fin 1 → Fin 2) ℂ) : (noisyInjectionChannel p hp hp1).apply ρ = ↑(1 - p) • (tMat * ρ * tMat.conjTranspose) + ↑p • (zMat * tMat * ρ * (zMat * tMat).conjTranspose)

★ A Z-error on the resource is a Z-error on the output: the noisy injection channel is (1 − p) T ρ T† + p Z T ρ T† Z.