signedPowerNativeCost_monotone
plain-language theorem explainer
The native cost built from the sign-extended power character χ(x)=sgn(x)|x|^(m+1) is monotone on positive integer ratio orbits: larger rational display yields larger cost display. Anyone assembling the anchor-free structural ledger for power characters cites this. The proof rewrites to the rational J-cost of signedPow and applies J-monotonicity plus signed-power monotonicity on [1,∞).
Claim. For every natural number $m$, the map $F_m$ sending a ratio orbit $q$ to the native cost of the sign-extended power $\mathrm{sgn}(q)\,|q|^{m+1}$ (with the unit orbit sent to zero) is monotone on positive integer orbits: if $a,b$ are positive integer orbits and $a\le b$ as rationals, then $F_m(a)\le F_m(b)$ as rationals.
background
In the Primitive Recognition Calculus, ratio orbits are discrete ratio objects with a verifier display toRat into $\mathbb{Q}$. A native cost is a self-map on ratio orbits; the structural monotone field asks that on positive integer orbits (orbits whose rational display is a positive integer), order of displays is preserved by the cost.
The signed power character is $\chi_m(x)=\mathrm{sgn}(x),|x|^{m+1}$. The associated native cost signedPowerNativeCost m sends the unit orbit to zero and otherwise pushes the orbit through signedPow then the rational J-cost $J_q$ (the discrete cost on $\mathbb{Q}$). Upstream, signedPowerNativeCost_toRat identifies the display of this cost with $J_q(\mathrm{signedPow}, m, q)$.
Local setting is gauge-orbit cost from real characters: one builds candidate native costs from real multiplicative characters and checks the structural ledger fields (base RCL pack without the two-point anchor, sign reversal, monotonicity, zero calibration).
proof idea
Tactic proof. Fix positive integer orbits $a,b$ with $a.\mathrm{toRat}\le b.\mathrm{toRat}$. Rewrite both cost displays by signedPowerNativeCost_toRat, reducing the goal to $J_q(\mathrm{signedPow}, m, a)\le J_q(\mathrm{signedPow}, m, b)$.
From the positive-integer witness for $a$, obtain $1\le a.\mathrm{toRat}$. Then signedPow_of_one_le gives $1\le\mathrm{signedPow}, m, a$, and signedPow_mono gives $\mathrm{signedPow}, m, a\le\mathrm{signedPow}, m, b$. Finish by jq_mono, the monotonicity of the rational J-cost on arguments $\ge 1$.
why it matters
Monotonicity is one of the four structural fields in the anchor-free native-cost ledger. Downstream, signedPowerNativeCost_sansAnchor packages base-sans-two, sign-reversing, monotone, and zero-calibrated into PRCStructuralNativeCostHypothesesSansAnchor for every nonnegative exponent $m$, so every parity of the power character inhabits the ledger.
That packing is the bridge from concrete power characters to the real-character factorization story in this module: once the structural hypotheses hold, the cost is a candidate for the gauge-orbit / real-character factorization path. In Recognition Science terms this is cost-side structure supporting the J-cost uniqueness chain (T5) and the Recognition Composition Law on discrete orbits, not a new forcing step by itself.
No scaffolding remains on this lemma; it is fully proved and only feeds the sans-anchor assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.