Exact addition
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.
1/2 + 1/3 = 5/6, exactly — no floating point anywhere in the corpus's arithmetic.
Proposition
eq (add ⟨1,2⟩ ⟨1,3⟩) ⟨5,6⟩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