PRCNativeCostMonotone
plain-language theorem explainer
Defines monotonicity for a native cost map on ratio orbits: on positive integer orbits, larger rational imbalance never yields a smaller cost value. Cost and gauge-orbit authors cite it as a field of the anchor-free RCL pack and as the target of concrete monotone lemmas. It is a pure Prop abbreviation, not a proved statement.
Claim. A map $F$ from ratio orbits to ratio orbits is native-cost monotone when, for all positive integer orbits $a,b$ (orbits whose rational display equals some natural number $\ge 1$), $a^{\mathrm{rat}} \le b^{\mathrm{rat}}$ implies $(F a)^{\mathrm{rat}} \le (F b)^{\mathrm{rat}}$.
background
In the primitive recognition calculus, a ratio orbit packages a signed integer numerator over a nonzero distinction-nat denominator. The verifier map toRat sends it to $\mathbb{Q}$ by ordinary division; the internal equality is cross-multiplication, not floating-point comparison.
A positive integer orbit is one whose rational display equals some natural $n \ge 1$. Native cost maps act on ratio orbits and are later required to obey the Recognition Composition Law and related structural axioms. Monotonicity is the order-preservation half of that pack: cost is not allowed to fall as the displayed positive integer imbalance grows.
The same predicate appears in the real-character factorization layer as a field of the anchor-free hypothesis bundle (RCL base without the two-point calibration, plus sign-reversal, zero-calibration of the doubled trace, and this monotone clause).
proof idea
No proof: the declaration is a definitional Prop. It expands to the universal quantification over positive integer orbits $a,b$ that $a.\mathrm{toRat} \le b.\mathrm{toRat}$ forces $(F a).\mathrm{toRat} \le (F b).\mathrm{toRat}$. Downstream theorems discharge it by rewriting $F$ on rationals and applying ordinary inequalities on $\mathbb{Q}$ or $\mathbb{N}$.
why it matters
Monotonicity is one of the structural ledger axioms that pin native cost before uniqueness and minimality certificates. It is a required field of SansAnchorHypotheses, so every gauge-orbit and real-character factorization argument that works without the two-point anchor inherits it.
Concrete cost constructors prove the predicate: canonical selected native cost, signed-power native cost, and sign-gauge native cost each supply a monotone lemma targeting this definition. Downstream, positive charging at orbit two and related classification results rely on the monotone field inside the sans-anchor pack.
In the broader Recognition chain this is bookkeeping for the J-cost side (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ and the RCL identity), not a derivation of $\varphi$ or dimension. It keeps cost nondecreasing on the positive integer ladder so later uniqueness and selection theorems stay well-posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.