PRCJCostDistance_toRat
plain-language theorem explainer
The PRC J-cost distance between two primitive-recognition rationals, once projected to ordinary rationals, equals the explicit formula J(1+(x-y)^2) on their rational displays. Anyone transporting metric, order, or continuity facts from verifier Q into the PRC quotient cites this display identity. The proof unfolds both sides and rewrites through the cost and square-gap transport lemmas.
Claim. For any two primitive-recognition rationals $a,b$, the ordinary-rational display of their PRC $J$-cost distance equals $J\bigl(1+(x-y)^2\bigr)$ at the rational displays $x$ of $a$ and $y$ of $b$, where $J(g)=(g+g^{-1})/2-1$.
background
In the Primitive Recognition Calculus, rationals are ratio-orbit quotient classes (nonzero-denominator orbits identified by cross-multiplication), not bare Mathlib $\mathbb{Q}$. A verifier display map sends each class to an ordinary rational via numerator and denominator orbits.
The $J$-cost is $J(g)=(g+g^{-1})/2-1$, the unique cost forced by the Recognition Composition Law (T5). Internally, the PRC $J$-cost distance is built from a square-gap on those classes. The sibling display formula writes the same expression on ordinary rationals: set $g=1+(x-y)^2$, then apply $J(g)$.
This module sits in the foundation layer that builds ordered-field and null-distance structure from PRC primitives, so analytic estimates stated on $\mathbb{Q}$ can be transported back into the quotient.
proof idea
Short tactic proof. Unfold the internal PRC distance and the rational display formula, then rewrite with two transport lemmas: the $J$-cost on PRC rationals displays as the ordinary cost on their rational images, and the square-gap likewise commutes with the display map. No case analysis or induction.
why it matters
Display bridge for the whole PRC real-construction stack. The conditional triangle certificate packages it as the distance-display field, reducing PRC triangle transport to a verifier-rational inequality (Build Order step 9a). Translation invariances (left/right add, double negation) prove distance equalities by injecting through the display map and simplifying the rational formula. Boundedness-modulus and order-congruence lemmas turn small-distance hypotheses into ordinary square-increment bounds the same way; product-continuity targets also depend on it. Within RS, $J$ is the T5-forced cost; commuting its distance with the rational embedding is the bookkeeping that lets $\mathbb{Q}$-side estimates lift to the PRC quotient and the null-distance setoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.