Empirical/QM: Two-qubit gates (CNOT, SWAP, CZ)

Category: 3-Local (promotion-ready to 2-Framework on demand).

Pure linear-algebra definitions for the canonical two-qubit gates on Matrix (Fin 4) (Fin 4) ℂ, with their involutivity properties (G * G = 1). These gates are real Hermitian permutation/diagonal matrices, so involutivity coincides with unitarity: each qmG*_hermitian (Gᴴ = G) combines with the involutive qmG*_mul_self to give qmG*_unitary (Gᴴ * G = 1), now proved for every gate. No CSD ontology; the CSD-side reading lives in the companion Empirical/CSD/Gates/TwoQubit.lean.

Contents

• qmCNOT: controlled-NOT, involutive, Hermitian, unitary.
• qmSWAP: swap, involutive, Hermitian, unitary.
• qmCZ: controlled-Z, involutive, Hermitian, unitary.

Basis order |00⟩, |01⟩, |10⟩, |11⟩ (qubit-0 = high bit, qubit-1 = low bit). Function-based matrix definitions; the !! notation fails to propagate ℂ elaboration cleanly for 4×4.

noncomputable def CSD.Empirical.QM.Gates.qmCNOT : Matrix (Fin 4) (Fin 4) ℂ

Controlled-NOT gate on Fin 4.

Equations

• CSD.Empirical.QM.Gates.qmCNOT = Matrix.of fun (i j : Fin 4) => match i, j with | 0, 0 => 1 | 1, 1 => 1 | 2, 3 => 1 | 3, 2 => 1 | x, x_1 => 0

theorem CSD.Empirical.QM.Gates.qmCNOT_mul_self : qmCNOT * qmCNOT = 1

CNOT is involutive: CNOT * CNOT = 1.

theorem CSD.Empirical.QM.Gates.qmCNOT_hermitian : qmCNOT.conjTranspose = qmCNOT

CNOT is Hermitian (real symmetric {0,1} permutation matrix): CNOTᴴ = CNOT.

theorem CSD.Empirical.QM.Gates.qmCNOT_unitary : qmCNOT.conjTranspose * qmCNOT = 1

CNOT is unitary: CNOTᴴ * CNOT = 1 (Hermitian + involutive).

noncomputable def CSD.Empirical.QM.Gates.qmSWAP : Matrix (Fin 4) (Fin 4) ℂ

SWAP gate on Fin 4.

Equations

• CSD.Empirical.QM.Gates.qmSWAP = Matrix.of fun (i j : Fin 4) => match i, j with | 0, 0 => 1 | 1, 2 => 1 | 2, 1 => 1 | 3, 3 => 1 | x, x_1 => 0

theorem CSD.Empirical.QM.Gates.qmSWAP_mul_self : qmSWAP * qmSWAP = 1

SWAP is involutive.

theorem CSD.Empirical.QM.Gates.qmSWAP_hermitian : qmSWAP.conjTranspose = qmSWAP

SWAP is Hermitian: SWAPᴴ = SWAP.

theorem CSD.Empirical.QM.Gates.qmSWAP_unitary : qmSWAP.conjTranspose * qmSWAP = 1

SWAP is unitary: SWAPᴴ * SWAP = 1.

noncomputable def CSD.Empirical.QM.Gates.qmCZ : Matrix (Fin 4) (Fin 4) ℂ

Controlled-Z gate: phase-flip on |11⟩.

Equations

• CSD.Empirical.QM.Gates.qmCZ = Matrix.of fun (i j : Fin 4) => match i, j with | 0, 0 => 1 | 1, 1 => 1 | 2, 2 => 1 | 3, 3 => -1 | x, x_1 => 0

theorem CSD.Empirical.QM.Gates.qmCZ_mul_self : qmCZ * qmCZ = 1

CZ is involutive.

theorem CSD.Empirical.QM.Gates.qmCZ_hermitian : qmCZ.conjTranspose = qmCZ

CZ is Hermitian (real diagonal {1,-1} matrix): CZᴴ = CZ.

theorem CSD.Empirical.QM.Gates.qmCZ_unitary : qmCZ.conjTranspose * qmCZ = 1

CZ is unitary: CZᴴ * CZ = 1.