PRCNativeCostSignReversing
plain-language theorem explainer
Predicate on maps F from rational orbits to rational orbits: if r displays as the sign flip of q, then F(r) displays as -F(q)-2. Equivalent to oddness of the doubled trace T=2(F+1). Cited when packing structural native-cost hypotheses and when excluding absolute-value generators. Pure Prop definition; no proof content.
Claim. A map $F$ sending rational orbits to rational orbits is sign-reversing when, for all orbits $q,r$ with rational display $r=-q$, the display of $F(r)$ equals $-F(q)-2$. Equivalently, the doubled trace $T=2(F+1)$ satisfies $T(-q)=-T(q)$.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator. The verifier map toRat sends such an orbit to $\mathbb{Q}$ by ordinary division; it is a transport wrapper whose internal equality is cross-multiplication.
Native cost candidates are maps $F$ on these orbits. The doubled trace is $T=2(F+1)$; the classical J-cost sits one step below that normalization. Sign reversal of a distinction is the orientation flip $q\mapsto -q$ on displays. The doc-comment states the intended law as $T(-q)=-T(q)$, rewritten on $F$ as $F(-q)=-F(q)-2$.
This module sits in the structural ledger for PRC native cost: it records which algebraic properties a candidate cost must obey before uniqueness and minimality certificates apply. Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) all live on the same J-family; the present predicate is the discrete orbit-level form of oddness under orientation flip.
proof idea
Definitional: the body is the 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 proofs discharge it by rewriting the candidate's toRat formula, substituting the hypothesis $r=-q$, and applying the corresponding sign law on the generating character (e.g. jq_neg, signedPow_neg).
why it matters
Sign reversal is one of the four fields in the anchor-free structural pack (SansAnchorHypotheses): base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. That pack is the hypothesis interface for real-character factorization of native cost without fixing an anchor.
Inside this ledger it is load-bearing as an exclusion filter. The absolute-value generated cost fails it on the pair (one, negative-one), so it is ruled out with no reference to the canonical cost's values. Conversely, the canonical selected cost and the signed-power / sign-gauge generators are proved to satisfy it, feeding gauge-orbit constructions in GaugeOrbitFromRealCharacter.
In the broader RS chain this is the discrete shadow of J-oddness under $x\mapsto 1/x$ and orientation flip, consistent with T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. It does not itself force $\phi$ or the eight-tick octave; it only constrains the cost display's parity under sign change.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.