The magic layer: the T gate escapes the Clifford closure (candidate 5)

Category: 1-Mathlib (CSD-free).

Glossary: https://glossary.constraintsurfacedynamics.com/magic-state/ Plain-language, CSD-role and formal statements of magic states, with this module as their Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The precise complement of the Gottesman–Knill mechanism (plan specs/magic-plan.md): GK-2 proved that H, S, CNOT conjugate every Pauli to a phase times a Pauli — the closure that makes Clifford circuits classically trackable. This module proves the boundary is real: the T gate (the π/8 gate) breaks it, which is why T is the standard route to universality and why magic states are a resource.

• The Clifford hierarchy, level by level: T² = S (tGate_tGate — T sits one level above the Clifford group, its square descending into it), and ★ tGate_conj_X: T X T† = (X + i·XZ)/√2 — conjugation by T carries the Pauli X out of the Pauli family but into its Clifford-algebra span: the level-3 hierarchy statement, as a closed operator identity.
• ★★ The no-go (tGate_conj_X_not_pauli): there are no c, a, b with T X T† = c·X^a Z^b. Together with GK-2 this brackets the Clifford group sharply: H, S, CNOT stay inside the Pauli-conjugation closure, T provably leaves it. The proof pins two coordinates and derives 1 = ±i — a two-line arithmetic absurdity.
• The magic state |T⟩ = T·H|0⟩ (magicState), coordinates (1, e^{iπ/4})/√2 (magicState_apply), unit norm (inner_magicState_self) — the resource state whose consumption implements T by Clifford operations alone in the standard injection circuit.

Honest scope. This module formalises what magic is — the provable escape from the Clifford closure and the resource state — not how it is used or distilled: the Bravyi–Kitaev 15-to-1 distillation protocol is not attempted (⚠️ RESIDUE(R-004)), no universality claim is made — that would need a gate-synthesis density theorem (⚠️ RESIDUE(R-005)) — and the gate-teleportation circuit injecting T from magicState is not attempted (⚠️ RESIDUE(R-006)). No priority claim of any kind (CL-061 rule).

The T gate

noncomputable def QuantumInfo.tPhase : ℂ

The T phase e^{iπ/4}.

Equations

• QuantumInfo.tPhase = Complex.exp (↑(Real.pi / 4) * Complex.I)

noncomputable def QuantumInfo.tPhaseInv : ℂ

The inverse T phase e^{−iπ/4}.

Equations

• QuantumInfo.tPhaseInv = Complex.exp (↑(-(Real.pi / 4)) * Complex.I)

theorem QuantumInfo.tPhase_mul_inv : tPhase * tPhaseInv = 1

theorem QuantumInfo.tPhaseInv_mul : tPhaseInv * tPhase = 1

theorem QuantumInfo.tPhase_sq : tPhase * tPhase = Complex.I

T² = S at the phase level: (e^{iπ/4})² = i.

theorem QuantumInfo.tPhase_ne_zero : tPhase ≠ 0

theorem QuantumInfo.sqrt_two_div_two : √2 / 2 = (√2)⁻¹

√2/2 = (√2)⁻¹.

theorem QuantumInfo.tPhase_eq : tPhase = (↑√2)⁻¹ * (1 + Complex.I)

The explicit value e^{iπ/4} = (1 + i)/√2.

theorem QuantumInfo.tPhaseInv_eq : tPhaseInv = (↑√2)⁻¹ * (1 - Complex.I)

The explicit value e^{−iπ/4} = (1 − i)/√2.

noncomputable def QuantumInfo.tGate {n : ℕ} (j : Fin n) (ψ : QReg n) : QReg n

The T gate (π/8 gate) on qubit j: phase e^{iπ/4} on the z_j = 1 branch.

Equations

• QuantumInfo.tGate j ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => QuantumInfo.tPhase ^ ↑(z j) * ψ.ofLp z

noncomputable def QuantumInfo.tGateInv {n : ℕ} (j : Fin n) (ψ : QReg n) : QReg n

The inverse T gate.

Equations

• QuantumInfo.tGateInv j ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => QuantumInfo.tPhaseInv ^ ↑(z j) * ψ.ofLp z

@[simp]

