oddPowerGeneratedNativeCost
plain-language theorem explainer
Defines the native cost obtained by raising a rational orbit to an odd power 2k+1. The case k=0 recovers the canonical cost; each k≥1 is a distinct gauge-orbit point. Cost and gauge-orbit work cites it as the odd-power family. The body is a one-line specialization of the general power-generated cost to odd exponents.
Claim. For each natural number $k$, the map sending a rational orbit $q$ to the native cost generated by $q \mapsto q^{2k+1}$. Equivalently, it is the power-generated native cost at exponent $2k+1$.
background
In the primitive recognition calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Native costs act on these orbits and are compared via cross-equality of displays.
The general power-generated native cost sends $q$ to the orbit of $q^n$ (or zero when $q=1$). Odd exponents are singled out because parity controls gauge-orbit membership: even powers collapse into the odd family under signed-power identification, while the pure sign gauge sits outside every positive odd power.
This module builds the structural ledger of PRC-native costs: which maps arise from characters, which are minimal, and how the gauge orbit is parametrized. The odd-power family is the main discrete spine of that orbit.
proof idea
One-line definitional wrapper: apply the general power-generated native cost at the odd exponent $n = 2k+1$. No further proof obligations; the specialization inherits the closed-form and nonnegativity properties already proved for arbitrary powers.
why it matters
This is the standard parametrization of the odd-power branch of the gauge orbit. Downstream, the cube cost is exactly the $k=1$ member, and injectivity at the anchor separates it from the canonical $k=0$ cost. Classification results state that every anchor-free structural inhabitant is either the sign gauge or some odd-power generated cost (open corrected form: sign-or-odd-power family). Comparison lemmas show the pure sign cost is never an odd-power cost, and even signed powers recover this family. In the Recognition forcing picture this sits under native $J$-cost uniqueness (T5) and the structural ledger that feeds uniqueness and minimality certificates for the canonical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.