signedPowerNativeCost
plain-language theorem explainer
The signed-power native cost of order m is the PRC J-cost of the character χ(x)=sgn(x)·|x|^(m+1) on ratio orbits. Gauge-orbit classification cites it as the nondegenerate branch of every anchor-free structural native cost. The body is a three-line case split: the zero orbit at the unit, otherwise J composed with the signed power of the rational display.
Claim. For each $m\in\mathbb{N}$ and ratio orbit $q$, the signed-power native cost returns the zero orbit when $q$ displays as the rational $1$, and otherwise returns the ratio-orbit J-cost $J(\chi_m(q))$, where $\chi_m(x)=\mathrm{sgn}(x)\,|x|^{m+1}$ (equivalently $x\,|x|^m$).
background
Ratio orbits are the PRC display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator, with toRat the verifier map to $\mathbb{Q}$. The native cost object on that display is the ratio-orbit J-cost $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit; it is the discrete stand-in for the unique continuous cost forced by the Recognition Composition Law (T5).
The character feeding that cost is the sign-extended power signedPow m x = x·|x|^m, i.e. $\mathrm{sgn}(x),|x|^{m+1}$. Multiplicativity is then one absolute-value identity away, with no sign case split. The inverse section ratioOrbitOfRat lifts a classical rational back into a ratio orbit so the character can be tested inside the PRC ledger.
This module builds candidate native costs from real-character factorizations and checks which ones satisfy the structural (anchor-free) native-cost hypotheses. The signed-power family is the main nondegenerate candidate beside the pure sign gauge.
proof idea
Definition by cases on the rational display. If $q$ maps to $1$, return the zero ratio orbit (so $J(1)=0$ is hard-wired). Otherwise evaluate signedPow m on q.toRat, re-embed via ratioOrbitOfRat, and apply onRatioOrbit. No lemmas are invoked; the body is pure composition of those four primitives.
why it matters
This is the concrete family that the gauge-orbit classification lands on. Downstream, GaugeOrbitIsSignedPowerFamily asserts that every anchor-free structural native cost is either the sign gauge or some signedPowerNativeCost m. The classification theorem nontrivial_is_signedPower identifies the nondegenerate branch with this family once the rational trace at 2 is not 2 and the character values on naturals are pure powers.
Even indices recover the older odd-power family (signedPowerNativeCost_even_eq_oddPower), so the signed-power family strictly contains it. That containment is what refutes the narrower "sign or odd power" claim: the exponent-two member is neither the sign cost nor any odd power (GaugeOrbitIsSignOrOddPowerFamily_refuted). Base structural lemmas (signedPowerNativeCost_base, monotonicity, calibration failures at the unit) all quantify over this definition.
In the forcing chain this sits under T5 (J-uniqueness): once J is fixed, the remaining freedom in structural native costs is exactly which real character feeds it, and the signed powers are the surviving discrete family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.