signedPow
plain-language theorem explainer
Defines the sign-extended power map on rationals: x·|x|^m, equal to sgn(x)·|x|^(m+1). The packaging avoids sign case splits so multiplicativity is one abs_mul step. Downstream gauge-orbit work builds native costs and the nondegenerate classification branch from this character.
Claim. For $m\in\mathbb{N}$ and $x\in\mathbb{Q}$, set $\mathrm{signedPow}(m,x):=x\cdot|x|^m$. Equivalently $\mathrm{signedPow}(m,x)=\mathrm{sgn}(x)\cdot|x|^{m+1}$.
background
This module classifies anchor-free structural native costs on ratio orbits by real-character factorization. A native cost is a map on ratio orbits obeying the structural ledger axioms (without an anchor calibration). Real characters on the multiplicative group supply candidate generators for those costs.
The sign-extended power $\chi_m(x)=\mathrm{sgn}(x)\cdot|x|^{m+1}$ is the basic nontrivial real character used here. Writing it as $x\cdot|x|^m$ keeps the formula multiplicative without case analysis on the sign of $x$: the identity $|xy|=|x||y|$ does the work.
Sibling constructions include the pure sign gauge cost and the odd-power generated family. The open classification goal is that every anchor-free structural inhabitant is either the zero-exponent sign cost or an odd-power generated cost.
proof idea
One-line definitional abbreviation: the body is the term $x\cdot|x|^m$. No tactics or lemmas. The doc-comment records the intended identity with $\mathrm{sgn}(x)\cdot|x|^{m+1}$, which follows from $x=\mathrm{sgn}(x)\cdot|x|$ on nonzero rationals (and holds at zero by direct check).
why it matters
This is the algebraic generator for the nondegenerate branch of the gauge-orbit classification. signedPowerNativeCost builds the native cost by applying the map on the rational representative of a ratio orbit (with the unit orbit sent to zero). That cost is the target of nontrivial_is_signedPower, which states that under SansAnchor hypotheses and a nontrivial rational trace at 2, a character that is a pure power on naturals matches the signed-power native cost on every ratio orbit.
Algebraic lemmas (signedPow_div, signedPow_inv, signedPow_even, and the toRat bridge) feed those comparisons. The open proposition GaugeOrbitIsSignOrOddPowerFamily packages the corrected classification: every anchor-free structural inhabitant is either the sign gauge cost or an odd-power generated cost. In the Recognition cost layer this pins which real characters can appear as structural native costs once the anchor is dropped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.