one

Positive PRC ratios form the input surface for recognizer comparisons: a structure pairing a PRC rational with a positivity witness. The module sits in the Primitive Recognition Calculus bridge that connects that surface to recognizer cost and the law-of-logic target.

Upstream cost notions in the foundation treat recognition cost as a J-cost (or a derived comparator cost) on positive ratios. The unit ratio is the multiplicative identity against which those costs are normalized; its rational embedding is the ordinary $1\in\mathbb{Q}$.

Sibling definitions in the same file assign the quotient-level PRC J-cost to a positive ratio and build the recognizer-bridge certificate that ties the PRC surface to the multiplicative recognizer law.

Definitional construction: set the underlying PRC rational to $1$. The positivity field is proved by rewriting through the characterization that positivity is equivalent to a positive rational image, changing the goal to $0 < \mathrm{toRat}(1)$, unfolding the embedding of one, and closing with norm_num.

Supplies the base point of the positive-ratio surface inside RecognizerBridge. Downstream siblings (quotient J-cost on positive ratios, the recognizer-law bridge target, and the bridge certificate) treat this unit as the identity input for cost evaluation and for stating that the PRC recognizer matches the forced J-cost law. In the broader forcing chain, J vanishes at the multiplicative identity ($J(1)=0$), so the unit ratio is the zero-cost reference before rung ladders, eight-tick structure, or dimension forcing are applied. No external used-by edges are recorded yet; the declaration is local scaffolding for the bridge certificate in this module.