signedPowerNativeCost_one_two_toRat
plain-language theorem explainer
The signed-power native cost with parameter m=1, at the ratio orbit 2, displays as the rational J-cost of 4. Anyone separating the quadratic signed-power character from odd-power or sign-gauge costs cites this anchor evaluation. The proof rewrites through the general display lemma and reduces signedPow at 2 by arithmetic.
Claim. Let $\chi(x)=\mathrm{sgn}(x)\,|x|^2$ be the sign-extended power character with exponent parameter $m=1$. The native cost it generates, evaluated at the ratio orbit $2$, has rational display equal to $J_q(4)$.
background
In this module, native costs are built from real characters on ratio orbits. The signed power map is $\mathrm{signedPow}(m,x)=x,|x|^m$, equivalently $\mathrm{sgn}(x),|x|^{m+1}$, chosen so multiplicativity needs only one absolute-value identity and no sign cases. The associated native cost sends a ratio orbit $q$ to zero when $q$ displays as $1$, and otherwise to the orbit of that signed power of the display.
The anchor point here is the ratio orbit $\mathrm{two}$, whose rational display is $2$. The structural ledger supplies $J_q$, the rational J-cost used as the verifier display of a cost orbit. Upstream, the general display theorem states that the signed-power native cost at any $q$ displays as $J_q$ of the signed power of $q$'s rational value.
Locally the goal is a concrete calibration: the $m=1$ (quadratic) member of the signed-power family, evaluated at $2$, must charge $J(4)$ so later non-identity arguments can compare displays at a single point.
proof idea
Term-mode proof in two steps. First rewrite by the general display lemma for signed-power native cost, which reduces the left-hand side to $J_q(\mathrm{signedPow},1,\mathrm{two.toRat})$, and by the simp fact that $\mathrm{two}$ displays as $2$. Then norm_num on the definition $\mathrm{signedPow},m,x=x,|x|^m$ evaluates $2\cdot|2|^1=4$, yielding $J_q(4)$.
why it matters
This is the concrete anchor evaluation that powers two separation theorems in the same module: the $m=1$ signed-power cost is not identically the odd-power generated native cost for any $k$, and it is not identically the sign-gauge native cost. Both proofs assume pointwise cross-equality, specialize to the orbit $2$, and compare rational displays; the left display is exactly this lemma's $J_q(4)$.
In the Recognition cost layer, distinct real characters must induce distinct native costs on ratio orbits before gauge-orbit classification can proceed. The evaluation sits under the J-cost infrastructure (T5 uniqueness of $J$) and the structural ledger that transports costs to rationals. It does not itself force uniqueness of $J$, but it supplies the numerical witness used to keep the signed-power family off the odd-power and sign-gauge orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.