signedPow_zero_arg
plain-language theorem explainer
At argument zero the signed-power map returns zero for every natural exponent m. Gauge-orbit classification and zero-calibration of signed-power native costs cite this base case. Proof is a one-line simp that unfolds the definition x·|x|^m.
Claim. For every natural number $m$, the signed power $x \mapsto x \cdot |x|^m$ evaluates to $0$ at $x = 0$.
background
In the cost layer, gauge orbits of real characters are classified by comparing native costs on ratio orbits. The auxiliary map signedPow packages a sign-extended monomial: it is defined by $x \cdot |x|^m$, equivalently $\mathrm{sgn}(x)\cdot|x|^{m+1}$. The product form makes multiplicativity a single absolute-value identity, with no sign case split.
The ambient module builds native costs from real-character factorizations and structural ledger data (PRC native cost). Zero calibration of those costs requires knowing how the signed power behaves at the origin, which is the content of this lemma.
proof idea
One-line wrapper: unfold the definition of the signed power and simplify. Substituting $x = 0$ into $x \cdot |x|^m$ immediately yields $0$.
why it matters
This is the origin base case for signed-power native costs. Downstream, signedPowerNativeCost_zero_calibrated uses it to discharge the PRC doubled-trace zero-calibration predicate for every exponent $m$. The gauge-orbit classification theorem nontrivial_is_signedPower identifies the nondegenerate branch with a sign-extended power cost and likewise relies on this evaluation at zero when matching cross-equalities on ratio orbits.
Within Recognition Science cost theory, signed-power costs sit on the J-cost / real-character side of the forcing chain: they supply the concrete orbit representatives against which structural native costs are compared. The lemma is small but closes the zero slot that every such comparison must hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.