canonicalSelectedNativeCost_sans_two_hypotheses
plain-language theorem explainer
The canonical selected native cost (J-cost with the unit orbit sent to zero) inhabits the slim native-cost class with the two-point calibration anchor stripped. Anyone proving non-vacuity of that sans-two class cites this. The proof is a one-line projection: slim membership plus the bridging iff yields the sans-two conjunct.
Claim. Let $F$ be the canonical selected native cost (the $J$-cost on ratio orbits, with the unit orbit mapped to the literal zero representative). Then $F$ satisfies the slim ledger minus the two-point anchor: base native-cost hypotheses without two-calibration, prime-pair product calibration, signed-unit calibration, and zero calibration of the doubled trace.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits that are meant to realize the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ (T5). The canonical selected native cost is that $J$-cost with the unit orbit forced to the literal zero representative; it is the standard non-vacuity witness for the full zero-calibrated prime-signed strengthened hypothesis class.
The slim class packages the strengthened native-cost hypotheses (including zero and signed-unit calibration and prime-pair product cost). The sans-two variant drops only the two-point anchor: the requirement that $F$ fix the ratio orbit $2$ in the cross-equality sense $F(2)\sim 2$. A bridging equivalence states that slim membership is exactly sans-two membership plus that two-point calibration.
Upstream, the canonical witness is already known to inhabit the full slim class. This declaration peels off the two-point field so the remaining package can be cited on its own.
proof idea
One-line term proof. Start from canonicalSelectedNativeCost_slim_hypotheses (canonical $F$ lies in the slim class). Apply the forward direction of slim_iff_sansTwo_and_two_calibrated, which decomposes slim membership as the conjunction of sans-two membership and two-point calibration of $F(2)$. Project the first conjunct. No new arithmetic is done.
why it matters
This is the non-vacuity certificate for the sans-two calibration class: the canonical $J$-witness really does live there. The module doc on the bridging iff frames the companion refutation as a necessity statement about the slim ledger's own two-point field; without a inhabited sans-two side, that necessity claim would be vacuous.
No downstream consumers are wired yet (used_by is empty). In the broader RS forcing chain this sits under T5 $J$-uniqueness and the Recognition Composition Law: it keeps the native-cost hypothesis lattice stratified so calibration obligations can be discharged or refuted one field at a time. The companion Liouville-twist display (sibling material) is noted as satisfying every slim field except the two-point anchor, which is exactly the class certified here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.