canonicalSelectedNativeCost_signReversing
plain-language theorem explainer
The canonical selected native cost obeys sign reversal on ratio orbits: if the display of r is the negative of the display of q, then the cost display of r equals the negated cost of q minus 2. Anyone assembling the structural or sign-reversing native-cost hypothesis bundles cites this. The proof reduces both sides to the rational J-display and finishes by a zero/nonzero case split plus ring algebra.
Claim. Let $F$ be the canonical selected native cost on ratio orbits. Whenever two orbits $q,r$ satisfy $\mathrm{display}(r)=-\mathrm{display}(q)$, one has $\mathrm{display}(F(r))=-\mathrm{display}(F(q))-2$. Equivalently, with $T=2(F+1)$, orientation reversal gives $T(-q)=-T(q)$.
background
In the primitive recognition calculus, ratio orbits carry a rational display toRat (numerator over denominator). The J-display on a rational is $j(t)=(t+t^{-1})/2-1$, the same functional form forced uniquely at T5 of the forcing chain. The canonical selected native cost sends the unit orbit to the zero representative and otherwise applies the on-orbit J map; its display therefore equals $j$ on every orbit (including the unit branch, where both sides are 0).
Sign reversal is the structural axiom that reversing the orientation of a distinction negates the doubled trace: with $T=2(F+1)$, one wants $T(-q)=-T(q)$, written on displays as $F(-q)=-F(q)-2$. The local module packages this as a Prop on maps $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ and then certifies that the canonical selection satisfies it, alongside positivity and monotonicity, as part of the structural ledger.
proof idea
Introduce orbits $q,r$ with $\mathrm{display}(r)=-\mathrm{display}(q)$. Rewrite both cost displays via the identity that the canonical selection displays as $j$ on every orbit. After substituting the hypothesis, it remains to check $j(-t)=-j(t)-2$ for $t=\mathrm{display}(q)$.
Split on whether $t=0$. The zero case is immediate numerical evaluation. On the nonzero branch, unfold $j$, use the inversion identity for negatives, and close by ring.
why it matters
This is one of the two structural axioms discharged for the canonical native cost inside the structural ledger. Downstream it is packed into the non-vacuity witness for the sign-reversing native-cost hypothesis class and into the full structural hypothesis bundle (native + sign-reversing + monotone).
Framework-wise it confirms that the T5 J-cost, once selected and zero-calibrated on ratio orbits, inherits the orientation-reversal law expected of a doubled-trace cost. Without this lemma the structural ledger would be vacuous: one would have the Prop but no concrete $F$ known to satisfy it. It does not itself force uniqueness of $J$; uniqueness lives upstream in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.