Swap

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

SWAP is unitary and its own inverse.

Proposition

Same 4 (mm 4 SWAP (dag SWAP)) idm ∧ Same 4 (mm 4 SWAP SWAP) idm

Proof

By decide in quantum.lean. Checked by the Lean kernel: it depends on no axiom.

Sources and identifiers

• Lean source · src/pair/lean/proofs/quantum.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778

Proved in the same file

• Gi add re
• Gi add im
• Gi mul re
• Gi zero re
• Gi one re
• Gi zero im
• Gi one im
• H unitary
• H squared
• Paulis unitary
• Y unitary
• S squared
• Cnot
• Toffoli
• Omega fourth
• T gate
• Bell state
• Ghz state
• Chsh classical bound
• Chsh quantum value
• Teleport exact
• Teleport no signalling
• Superdense exact
• Both ways
• No cloning
• Cnot copies the basis
• Stabilizer hadamard
• Stabilizer phase
• Stabilizer cnot
• Deutsch jozsa
• Promise census
• Grover search
• Qft unitary
• Phase estimation exact
• Swap routing
• Unrouted differs
• Routed depth
• Repetition corrects
• Repetition fails on two
• Steane corrects
• Steane css
• Shor nine
• Distance corrects
• Pauli products
• Pauli anticommute
• Pauli square adjoint trace
• Hadamard exchanges phase and bit
• Ghz mermin quantum
• Ghz mermin classical
• No communication
• Alice changes the pair
• Toll is uniform
• Entanglement swapping
• No pairs no swapping
• Sixty degrees is a primitive sixth root of unity
• Zero plus an integer is that integer
• Zero times an integer is zero
• Rotation by sixty degrees keeps the eisenstein integers
• The rotation leaves the integers and keeps the norm
• Six is the first perfect number and a tetrahedron sums to 720
• The doubling circuit steps forty eighty one sixty and back
• The six two star is the two triangles and not the doubling cycle
• The two reflections connect the three trinities
• The two mirrors compose to the forty degree step
• The nines reflection carries the doubling circuit onto itself
• A two to one fold of addresses is many to one by pigeonhole

All machine-checked theorems