signedPow_one_arg
plain-language theorem explainer
For every natural number m, the signed power map sends 1 to 1. Anyone reducing native cost on ratio orbits under odd-power gauges cites this base case. The proof is a one-line simp unfolding of the definition signedPow m x = x·|x|^m.
Claim. For every natural number $m$, the signed power $x\mapsto x\,|x|^m$ evaluates to $1$ at $x=1$: $1\cdot|1|^m=1$.
background
In the gauge-orbit cost module, signed powers implement odd integer gauges on rational ratio values without sign case splits. The definition is signedPow m x := x * |x|^m, equivalently $\mathrm{sgn}(x),|x|^{m+1}$. Multiplicativity then follows from a single absolute-value identity.
The surrounding development builds native cost displays on ratio orbits from real-character factorizations of the Recognition cost $J$, so that sign-reversing and power gauges act cleanly on the rational trace. The unit point $x=1$ is the calibrated zero of $J$ and of the native cost, so its image under every gauge must stay fixed.
proof idea
One-line wrapper: unfold signedPow and run simp. After expansion one has $1\cdot|1|^m$, which reduces to $1$ by the usual absolute-value and power simp lemmas.
why it matters
Downstream, signedPowerNativeCost_toRat uses this identity in the branch where the ratio orbit is the unit: after rewriting the native cost definition and discharging q.toRat = 1, the proof rewrites via signedPow_one_arg and normalizes the $J$-cost of $1$ to zero. Without the unit fixed point, the rational-trace comparison between signed-power native cost and $J\circ$ signedPow would fail at the calibrated origin.
In the broader cost story this keeps gauge orbits of the real-character factorization anchored at the Recognition zero, consistent with $J(1)=0$ from T5 uniqueness of the cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.