signReversing_forces_signed_unit
plain-language theorem explainer
If a native cost map sends the unit orbit to zero and obeys ledger sign-reversal, it is automatically signed-unit calibrated. Round-4 uniqueness proofs cite this to drop signed-unit as an independent axiom. The argument evaluates antisymmetry at the unit against its negative and finishes by rational-display arithmetic.
Claim. Let $F$ send ratio orbits to ratio orbits. Suppose $F(1)=0$ and $F$ is sign-reversing: whenever the rational display of $r$ equals the negation of that of $q$, one has $(F r)^{\mathrm{rat}}=-(F q)^{\mathrm{rat}}-2$. Then $F$ is signed-unit calibrated (the former independent calibration at the negative unit follows).
background
Ratio orbits are integer-numerator / nonzero-denominator displays of rational distinctions, with verifier map toRat. Cross-equality of two orbits is equivalent to equality of their rational displays (crossEq_iff_toRat_eq).
Sign reversal is the ledger antisymmetry axiom: if $r^{\mathrm{rat}}=-q^{\mathrm{rat}}$, then $(F r)^{\mathrm{rat}}=-(F q)^{\mathrm{rat}}-2$. Equivalently, with doubled trace $T=2(F+1)$, one has $T(-q)=-T(q)$. The module builds structural ledgers for the PRC native cost; round 4 replaces the older signed-unit calibration by this intrinsic antisymmetry.
The unit and zero orbits display as $1$ and $0$. The negative-unit orbit displays as $-1$. Signed-unit calibration is the residual condition that pins $F$ at that negative unit; the claim is that unit-normalization plus sign reversal already force it.
proof idea
First record that the negative-unit orbit displays as $-1$, matching the negation of the unit display. Instantiate the sign-reversal hypothesis at the pair (unit, negative unit). Unfold signed-unit calibration, transport via crossEq_iff_toRat_eq and the orbit-level $J$-display jq_onRatioOrbit, substitute the unit-normalization $F(1)=0$, and finish with norm_num on the rational $J$-cost at $-1$. The computation yields the required calibration identity.
why it matters
Doc-comment thesis: the signed-unit field is not an assumption; ledger antisymmetry at the unit produces it. Downstream, signReversing_class_forces_slim uses this to prove the round-4 class and the round-2 slim ledger carve out the same costs, so sign reversal is a strictly better-behaved stand-in, not a weakening. That feeds the round-4 terminal PRCSignReversingNativeCostUniquenessTarget_proved (sign-reversing ledger forces the canonical cost) and, through the structural ladder, structural_forces_slim and the round-5 terminal uniqueness theorem. In the broader RS chain this is bookkeeping on the native $J$-cost side of T5 uniqueness, clearing an axiom that looked independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.