onPRCRat
plain-language theorem explainer
Lifts the primitive recognition J-cost from ratio-orbit representatives to the PRC rational quotient, so each class maps to the class of J(q) = (q + q^{-1})/2 - 1. Cited by anyone building rational-field structure, J-cost distance, or the recognizer bridge. Well-definedness is a Quot.lift whose coherence uses injectivity of the rational display.
Claim. There is a well-defined map $J_{\mathbb{Q}}:\mathrm{PRCRat}\to\mathrm{PRCRat}$ sending the quotient class of a ratio orbit $q$ to the class of $J(q)=\frac{q+q^{-1}}{2}-1$, where $\mathrm{PRCRat}$ is the nonzero-denominator ratio-orbit quotient identified by cross-multiplication.
background
Primitive Recognition Calculus builds rationals before reals. A ratio orbit is an integer-level display of a fraction; two orbits are equivalent when cross-multiplication agrees. PRC rationals are the quotient of that setoid (K4.8). The verifier map toRat sends an orbit to an ordinary rational and is injective on the quotient, so equal displays mean equal classes.
At orbit level the PRC J-cost is the algebraic object $J(q)=((q+q^{-1})/2)-1$, written as orbit arithmetic (add, reciprocal, half, subtract one). That is the same closed form forced uniquely later in the T5 step of the forcing chain; here it is only the rational object, not the real-analytic uniqueness theorem.
This module equips the quotient with field operations and certificates. The present definition is the transport of orbit-level J to that quotient so later distance and cost maps can live on PRC rationals rather than raw representatives.
proof idea
Definition by Quot.lift: on a representative orbit $q$, return the class of the orbit-level J-cost. Coherence: if two orbits are setoid-equivalent, their images must agree in the quotient. Apply injectivity of the rational display on classes; unwind the constructor display; replace each side by the known rational formula for orbit-level J; then use that setoid equivalence is equivalent to equal rational displays, so the two J-values match.
why it matters
Gives the quotient-native J-cost used everywhere the rational layer talks about cost rather than representatives. Downstream: the simp lemma for constructors, the identity that the display of $J_{\mathbb{Q}}(q)$ is $(q+q^{-1})/2-1$, and normalization invariance of the lift. The rational-field certificate structure sits in the same module as the algebraic backbone. RealCauchy builds J-cost distance by sending additive separation through $1+(a-b)^2$ then applying this map. RecognizerBridge assigns cost of a positive ratio by the same lift. Framework landmark: this is the rational avatar of the T5 J-form $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), before real completeness and uniqueness are bridged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.