PRCNativeCostSignReversing
plain-language theorem explainer
Sign-reversal property for a native cost map F on rational orbits: if r displays as −q then F(r) displays as −F(q)−2. Equivalent to the doubled trace T=2(F+1) being odd under orientation flip. Structural-ledger and uniqueness arguments cite it to keep signed costs and exclude absolute-value or even-power generators. Pure Prop definition; no proof obligations.
Claim. A map $F$ from rational orbits to rational orbits is sign-reversing when, for all orbits $q,r$ with rational display $r=-q$, the display of the image satisfies $F(r)=-F(q)-2$. (Equivalently, the doubled trace $T=2(F+1)$ obeys $T(-q)=-T(q)$.)
background
In the Primitive Recognition Calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator, with verifier display toRat sending the orbit to $\mathbb{Q}$ by ordinary division. Native cost candidates are endomorphisms $F$ of that orbit type; their displays are compared after transport to rationals.
The doubled trace is $T=2(F+1)$. Sign reversal of a distinction should negate $T$, i.e. $T(-q)=-T(q)$. Expanding gives the display law $F(-q)=-F(q)-2$ used here. The module Cost.RealCharacterFactorization packages this (with monotonicity, base-sans-two, and zero-calibration) into anchor-free hypothesis packs for real-character factorizations of native cost.
Upstream, the same Prop is named in PRCNativeCostStructuralLedger, where the doc states: "Reversing the orientation of a distinction negates its doubled trace... written on displays as $F(-q)=-F(q)-2$."
proof idea
Definition only: the body is the universal Prop
$\forall q,r,; r.\mathrm{toRat}=-q.\mathrm{toRat}\Rightarrow (F r).\mathrm{toRat}=-(F q).\mathrm{toRat}-2$.
No tactics, no lemmas. Downstream theorems discharge or refute the Prop by rewriting the concrete cost's toRat formula and using rational arithmetic (e.g. signedPow_neg, trichotomy on the sign of $q$).
why it matters
This is one of the four fields of SansAnchorHypotheses, the anchor-free pack that real-character factorizations must satisfy. Downstream it is proved for the canonical selected native cost, for sign-gauge native cost, and for signed-power native costs; it is refuted for absolute-value generated cost and for even power-generated costs.
The absolute-value failure is load-bearing: the ledger doc calls it "the round-3 witness that the signed-unit field was load bearing; it is excluded by sign reversal directly, with no reference to the canonical cost's value." Even powers fail because they cannot distinguish $-q$ from $q$, forcing a constant $-1$ cost that contradicts the anchor. Together these pin the signed, odd character of the unique native cost that later feeds J-uniqueness (T5) and the Recognition Composition Law on the real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.