PRCPositiveRatio
plain-language theorem explainer
Positive PRC ratios package a primitive-recognition rational together with a positivity witness. They form the typed input surface on which recognizer J-costs are evaluated. Anyone wiring PRC comparisons into the classical J-cost bridge cites this carrier. As a structure definition there is no proof body; the positivity field is the only constraint.
Claim. A positive PRC ratio is a pair $(v, p)$ where $v$ is a PRC rational and $p$ asserts that $v$ is positive (equivalently, its underlying rational is strictly greater than zero). These pairs are the domain of the quotient-level recognition cost $J(v) = (v + v^{-1})/2 - 1$.
background
The Primitive Recognition Calculus (PRC) builds recognition comparisons from rationals before any real analysis is introduced. PRCRat is the PRC rational type; positivity is the predicate that the underlying rational is strictly positive, so inversion and the symmetric mean $(x+x^{-1})/2$ are well-defined.
This module sits in the RecognizerBridge layer: it connects PRC-native costs to the classical Recognition Science cost $J(x)=\cosh(\log x)-1$, also written $(x+x^{-1})/2-1$ (the T5 J-cost). Upstream material supplies certified analytic protocols, dyadic real values, and canonical arithmetic objects; those are used later when costs are displayed as reals, not in the structure itself.
Locally, positive ratios are the only legal inputs to recognizer comparisons. The unit ratio (value $1$) is the canonical base point of the type.
proof idea
No proof: this is a structure definition. It records a PRC rational field value and a proof field positive that PRCRat.positive holds of that value. Downstream constructors (e.g. the unit ratio) discharge positivity by rewriting to the underlying rational and using the known positivity of $1$.
why it matters
This carrier is the typed doorway into the PRC recognizer bridge. Every cost map in the module takes a positive ratio: the quotient-level PRC J-cost, its rational display $(v+v^{-1})/2-1$, the real identification with Cost.Jcost, and the named recognition-cost alias all depend on it. The bridge certificate and its target proposition likewise quantify over this type.
In the broader framework it is the discrete, positivity-guarded surface on which T5 J-uniqueness is instantiated before continuous or measure-theoretic forcing. Without the positivity witness, inversion in the RCL identity and the J-cost formula would be ill-typed at the PRC layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.