cost
plain-language theorem explainer
Assigns the quotient-level Primitive Recognition Calculus J-cost to a positive ratio, returning a PRC rational. Anyone working with recognizer comparisons, cost-rate actions, or J-cost derived observables cites this as the canonical cost map on the PRC positive-ratio surface. The body is a one-line application of the PRC J-cost evaluator on the underlying rational value.
Claim. For a positive PRC ratio $r$ (a PRC rational together with a positivity witness), the cost of $r$ is the quotient-level PRC $J$-cost of its underlying value, as an element of the PRC rationals.
background
Primitive Recognition Calculus works with PRC rationals (PRCRat) as the discrete carrier for ratios before real display. A positive PRC ratio is a pair: a PRC rational value and a proof that it is positive. That structure is the input surface for recognizer comparisons in this bridge module.
The classical Recognition Science cost is the unique $J$ forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ (T5). Parallel modules define related costs: observer forcing takes cost of a recognition event as $J$ of its state; multiplicative recognizers induce a derived cost on positive reals; cosmology uses summed weighted $J$-costs over events. Here the cost stays at the PRC-rational level rather than jumping to $\mathbb{R}$.
The module sits between inevitability results for the primitive calculus and the rational-field layer (onPRCRat), packaging the J-cost so downstream bridges can treat positive ratios uniformly.
proof idea
Pure definition, not a proof. The body applies PRCJCost.onPRCRat to the underlying value field of the positive-ratio structure. No tactics, no lemmas unfolded beyond that evaluator; the positivity witness is not re-checked in the body because the J-cost map is already typed to act on the rational carrier via the rational-field embedding.
why it matters
This is the local cost map that lets the recognizer bridge speak the same J-language as the rest of the monolith. Downstream, the Action.EulerLagrange development uses cost-rate structure whose EL equation reduces to $J'(q)=0$, with uniqueness of the constant path $\gamma\equiv 1$ among positive continuous paths (least-action ground state). Acoustics certificates (pitch JND fraction bounds, speech intelligibility) inherit non-negativity, reciprocity, and zero-at-unity from the same J-cost family.
In the forcing chain this sits under T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Keeping cost at PRC-rational level supports certified bridges before real display, which sibling certificates in this module target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.