Empirical/QM: Multi-qubit gates (Toffoli, Fredkin)

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

Universal classical reversible logic via Toffoli (CCNOT) and Fredkin (CSWAP) gates on three qubits. Both are 8×8 real symmetric permutation matrices — Hermitian and involutive, hence unitary. Each qmG_hermitian (Gᴴ = G) combines with the involutive qmG_mul_self to give the unitarity qmG_unitary (Gᴴ * G = 1), now proved for both gates.

Contents

• qmToffoli (CCNOT): flips qubit 2 iff qubits 0 and 1 are both 1; Hermitian, unitary.
• qmFredkin (CSWAP): swaps qubits 1 and 2 iff qubit 0 is 1; Hermitian, unitary.

Basis order: |000⟩, |001⟩, ..., |111⟩ = Fin 8.

Function-based matrix definitions (the !! notation fails to propagate ℂ elaboration cleanly for 8×8 sparse permutations).

noncomputable def CSD.Empirical.QM.Gates.qmToffoli : Matrix (Fin 8) (Fin 8) ℂ

Toffoli (CCNOT) gate on Fin 8. Permutes |110⟩ ↔ |111⟩, acts as identity elsewhere. Basis order: bit 0 high, bit 2 low, so |110⟩ = Fin 6 and |111⟩ = Fin 7.

Equations

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

theorem CSD.Empirical.QM.Gates.qmToffoli_mul_self : qmToffoli * qmToffoli = 1

Toffoli is involutive.

theorem CSD.Empirical.QM.Gates.qmToffoli_hermitian : qmToffoli.conjTranspose = qmToffoli

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

theorem CSD.Empirical.QM.Gates.qmToffoli_unitary : qmToffoli.conjTranspose * qmToffoli = 1

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

noncomputable def CSD.Empirical.QM.Gates.qmFredkin : Matrix (Fin 8) (Fin 8) ℂ

Fredkin (CSWAP) gate on Fin 8. Permutes |101⟩ ↔ |110⟩, acts as identity elsewhere.

Equations

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

theorem CSD.Empirical.QM.Gates.qmFredkin_mul_self : qmFredkin * qmFredkin = 1

Fredkin is involutive.

theorem CSD.Empirical.QM.Gates.qmFredkin_hermitian : qmFredkin.conjTranspose = qmFredkin

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

theorem CSD.Empirical.QM.Gates.qmFredkin_unitary : qmFredkin.conjTranspose * qmFredkin = 1

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