signedPow_neg
plain-language theorem explainer
Odd-powered signed powers reverse sign: for any natural m and rational x, the signed power of −x equals the negation of the signed power of x. Cost and gauge-orbit arguments cite this when checking that a native cost is sign-reversing. The proof unfolds the definition, applies |−x|=|x|, and finishes by ring.
Claim. For every natural number $m$ and every rational $x$, the signed power satisfies $\mathrm{signedPow}(m,-x)=-\mathrm{signedPow}(m,x)$, where $\mathrm{signedPow}(m,x):=x\,|x|^m$ (equivalently $\mathrm{sgn}(x)\,|x|^{m+1}$).
background
In the Cost module on gauge orbits from real characters, the auxiliary map signedPow is defined by $x\mapsto x,|x|^m$. The doc-comment records the intent: write $\mathrm{sgn}(x),|x|^{m+1}$ as $x,|x|^m$ so multiplicativity is one absolute-value identity away and needs no sign case split.
The surrounding development builds native-cost displays and real-character factorizations on the structural ledger (PRC native cost). Sign-reversing behaviour of those costs is a standing structural requirement: flipping the rational argument must flip the cost value. This lemma isolates the pure algebraic sign flip for the power map itself, before it is packaged into a native-cost predicate.
Upstream, only the definition of the signed power is required; no deeper Recognition forcing (T5–T8) enters at this layer.
proof idea
Term-mode proof in two steps. First simp only [signedPow, abs_neg] unfolds the definition on both sides and rewrites $|-x|$ to $|x|$. The goal becomes $(-x),|x|^m = -(x,|x|^m)$. Then ring closes the rational identity. No induction on $m$ and no case split on the sign of $x$ are needed.
why it matters
Parent use is signedPowerNativeCost_signReversing, which shows that the native cost built from signed powers is sign-reversing in the PRC sense. That proof rewrites both sides to rationals, substitutes the hypothesis $r=-q$, and applies this lemma together with the corresponding sign flip for the J-cost on rationals.
In the Recognition Cost layer, sign-reversing native costs are the gauge-compatible displays that sit under real-character factorization and structural ledger comparisons. The lemma is local algebra, not a forcing-chain step, but it is the exact identity that lets the signed-power family inherit the sign-reversing axiom required of native costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.