Sixty degrees is a primitive sixth root of unity
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.
SIXTY DEGREES IS A PRIMITIVE SIXTH ROOT: ω² = ω − 1, ω³ = −1, ω⁶ = 1 and no smaller power is 1.
Proposition
EI.ω * EI.ω = EI.ω + -1 ∧ EI.pow EI.ω 3 = -1 ∧ EI.pow EI.ω 6 = 1 ∧ (List.range' 1 5).all (fun k => EI.pow EI.ω k != 1)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
- Swap
- 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
- 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