toRat_add
plain-language theorem explainer
Addition on PRC rationals (ratio-orbit quotient classes) is compatible with the verifier map into Mathlib ℚ: the display of a sum is the sum of the displays. Anyone proving ring laws or continuity estimates by transport to ℚ cites this. The proof is a double quotient induction that reduces to the already-proved RatioOrbit-level identity.
Claim. For any two PRC rationals $a,b$ (nonzero-denominator ratio-orbit classes under cross-multiplication), if $\mathrm{toRat}$ is the verifier display into $\mathbb{Q}$, then $\mathrm{toRat}(a+b)=\mathrm{toRat}(a)+\mathrm{toRat}(b)$.
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer numerator (SignedOrbit) over a nonzero DistinctionNat denominator. The map toRat sends such a display to the ordinary rational $(num.toInt)/(den.toNat)$ in Mathlib $\mathbb{Q}$; the doc tags this as an A5 transport wrapper whose internal characterization is cross-multiplication.
PRCRat is the quotient of RatioOrbit by the setoid that identifies displays with equal cross-products of numerators and denominators (K4.8). Addition is defined on representatives and descends to the quotient. The sibling theorem add_toRat already states the same identity at the RatioOrbit level, by unfolding add and toRat and rewriting through SignedOrbit.add_toInt and scaleByNat_toInt.
This module sits in the foundation layer that builds integers and rationals from orbit arithmetic before real completeness and J-cost continuity arguments.
proof idea
Term-mode proof by double Quot.induction_on on $a$ and $b$. After induction, the goal is exactly the RatioOrbit statement (RatioOrbit.add a b).toRat = a.toRat + b.toRat, which is discharged by the upstream lemma RatioOrbit.add_toRat. No new arithmetic is done at the quotient level.
why it matters
This is the simp lemma that lets every later argument treat PRCRat addition as ordinary rational addition after transport. Immediate children include toRat_sub (via add of a negate), and the RationalsFromLogic transfer proofs add_assoc', add_comm', add_left_neg', and add_mul', which rewrite equality of LogicRat sums to ℚ and finish by ring.
Downstream foundation targets also use it when building concrete PRCRat constants such as two = 1+1 and four = two+two inside PRCJCostDistanceIncrementTriangleTarget_proved and the mul-bounded continuity target. Those feed J-cost distance estimates on the path toward real structure forced by the Recognition Composition Law and the T5–T8 chain. Without quotient-level add/toRat compatibility, the transport principle eq_iff_toRat_eq cannot move ring identities back from Mathlib ℚ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.