IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RecognizerBridge
Module that treats positive Primitive Recognition Calculus (PRC) ratios as the input surface for recognizer comparisons. It packages ratio cost into a displayable recognition cost, links that cost to the classical J-cost on reals, and records a proved bridge target toward the Law of Logic. Downstream Kernel imports the certificate. Structure is mostly definitions plus a short certificate assembly, not a deep proof tree.
claimPositive PRC ratios $r > 0$ form the comparison domain. A recognition cost $C(r)$ is defined on that domain, with rational and real presentations, and the real form agrees with the J-cost $J(x) = \frac{x+x^{-1}}{2}-1$. The module states a Law-of-Logic bridge target for the recognizer and packages a certificate that the target is proved.
background
Primitive Recognition Calculus works with ratios rather than absolute scales: only relative magnitudes enter recognition comparisons. This module fixes the positive-ratio surface as that input. Sibling objects introduce a unit ratio, a cost on positive ratios, and coercions of that cost to rationals and to reals.
On the real line the cost is identified with the standard Recognition Science J-cost (the unique symmetric cost forced by the Recognition Composition Law and the T5 uniqueness step). The module sits between RationalField (ratio arithmetic) and Inevitability (forcing that the cost shape is unavoidable), and is consumed by Kernel as the recognizer-facing bridge layer.
Notation is RS-native: costs are dimensionless defects of the form $J$, not laboratory energies. Display helpers expose the cost for certificate and audit surfaces without changing the underlying Prop.
proof idea
Definition-heavy module. Positive ratios and the cost functional are introduced as data; cost_toReal_jcost records agreement with $J$ on reals. The Law-of-Logic bridge appears as an explicit target proposition together with a ..._proved witness. A certificate bundle (PRCRecognizerBridgeCertificate / prc_recognizer_bridge_certificate) assembles those pieces for Kernel import. No long tactic development: the argument is packaging and the real-cost identification, not a multi-step derivation inside this file.
why it matters in Recognition Science
Recognizer comparisons need a clean, positive-ratio domain and a cost that matches the forced J-functional before any Kernel-level law can be stated. This module is that interface: it feeds PrimitiveRecognitionCalculus.Kernel via module import and supplies the proved bridge target plus certificate that Kernel can treat as settled input.
In the broader forcing chain, tying PRC cost to $J$ keeps the recognizer on the same T5 uniqueness track as the rest of the monolith (RCL, $\phi$ fixed point, eight-tick structure). Without this bridge, Kernel would either re-derive cost identity or accept an uncertified comparison surface. The certificate pattern also matches other Foundation audit objects: a named target, a proved flag, and a single exportable certificate term.
scope and limits
- Does not derive J-uniqueness; assumes the cost–J link rather than replaying T5.
- Does not prove full Kernel recognizer laws; only the bridge target and certificate.
- Does not treat non-positive or zero ratios as comparison inputs.
- Does not fix physical units, masses, or coupling constants; cost stays dimensionless.
- Does not expand Inevitability or RationalField proofs; it only imports them.
used by (1)
depends on (2)
declarations in this module (11)
-
structure
PRCPositiveRatio -
def
one -
def
cost -
theorem
cost_toRat -
theorem
cost_toReal_jcost -
def
PRCRecognitionCost -
theorem
PRCRecognitionCost_display -
def
PRCRecognizerLawOfLogicBridgeTarget -
theorem
PRCRecognizerLawOfLogicBridgeTarget_proved -
structure
PRCRecognizerBridgeCertificate -
theorem
prc_recognizer_bridge_certificate