PRCRecognizerLawOfLogicBridgeTarget
plain-language theorem explainer
Names the exact uniqueness target that links Primitive Recognition Calculus recognizer costs to the continuous Law-of-Logic theorem: any reciprocal, normalized, composition-law, calibrated cost continuous on positives equals J(x)=(x+x^{-1})/2-1. Downstream certificates and the proved bridge cite this Prop. The body is a pure Prop abbreviation packing the standard uniqueness hypotheses.
Claim. The bridge target asserts: for every $F:\mathbb{R}\to\mathbb{R}$, if the Aczél smoothness package holds, $F$ is reciprocal ($F(x)=F(x^{-1})$ for $x>0$), normalized ($F(1)=0$), satisfies the recognition composition law, is calibrated ($G''(0)=1$ for $G(t)=F(e^t)$), and is continuous on $(0,\infty)$, then $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.
background
Primitive Recognition Calculus builds recognizer costs on positive ratios and needs a clean handoff into the already-proved continuous uniqueness theorem for recognition cost. The classical cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced as the unique solution under the Recognition Composition Law once reciprocity, normalization, calibration, and continuity are imposed.
The hypotheses packed here are the standard Law-of-Logic package: reciprocity $F(x)=F(1/x)$; normalization $F(1)=0$; the composition identity; calibration $\lim_{t\to 0} 2F(e^t)/t^2=1$ (equivalently $G''(0)=1$); continuity on $(0,\infty)$; and the Aczél smoothness package, which upgrades continuous d'Alembert solutions $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ to $C^\infty$ (constants or $\cosh(\lambda t)$).
This module sits in the Foundation recognizer-bridge layer: it does not reprove uniqueness, it names the exact Prop that the existing bridge theorem discharges.
proof idea
No proof: this is a definition of a proposition. The body is a single universal quantifier over $F$ conjoined with the six standard uniqueness hypotheses, concluding pointwise equality with $J$ on positives. The companion theorem PRCRecognizerLawOfLogicBridgeTarget_proved discharges it in one step by applying PRCJCost.bridge_to_existing_jcost_uniqueness to those same hypotheses.
why it matters
This is the named interface between PRC recognizer costs and T5 J-uniqueness in the forcing chain. The Recognition Composition Law plus reciprocity, normalization, calibration, and continuity force $J(x)=(x+x^{-1})/2-1$; packaging that claim as an explicit Prop lets the recognizer surface close without re-deriving the continuous uniqueness argument.
Downstream, PRCRecognizerLawOfLogicBridgeTarget_proved asserts the Prop, and PRCRecognizerBridgeCertificate (Step 14) records that "the recognizer surface is closed through the existing continuous Law-of-Logic bridge," while noting that fully native arbitrary-cost uniqueness remains the separate PRC target in PRCJCost.lean. Citing this definition pins exactly which uniqueness statement the certificate relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.