prc_recognizer_bridge_certificate
plain-language theorem explainer
Packages the Primitive Recognition Calculus recognizer surface into a single certificate: positive ratios carry a recognition cost equal to the continuous J-cost, with the Law-of-Logic bridge already proved. Kernel and universal-foundation certificates cite it as Step 14. Proof is a structure assembly that plugs in preexisting lemmas and two reflexivity tags.
Claim. A recognizer-bridge certificate holds: the positive-ratio surface is nonempty; recognition cost is defined on it; for every positive PRC ratio $r$ with value $x$, the cost equals $(x+x^{-1})/2-1$ as a rational and equals $J(x)$ after real embedding; the continuous Law-of-Logic bridge target is proved. Fully native arbitrary-cost uniqueness remains a named open PRC target.
background
Primitive Recognition Calculus (PRC) works over a rational field of comparison ratios. A positive PRC ratio is a PRC rational together with a positivity witness; the unit ratio is the canonical seed. Recognition cost on such a ratio is the native PRC cost map, displayed as $(x+x^{-1})/2-1$ after conversion to ordinary rationals.
That display is exactly the continuous J-cost $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness) once cast to reals. The module closes the recognizer surface by bridging PRC costs into the existing continuous Law-of-Logic path rather than re-deriving uniqueness from scratch.
Upstream, cost_toReal_jcost equates the real cast of the PRC cost to Cost.Jcost, and PRCRecognitionCost_display records the rational identity. The certificate structure records nonempty surfaces, those identities, the Law-of-Logic bridge proof, and named tags for the remaining native-uniqueness target.
proof idea
Tactic proof that builds the certificate structure field by field. Positive-ratio surface is witnessed by the unit ratio. Recognition-cost surface is witnessed by the PRC recognition-cost map. Cost display is the already-proved rational identity. The real J-cost bridge is discharged by introducing an arbitrary positive ratio and applying cost_toReal_jcost. Law-of-Logic bridge is the preexisting proved target. Native-uniqueness name and strength tag are closed by reflexivity.
why it matters
Step 14 of the PRC recognizer program: it certifies that the discrete recognizer surface is closed through the continuous Law-of-Logic bridge, so downstream foundation layers need not rebuild cost identities. Feeds kernel_first_pass_certificate (K7/A2 first-pass kernel inhabited) and prc_universal_foundation_conditional_certificate, which packages kernel, real complete ordered field, and trace logic into the conditional universal foundation.
Framework landmark: the cost identity is T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$. The certificate deliberately leaves fully native arbitrary-cost uniqueness as the named open target from PRCJCost, so the continuous bridge is the present closure path rather than a claim of native uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.