PRCSignReversingNativeCostHypotheses
plain-language theorem explainer
Packages the round-4 native-cost hypothesis class on a map F from rational orbits to orbits: strengthened base axioms (RCL, normalization, prime-pair product calibration), intrinsic sign reversal F(-q)=-F(q)-2, and zero-orbit calibration of the doubled trace. Cited by the uniqueness target and by the equivalence proof that this class matches the slim signed ledger. Pure structure definition, no proof body.
Claim. A predicate on maps $F$ from rational orbits to rational orbits asserting three properties: (i) $F$ satisfies the strengthened native-cost interface (base Recognition Composition Law, normalization, and prime-pair product calibration at cost level); (ii) sign reversal: whenever $r$ displays $-q$, one has $F(r)=-F(q)-2$ (equivalently the doubled trace $T=2(F+1)$ obeys $T(-q)=-T(q)$); (iii) the doubled trace is zero-calibrated, $T(0)=0$.
background
In the Primitive Recognition Calculus, costs are maps $F$ on RatioOrbit displays (signed numerator over nonzero orbit denominator). The native doubled trace is $T_F(q)=2(F(q)+1)$; for character-generated costs this equals $\chi(q)+\chi(q)^{-1}$.
The strengthened interface keeps the older RCL/normalization/calibration package and adds prime-pair product calibration after the two-adic no-go. Sign reversal is the intrinsic antisymmetry: reversing orientation of a distinction negates the doubled trace, written on displays as $F(-q)=-F(q)-2$. Zero calibration fixes the free value $T(0)$ that the nonzero d'Alembert law cannot constrain, requiring $T(0)=0$.
This module's structural ledger organizes successive hypothesis classes (slim, signed-strengthened, sign-reversing). Round 4 drops signed-unit calibration in favor of the antisymmetry axiom plus the zero orbit.
proof idea
No proof: this is a Prop-valued structure bundling three named fields. Inhabitants are built by supplying a strengthened package, a proof of sign reversal on opposite rational displays, and zero-calibration of nativeCostDoubledTrace F. Downstream theorems assemble those fields componentwise (e.g. from the canonical selected cost).
why it matters
Defines the round-4 uniqueness class used by PRCSignReversingNativeCostUniquenessTarget: every $F$ in the class must agree with the canonical on-orbit cost. Non-vacuity is recorded by canonicalSelectedNativeCost_signReversing_hypotheses. The exchange theorem signReversing_class_forces_slim shows the class is equivalent to the round-2 slim ledger, so sign reversal is a cleaner stand-in for signed-unit calibration, not a weakening.
In the broader forcing chain this sits inside the native-cost uniqueness route toward the J-cost $J(x)=(x+x^{-1})/2-1$ (T5) and the Recognition Composition Law, before $\varphi$ and the eight-tick structure are forced. It closes a ledger design choice: antisymmetry plus zero orbit replace an extrinsic unit calibration while preserving the same cost class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.