PRCRecognitionCost
plain-language theorem explainer
Names the recognition cost of a positive PRC ratio as a PRC rational, equal to the quotient-level J-cost of its value. Anyone wiring the primitive recognition calculus into the continuous Law-of-Logic bridge cites this surface. The body is a one-line projection onto the existing positive-ratio cost map.
Claim. For a positive PRC ratio $r$ (a PRC rational $v$ with a positivity witness), the recognition cost of $r$ is the PRC rational $J$-cost of $v$.
background
Primitive Recognition Calculus (PRC) builds rationals as quotient classes of ratio orbits (nonzero-denominator pairs identified by cross-multiplication). Positive PRC ratios package such a rational with a positivity witness; they are the input surface for recognizer comparisons.
Across the foundation stack, recognition cost is the $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely by the Recognition Composition Law and T5. In this module the sibling map already assigns to each positive ratio the quotient-level PRC $J$-cost of its underlying value via PRCJCost.onPRCRat.
The local setting is the recognizer bridge: close the PRC surface through the existing continuous Law-of-Logic bridge, while full native uniqueness of arbitrary costs remains a named PRC target.
proof idea
One-line definitional wrapper. The body is exactly the sibling cost on positive PRC ratios, which itself is PRCJCost.onPRCRat applied to the underlying PRC rational. No tactics, no lemmas beyond that projection.
why it matters
Gives the named recognition-cost surface required by the Step 14 bridge certificate. Downstream, the display theorem proves that converting this cost to an ordinary rational recovers $(v+v^{-1})/2-1$, and the certificate structure packages nonempty positive-ratio and cost surfaces together with that display identity and the real $J$-cost bridge.
In the forcing chain this is the PRC-side handle on T5 $J$-uniqueness and the RCL cost, not a new derivation of $J$. It feeds the certificate that the recognizer surface is closed through the continuous Law-of-Logic bridge; fully native arbitrary-cost uniqueness stays open in PRCJCost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.