PRCNativeCostPositive
plain-language theorem explainer
Positivity for a native cost map F on ratio orbits: every positive rational orbit is sent to a non-negative one. The property is stated as a Prop so that structural forcing can derive it rather than assume it. Downstream theorems prove the canonical selected cost satisfies it, and that any F meeting the structural native-cost hypotheses is positive. Citation target for the free-side stratification ledger.
Claim. A map $F$ from ratio orbits to ratio orbits is positive when, for every orbit $q$ with positive rational representative, the image $F(q)$ has non-negative rational representative: $\forall q,\; 0 < \mathrm{rat}(q) \Rightarrow 0 \le \mathrm{rat}(F(q))$.
background
In the Primitive Recognition Calculus, native costs act on ratio orbits (equivalence classes of positive rational ratios under the integer-rational carrier). The map toRat extracts a canonical rational representative. Cost in the broader RS stack is the J-cost $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness), which is non-negative on positive reals and zero only at $x=1$.
This module builds a structural ledger for native costs on that countable carrier. Positivity is one of the structural axioms the ledger tracks: recognizing a positive imbalance should never pay. The doc-comment stresses that the property is derived later, not postulated. Sibling facts about the closed-form $J$-on-orbits map (jq_nonneg, jq_eq_zero) supply the analytic content once a candidate $F$ is identified with that form.
Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) all inherit non-negativity from $J$; the present definition is the orbit-level packaging used by the PRC structural certificate.
proof idea
Definitional: the body is the universal statement that positive rational orbits map to non-negative ones. No proof obligations. Downstream one-liners discharge instances by rewriting the candidate $F$ to the closed $J$-on-orbit form and applying jq_nonneg.
why it matters
Pins the positivity half of the structural native-cost interface. structural_forces_positive turns it into a theorem: any $F$ satisfying the structural hypotheses is positive, so "recognizing a positive imbalance never pays" is forced rather than axiomatic. canonicalSelectedNativeCost_positive checks the selected canonical cost against the same Prop via jq_nonneg. Both feed StructuralStratificationCertificate, whose uniqueness field forces the canonical cost on the free side and leaves only a unit-size anchor free.
Framework link: non-negativity of $J$ is the T5 landmark; packaging it as a native-cost structural axiom lets the ledger separate what arithmetic forces from what calibration fixes. No open scaffold: the Prop is closed and the forcing theorem already derives it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.