Amplitude normalisation
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.
Amplitude normalisation |α|² + |β|² = 1, exactly, on the 3-4-5 triple: (3/5)² + (4/5)² = 1. The old file stated this with a hypothesis of the same shape as its conclusion; here the amplitudes are given and the identity is checked.
Proposition
3 * 3 + 4 * 4 = 5 * 5Proof
By decide in rational.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/rational.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778