canonicalSelectedNativeCost_signReversing_hypotheses
plain-language theorem explainer
The canonical selected native cost (J-cost with unit orbit sent to zero) inhabits the round-4 sign-reversing hypothesis class. Anyone citing non-vacuity of that class, or equating it with the slim ledger, needs this witness. The proof is a three-field structure pack: strengthened and zero-calibrated from the slim hypotheses, sign-reversing from a prior lemma on the same cost.
Claim. Let $F$ be the canonical selected native cost (the $J$-cost on ratio orbits, with the unit orbit mapped to the zero representative). Then $F$ satisfies the round-4 sign-reversing native-cost hypotheses: it is strengthened, it is sign-reversing, and its doubled trace is zero-calibrated.
background
Native costs in the Primitive Recognition Calculus are maps on ratio orbits. The canonical selected native cost is the $J$-cost of the forcing chain ($J(x)=(x+x^{-1})/2-1$, T5 uniqueness), with the unit orbit forced to the literal zero representative. That choice is the standard non-vacuity witness for the full zero-calibrated prime-signed strengthened class.
The round-4 class packages three requirements on such an $F$: the strengthened native-cost axioms (base plus prime pairs), an intrinsic sign-reversal (antisymmetry) axiom, and zero-calibration of the doubled trace. Relative to the round-2 slim ledger, signed-unit calibration is dropped and sign reversal stands in its place.
Upstream, the slim-hypotheses theorem already places this cost in the round-2 class, and a dedicated sign-reversing lemma proves the antisymmetry property for the same $F$.
proof idea
Pure term-mode structure construction; no new algebra. The strengthened field is projected from the slim-hypotheses witness via its signed-strengthened component. The sign_reversing field is the already-proved antisymmetry lemma for the canonical selected cost. The zero_calibrated field is taken directly from the same slim-hypotheses witness. The declaration only repackages those three facts into the round-4 interface.
why it matters
Supplies the non-vacuity certificate for the round-4 class on the canonical $J$-cost witness. The module remark after the proof states the exchange is real both ways: round-4 and the round-2 slim ledger carve out the same costs, so sign reversal is a strictly better-behaved stand-in for signed-unit calibration, not a weakening. That comparison is the structural point of the ledger module.
In the Recognition framework this sits under foundation cost selection tied to T5 $J$-uniqueness. No recorded downstream consumers yet; the theorem is itself the occupancy witness others would cite when working in the sign-reversing interface rather than the slim signed-unit one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.