signedPow_mul
plain-language theorem explainer
Multiplicativity of the signed power map on rationals: for natural m and rationals x,y, the signed power of a product equals the product of the signed powers. Cost-gauge and native-cost constructions cite this when pushing products through the signed-power display. The proof unfolds the definition, applies absolute-value multiplicativity and power laws, then closes by ring arithmetic.
Claim. For every natural number $m$ and rationals $x,y$, $$xy\cdot|xy|^m=(x\cdot|x|^m)(y\cdot|y|^m).$$ Equivalently, writing the map as $\mathrm{sgn}(z)\,|z|^{m+1}$, the identity is $\mathrm{sgn}(xy)\,|xy|^{m+1}=(\mathrm{sgn}(x)\,|x|^{m+1})(\mathrm{sgn}(y)\,|y|^{m+1})$.
background
In this module the signed power is defined by $\mathrm{signedPow},m,x:=x\cdot|x|^m$. That form is deliberately $x$ times a nonnegative power of the absolute value, so it equals $\mathrm{sgn}(x),|x|^{m+1}$ without a separate sign case split. The definition's doc-comment states that multiplicativity is then one absolute-value product identity away.
The surrounding development builds gauge-orbit and native-cost displays from real-character factorizations of structural PRC cost. Signed powers appear as the algebraic skeleton of those displays on rational ratio orbits: they carry both magnitude (via $|x|^m$) and orientation (via the leading factor of $x$).
Upstream, the absolute-value multiplicativity lemma on signed orbits (and its rational counterpart used here) supplies $|xy|=|x|,|y|$. Together with the usual power law $(ab)^m=a^m b^m$, that is the only nontrivial input.
proof idea
Term-mode proof in two steps. First simp only unfolds the definition of signed power on both sides and rewrites with absolute-value multiplicativity and the power-of-a-product law, yielding an equality of rational polynomials in $x$, $y$, $|x|$, and $|y|$. Then ring discharges the remaining commutative-ring identity. No case analysis on signs is required, which is exactly why the definition was written as $x\cdot|x|^m$ rather than an explicit sign times a power.
why it matters
This is the product half of the signed-power homomorphism used throughout the gauge-orbit cost layer. Downstream, division multiplicativity is obtained in one rewrite by expressing division as multiplication by the inverse and invoking this lemma together with the inverse law. The same identity is applied inside the base native-cost hypotheses for the signed-power cost family: reciprocal and cross-equality obligations reduce to rational identities on signed powers, and products of ratio-orbit values must pass through this map cleanly.
In the broader Recognition cost story, native cost on ratio orbits must respect the multiplicative structure of the orbit group while remaining compatible with the J-cost / real-character factorization. Signed powers give a concrete rational model of that structure; without multiplicativity, the signed-power native-cost candidate could not inherit the reciprocal and calibration hypotheses required of a PRC native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.