onPRCRat_mk
plain-language theorem explainer
The rational J-cost sends the quotient class of a ratio-orbit display to the class of that display's orbit-level J-cost. Anyone rewriting mixed constructor and cost expressions on PRC rationals will cite this simp rule. The equality is definitional: the cost is a Quot.lift of the orbit map, so the proof is reflexivity.
Claim. For every ratio-orbit display $q$, the PRC rational $J$-cost of the quotient class of $q$ equals the quotient class of the ratio-orbit $J$-cost of $q$: $J([q])=[J(q)]$, where $J(q)=((q+q^{-1})/2)-1$ at the orbit level.
background
PRC rationals are the quotient of ratio-orbit displays by the cross-multiplication setoid (K4.8): two displays represent the same rational when their numerators and denominators cross-multiply equal. A ratio orbit itself is an integer (signed-orbit) numerator over a nonzero distinction-nat denominator (K4.7).
At orbit level the native cost is the usual RS $J$-shape $J(q)=((q+q^{-1})/2)-1$, built from add, reciprocal, multiply-by-half, and subtract-one on ratio orbits. The rational cost is the lift of that map through the quotient constructor, so it is a well-defined function on equivalence classes rather than a choice of representative.
This module sits in the Primitive Recognition Calculus foundation: it equips the rational quotient with field operations and the lifted cost before real completion and uniqueness arguments.
proof idea
One-line reflexivity. The rational cost is defined as Quot.lift of the map sending a ratio orbit $q$ to the class of its orbit-level $J$-cost. Applying that lift to the class constructor on $q$ therefore reduces definitionally to the class of onRatioOrbit q, and rfl closes the goal. No separate well-definedness or injectivity argument is needed at the call site; that work lives in the lift's proof obligation.
why it matters
This simp lemma is the constructor interface for the rational $J$-cost: without it, every rewrite that mixes PRCRat.mk with the lifted cost must unfold the Quot.lift by hand. It pins the discrete side of T5's $J$-shape $J(x)=(x+x^{-1})/2-1$ on the rational quotient before continuity and uniqueness bridge to the reals.
No downstream dependents are recorded yet; the lemma is infrastructure for later field identities, positivity facts, and the real-extension path in the same calculus stack. It does not itself prove RCL or $J$-uniqueness, but it makes those statements stateable cleanly on PRCRat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.