PRCRecognitionCost_display
plain-language theorem explainer
On any positive PRC ratio with rational value x, the recognition cost displayed in Q equals (x + x^{-1})/2 - 1, the classical J-cost. Bridge authors cite it when wiring PRC costs into the Law-of-Logic uniqueness surface. The proof is a one-line wrapper of the sibling cost_toRat identity.
Claim. For every positive PRC ratio $r$ with rational value $x$, the recognition cost of $r$, transported to $\mathbb{Q}$, equals $\frac{x + x^{-1}}{2} - 1$.
background
Primitive Recognition Calculus (PRC) works with certified rational ratios before any real embedding. A positive PRC ratio is a PRC rational together with a positivity witness; it is the input surface for recognizer comparisons. Recognition cost on such a ratio is the structure field cost, packaged here as PRCRecognitionCost.
The display map toRat is a verifier transport from ratio orbits to ordinary rationals (spec tag A5: internal equality is cross-multiplication). The target formula is the unique J-cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Upstream, cost_toRat already proves the same identity on the raw cost field.
This module sits in the RecognizerBridge layer that connects PRC costs to the existing Law-of-Logic uniqueness theorem (forcing chain T5).
proof idea
One-line term wrapper: apply the sibling theorem cost_toRat at the given positive ratio. That lemma reduces via PRCJCost.onPRCRat_toRat on the underlying PRC rational, so no new algebra is done here. Unfolding PRCRecognitionCost (definitionally r.cost) makes the goals identical.
why it matters
This is the exact bridge target from PRC recognizer costs into Law-of-Logic uniqueness. Downstream, prc_recognizer_bridge_certificate installs it as the cost_display field of PRCRecognizerBridgeCertificate, alongside the positive-ratio surface and the real J-cost bridge.
In the Recognition Science forcing chain, T5 forces J-uniqueness: the only admissible cost compatible with the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$. Displaying PRC costs in that closed form lets the certificate hand off to the already-proved uniqueness theorem rather than re-deriving it inside PRC. Without this identity, the certificate cannot claim that the PRC cost surface is the same J that the rest of the monolith uses for mass ladders, eight-tick structure, and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.