onRatioOrbit_toReal_jcost
plain-language theorem explainer
The PRC rational cost of a ratio orbit, after casting to a real, equals the classical continuous J-cost of that same ratio. Anyone bridging the discrete primitive-recognition cost surface to the real uniqueness theorem cites this equality. The argument is a short rewrite: apply the rational closed form, unfold J, push rational casts, and normalize.
Claim. For every rational orbit $q$ (signed-orbit numerator over a nonzero distinction-nat denominator), the real embedding of the PRC rational cost of $q$ equals $J(r)$, where $r$ is the real image of the rational value of $q$ and $J(x)=\frac{x+x^{-1}}{2}-1$.
background
In Recognition Science the continuous recognition cost on positive reals is the unique J-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law (T5). The same formula appears as Cost.Jcost and as the cost of a recognition event in the observer-forcing layer.
The Primitive Recognition Calculus (PRC) works with discrete displays before the real continuum. A RatioOrbit is an integer-numerator / nonzero-orbit-denominator rational display. The sibling map onRatioOrbit assigns to each such display a rational cost; onRatioOrbit_toRat gives its closed form on the underlying rational.
This lemma is the transport step: it says that after embedding into $\mathbb{R}$, that rational cost is exactly the classical $J$ evaluated at the same ratio. It sits in the PRC J-cost module that packages the discrete cost surface and its bridge to the continuous theory.
proof idea
Rewrite the left-hand side by the sibling identity onRatioOrbit_toRat, which replaces the PRC cost by its explicit rational expression in the underlying ratio. Unfold the definition of Cost.Jcost to $(x+x^{-1})/2-1$. Push the rational-to-real cast through subtraction, division, addition, and inversion via the standard Rat.cast_* lemmas. Finish by norm_num, which checks the two algebraic expressions agree after casting.
why it matters
This is the real-bridge field of prc_jcost_certificate, the package theorem that closes the PRC rational cost surface through canonical RCL and "bridges honestly to the existing continuous-real uniqueness theorem." Without the equality, the discrete PRC cost would be only formally analogous to $J$; with it, every rational orbit display is certified to carry the same numerical cost that T5 uniqueness assigns on $\mathbb{R}_{>0}$.
In the forcing chain this is the discrete-to-continuous handoff for the J-cost: T5 forces $J(x)=\cosh(\log x)-1$ on reals, and this lemma shows the PRC rational formula is that same $J$ on the dense rational skeleton. Downstream certificate consumers can therefore quote continuous uniqueness while computing on orbit displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.