signedPowerNativeCost_even_eq_oddPower
plain-language theorem explainer
Even indices of the signed-power native cost agree, on rational displays, with the odd-power generated family. Classification proofs that enlarge the gauge-orbit family from odd powers to all nonnegative exponents cite this containment. The argument is a three-step rewrite through the two toRat lemmas and the even-index identity for signedPow.
Claim. For every $k \in \mathbb{N}$ and every rational orbit $q$, the rational display of the signed-power native cost at even index $2k$ equals the rational display of the odd-power generated native cost at index $k$: $(C^{\mathrm{sgn}}_{2k}(q))^{\mathbb{Q}} = (C^{\mathrm{odd}}_k(q))^{\mathbb{Q}}$.
background
In the PRC ledger, costs are maps on RatioOrbit (integer numerator over nonzero orbit denominator), compared after the verifier display toRat. The signed-power native cost at index $m$ is the cost generated by the sign-extended character $\chi(x)=\mathrm{sgn}(x),|x|^{m+1}$, with a zero branch at the unit orbit. The odd-power generated native cost is the earlier family built from ordinary odd powers $x^{2k+1}$.
The local module builds gauge-orbit candidates from real-character factorizations without an anchor hypothesis. Upstream, signedPow_even states that at an even index the sign-extended power collapses to the ordinary odd power: $\mathrm{signedPow}(2k,x)=x^{2k+1}$. The two toRat lemmas then identify each native-cost constructor with the corresponding $J$-style rational evaluation jq of that power.
proof idea
One-line tactic proof: rewrite the left side by signedPowerNativeCost_toRat, the right side by oddPowerGeneratedNativeCost_toRat, then apply signedPow_even so both sides become jq of the same odd power of q.toRat. No case splits remain after those three rewrites.
why it matters
This is the containment step that lets the signed-power family absorb the older odd-power family. Downstream, GaugeOrbitIsSignedPowerFamily records the proved classification: every anchor-free structural inhabitant is the sign cost (exponent zero) or a signed-power cost at some $m$, and its doc explicitly notes that odd powers are the even indices via this theorem. The narrower claim GaugeOrbitIsSignOrOddPowerFamily (sign or odd power only) is then refuted by exhibiting the exponent-two signed-power member, which is neither sign nor any odd power; the refutation and the corrected classification both depend on knowing how the two families nest. In the Recognition cost story this closes a gauge-orbit gap on the way from structural native-cost hypotheses to a complete discrete family, without touching the T5 $J$-uniqueness or RCL identities directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.