canonicalSelectedNativeCost_positive
plain-language theorem explainer
The canonical native cost on ratio orbits is nonnegative on every orbit whose rational display is positive. Structural-ledger and PRC-cost developments cite this as the derived positivity axiom (recognizing a difference never pays). The proof rewrites the selected cost to the closed J-formula and applies elementary nonnegativity of that formula on positive rationals.
Claim. Let $F$ be the canonical selected native cost on ratio orbits (the $J$-cost with the unit orbit sent to the zero representative). Then $F$ is positive: for every ratio orbit $q$ with rational display $t = q_{\mathrm{rat}} > 0$, the rational display of $F(q)$ satisfies $(F(q))_{\mathrm{rat}} \ge 0$.
background
In the primitive recognition calculus, native costs act on ratio orbits: multiplicative orbits of positive rationals under the distinction structure. The J-cost is the unique cost forced by the Recognition Composition Law, with closed form $J(t)=(t+t^{-1})/2-1$ on $t>0$ (written here as the rational map underlying the orbit cost).
The canonical selected native cost is that J-cost with a zero-calibration choice at the unit: it returns the literal zero orbit when the display equals 1, and otherwise follows the on-orbit J map. A cost map $F$ is called positive when every orbit with positive rational display is sent to an orbit whose display is nonnegative. The module treats this as a derived structural property, not an assumption.
Two upstream facts feed the argument directly. The display of the canonical selected cost equals $J$ of the input display on every orbit. Separately, $J$ itself is nonnegative on every positive rational, by rewriting to the closed form and a positivity check.
proof idea
Fix a ratio orbit $q$ with positive rational display. Rewrite the rational display of the canonical selected cost at $q$ by the identification theorem that equates it with $J$ of that display. The goal becomes $J(t)\ge 0$ for $t>0$, which is exactly the elementary nonnegativity lemma for the closed J-formula (closed-form rewrite, then positivity). The whole argument is a three-step intro/rewrite/apply wrapper.
why it matters
This discharges the positivity half of the structural axioms for the canonical native cost inside the PRC structural-ledger module. The local doc frames the point sharply: positivity is derived, not assumed; recognizing a difference never pays. Together with the companion identification of the selected cost with $J$, it places the zero-calibrated J-witness inside the strengthened hypothesis class used for ledger forcing.
In the Recognition Science forcing chain this is the cost-side nonnegativity companion of T5 J-uniqueness, $J(x)=\cosh(\log x)-1$. The same module immediately continues into signed-unit calibration from ledger antisymmetry at the unit (Part 4). The dependency graph currently lists no external consumers; the lemma is a local certificate that the selected native cost satisfies the positivity structural axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.