ofRat
plain-language theorem explainer
Embeds a PRC rational into the classical real boundary by casting its conservative rational display to Lean's ℝ. Anyone wiring PRC arithmetic into continuum-level statements under the classical-extension tag cites this map. The body is a one-line coercion through the verifier rational display.
Claim. For every PRC rational $q$ (a ratio-orbit quotient class), the real-boundary embedding is the classical cast $(q^{\mathrm{display}}:\mathbb{R})$, where $q^{\mathrm{display}}$ is the conservative rational display of $q$.
background
PRC rationals are nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator (K4.8). Their verifier display toRat is a transport wrapper: it sends a ratio orbit to the ordinary rational (num : ℚ)/(den : ℚ), with the internal characterization remaining cross-multiplication (spec tag A5).
The real boundary in this module is an abbreviation for Lean's complete real line ℝ, reached only under the classical-extension tag (K4.14). The local setting is the first continuum boundary of Primitive Recognition Calculus: rationals already constructed internally must sit inside that classical ℝ so later completion, Cauchy, and cost-forcing arguments can quote ordinary real arithmetic.
Upstream siblings embed the same rationals into other carriers (constant Cauchy ledgers, null-distance quotients, Delta-real protocols). This definition is the forgetful classical display of that family.
proof idea
One-line definition. Apply the conservative rational display of the PRC rational, then cast the resulting ordinary rational into ℝ. No lemmas, no tactics: pure coercion through the A5 transport wrapper.
why it matters
Closes K4.14/A5: the rational spine of PRC sits inside the classical real boundary. Downstream, Delta-real protocols use the same embedding so that value(ofRat q) = q and the Phase-1 headline display_real_forgetful can assert surjectivity of value, faithfulness of observational equality, and ring homomorphism of protocol operations. Certified analytic protocol and transformer evaluators route rational literals through this map. The continuum capstone forced_J_on_completion needs rationals inside the completed carrier so the reciprocal-symmetric RCL plus calibration can force $J(x)=(x+1/x)/2-1$ on the completion (T5 J-uniqueness). Sibling lemmas (ofRat_add, ofRat_mul, ofRat_neg, ofRat_inv) turn the bare embedding into a field homomorphism; the boundary certificate and completeness claim sit on top of that package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.