powerGeneratedNativeCost_monotone
plain-language theorem explainer
For every natural exponent n, the native cost generated by the power map q ↦ q^n is monotone on positive integer ratio orbits: larger imbalance never lowers cost. Anyone assembling the structural ledger for power-generated costs cites this. The proof reduces to rational display, then applies monotonicity of the rational J-cost jq under the power map on [1, ∞).
Claim. For every natural number $n$, the map $F_n$ sending a ratio orbit $q$ to the native cost of $q^n$ (or zero when $q=1$) is monotone on positive integer orbits: if $a,b$ are positive integer orbits and $a\le b$ as rationals, then $F_n(a)\le F_n(b)$ as rationals.
background
In the Primitive Recognition Calculus structural ledger, native costs are maps on ratio orbits. A ratio orbit is displayed as a rational via toRat (numerator over denominator). Positive integer orbits are those whose rational display is a positive integer.
Monotonicity is the predicate that on such orbits, cost does not decrease when the rational imbalance grows: if $a.toRat \le b.toRat$ then $(F a).toRat \le (F b).toRat$. The power-generated native cost $F_n$ is the cost of $q \mapsto q^n$, with the unit orbit sent to zero.
The comparison is carried by the rational cost $jq(s) = (s + s^{-1})/2 - 1$ (the discrete J-cost on $\mathbb{Q}_{>0}$). Upstream, $jq$ is already known monotone on $[1,\infty)$: if $1 \le s \le t$ then $jq(s) \le jq(t)$. That fact is the engine here.
proof idea
Tactic proof. Fix orbits $a,b$ that are positive integer orbits with $a.toRat \le b.toRat$. Rewrite both $(F_n a).toRat$ and $(F_n b).toRat$ via the transport lemma that identifies the power-generated cost with $jq$ of the powered rational. From the positive-integer hypothesis get $1 \le a.toRat$. Apply $jq$-monotonicity: $1 \le a.toRat^n$ by one_le_pow₀, and $a.toRat^n \le b.toRat^n$ by pow_le_pow_left₀ (using nonnegativity of $a.toRat$ via $0 \le 1 \le a.toRat$). Conclude $jq(a.toRat^n) \le jq(b.toRat^n)$.
why it matters
Power-generated costs are the main family tested against the native-cost structural hypotheses. This lemma supplies the monotone field for every exponent, even and odd alike.
Downstream, oddPowerGeneratedNativeCost_sansAnchor packages the odd-power family as satisfying the full structural hypotheses without the two-point anchor, citing this result as its monotone component. Likewise evenPowerGeneratedNativeCost_sans_signReversing records that even powers meet the anchor-free ledger except sign reversal, again using this monotonicity.
In the Recognition framework this sits under the native-cost uniqueness program tied to T5 J-uniqueness and the Recognition Composition Law: only costs compatible with J on positive orbits survive. Establishing monotonicity for the entire power family narrows which generators can serve as the native cost before parity and calibration split the candidates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.