signedPow_mono
plain-language theorem explainer
On rationals at least 1, the map x ↦ x·|x|^m is monotone for every natural m. Anyone building monotone native-cost displays from odd powers of a positive base cites this. The proof reduces to nonnegativity of a and b, ordinary power monotonicity, and a two-step product comparison after dropping absolute values.
Claim. For every natural number $m$ and rationals $a,b$ with $1 \le a \le b$, one has $a\,|a|^m \le b\,|b|^m$. Equivalently, the sign-extended power $x \mapsto \mathrm{sgn}(x)\,|x|^{m+1}$ is monotone on $[1,\infty)\cap\mathbb{Q}$.
background
The ambient module builds gauge-orbit native costs from real-character factorizations of the structural ledger cost. The auxiliary signedPow is defined by $x\cdot|x|^m$, which equals $\mathrm{sgn}(x),|x|^{m+1}$ and keeps multiplicativity a single absolute-value identity away from case splits.
Native-cost displays in this file (sign-gauge and signed-power variants) must be monotone on the positive ray so they qualify as PRC native costs. Monotonicity of the underlying rational map is the arithmetic step before lifting to the ledger carrier.
Upstream, ordinary ordered-field facts are used: transitivity of $\le$ on $\mathbb{Q}$, nonnegativity of powers when the base is nonnegative, and $1\le a\Rightarrow 1\le a^m$. No Recognition-specific forcing (T5–T8) enters here; the lemma is pure ordered arithmetic supporting the cost layer.
proof idea
From $1\le a$ obtain $0\le a$, then $0\le b$ by transitivity with $a\le b$. Power monotonicity gives $a^m\le b^m$, and $1\le a$ yields $1\le a^m$. Rewrite both sides of the goal via the definition and drop absolute values by nonnegativity, so the claim is $a\cdot a^m\le b\cdot b^m$. Split the product: first multiply $a\le b$ on the right by the nonnegative $a^m$, then multiply $a^m\le b^m$ on the left by the nonnegative $b$.
why it matters
Feeds directly into signedPowerNativeCost_monotone, which asserts that the signed-power native-cost display is PRC-monotone. That display is one of the concrete real-character candidates used to realize gauge-orbit costs without an anchor, sitting beside the sign-gauge native cost in the same module.
In the broader Recognition cost story, monotone native costs are the bridge from the J-cost / RCL layer to ledger-level comparisons. Establishing monotonicity of the odd-power map on $[1,\infty)$ is the elementary gate that lets signed-power displays inherit the structural factorization hypotheses already proved for the sans-anchor real character. No open scaffold remains: the theorem is fully proved and only the downstream native-cost packaging depends on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.