canonicalSelectedNativeCost_structural_hypotheses
plain-language theorem explainer
The canonical selected native cost (J-cost with the unit orbit sent to the zero representative) inhabits the structural ledger: base native axioms plus sign reversal, monotonicity, and zero-orbit calibration. Cite this for non-vacuity of that ledger after the prime-pair product family and signed-unit calibration have been dropped. The proof is a four-field term packing the slim-class witness with the dedicated sign-reversal and monotonicity lemmas.
Claim. Let $F$ be the canonical selected native cost on ratio orbits (the $J$-cost with the unit orbit mapped to the literal zero representative). Then $F$ satisfies the structural native-cost hypotheses: the base native-cost axioms (reciprocity, normalization invariance, nonzero composition law, unit-zero, orbit-2 anchor), sign reversal, monotonicity, and zero-orbit calibration of the doubled trace.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits. The structural ledger packages the base native axioms (reciprocity, normalization invariance, the nonzero composition law, unit-zero, and the single orbit-2 anchor) together with sign reversal, monotonicity, and the zero-orbit convention on the doubled trace. Relative to the round-2 slim ledger, the countable prime-pair product family and the signed-unit calibration are both removed; nothing that replaces them mentions the canonical cost.
The canonical selected native cost is the $J$-cost with the unit orbit sent to the literal zero representative. It is the standard non-vacuity witness for the fuller zero-calibrated prime-signed strengthened class. Upstream, that witness already inhabits the slim class via a round-trip through the slim/full equivalence, and separate lemmas establish its sign-reversal and monotonicity on ratio orbits (via the $J$-display and the monotone comparison for $J$).
proof idea
Term-mode structure construction, not a tactic script. The four fields of the structural ledger are filled as follows: the base native component is projected from the slim-class witness (itself obtained from the full-class witness by the slim/full equivalence), after walking through the signed-strengthened and strengthened layers; sign reversal and monotonicity are the dedicated lemmas already proved for this cost; zero-orbit calibration is taken directly from the slim-class witness. No new analytic work occurs here.
why it matters
This is the non-vacuity certificate for the structural ledger: the structural hypothesis class is inhabited, so uniqueness and stratification results about it are not vacuous. Downstream it feeds the structural stratification certificate, which packages uniqueness of the structural class, contraction of the slim class into the structural one, positivity, and a gauge-inhabited refutation of the sans-anchor uniqueness target.
In the broader Recognition framework this sits under the native-cost side of the forcing story that isolates $J(x)=(x+x^{-1})/2-1$ (T5 J-uniqueness and the Recognition Composition Law). The structural ledger is the cleaned axiom set after dropping the prime-pair product family as redundant against monotonicity; this theorem shows the canonical $J$-witness still lives there.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.