add
plain-language theorem explainer
The add definition supplies the standard rational sum on the quotient LogicRat by lifting the cross-multiplication formula from PreRat representatives. Researchers constructing the Recognition Science number system from logic would cite it to equip the rationals with an additive operation compatible with the integer layer. The implementation is a Quotient.lift₂ wrapper whose well-definedness reduces via toInt and linear_combination to ordinary integer arithmetic.
Claim. Addition on the field of fractions $LogicRat$ is defined by lifting the map $(p,q)mapsto mk(p.num·q.den + q.num·p.den, p.den·q.den)$ from $PreRat×PreRat$ to the quotient, where $mk$ constructs an element of $LogicInt$ and the denominator is required nonzero.
background
LogicRat is the quotient of PreRat by the setoid ratRel, where PreRat pairs a LogicInt numerator with a LogicNat denominator; this yields the field of fractions of LogicInt. The upstream module IntegersFromLogic supplies the ring operations on LogicInt together with the transfer map toInt and the soundness theorem that converts equations in LogicInt into statements about ordinary integers. The transfer principle eq_iff_toInt_eq states that an equality holds in LogicInt if and only if it holds after applying toInt, allowing all ring identities to be checked in Int.
proof idea
Quotient.lift₂ is applied to the concrete formula mk (p.num * q.den + q.num * p.den) (p.den * q.den) with a nonzeroness guard using mul_eq_zero. Well-definedness is shown by rintro on four representatives and two equivalence proofs, followed by apply sound, rw eq_iff_toInt_eq, simp with toInt_add and toInt_mul, extraction of two auxiliary congruences, and a linear_combination step that assembles the integer identity.
why it matters
The definition completes the additive structure on LogicRat and is immediately installed as the Add instance, supplying the group operation required for the subsequent field axioms in the same module. It sits inside the foundation layer that derives the rationals directly from the logic integers, a prerequisite for the phi-ladder mass formulas and the constants (c=1, ħ=phi^{-5}) that appear later in the forcing chain. No downstream uses are recorded yet, indicating it remains an internal building block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.