powerGeneratedNativeCost_not_signReversing
plain-language theorem explainer
Even-power generated native costs fail sign reversal on ratio orbits. Classification of anchor-free structural costs cites this to drop every even exponent from the gauge orbit. The proof assumes sign reversal, evaluates at the anchor pair $2$ and $-2$, uses $(-2)^n=2^n$ for even $n$, and contradicts nonnegativity of the native $J$-display.
Claim. For every even natural number $n$, the native cost $F$ generated by the $n$-th power map on ratio orbits is not sign-reversing: it is not the case that whenever $r$ is the orientation reverse of $q$ (i.e. $r$ displays as $-q$), one has $F(r)=-F(q)-2$ in the doubled-trace display.
background
In the primitive recognition calculus, ratio orbits are discrete imbalance carriers with a verifier display toRat into $\mathbb{Q}$. A native cost is a self-map $F$ of ratio orbits. Sign reversal is the structural condition that orientation flip negates the doubled trace: if $r$ displays as $-q$, then $F(r)$ displays as $-F(q)-2$ (equivalently $T(-q)=-T(q)$ for $T=2(F+1)$).
Power-generated native costs raise the rational display to the $n$-th power and re-embed. The sibling nonnegativity fact jq_nonneg records that the native $J$-display is nonnegative on positive rational displays. The module builds a structural ledger that isolates which ledger fields each candidate family satisfies or fails.
The local setting is the PRC native-cost structural ledger: an anchor-free checklist (including sign reversal) used to stratify candidate costs before uniqueness and gauge-orbit classification.
proof idea
Assume for contradiction that the even-power cost is sign-reversing. Instantiate the universal quantifier at the anchor orbit $2$ and at the orbit of $-2$, using that the latter displays as $-2$. Evenness gives $(-2)^n=2^n$. Transport both sides of the sign-reversal identity through the power-generated display lemmas and the ratio-orbit toRat wrappers; the two power displays collapse, so the identity becomes a numerical relation on the native $J$-display of $2^n$. Positivity of $2^n$ plus jq_nonneg yields a nonnegative value that cannot satisfy the forced linear relation; linarith closes.
why it matters
This is the single-field exclusion that makes even powers fail the anchor-free ledger for exactly one reason: sign reversal. Downstream, evenPowerGeneratedNativeCost_not_sansAnchor applies it at exponent $2k+2$ to show even-power costs miss the full sans-anchor hypothesis bundle. That exclusion feeds structuralStratificationCertificate_holds (positivity, slimness, uniqueness, and gauge inhabitation sides of the certificate).
It also underwrites the corrected open classification GaugeOrbitIsSignOrOddPowerFamily: every anchor-free structural inhabitant is either the zero-exponent sign cost or an odd-power generated cost. In the broader RS forcing picture this is ledger hygiene on the native cost side of the $J$-uniqueness chain (T5), not a spacetime or constants claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.