signedPowerNativeCost_base
plain-language theorem explainer
For every natural number m, the native cost built from the sign-extended power character χ(x)=sgn(x)|x|^(m+1) satisfies the four base PRC native-cost axioms that omit two-calibration: reciprocity, normalized invariance, the canonical Recognition Composition Law, and unit-zero. Anyone assembling the anchor-free structural ledger for power characters cites this. The proof reduces each field to the rational J-cost via toRat, then applies signed-power multiplicative identities and the known J identities.
Claim. For every $m\in\mathbb{N}$, the map $C_m$ on ratio orbits induced by the sign-extended power $\chi(x)=\mathrm{sgn}(x)\,|x|^{m+1}$ (sending the unit orbit to zero cost, and otherwise pushing the orbit of $\chi(q)$ through the rational $J$-cost) satisfies: (i) $C_m(q^{-1})=C_m(q)$ after cross-equality; (ii) $C_m$ is invariant under ratio normalization; (iii) the canonical RCL identity $C_m(xy)+C_m(x/y)=2C_m(x)C_m(y)+2C_m(x)+2C_m(y)$ on nonzero orbits; (iv) $C_m(1)=0$.
background
The module builds gauge-orbit native costs from real characters on ratio orbits. A ratio orbit is an equivalence class of nonzero rationals under the ledger's cross-equality; toRat picks a canonical representative. The signed power signedPow m x := sgn(x)·|x|^(m+1) is a group homomorphism on $\mathbb{Q}^\times$ (multiplicative, preserves inverses and quotients).
The associated native cost signedPowerNativeCost m sends the unit orbit to zero and otherwise applies the rational $J$-cost jq to the signed power of the representative, then re-embeds as an orbit. The target interface PRCNativeCostHypothesesSansTwoCalibration packages the structural ledger axioms that do not yet demand the two-calibration (the special value at the orbit of 2): reciprocity under inversion, invariance under distinction-normalization, the canonical Recognition Composition Law on the orbit algebra, and vanishing at the unit.
Upstream, signedPowerNativeCost_toRat identifies the cost's rational value with jq(signedPow m q.toRat), and the signed-power lemmas signedPow_mul, signedPow_inv, signedPow_div supply the character identities needed to transport RCL and reciprocity from jq.
proof idea
Four structure-field tactics, each reducing through RatioOrbit.crossEq_iff_toRat_eq and signedPowerNativeCost_toRat.
- reciprocal: rewrite both sides to
jq, applyRatioOrbit.recip_toRatandsignedPow_inv, finish withjq_inv. - normalized_invariant: same toRat reduction, then
DistinctionNat.normalizeRatio_toRat(normalization does not change the rational value, so the cost is unchanged). - canonical_rcl: expand orbit addition/multiplication/division and the constant two via their toRat lemmas; rewrite with
signedPow_mulandsignedPow_div; discharge byjq_rclat the nonzero signed powers (signedPow_ne_zero). - unit_zero: unfold the definition and take the
if_posbranch atRatioOrbit.one_toRat.
why it matters
This is the base block of the power-character ledger. Downstream, signedPowerNativeCost_sansAnchor assembles it with sign-reversal, monotonicity, and zero-calibration to conclude that every nonnegative integer exponent inhabits the full anchor-free structural native-cost interface: "The sign-extended power character satisfies every structural field, including orientation reversal, at every index and so at both parities of exponent."
In the Recognition framework the native cost is the discrete avatar of the unique $J$-cost forced by T5 ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Showing that the entire one-parameter family of sign-extended powers satisfies the base axioms (before two-calibration and anchoring) supplies an infinite supply of concrete ledger realizations compatible with RCL, which later feed gauge-orbit and real-character factorization arguments in the cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.