signedPowerNativeCost_toRat
plain-language theorem explainer
The rational display of the signed-power native cost on a ratio orbit equals the rational J-cost of the signed power of that orbit's rational value. Anyone checking that sign-extended power characters induce well-defined native costs on RatioOrbit cites this bridge. The proof is a two-branch case split on the unit orbit after unfolding the cost definition.
Claim. For every natural number $m$ and every ratio orbit $q$, the rational display of the signed-power native cost of $q$ equals $J_q\bigl(\mathrm{sgn}(x)\,|x|^{m+1}\bigr)$ where $x$ is the rational display of $q$. Equivalently, $(\mathrm{signed\text{-}power\ cost}_m(q)).\mathrm{toRat} = J_q(x\,|x|^m)$.
background
Ratio orbits are the discrete rational displays of the primitive recognition calculus: an integer numerator over a nonzero distinction denominator, with toRat the verifier map to $\mathbb{Q}$. The zero orbit displays as $0$.
The signed power on rationals is $x\mapsto x,|x|^m$, equivalently $\mathrm{sgn}(x),|x|^{m+1}$, chosen so multiplicativity needs only one absolute-value identity. The signed-power native cost sends a ratio orbit $q$ to the zero orbit when $q$ displays as $1$, and otherwise to the orbit display of that signed power of $q$'s rational value.
The structural ledger supplies $J_q$, the rational J-cost, together with the identity that $J_q$ on an orbit built from a rational recovers $J_q$ of that rational. This lemma is the transport statement that the cost's orbit-level definition agrees with applying $J_q$ after the signed power on the rational display.
proof idea
Unfold the definition of the signed-power native cost, then case on whether $q$'s rational display equals $1$.
Unit case: the cost is the zero orbit, so the left side is $0$ by zero_toRat. The right side is $J_q(\mathrm{signedPow},m,1)$; signedPow_one_arg gives $1$, and norm_num on $J_q$ closes $J_q(1)=0$.
Non-unit case: rewrite with the negative branch of the definition, apply jq_onRatioOrbit (J-cost on an orbit from a rational equals J-cost of that rational), then ratioOrbitOfRat_toRat to cancel the orbit wrapper. Both sides match.
why it matters
This is the basic display identity for the whole signed-power cost family. Downstream, signedPowerNativeCost_base uses it twice to discharge reciprocity in the sans-two-calibration native-cost hypotheses; monotonicity, sign-reversal, zero-calibration, and the even-index recovery of the odd-power family all route through the same toRat equality.
In the classification module, nontrivial_is_signedPower identifies the nondegenerate gauge-orbit branch with a signed-power native cost; the cross-equality proof depends on this transport. Within Recognition cost structure, the family extends the odd-power generators by a sign character while remaining on the rational orbit ledger, feeding the real-character factorization path that organizes admissible native costs before anchor calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.