canonicalSelectedNativeCost_monotone
plain-language theorem explainer
The canonical selected native cost is monotone on positive integer ratio orbits: if the displayed rational of a does not exceed that of b, the cost of a does not exceed the cost of b. Anyone assembling the structural native-cost hypothesis pack cites this. The proof rewrites both sides to the rational J-display jq and applies the elementary monotonicity of jq on [1, ∞).
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 monotone on positive integer orbits: whenever $a$ and $b$ are positive integer orbits and $a$ displays as a rational $\le$ the display of $b$, the rational display of $F(a)$ is $\le$ that of $F(b)$.
background
In the Primitive Recognition Calculus ledger, a native cost is a map $F$ on ratio orbits. Two structural axioms are isolated here: positivity (recognizing a difference never pays) and monotonicity (on positive integer orbits, cost does not fall as imbalance grows). Monotonicity is the predicate that for positive integer orbits $a,b$ with $a.toRat \le b.toRat$, one has $(F a).toRat \le (F b).toRat$.
The canonical selected native cost is the $J$-cost witness with the unit orbit forced to the literal zero representative; it is the non-vacuity witness for the zero-calibrated prime-signed strengthened class. A companion lemma records that its rational display equals $jq$ on every orbit (both sides zero on the unit branch). The function $jq$ is the rational form of the unique T5 cost $J(x)=(x+x^{-1})/2-1$, and $jq$ is already known to be monotone on $[1,\infty)$.
proof idea
Term-mode proof by introduction of the two positive-integer-orbit hypotheses and the display inequality $a.toRat \le b.toRat$. Rewrite both cost displays via the identity that the canonical selected cost equals $jq$ on the rational display. The remaining goal is $jq$-monotonicity; feed $jq_mono$ the lower bound $1 \le a.toRat$ (cast from the positive-integer-orbit certificate) and the given inequality $a.toRat \le b.toRat$.
why it matters
This closes the monotone slot in the structural native-cost hypothesis record for the canonical witness. Downstream, canonicalSelectedNativeCost_structural_hypotheses packages native, sign-reversing, and monotone fields into a single non-vacuity certificate for the structural ledger; the monotone field is exactly this theorem.
In the broader Recognition chain the cost is the unique T5 $J$ forced by the Recognition Composition Law. Monotonicity on positive integer orbits is the discrete imbalance-ordering property expected of that cost before continuous calculus is restored. Without it the structural pack would be empty and the selected witness would not certify the ledger axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.