signedPow_ne_zero
plain-language theorem explainer
For any natural m and nonzero rational x, the signed power x·|x|^m is nonzero. Gauge-orbit and native-cost constructions cite this to keep signed-power displays off the zero locus. The argument is a one-line wrapper: absolute value preserves nonzeroness, powers of nonzero rationals stay nonzero, and the product is nonzero.
Claim. For every $m \in \mathbb{N}$ and every $x \in \mathbb{Q}$ with $x \neq 0$, one has $x \cdot |x|^m \neq 0$.
background
In the cost module that builds gauge orbits from real characters, the signed power is the display map $\mathrm{signedPow}, m, x := x \cdot |x|^m$ (equivalently $\mathrm{sgn}(x)\cdot|x|^{m+1}$). The product form is chosen so multiplicativity is one absolute-value identity away and needs no sign case split.
Native-cost hypotheses on ratio orbits require the display never hit zero on nonzero rationals: zero would collapse the orbit arithmetic and break reciprocal and calibration identities. The local setting is the structural ledger for PRC native cost without the two-calibration clause, imported alongside real-character factorization.
Upstream, product nonzeroness (orbit form K4.7, and the field form used here) guarantees that nonzero factors stay nonzero under multiplication; absolute-value and power lemmas supply the second factor.
proof idea
One-line wrapper. From $x \neq 0$ deduce $|x| \neq 0$, hence $|x|^m \neq 0$ by the standard power-nonzero lemma. Apply product nonzeroness to the two factors $x$ and $|x|^m$ in the definition of the signed power. No case analysis on the sign of $x$.
why it matters
Feeds signedPowerNativeCost_base, which installs the PRC native-cost hypotheses (sans two-calibration) on the signed-power native cost of order $m$. That base is the bridge from real-character factorization of the J-cost to a gauge-orbit display that stays reciprocal and off zero.
In the Recognition framework this sits in the Cost layer supporting the real-character route to native cost structure: J-uniqueness (T5) and the Recognition Composition Law force the cost shape; signed powers give concrete orbit representatives once the character is fixed. Without nonzeroness, the reciprocal identity used downstream (signedPow_inv in the reciprocal clause) would be undefined on the zero locus.
No open scaffold: the claim is fully proved and only discharges a side condition for the native-cost package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.