Qubits

def transl₂ : Fin 2 × Fin 2 → Fin 4

To use Fin 4 × Fin 4 matrices to manipulate 2 qubits.

Equations

• transl₂ (0, 0) = 0
• transl₂ (0, 1) = 1
• transl₂ (1, 0) = 2
• transl₂ (1, 1) = 3

def transl₃ : Fin 2 × Fin 2 × Fin 2 → Fin 8

To use Fin 8 × Fin 8 matrices to manipulate 3 qubits.

Equations

• transl₃ (0, 0, 0) = 0
• transl₃ (0, 0, 1) = 1
• transl₃ (0, 1, 0) = 2
• transl₃ (0, 1, 1) = 3
• transl₃ (1, 0, 0) = 4
• transl₃ (1, 0, 1) = 5
• transl₃ (1, 1, 0) = 6
• transl₃ (1, 1, 1) = 7

def transl₃'' : (Fin 2 × Fin 2) × Fin 2 → Fin 8

An "associative variant" for using Fin 8 × Fin 8 matrices to manipulate 3 qubits.

Equations

• transl₃'' ((0, 0), 0) = 0
• transl₃'' ((0, 0), 1) = 1
• transl₃'' ((0, 1), 0) = 2
• transl₃'' ((0, 1), 1) = 3
• transl₃'' ((1, 0), 0) = 4
• transl₃'' ((1, 0), 1) = 5
• transl₃'' ((1, 1), 0) = 6
• transl₃'' ((1, 1), 1) = 7

noncomputable def transl3 {a b : ℕ} : (Fin b → Fin a) → Fin (a ^ b)

Equations

• transl3 = ⋯.mpr (Fintype.equivFin (Fin b → Fin a)).toFun

def transl {a b : ℕ} : (Fin b → Fin a) → Fin (a ^ b)

Equations

• transl v = finFunctionFinEquiv v

def transl₃' : Fin 2 × Fin 2 × Fin 2 → Fin 8

Equations

• transl₃' p = (p.1.mkDivMod p.2.1).mkDivMod p.2.2

def translate₂ : Matrix (Fin 4) (Fin 4) ℂ → Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

Equations

• translate₂ A x y = A (transl₂ x) (transl₂ y)

def translate₃ : Matrix (Fin 8) (Fin 8) ℂ → Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Equations

• translate₃ A x y = A (transl₃ x) (transl₃ y)

def translate₃' : Matrix (Fin 8) (Fin 8) ℂ → Matrix ((Fin 2 × Fin 2) × Fin 2) ((Fin 2 × Fin 2) × Fin 2) ℂ

Equations

• translate₃' A x y = A (transl₃'' x) (transl₃'' y)

def toffoli₀ : Matrix (Fin 8) (Fin 8) ℂ

Equations

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

def cnot₀ : Matrix (Fin 4) (Fin 4) ℂ

Equations

• cnot₀ = !![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 0, 1; 0, 0, 1, 0]

def toffoli : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Equations

• toffoli = translate₃ toffoli₀

def toffoli' : Matrix ((Fin 2 × Fin 2) × Fin 2) ((Fin 2 × Fin 2) × Fin 2) ℂ

Equations

• toffoli' = translate₃' toffoli₀

def cnot : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

Equations

• cnot = translate₂ cnot₀

theorem toffoli_unchange {a b c : Fin 2} (h : ¬(a = 1 ∧ b = 1)) : toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c))

theorem toffoli_change (c : Fin 2) : toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e c)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e (1 - c)))

theorem kroneckerMap_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {w : Matrix α β ℂ} (hw : w ≠ 0) {x y : Matrix (α × γ) (β × δ) ℂ} (h₂ : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) w x = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) w y) : x = y

theorem kroneckerMap_injective₀ {α : Type u_1} {β : Type u_2} {w : Matrix α β ℂ} (hw : w ≠ 0) {x y : Matrix α β ℂ} (h₂ : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) w x = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) w y) : x = y

theorem e_ne_zero {z : Fin 2} : e z ≠ 0

theorem toffoli_characterize (a b c : Fin 2) : toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c)) = if a = 1 ∧ b = 1 then Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e (1 - c))) else Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c))

theorem negation_using_toffoli (a : Fin 2) : toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e 1)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e (1 - a)))

If we inspect the third qubit on input (a,1,1) we find 1-a.

