signedPowerNativeCost_sansAnchor
plain-language theorem explainer
For every natural number m, the native cost from the sign-extended power character χ(x)=sgn(x)|x|^(m+1) meets the full anchor-free structural ledger: reciprocity without two-calibration, orientation reversal, monotonicity, and zero calibration. Classification theorems and uniqueness refutations cite this packing to admit every nonnegative integer exponent. The proof is a four-field structure instance wiring existing field lemmas.
Claim. For every $m\in\mathbb{N}$, the native cost generated by the sign-extended power character $\chi(x)=\mathrm{sgn}(x)\,|x|^{m+1}$ satisfies the anchor-free structural native-cost hypotheses: base reciprocity without two-calibration, sign-reversal under orientation flip, monotonicity on the positive ray, and zero calibration at the unit orbit.
background
In the Primitive Recognition Calculus ledger, a native cost on ratio orbits is a map $F$ that turns each orbit into another orbit and is judged by structural fields rather than by an a-priori $J$-formula. The anchor-free package drops the two-calibration (unit-gauge) field and retains reciprocity without that calibration, sign-reversal, monotonicity, and zero calibration at the unit.
The sign-extended power character is $\chi(x)=\mathrm{sgn}(x),|x|^{m+1}$. Its induced native cost sends the unit orbit to zero and otherwise pushes the rational representative through the signed power map. Sibling lemmas already establish each structural field separately: base reciprocity without two-calibration, sign-reversal via $\mathrm{signedPow}(-q)=-\mathrm{signedPow}(q)$, monotonicity on orbits with rational representative at least one, and zero calibration.
The local module builds the gauge orbit of real characters and asks which of those characters produce full structural inhabitants. This declaration is the packing step that puts every nonnegative integer exponent onto the anchor-free ledger.
proof idea
Term-mode structure instance. The goal type is the anchor-free structural hypothesis bundle applied to the signed-power native cost at index $m$. Each field is discharged by the corresponding already-proved lemma at the same $m$: base without two-calibration, sign-reversing, monotone, and zero-calibrated. No new algebra is done here; the declaration only assembles the four field proofs into one inhabitant certificate.
why it matters
This is the membership certificate that lets every nonnegative integer exponent sit inside the anchor-free structural class. Downstream, the gauge-orbit classification states that every anchor-free structural inhabitant is either the pure sign cost or some signed-power cost at an index $m$; the proof of that classification (under the six-exponentials trace input) needs exactly this packing. The same certificate refutes the narrower claim that only the sign cost and odd powers appear: the $m=1$ (exponent-two) member is structural yet neither sign nor odd power.
It also feeds the ledger-level uniqueness refutation: the anchor-free structural package does not force the canonical cost, so the missing anchor field is a genuine unit-gauge choice rather than redundant structure. Minimality arguments that isolate the canonical member among odd-power costs likewise rely on having the full signed-power family available as structural competitors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.