oddPowerGeneratedNativeCost_zero
plain-language theorem explainer
At gauge index zero the odd-power native cost collapses to the ordinary rational J-cost on a ratio orbit. Anyone citing the structural ledger of PRC native costs uses this to pin the canonical member of the odd-power family. The proof rewrites both sides to the rational J-display and simplifies the exponent 2·0+1 to 1.
Claim. For every rational orbit $q$, the native cost generated by the odd power $x\mapsto x^{2k+1}$ at $k=0$ agrees, after transport to $\mathbb{Q}$, with the PRC rational $J$-cost $J(q)=((q+q^{-1})/2)-1$.
background
In the Primitive Recognition Calculus, costs are carried on ratio orbits: integer-numerator / nonzero-denominator displays that transport to $\mathbb{Q}$ by toRat. The PRC rational $J$-cost on such an orbit is $J(q)=((q+q^{-1})/2)-1$, realized as the ratio-orbit object onRatioOrbit and, after transport, as the rational function jq.
The structural ledger packages a one-parameter family of native costs generated by odd powers $q\mapsto q^{2k+1}$. By definition the $k$-th member is the power-generated native cost at exponent $2k+1$; the doc-comment states that $k=0$ is the canonical cost and every $k\ge 1$ is a distinct gauge-orbit point. The companion identity oddPowerGeneratedNativeCost_toRat says the transported value is exactly jq of the odd power of the rational display.
This module sits inside the foundation layer that builds native cost uniqueness and minimality certificates from the Recognition Composition Law and the forced $J$-shape (T5).
proof idea
One short rewrite chain. Apply oddPowerGeneratedNativeCost_toRat at $k=0$ to replace the left-hand side by jq(q.toRat^(2·0+1)). Apply the simp lemma jq_onRatioOrbit to replace the right-hand side by jq(q.toRat). Then norm_num collapses the exponent $2·0+1$ to $1$ and uses $x^1=x$, so both sides are identical.
why it matters
This is the anchor identity that makes the odd-power family a genuine gauge orbit around the answer rather than a swarm of impostor costs. Downstream, cubeGeneratedNativeCost_two_not_canonical invokes the $k=0$ case (via injectivity of the odd-power anchor) to show that the cube-generated cost at the orbit of two is not cross-equal to the canonical onRatioOrbit cost. In the broader Recognition chain this protects the uniqueness of the T5 $J$-cost $J(x)=(x+x^{-1})/2-1$ when native costs are generated by odd powers on ratio orbits, keeping the structural ledger aligned with the forced cost rather than with higher odd-power deformations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.