PRCRecognizerBridgeCertificate
plain-language theorem explainer
Step-14 Prop certificate closing the PRC recognizer surface: positive ratios exist, recognition cost is the rational J-display $(r+r^{-1})/2-1$, its real cast equals Cost.Jcost, and continuous Law-of-Logic uniqueness forces any qualifying $F$ to equal $J$. Kernel and universal-foundation certificates cite it. The structure only packages obligations; the companion theorem supplies the witnesses.
Claim. A certificate asserting: nonempty positive PRC ratios; a recognition-cost map from those ratios into PRC rationals; for every positive ratio $r$, the recognition cost equals $(r+r^{-1})/2-1$ as a rational; that cost, cast to $\mathbb{R}$, equals $J(r)$ with $J(x)=(x+x^{-1})/2-1$; and the continuous Law-of-Logic bridge (any Aczel-smooth reciprocal normalized composition-law calibrated continuous $F:(0,\infty)\to\mathbb{R}$ equals $J$), plus named reflexive tags for the native cost-uniqueness target and classical-extension strength.
background
Primitive Recognition Calculus (PRC) builds a native arithmetic and cost surface before bridging into the continuous Recognition Science cost. Positive PRC ratios (PRCPositiveRatio) are the comparison inputs: a PRC rational together with a positivity witness. Recognition cost on such a ratio is the sibling map that returns a PRC rational.
Upstream, the RS cost is the familiar $J(x)=(x+x^{-1})/2-1$ (T5 J-form). The Law-of-Logic bridge target states that any real function $F$ that is Aczel-smooth, reciprocal, normalized, composition-law compliant, calibrated, and continuous on $(0,\infty)$ must equal $J$ pointwise on positives. That is the continuous uniqueness route already proved in the Cost functional-equation stack.
This module sits between the integer/rational PRC layer and the kernel/universal-foundation certificates. Step 14 records that the recognizer surface is closed through that existing continuous bridge, while fully native arbitrary-cost uniqueness remains a separately named PRC target.
proof idea
No proof body: this is a Prop-valued structure definition. Each field is an obligation or a reflexive naming tag. Nonemptiness fields demand concrete witnesses (a positive unit ratio; the recognition-cost function). The two cost identities demand the rational J-display and its real cast equal to Cost.Jcost. The Law-of-Logic field is exactly the continuous uniqueness target. The last two fields are intentional identity equalities that pin the named native-uniqueness target and the classical-extension strength tag by name. The companion theorem prc_recognizer_bridge_certificate fills every field.
why it matters
In the PRC forcing stack this is the Step-14 recognizer-bridge certificate. It ties the discrete PRC cost surface to T5 J-uniqueness via the continuous Law-of-Logic route (RCL composition law, reciprocity, normalization, calibration, continuity), without claiming the harder fully native uniqueness theorem still named in PRCJCost.
Downstream, prc_recognizer_bridge_certificate inhabits it; KernelFirstPassCertificate bundles first-pass kernel stages; and both PRCUniversalFoundationCertificate and the conditional variant compose top-level PRC surfaces with the native-cost ledger. The certificate therefore marks where continuous uniqueness is accepted as the bridge while native arbitrary-cost uniqueness stays an open named target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.