signReversing_class_forces_slim
plain-language theorem explainer
Sign-reversing native-cost hypotheses on a ratio-orbit map F already imply the zero-calibrated signed strengthened package (the slim ledger). Anyone comparing round-4 antisymmetry axioms with round-2 signed-unit calibration cites this equivalence direction. The proof is a structure assembly: copy strengthened and zero-calibration, and obtain the signed unit from the dedicated forcing lemma.
Claim. Let $F$ map ratio orbits to ratio orbits. If $F$ satisfies the strengthened native-cost package, the intrinsic sign-reversal axiom, and zero-calibration of the doubled-trace cost, then $F$ satisfies the zero-calibrated signed strengthened native-cost hypotheses: the same strengthened base, a signed unit at the identity orbit, and the same zero calibration.
background
In the primitive recognition calculus, native costs on ratio orbits are constrained by successive hypothesis packages. The strengthened native-cost package is the base layer. The round-2 slim ledger adds a signed-unit calibration (the cost distinguishes the unit orbit with a fixed sign) together with zero-calibration of the doubled-trace cost.
The round-4 class replaces that signed-unit field by an intrinsic sign-reversal axiom: the cost flips sign under orbit inversion, while keeping the strengthened base and zero-calibration. The module treats these as competing presentations of the same cost class on ratio orbits, not as unrelated axiom lists.
Upstream, recognition costs are J-type costs on ratios (observer forcing, multiplicative recognizers, rung coarsening). Here the object is structural: which Prop-packages on $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ carve out the same native costs.
proof idea
Term-mode structure construction, not a tactic script. The target package has two fields: a signed-strengthened block and a zero-calibration field.
Zero-calibration is copied verbatim from the hypothesis. Inside the signed-strengthened block, the strengthened subpackage is likewise copied. The only nontrivial field is the signed unit: it is supplied by signReversing_forces_signed_unit, fed the unit-zero fact from the native strengthened package and the sign-reversing axiom. No analytic evaluation of a canonical cost value is required.
why it matters
Doc-comment claim: the exchange runs both ways, so round-4 sign reversal and the round-2 slim ledger select the same costs. Sign reversal is therefore a strictly better-behaved stand-in for signed-unit calibration, not a weakening: antisymmetry is intrinsic and does not hard-wire a unit calibration constant.
In the Recognition foundation this sits inside the native-cost minimality and structural-ledger work that pins which cost functionals on ratio orbits are admissible before mass ladders and constants are read off. It supports the broader forcing story in which J-type costs and their discrete orbit presentations are uniquely constrained (T5 J-uniqueness lineage), here at the level of hypothesis packages rather than the closed form of $J$.
No downstream consumers are recorded yet; the lemma is a ledger-closure step equating two presentations of the same class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.