PRCRat
plain-language theorem explainer
PRC rationals are quotient classes of ratio orbits under cross-multiplication equivalence of orbit-level numerators and denominators. Anyone building PRC arithmetic, the η map into completed reals, or K4.8 rational structure cites this carrier. The definition is the bare quotient type Quot of the ratio-orbit setoid; constructors and the conservative ℚ display sit in the namespace.
Claim. Let ratio orbits be pairs of orbit-level numerator and nonzero denominator. Identify two ratio orbits when their cross-multiplied numerators and denominators agree (the ratio-orbit equivalence). The type of PRC rationals is the set of equivalence classes of that relation.
background
Primitive Recognition Calculus builds number systems from orbit data rather than from classical $\mathbb{Z}$ and $\mathbb{Q}$ as primitives. A ratio orbit packages an orbit-level numerator with a nonzero-denominator orbit; two such displays are equivalent when cross-multiplication of the orbit numerators and denominators agrees. That relation is packaged as the setoid ratioOrbitSetoid (relation ratioOrbitEquiv, proved an equivalence).
The present declaration names the corresponding quotient type: PRC rationals are those classes. The module also supplies the display constructor from a ratio orbit and a well-defined lift toRat into classical $\mathbb{Q}$, justified by the fact that ratio-orbit equivalence is exactly equality of the classical rational values of the displays.
Local setting is K4.8 of the IntegerRational development: rationals as nonzero-denominator ratio-orbit quotients, parallel to the signed-orbit treatment of PRC integers earlier in the same module.
proof idea
Definitional, not a proof. The carrier is Quot ratioOrbitSetoid. In the namespace, mk is Quot.mk on a ratio orbit. toRat is Quot.lift of RatioOrbit.toRat, with respectfulness discharged by the biconditional that ratio-orbit equivalence holds iff the two displays have equal classical rational values.
why it matters
This is the native rational carrier for PRC. Downstream, field operations and algebraic laws on PRC rationals are stated on this type; the used-by graph already shows the integer-side arithmetic suite and, more structurally, the M0a unit map etaQ : PRCRat → RealDelta, which sends a PRC rational to the class of its constant regular sequence. That map is the carrier morphism of the Forced ⊣ Classical adjunction program (Grow/EtaCompletion).
In the broader Recognition stack, rationals sit under the completeness and continuity layers that feed real structure used by cost and display arguments. The definition itself is not a forcing step (T0–T8), but it is the K4.8 substrate those later continuity and completion results quote when they need a quotient-native $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.