The rotation leaves the integers and keeps the norm
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.
BUT NOT IN ℤ: the rotation of 1 is ω itself, which is no ordinary integer — the pasted claim's own list held 3/2 and −7/2, which are the real parts of exactly such elements. The norm is kept and is multiplicative on a box.
Proposition
EI.ω * 1 = EI.ω ∧ (EI.ω * 1).b ≠ 0 ∧ (List.range 5).all (fun a => (List.range 5).all (fun b => EI.norm (EI.ω * ⟨(a : Int) - 2, (b : Int) - 2⟩) == EI.norm ⟨(a : Int) - 2, (b : Int) - 2⟩)) ∧ (List.range 6).all (fun k => EI.norm (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
- 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
- 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