theorem partialTraceLeft_tensor_rankOne_basis {R : Type u_1} [RCLike R] {k : Type u_2} [Fintype k] [DecidableEq k] (i : k) (M : Matrix (k × k) (Fin 1 × Fin 1) R) : partialTraceLeft (pureState' (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e i) M)) = pureState' M

theorem partialTraceLeft_tensor_rankOne_basis' {R : Type u_1} [RCLike R] {k : Type u_2} [Fintype k] [DecidableEq k] (i : k) (M : Matrix k (Fin 1) R) : partialTraceLeft (pureState' (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e i) M)) = pureState' M

theorem negation_using_toffoli'' (a : Fin 2) : have t := toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e 1)); partialTraceLeft (pureState' t) = pureState' (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e (1 - a)))

theorem negation_using_toffoli' (a : Fin 2) : partialTraceLeft (partialTraceLeft (pureState' (toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e 1))))) = pureState' (e (1 - a))

May 21, 2026. Best result so far on computing negation using Toffoli gate.

noncomputable def bit_from_pureState (M : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin 1) (Fin 1) ℂ

Equations

• bit_from_pureState M = !![0; 1].conjTranspose * M * !![0; 1]

theorem bit_from_pureState_eq (i : Fin 2) : bit_from_pureState (pureState' (e i)) = !![↑↑i]

theorem bit_from_pureState_eq' (i : Fin 2) : bit_from_pureState (pureState' (e i)) 0 0 = ↑↑i

