cost_selection_native_slim_holds
plain-language theorem explainer
The slim native cost-selection package holds at δ-only strength on the public spine: uniqueness of the canonical cost under base, prime-pair, signed-unit, and zero-orbit hypotheses, plus non-vacuity and exclusion of the zero map, with the all-prime calibration family dropped from the price. Ledger auditors and minimality deposits cite it. The proof is a one-line tagging of an already-proved package inhabitant.
Claim. The slim native cost-selection package is deposited on the public spine at $\delta$-only strength. Explicitly: every native cost on ratio orbits that satisfies the base axioms, prime-pair product constraints, signed unit calibration, and zero-orbit condition agrees pointwise (under cross-equality) with the canonical cost; the slim class is inhabited by a round-1 witness; and the constant-zero map is excluded from the hypotheses.
background
Primitive Recognition Calculus selects a native cost on ratio orbits. The canonical choice is the doubled $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely in the broader forcing chain (T5). Native costs are maps $F$ on ratio orbits compared via cross-equality to the orbit restriction of that canonical cost.
Round 1 packaged uniqueness under a longer ledger that still carried an all-prime calibration family as an open cost-level minimality item. The slim package deletes that family from the price: uniqueness under base + prime-pair products + signed unit + zero orbit, a non-vacuity witness, and exclusion of the constant-zero map. The deposit uses the PublicSpine tagged-statement convention on the countable carrier at strength $\delta$-only.
Upstream cost language includes total recognition cost as a multiset sum of a ratio weight, and costs induced by multiplicative recognizers via derived comparators on positive ratios.
proof idea
Term-mode one-line wrapper. The structure field holds is filled by the already-established inhabitant costSelectionPackageNativeSlim_holds, which assembles the three slim conjuncts (uniqueness target, non-vacuity existential, zero-cost exclusion) into CostSelectionPackageNativeSlim. No new algebra is done here; the declaration only tags that package at StrengthTag.deltaOnly for the public spine.
why it matters
This is the contracted deposit for native cost selection (prereg PREREG-jfree-minimality-20260724). Round 1 left all-prime cost-level minimality open; the module notes that item is now DERIVABLE, so the contracted ledger shrinks to four premises. Downstream, nativeCostSelectionSlimPremiseLedger_all_deltaOnly audits that every entry of the slim ledger stays at the $\delta$-only floor.
In the Recognition framework this locks the local uniqueness half of cost selection to the same $J$ forced globally by T5 and the Recognition Composition Law, without paying the all-prime axis field in the deposit price. It feeds the slim premise ledger rather than a new physical constant; the mass ladder, eight-tick octave, and $D=3$ sit upstream or sideways of this package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.