toRat_sub
plain-language theorem explainer
The verifier display from primitive recognition rationals into ordinary rationals preserves subtraction. Anyone transporting order, positivity, or metric comparisons from PRC rationals into ℚ cites this simp lemma. The proof unfolds subtraction as addition of a negation, rewrites by the add and negate transport lemmas, and finishes with ring on ℚ.
Claim. For any two primitive recognition rationals $a$ and $b$, the ordinary rational display of their difference equals the difference of their displays: if $\tau$ denotes the verifier map into $\mathbb{Q}$, then $\tau(a-b)=\tau(a)-\tau(b)$.
background
Primitive recognition rationals (K4.8) are nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. The verifier display sends a ratio orbit (or its quotient class) to an ordinary rational by taking the signed integer numerator over the natural denominator; the internal characterization remains cross-multiplication.
Subtraction on these classes is not primitive: it is addition of a pointwise negation of signed orbits (swap the positive and negative parts). Upstream simp lemmas already show that the verifier display preserves addition and negation, each proved by quotient induction down to the corresponding RatioOrbit identity.
proof idea
Short term-mode reduction. Rewrite the goal by exposing subtraction as addition of a negation. Apply the two upstream transport lemmas (display preserves add; display preserves negate). The resulting equality on $\mathbb{Q}$ is closed by ring.
why it matters
Direct input to the order-transport theorem in RealCauchy that equates the internal strict order on primitive recognition rationals with ordinary comparison of their rational displays (via positivity of the difference). That bridge is required before Cauchy-real constructions can sit on top of the orbit arithmetic stack. The lemma is foundation-layer bookkeeping: it keeps the verifier map a ring homomorphism on the additive structure built from recognition orbits, before completeness and continuity modules take over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.