nativeCostSelectionSlimPremiseLedger
plain-language theorem explainer
A four-entry contracted premise ledger for the slim native-cost selection deposit. Each entry records a calibration or reciprocity package and the countermodel that forces it, all tagged δ-only. Downstream uniqueness and minimality arguments cite this list as the exact hypothesis floor. The body is a literal list literal, not a derived construction.
Claim. The slim native-cost premise ledger is the four-element list of strength claims: (1) base reciprocity, normalization invariance, canonical recognition composition on nonzero orbits, unit-zero and two-point calibration; (2) calibration on products of two prime directions; (3) calibration at the signed unit $-1$; (4) zero-orbit calibration of the doubled trace. Every entry is marked $\delta$-only and carries the named necessity countermodel that forces the corresponding hypothesis.
background
In the Primitive Recognition Calculus, native cost selection asks which cost functionals on ratios are forced once a minimal calibration package is fixed. The Recognition Composition Law (RCL) constrains the cost $J$ on nonzero multiplicative orbits by $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; the classical unique solution is $J(x)=(x+x^{-1})/2-1$ (T5). Calibration axioms pin curvature at the identity (second log-derivative equal to 1) and fix values on distinguished configurations so that the cost is not a free family.
Strength claims package each hypothesis with a tag and a necessity statement: the tag deltaOnly means the claim sits at the minimal $\delta$-calibration floor rather than a stronger structural demand. Upstream cost and calibration infrastructure (CostAxioms.Calibration, CostFromDistinction.Calibration, MultiplicativeRecognizer cost, RungCoarsen cost) supplies the language in which those packages are stated. The module contracts the full native-cost hypothesis surface into a short ledger used by slim uniqueness targets.
proof idea
Definitional list literal. Four StrengthClaim records are written out by hand: labels base, prime_pair_products, signed_unit, zero_orbit; each carries StrengthTag.deltaOnly and a prose statement naming the mathematical package and the refuting countermodel (two-adic axis twist, two-adic product slip, absolute-value cost, zero-flat countermodel). No lemmas are applied; the value is the list itself.
why it matters
This ledger is the contracted hypothesis surface for slim native-cost minimality. The immediate consumer is nativeCostSelectionSlimPremiseLedger_all_deltaOnly, which proves every entry stays at the $\delta$-only floor. That fact underwrites the claim that the slim deposit does not smuggle stronger structural axioms past the referee.
In the broader Recognition chain, native-cost uniqueness feeds the forcing of $J$ (T5) and the self-similar fixed point $\phi$ (T6) once reciprocity and calibration are locked. The four necessity pointers (two-adic twist, prime-pair products, absolute-value cost, zero-flat model) document why each line cannot be dropped: without it a known countermodel survives. The ledger therefore records the exact minimal package against which uniqueness and selection theorems in this module are measured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.