cost_toReal_jcost
plain-language theorem explainer
For every positive Primitive Recognition Calculus ratio, the real embedding of its rational recognition cost equals the classical J-cost of the real embedding of its value. Authors bridging the discrete PRC cost surface to the continuous RS cost functional cite this identity. The argument is a short cast-commutation: expose the rational cost formula, unfold J-cost, push rational casts through the arithmetic, and close by norm_num.
Claim. For every positive PRC ratio $r$, writing $c$ for its recognition cost as a rational and $v$ for its value as a rational, the real number corresponding to $c$ equals $J(v_{\mathbb{R}})$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The RS recognition cost on a positive real ratio is the functional $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$. It is the unique symmetric cost forced by the Recognition Composition Law and appears as T5 (J-uniqueness) in the unified forcing chain. Several modules expose the same formula under the name Jcost.
A positive PRC ratio packages a positive element of the Primitive Recognition Calculus rational field together with a positivity witness. It is the declared input surface for recognizer comparisons in this bridge module. The sibling rational cost map sends such a ratio to a rational whose arithmetic shape matches the J-expression before any real embedding.
The local setting is the RecognizerBridge layer of Primitive Recognition Calculus: discrete PRC costs must be shown to display as the continuous J-cost used by multiplicative recognizers and observer forcing. Upstream, the rational cost identity supplies the exact algebraic form that this theorem embeds into $\mathbb{R}$.
proof idea
Term-mode proof by successive rewrites. First apply the sibling rational cost identity to replace the left-hand side with the explicit rational J-expression in the ratio's value. Unfold the real cost functional $J(x)=(x+x^{-1})/2-1$. Push the rational-to-real cast through subtraction, division, addition, and inversion via the standard Rat.cast_* lemmas. The two sides then match definitionally up to trivial arithmetic, discharged by norm_num.
why it matters
This identity is the real-display leg of the PRC recognizer bridge. The sole downstream consumer is the bridge certificate theorem, which packages a positive-ratio surface, a recognition-cost surface, a display map, and a real_jcost_bridge field; the present result discharges that field.
In framework terms it ties the discrete PRC cost calculus to the continuous J-cost forced at T5, the same functional used by observer forcing (cost of a recognition event is its J-cost) and by multiplicative recognizer derived costs. Without the cast identity, the certificate cannot claim that PRC recognition cost displays as classical RS cost on positive ratios. It does not itself force J-uniqueness or the eight-tick/D=3 steps; it only aligns the two presentations already present in the stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.