signedPowerNativeCost_one_not_oddPower
plain-language theorem explainer
The exponent-two sign-extended power cost never agrees, on every ratio orbit, with any odd-power generated native cost. Classification arguments for gauge-orbit candidates of the Recognition cost cite this to exclude the whole odd-power family for the m=1 signed character. The proof specializes the assumed identity at the anchor orbit 2, reduces both sides to rational displays, and obtains the impossible equality 4 = 2^{2k+1}.
Claim. For every $k \in \mathbb{N}$, it is false that for all ratio orbits $q$ the native cost of the sign-extended character $\chi(x)=\mathrm{sgn}(x)\,|x|^2$ is cross-equivalent to the native cost generated by the odd power of exponent $2k+1$ at $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator; two such orbits are cross-equivalent when the signed cross-multiples balance (the internal stand-in for rational equality). The verifier display toRat recovers ordinary rationals, and crossDisp turns cross-equivalence into equality of those displays.
The signed-power native cost of parameter $m$ is the cost map induced by the real character $\chi(x)=\mathrm{sgn}(x),|x|^{m+1}$. For $m=1$ this is the pure quadratic sign-extended character. At the distinguished anchor orbit $2$ it charges the $J$-display of $4$ (i.e. its rational value is $J_q(4)$). Odd-power generated native costs form the competing family indexed by $k$, with rational display $2^{2k+1}$ at the same anchor.
The ambient module studies which real-character factorizations can reproduce the Recognition cost up to gauge. The present statement is a concrete non-identity between two candidate families on that ledger.
proof idea
Assume for contradiction a universal cross-equivalence between the $m=1$ signed-power cost and the odd-power cost of index $k$. Specialize at the anchor orbit $2$ and apply the display lemma crossDisp to obtain equality of rational values. Rewrite via the known evaluations: the left side is $J_q(4)$ and the right side is the odd-power display at $2$. Injectivity of $J_q$ on $[1,\infty)$ then forces the ordinary equality $4=2^{2k+1}$.
Case-split on $k$. If $k=0$ the right side is $2$, contradicting $4=2$. If $k\ge 1$ then $2k+1\ge 3$, so $8\le 2^{2k+1}=4$, again a contradiction. Both branches discharge the assumption.
why it matters
Downstream, GaugeOrbitIsSignOrOddPowerFamily_refuted uses this lemma (together with the companion non-identity against the pure sign gauge) to kill the corrected classification claim that every sans-anchor real-character cost is either the sign cost or some odd-power cost. The exponent-two signed member is a concrete counterexample to that dichotomy.
In the broader Recognition framework this sits inside the cost-uniqueness chain that forces the $J$-cost of T5: only the canonical $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) survives as the composition-law cost. Ruling out entire gauge-orbit families generated by power characters is part of closing off alternative real-character presentations before the forcing chain locks $J$, $\varphi$, the eight-tick period, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.