ofRat
plain-language theorem explainer
Embeds a PRC rational as a point of the closed null-distance real carrier (Cauchy ledgers modulo null distance). Anyone building constants, protocols, or the forced-J completion cites this map as the rational inclusion. The body is a one-line wrapper through the already-proved transitive null-distance quotient constructor.
Claim. There is a canonical embedding $\iota:\mathbb{Q}_{\mathrm{PRC}}\hookrightarrow R_{\mathrm{null}}$ sending each PRC rational to its constant Cauchy ledger class in the quotient of Cauchy ledgers by the null-distance relation (transitivity already established).
background
Primitive Recognition Calculus builds reals internally from ledger data rather than importing classical $\mathbb{R}$. PRC rationals are ratio-orbit quotient classes (nonzero-denominator pairs identified by cross-multiplication). Cauchy ledgers are sequences of those rationals with a PRC Cauchy condition; two ledgers are null-distance when their J-cost separation vanishes in the limit.
The closed carrier is the quotient of Cauchy ledgers by that null-distance relation, once transitivity is available. Upstream, the constant-sequence embedding already places a PRC rational into the pre-quotient Cauchy type. The present map is the same embedding after quotienting by the proved transitive null relation, yielding the final PRC real carrier used by continuum and protocol layers.
proof idea
One-line definitional wrapper. It applies the generic null-quotient rational embedding at the concrete proof that null distance is transitive (itself obtained from the J-cost triangle-modulus certificate). No extra algebra: the constant Cauchy ledger of $q$ is formed and then passed to the quotient constructor.
why it matters
This is the rational spine of the PRC real line. Downstream, Delta-real protocols use the analogous constant rational protocol; display-forgetful theorems need $\mathrm{value}(\mathrm{ofRat},q)=q$ and faithfulness of the embedding. Certified analytic evaluators route rational literals through the same inclusion. On the continuum side, the capstone forced-$J$ theorem on the completion relies on a real carrier in which rationals sit densely via this map, so the reciprocal-symmetric RCL plus calibration can force $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness) on the completed object. Without a closed null quotient and its rational embedding, the completion step and the forgetful bridge to classical reals do not type-check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.