nativeCostSelectionPremiseLedger
plain-language theorem explainer
Itemized premise ledger for the native cost-selection deposit: five δ-only strength claims that pin which calibrations and reciprocity axioms are paid to force the native cost. Anyone citing the cost-selection package or its slim contraction uses this list as the explicit price tag. The body is a literal five-element list of labeled StrengthClaim records, not a derived proof.
Claim. Define the native cost-selection premise ledger as the finite list of five strength claims, each tagged $\delta$-only: (i) base reciprocity, normalization invariance, canonical recognition composition on nonzero orbits, unit-zero and two-point calibration; (ii) calibration on products of two prime directions; (iii) calibration at the signed unit $-1$; (iv) calibration on every native prime axis (countable family); (v) zero-orbit calibration of the doubled trace.
background
In the Primitive Recognition Calculus, a native cost on ratio orbits is forced only after a stated package of reciprocity, normalization, and calibration hypotheses. Calibration (CostAxioms / CostFromDistinction) fixes curvature or distinguished inconsistent configurations so the cost is unique rather than a free family. The Recognition Composition Law and unit-zero conditions live on nonzero orbits; the zero orbit and signed unit $-1$ are invisible to that core and must be calibrated separately.
This module packages those deposits as an explicit ledger of StrengthClaim records under the PublicSpine convention. Each entry names the mathematical content paid and the necessity witness (a refuted uniqueness target or character-orientation freedom) that shows why the item cannot be dropped. Upstream cost constructions (multiplicative recognizer cost, rung-coarsen doubled $J$-cost, measure-forcing dressings) supply the ambient cost language; the ledger itself only itemizes premises.
proof idea
Pure definitional list. Five records are written in place, each with a label, StrengthTag.deltaOnly, and a prose statement string pointing at the corresponding hypothesis package and its necessity refutation (base uniqueness twist, prime-pair slip, absolute-value cost, prime-axis orientation freedom, zero-flat countermodel). No tactics or lemmas are applied; downstream theorems read the list by membership.
why it matters
This ledger is the priced bill of materials for native cost selection. Downstream, nativeCostSelectionPremiseLedger_all_deltaOnly proves every entry sits at the $\delta$-only floor, so the weakest link of the deposit is uniform. The minimality theorem cost_selection_native_slim_holds contracts the package (same grade, all-prime family removed from the price) and cites this ledger as the full deposit being slimmed.
In the Recognition forcing picture this sits under cost uniqueness toward the $J$-cost fixed by T5 and the RCL: base reciprocity plus calibrations rule out alternate native costs, while the open note on all-prime axes records that cost-level minimality relative to base+pairs+sign remains undetermined. The zero-orbit and signed-unit lines close the gaps the nonzero RCL never sees.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.