PRCNativeCostMonotone
plain-language theorem explainer
Predicate asserting that a native cost map F on ratio orbits is nondecreasing when restricted to positive integer orbits: larger integer imbalance never lowers the displayed cost. Packaged into the anchor-free hypothesis bundle and discharged for power, sign-gauge, and canonical selected costs. Pure Prop definition; no proof content.
Claim. A map $F$ from ratio orbits to ratio orbits is monotone when, for all orbits $a,b$ that display positive integers, $a^{\mathbb{Q}} \le b^{\mathbb{Q}}$ implies $(F a)^{\mathbb{Q}} \le (F b)^{\mathbb{Q}}$, where $(\cdot)^{\mathbb{Q}}$ is the rational display of the orbit.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator, with toRat the verifier display as an ordinary rational (transport by cross-multiplication). A positive integer orbit is one whose display equals some natural $n \ge 1$.
Native cost maps send ratio orbits to ratio orbits and are constrained by the Recognition Composition Law pack (symmetry, calibration, d'Alembert/RCL identities on the doubled trace). Monotonicity is the structural demand that cost not decrease as positive-integer imbalance grows; the ledger doc states it as: "On positive integer orbits, cost does not decrease as the imbalance grows."
This module factors real characters of those costs. The same Prop appears in the structural ledger and is re-exported here so real-character and gauge-orbit developments can name the field without depending on the full ledger stack.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over pairs of positive-integer orbits of the inequality of their rational displays under $F$. No tactics, no lemmas applied; inhabitants discharge it by rewriting the concrete cost to a monotone rational function (e.g. $J$-style or power maps) on $\mathbb{Q}_{>0}$.
why it matters
Monotonicity is one field of SansAnchorHypotheses (with base-sans-two, sign-reversing, and zero-calibrated doubled trace). That pack is the anchor-free native-cost interface used to classify real characters and gauge orbits.
Downstream, it is proved for signed-power native costs, sign-gauge native cost, and the canonical selected native cost; it appears in the even-power generated ledger (everything except orientation) and in arguments that a nondegenerate inhabitant charges positively at orbit two. Together these pin which maps can serve as the unique $J$-cost of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$) once RCL and positivity are imposed.
Without this field, the ledger cannot exclude decreasing impostors or convert the two-point nondegeneracy into a strict positivity inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.