oddPowerGeneratedNativeCost_toRat
plain-language theorem explainer
On any rational orbit q, the native cost generated by the odd power map t ↦ t^(2k+1) displays as J(q^(2k+1)), where J is the standard cost (t+t⁻¹)/2−1. Anyone comparing gauge-orbit members or proving anchor injectivity of the odd-power family cites this. The proof is a one-line specialization of the general power-generated cost display.
Claim. For every natural number $k$ and every rational orbit $q$, the verifier rational of the native cost generated by the odd power $t\mapsto t^{2k+1}$ equals $J\bigl(q_{\mathbb{Q}}^{2k+1}\bigr)$, where $J(t)=(t+t^{-1})/2-1$ and $q_{\mathbb{Q}}$ is the rational display of $q$.
background
In the Primitive Recognition Calculus structural ledger, native costs on ratio orbits are displayed to ordinary rationals by toRat, which sends a numerator/denominator orbit pair to the corresponding $\mathbb{Q}$ value. The cost functional on rationals is the J-display $J(t)=(t+t^{-1})/2-1$, written jq in the ledger; this is the same J forced unique by the Recognition Composition Law (forcing step T5).
A ratio orbit is an integer numerator over a nonzero distinction-nat denominator. Power-generated native costs apply the map $q\mapsto q^n$ inside the orbit calculus and then take the native cost. The odd-power family is the special case $n=2k+1$: the $k=0$ member is the canonical cost, and each $k\ge 1$ is a distinct gauge-orbit point.
The upstream theorem powerGeneratedNativeCost_toRat already states that the $n$-power generated cost displays as $J(q_{\mathbb{Q}}^n)$ for arbitrary $n$. The odd-power statement is the restriction of that identity to odd exponents.
proof idea
One-line wrapper: instantiate the general power-generated display theorem at the odd exponent $n=2k+1$. Unfolding the definition of the odd-power generator (which is exactly power-generated cost at $2k+1$) makes the goals identical, so no further case analysis is needed here; the zero-at-unit and nonzero branches live in the upstream proof.
why it matters
This identity is the rational display lemma for the entire odd-power gauge family. Downstream it feeds the cube case ($k=1$), the proof that the $k=0$ member recovers the canonical cost, and anchor injectivity: at the orbit $2$ one obtains $J(2^{2k+1})$, and strict increase of $J$ above the unit separates distinct $k$.
In the Cost layer it is the comparison bridge used to show that even signed-power costs recover the odd-power family, that the exponent-one signed power is not any odd-power member, and that the pure sign-gauge cost lies outside the odd-power family. Those separations keep the gauge orbit honest: distinct generators really produce distinct costs rather than impostors of the canonical J-cost.
Framework-wise this sits under T5 J-uniqueness and the structural ledger that certifies which orbit maps still display as the forced cost $J$. It does not itself force $\phi$ or dimension; it only locks the rational shadow of the odd-power generators used in those uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.