oddPowerGeneratedNativeCost_sansAnchor
plain-language theorem explainer
For every natural number k, the native cost generated by the odd exponent 2k+1 meets the structural ledger hypotheses with the two-calibration anchor removed: base axioms without two-calibration, sign-reversal, monotonicity, and zero-calibrated doubled trace. Anyone building the infinite odd-power gauge orbit around the canonical native cost cites this. The proof is a four-field structure pack of the power-generated lemmas at n=2k+1.
Claim. For every natural number $k$, the native cost generated by the odd power $2k+1$ satisfies the structural native-cost hypotheses without the anchor: it obeys the base native-cost axioms without two-calibration, is sign-reversing, is monotone, and has zero-calibrated doubled trace.
background
In the Primitive Recognition Calculus structural ledger, a native cost is a map on ratio orbits that is meant to realize the J-cost (the unique solution of the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). The full structural package usually includes a two-calibration anchor that pins the cost at the orbit of $2$. The structure used here is the same package with that anchor stripped: base native-cost hypotheses without two-calibration, a sign-reversing law, monotonicity, and zero-calibration of the doubled-trace form.
The family under study is the power-generated native costs at odd exponents $n=2k+1$. Oddness matters because sign-reversal on ratio orbits needs an odd generator; the witness $n=2k+1$ is built into the hypotheses. Upstream cost language in the foundation treats recognition cost as J-cost on events and as derived cost of multiplicative recognizers; the ledger here is the structural distillation of those requirements on ratio-orbit maps.
proof idea
Term-mode structure constructor. Each of the four fields is discharged by the corresponding power-generated lemma at exponent $n=2k+1$:
- base without two-calibration from the power-generated base lemma;
- sign-reversing from the power-generated sign-reversing lemma, with oddness witness $\langle k,\mathsf{ring}\rangle$;
- monotone from the power-generated monotone lemma;
- zero-calibrated doubled trace from the power-generated zero-calibration lemma, with $n>0$ by
omega.
No extra algebra: the odd-power specialization is exactly the parameter choice $n=2k+1$.
why it matters
This is the uniform inhabitant theorem for the odd-power family inside the anchor-free structural ledger. Downstream, the cube-generated case is the $k=1$ specialization; the gauge-orbit theorem quotes it for every $k$ and pairs it with anchor separation (distinct odd exponents give distinct costs at the orbit of $2$, via strict increase of $J$ above the unit) to prove the gauge orbit is infinite. The structural stratification certificate then records that the anchor-free uniqueness target is refuted: the ledger is inhabited by a whole gauge family rather than a single map.
In framework terms this sits under native-cost uniqueness and gauge analysis around the forced J-cost (T5), clarifying that odd-power reparameterizations are gauge copies of the answer, not competing impostors. It does not itself force $J$; it populates the structural side of the stratification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.