PRCRecognizerLawOfLogicBridgeTarget_proved
plain-language theorem explainer
Any continuous positive-real cost that is reciprocal, normalized, calibrated, and obeys the Recognition Composition Law equals the unique J-cost on $(0,\infty)$. Foundation workers cite this when closing the Primitive Recognition Calculus recognizer surface against the existing Law-of-Logic uniqueness theorem. The proof is a one-line discharge of the named bridge target by the real-domain uniqueness lemma already proved in PRCJCost.
Claim. If $F:\mathbb{R}\to\mathbb{R}$ satisfies the Acz\'el smoothness package, is a reciprocal cost, is normalized, satisfies the composition law, is calibrated, and is continuous on $(0,\infty)$, then $F(x)=J(x)$ for every $x>0$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Primitive Recognition Calculus (PRC) builds recognition cost on positive ratios before landing on the classical real J-cost. The local bridge target asserts that any real function meeting the standard Law-of-Logic package equals $J$ pointwise on positives. That package is: Aczél regularity (smoothness commitment kept explicit), reciprocity $F(x)=F(x^{-1})$, normalization, the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ (and its $F$-analogue), calibration, and continuity on $(0,\infty)$.
Upstream, bridge_to_existing_jcost_uniqueness is the real-domain uniqueness theorem PRC currently uses; its doc states that the quantified Aczél package keeps the regularity commitment explicit. Sibling cost surfaces assign quotient-level PRC J-cost on positive ratios and display it against the classical $J$. The module sits in the foundation chain that forces $J$ uniqueness (T5) before $\varphi$, the eight-tick octave, and $D=3$.
proof idea
One-line wrapper. After introducing the function $F$ and the six package hypotheses plus the positive point $x$, the proof applies PRCJCost.bridge_to_existing_jcost_uniqueness with exactly those arguments. No extra algebraic work occurs here; the bridge target is definitionally the same quantified statement as that upstream uniqueness theorem.
why it matters
This declaration is Step 14 on the recognizer bridge: it closes the continuous Law-of-Logic surface so the PRC recognizer certificate can record a real $J$-cost bridge. Downstream, prc_recognizer_bridge_certificate consumes it as the real_jcost_bridge field; the module doc notes that the recognizer surface is thereby closed through the existing continuous bridge, while fully native arbitrary-cost uniqueness remains the named open PRC target in PRCJCost.
In the broader forcing chain this is the T5 J-uniqueness landing for the recognizer calculus: once costs are forced to $J(x)=\cosh(\log x)-1$, the self-similar fixed point $\varphi$ (T6) and the later octave and dimension steps sit on a single cost. The certificate does not yet replace the classical uniqueness engine; it only wires PRC into it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.