powerGeneratedNativeCost_signReversing
plain-language theorem explainer
For every odd natural number n, the native recognition cost generated by the power map q ↦ q^n reverses orientation: if r is the sign-flipped orbit of q, the cost of r equals the negated cost of q minus 2. Structural ledger proofs cite this when assembling sans-anchor hypotheses for odd-power costs. The argument is a short rewrite chain: odd powers preserve negation, and the base jq cost is itself sign-reversing.
Claim. If $n$ is an odd natural number, then the native cost $F$ generated by the power map $q \mapsto q^n$ is sign-reversing: whenever two ratio orbits satisfy $r=-q$ as rationals, one has $F(r)=-F(q)-2$ as rationals.
background
In the Primitive Recognition Calculus, native costs are maps on ratio orbits. Sign reversal is the structural property that flipping the orientation of a distinction negates the doubled trace: with $T=2(F+1)$, one has $T(-q)=-T(q)$, written on displays as $F(-q)=-F(q)-2$.
The power-generated native cost at exponent $n$ is the cost obtained by sending each orbit through $q\mapsto q^n$ and then applying the base jq cost. Odd exponents are special because $(-q)^n=-q^n$, so the sign of the ratio is remembered; even exponents forget it. The surrounding module builds a structural ledger of which native costs satisfy the PRC hypotheses (base behaviour, sign-reversing, monotone) without an anchor point.
Upstream, the same sign-reversing predicate appears in the real-character factorization layer as the orientation axiom on native costs.
proof idea
Short tactic proof. Introduce ratio orbits $q,r$ with $r$ the rational negation of $q$. Rewrite both sides of the goal by the evaluation lemma that reduces power-generated native cost to jq on the powered rational; substitute the negation hypothesis; apply the elementary identity that an odd power of a negative equals the negative of the power; finish with the base sign-reversal identity for jq. No case splits or induction.
why it matters
Discharges the sign-reversing field of the sans-anchor structural hypotheses for every odd-power native cost. Downstream, that package (base, sign-reversing, monotone) is assembled for $q\mapsto q^{2k+1}$ and feeds the structural stratification certificate, which records uniqueness, slim contraction, positivity, and gauge inhabitation for the PRC native-cost ledger.
In Recognition Science this is ledger infrastructure rather than a T0–T8 forcing step: it certifies that odd-power points of the gauge orbit remain orientation-reversing costs, with $k=0$ recovering the canonical cost and $k\ge 1$ giving distinct orbit points. Without it, the sans-anchor uniqueness target could not be stated for the odd-power family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.