theorem QuantumInfo.tGate_apply {n : ℕ} (j : Fin n) (ψ : QReg n) (z : Fin n → Fin 2) : (tGate j ψ).ofLp z = tPhase ^ ↑(z j) * ψ.ofLp z

@[simp]

theorem QuantumInfo.tGateInv_apply {n : ℕ} (j : Fin n) (ψ : QReg n) (z : Fin n → Fin 2) : (tGateInv j ψ).ofLp z = tPhaseInv ^ ↑(z j) * ψ.ofLp z

theorem QuantumInfo.tGate_tGateInv {n : ℕ} (j : Fin n) (ψ : QReg n) : tGate j (tGateInv j ψ) = ψ

theorem QuantumInfo.tGateInv_tGate {n : ℕ} (j : Fin n) (ψ : QReg n) : tGateInv j (tGate j ψ) = ψ

theorem QuantumInfo.tGate_tGate {n : ℕ} (j : Fin n) (ψ : QReg n) : tGate j (tGate j ψ) = sGate j ψ

The hierarchy descends: T² = S — the square of the non-Clifford gate is Clifford.

Conjugating X: out of the Pauli family, into its span

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

The single-bit label at j.

Equations

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

theorem QuantumInfo.unitV_apply_self {n : ℕ} (j : Fin n) : unitV j j = 1

theorem QuantumInfo.bdot_unitV {n : ℕ} (j : Fin n) (w : Fin n → Fin 2) : bdot (unitV j) w = w j

theorem QuantumInfo.tGate_conj_X {n : ℕ} (j : Fin n) (ψ : QReg n) : tGate j (pauliOp (unitV j) 0 (tGateInv j ψ)) = (↑√2)⁻¹ • (pauliOp (unitV j) 0 ψ + Complex.I • pauliOp (unitV j) (unitV j) ψ)

★ The level-3 hierarchy identity: T X T† = (X + i·XZ)/√2 — conjugation by T carries the Pauli X out of the Pauli family, but only into its two-term Clifford-algebra span.

theorem QuantumInfo.tGate_smul {n : ℕ} (j : Fin n) (c : ℂ) (ψ : QReg n) : tGate j (c • ψ) = c • tGate j ψ

The T gate is homogeneous.

theorem QuantumInfo.tGate_basisState {n : ℕ} (j : Fin n) (w : Fin n → Fin 2) : tGate j (basisState w) = tPhase ^ ↑(w j) • basisState w

The T gate on a basis state: a pure phase.

theorem QuantumInfo.tGateInv_basisState {n : ℕ} (j : Fin n) (w : Fin n → Fin 2) : tGateInv j (basisState w) = tPhaseInv ^ ↑(w j) • basisState w

The inverse T gate on a basis state: a pure phase.

theorem QuantumInfo.tconjX_basisState {n : ℕ} (j : Fin n) (w : Fin n → Fin 2) : tGate j (pauliOp (unitV j) 0 (tGateInv j (basisState w))) = (tPhaseInv ^ ↑(w j) * tPhase ^ ↑(w j + 1)) • basisState (w + unitV j)

T X T† on a basis state, in closed form.

theorem QuantumInfo.tGate_conj_X_not_pauli : ¬∃ (c : ℂ) (a : Fin 1 → Fin 2) (b : Fin 1 → Fin 2), ∀ (ψ : QReg 1), tGate 0 (pauliOp (unitV 0) 0 (tGateInv 0 ψ)) = c • pauliOp a b ψ

★★ The no-go: T is not Clifford. There are no c, a, b with T X T† = c · X^a Z^b — the conjugation escape is genuine, not a phase artefact. Pinning the two basis columns forces 1 = ±i.

The magic state

noncomputable def QuantumInfo.magicState : QReg 1

The magic state |T⟩ = T·H|0⟩ on one qubit.

Equations

• QuantumInfo.magicState = QuantumInfo.tGate 0 (QuantumInfo.hGate 0 (QuantumInfo.basisState fun (x : Fin 1) => 0))

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

Coordinates: |T⟩ = (|0⟩ + e^{iπ/4}|1⟩)/√2.

theorem QuantumInfo.inner_magicState_self : inner ℂ magicState magicState = 1

The magic state is a unit vector.