cost_toRat
plain-language theorem explainer
For any positive PRC ratio, the rational display of its recognition cost equals the classical J-cost of its rational value: (q + q^{-1})/2 - 1. Authors bridging Primitive Recognition Calculus costs into the forced recognizer cost cite this identity. The proof is a one-line wrapper around the rational-field J-cost evaluation on the underlying PRC rational.
Claim. Let $r$ be a positive PRC ratio with rational value $q$. Then the rational display of the recognition cost of $r$ equals $\frac{q + q^{-1}}{2} - 1$.
background
Primitive Recognition Calculus (PRC) works with certified rationals before any real embedding. A positive PRC ratio packages a PRC rational together with a positivity witness; that is the input surface for recognizer comparisons in this module.
The Recognition Science cost on positive ratios is the unique J-cost forced by the composition law: $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). Several upstream cost definitions (observer events, multiplicative recognizers, rung coarsening) all reduce to this same functional form once the comparator is fixed.
This bridge module sits between the PRC rational field and the existing real-valued cost infrastructure. The local goal is to show that PRC-native cost displays match the classical J-cost after the standard rational and real coercions.
proof idea
One-line wrapper. Apply the rational-field identity PRCJCost.onPRCRat_toRat to the underlying PRC rational r.value. That lemma already states that the PRC J-cost, displayed as a rational, equals $(q + q^{-1})/2 - 1$ for positive PRC rationals; the structure field projection supplies the argument.
why it matters
This is the rational half of the recognizer-cost bridge. Downstream, cost_toReal_jcost rewrites through it and casts into Cost.Jcost on reals, and PRCRecognitionCost_display re-exports the same identity for the named PRC recognition-cost display. Together they certify that PRC recognizer costs land on the forced J-cost of T5 in the unified forcing chain, rather than on an ad-hoc alternative. The bridge target certificate in this module depends on that match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.