Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RecognizerBridge

show as:
view Lean formalization →

Module that treats positive Primitive Recognition Calculus ratios as the comparison surface for a recognizer, equipping them with a cost that recovers the classical J-cost on the reals. It packages a Law-of-Logic bridge target and a certificate that the bridge is proved. Downstream Kernel imports this surface; anyone wiring PRC ratios into the forcing or recognition-cost stack would cite it.

claimPositive PRC ratios $r > 0$ form the input surface for recognizer comparisons. A recognition cost $C$ on those ratios maps to a rational cost and, on the reals, agrees with the J-cost $J(x) = \frac{x+x^{-1}}{2}-1$. The module states a Law-of-Logic bridge target for this recognizer and records a certificate that the target is discharged.

background

Primitive Recognition Calculus (PRC) works with ratios rather than absolute scales. This module fixes the positive-ratio surface as the place where a recognizer may compare two states: only $r > 0$ is admitted as input.

Cost is the comparison functional. The module defines a PRC recognition cost on those ratios, a display form, and conversion maps into rationals and reals. The real conversion is required to match the standard J-cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), the unique cost forced by the Recognition Composition Law in the T5 step of the unified forcing chain.

Upstream, the module sits on Inevitability and RationalField: inevitability supplies the structural pressure that a recognizer must exist in this calculus; the rational field supplies the arithmetic carrier for exact ratio arithmetic before the real embedding.

proof idea

Definition-and-certificate module rather than a single deep proof. It introduces the positive-ratio type, the unit ratio, and the cost API (including the real J-cost agreement lemma). It then names an explicit Law-of-Logic bridge target for the PRC recognizer and a proved flag for that target, and packages both into a bridge certificate constant. Argument structure is: fix the surface, attach cost compatible with J, assert the bridge target, record the certificate consumed by Kernel.

why it matters in Recognition Science

Without a fixed positive-ratio surface and a cost that recovers J, the PRC recognizer cannot be wired into the rest of Recognition Science: T5 J-uniqueness, the RCL identity, and later mass or coupling ladders all assume comparisons live on that cost. The module feeds Foundation.PrimitiveRecognitionCalculus.Kernel, which imports it as the bridge layer between raw PRC ratios and the kernel recognizer API. The Law-of-Logic bridge target and its certificate are the local closure objects: they mark that the recognizer comparison law is not an open hypothesis at this layer, so Kernel can treat the bridge as discharged rather than conditional.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)