toRat_add
plain-language theorem explainer
The canonical map toRat from the constructed rationals LogicRat to standard Q preserves addition. Foundation builders in Recognition Science cite this when verifying that the logic-derived rationals satisfy the field axioms. The proof uses double Quotient induction on representatives, reduces via the integer-level toInt_add and toInt_mul, then clears denominators with field_simp after non-zero checks via eq_iff_toInt_eq.
Claim. Let LogicRat be the field of fractions of the logic integers. The map toRat : LogicRat → Q satisfies toRat(x + y) = toRat x + toRat y for all x, y in LogicRat.
background
LogicRat is defined as the quotient of PreRat pairs by the setoid ratRel, yielding the field of fractions of LogicInt. The map toRat lifts the integer recovery toRat_mk, sending a representative (num, den) to (toInt num : Q) / (toInt den : Q). Upstream, toInt_add and toInt_mul establish that the integer map preserves ring operations, while eq_iff_toInt_eq transfers equalities between LogicInt and Int. toInt_zero supplies the base case for denominator checks.
proof idea
Double induction via Quotient.inductionOn on both arguments. After rcases on the PreRat pairs, simp rewrites toRat_mk together with toInt_add and toInt_mul. Non-zero denominator lemmas are proved by contradiction using eq_iff_toInt_eq and toInt_zero. The final step applies field_simp to equate the cleared fractions.
why it matters
This additivity is invoked directly by the ring laws add_assoc', add_comm', add_zero', add_left_neg' and add_mul' via eq_iff_toRat_eq reductions to Q. It closes the embedding of the logic rationals into classical mathematics, supplying the additive structure required for the phi-ladder mass formulas and later Hilbert-Polya constructions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.