Amplitude normalisation rational
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.
The same, as rationals: 9/25 + 16/25 = 1.
Proposition
eq (add ⟨9,25⟩ ⟨16,25⟩) ⟨1,1⟩Proof
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