theorem negation_using_toffoli''' (a : Fin 2) : bit_from_pureState (partialTraceLeft (partialTraceLeft (pureState' (toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e 1) (e 1)))))) 0 0 = 1 - ↑↑a

theorem scratch_off_tensor_general {R : Type u_1} [RCLike R] {i : Fin 2} (M : Matrix (Fin 2 × Fin 2) (Fin 1 × Fin 1) R) : partialTraceLeft (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e i) M * (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e i) M).conjTranspose) = M * M.conjTranspose

theorem scratch_off_tensor {R : Type u_1} [RCLike R] {i j k : Fin 2} : have v := Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e i) (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e j) (e k)); have B := v * v.conjTranspose; have Bl := partialTraceLeft B; Bl = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e j) (e k) * (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (e j) (e k)).conjTranspose

correct acc. to https://chatgpt.com/c/6a0ba46b-6c94-83e8-8262-52b4a2dc0954 This can be used to compute negation using the Toffoli gate.

theorem toffoli_characterize.TFAE (a b c : Fin 2) : [a = 1 ∧ b = 1, toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e (1 - c))), toffoli * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c)) ≠ Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e b) (e c))].TFAE

The usual characterization of the behavior of the Toffoli gate: the target bit (third bit) will be inverted if and only if the first and second bits are both 1 from https://en.wikipedia.org/wiki/Toffoli_gate

theorem toffoli_real : star toffoli = toffoli

theorem toffoli_unitary.aux : star toffoli * toffoli = 1

theorem toffoli_unitary : toffoli ∈ unitary (Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ)

Prove that toffolo is a unitary circuit.

noncomputable def toffoli_probability (startState : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 1 × Fin 1 × Fin 1) ℂ) : ℂ

Equations

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

noncomputable def toffoli_probability'' (startState : Fin 2 × Fin 2 × Fin 2 → ℂ) : ℂ

May 11, 2026. Using *ᵥ to simplify matrix structure.

Equations

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

noncomputable def toffoli_probability' (startState : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 1 × Fin 1 × Fin 1) ℂ) : ℂ

Equations

• toffoli_probability' startState = ∑ i : Fin 2 × Fin 2, have z := (toffoli * startState) (0, i.1, i.2) (0, 0, 0); star z * z

theorem toffoli_probability_eq : toffoli_probability = toffoli_probability'

def ket₀ : Matrix (Fin 2) (Fin 1) ℂ

Equations

• ket₀ = !![1; 0]

noncomputable def proj₀ : Matrix (Fin 2) (Fin 2) ℂ

Equations

• proj₀ = ket₀ * ket₀.conjTranspose

noncomputable def first_qubit_proj₀ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Equations

• first_qubit_proj₀ = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) proj₀ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 1)

noncomputable def gate_probability (startState : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 1 × Fin 1 × Fin 1) ℂ) : ℂ

Equations

• gate_probability startState = ((toffoli * startState).conjTranspose * first_qubit_proj₀ * (toffoli * startState)) (0, 0, 0) (0, 0, 0)

theorem cnot_basis (i j : Fin 2) : cnot * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e i) (e j) = if i = 0 then Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e i) (e j) else Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (e i) (e (1 - j))

def swap₃ : Equiv.Perm (Fin 3)

Equations

• swap₃ = { toFun := ![1, 0, 2], invFun := ![1, 0, 2], left_inv := swap₃._proof_2, right_inv := swap₃._proof_2 }

theorem isOne : 1 = !![1, 0; 0, 1]

def f {a b : ℕ} : Fin a × Fin b ⊕ Fin a × Fin b → Fin a × Fin b × Fin 2

Equations

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

def split {a b : ℕ} : Fin a × Fin b × Fin 2 → Fin a × Fin b ⊕ Fin a × Fin b

Equations

• split (u, v, w) = if w = 0 then Sum.inl (u, v) else Sum.inr (u, v)

def split' {a b : ℕ} : Fin 2 × Fin a × Fin b → Fin a × Fin b ⊕ Fin a × Fin b

Equations

• split' (u, v, w) = if u = 0 then Sum.inl (v, w) else Sum.inr (v, w)

noncomputable def quantumCircuit (A : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (σ : Equiv.Perm (Fin 2 × Fin 2 × Fin 2)) : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Given a circuit A that only touches 2 qubits, and a permutation P of 3 qubits, get a unitary as Pᵀ Q P where Q = A ⊕ I.

Equations

• quantumCircuit A σ = ((Equiv.symm σ).toPEquiv.toMatrix * Matrix.of fun (x y : Fin 2 × Fin 2 × Fin 2) => Matrix.fromBlocks A 0 0 1 (split' x) (split' y)) * (Equiv.toPEquiv σ).toMatrix

def Matrix.fromBlocks_id {a b : ℕ} (A : Matrix (Fin a × Fin b) (Fin a × Fin b) ℂ) : Matrix (Fin a × Fin b ⊕ Fin a × Fin b) (Fin a × Fin b ⊕ Fin a × Fin b) ℂ

Equations

• A.fromBlocks_id = Matrix.fromBlocks A 0 0 1

def Matrix.fromBlocks_split' {a b : ℕ} (A : Matrix (Fin a × Fin b) (Fin a × Fin b) ℂ) : Matrix (Fin 2 × Fin a × Fin b) (Fin 2 × Fin a × Fin b) ℂ

Equations

• A.fromBlocks_split' = Matrix.of fun (x y : Fin 2 × Fin a × Fin b) => Matrix.fromBlocks A 0 0 1 (split' x) (split' y)

def Matrix.prod_sum {a b : ℕ} : Matrix (Fin 2 × Fin a × Fin b) (Fin a × Fin b ⊕ Fin a × Fin b) ℂ

Equations

• Matrix.prod_sum x y = if y = split' x then 1 else 0

def Matrix.sum_prod {a b : ℕ} : Matrix (Fin a × Fin b ⊕ Fin a × Fin b) (Fin 2 × Fin a × Fin b) ℂ

Equations

• Matrix.sum_prod x y = if x = split' y then 1 else 0

theorem Matrix.fromBlocks_split'_eq {a b : ℕ} (A : Matrix (Fin a × Fin b) (Fin a × Fin b) ℂ) : A.fromBlocks_split' = prod_sum * A.fromBlocks_id * sum_prod

theorem fromBlocks_unitary (A : ↥(unitary (Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ))) : Matrix.fromBlocks (↑A) 0 0 1 ∈ unitary (Matrix (Fin 2 × Fin 2 ⊕ Fin 2 × Fin 2) (Fin 2 × Fin 2 ⊕ Fin 2 × Fin 2) ℂ)

def quantumCircuitUnitary'' (A : ↥(unitary (Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ))) : ↥(unitary (Matrix (Fin 2 × Fin 2 ⊕ Fin 2 × Fin 2) (Fin 2 × Fin 2 ⊕ Fin 2 × Fin 2) ℂ))

Equations

• quantumCircuitUnitary'' A = ⟨Matrix.fromBlocks (↑A) 0 0 1, ⋯⟩

theorem sum_prod_sum_1 : Matrix.sum_prod * Matrix.prod_sum = 1