nativeCostSelectionPremiseLedger_all_deltaOnly
plain-language theorem explainer
Every entry in the native cost-selection premise ledger carries the δ-only strength tag, so the deposit's weakest link is uniformly at the δ-floor. Auditors of the WIN-A native J-selection package cite this as the headline receipt that no continuum or classical-extension premise sneaks into the free-side ledger. The proof is a five-way case split on list membership followed by definitional equality.
Claim. For every strength claim $c$ belonging to the native cost-selection premise ledger, the strength tag of $c$ equals $\delta$-only.
background
In the Primitive Recognition Calculus, native cost selection isolates the unique zero-calibrated, prime-signed, strengthened cost $J$ on the countable $\delta$-native carrier (the free side of the meter). Strength tags grade how much classical or continuum machinery a deposit uses: deltaOnly is the floor, strictly below traceClosure and classicalExtension.
The premise ledger is an itemized list of StrengthClaim records packaging the reciprocity, normalization, RCL-on-orbits, unit-zero, and two-calibration hypotheses that underwrite the native package, together with the necessity countermodels that refute weaker uniqueness targets. Upstream, cost_selection_native_holds deposits the whole package at deltaOnly, while the continuum price-residue wall is separately tagged at classicalExtension.
This theorem is the uniform-tag audit of that ledger: every listed premise sits at the same floor.
proof idea
Introduce an arbitrary ledger member $c$ and its membership hypothesis. Unfold nativeCostSelectionPremiseLedger and the list-membership equations, obtaining a five-way disjunction. Case-split on the disjunction; in each branch substitute the concrete claim and close by reflexivity on the hard-coded tag := StrengthTag.deltaOnly field. No external lemmas are required beyond list membership simp lemmas.
why it matters
Recognition Science forces $J(x)=(x+x^{-1})/2-1$ (T5) and selects it on the native carrier before any continuum extension. The WIN-A deposit (cost_selection_native_holds) claims that selection lives strictly below the continuum wall on the K1 strength ledger. This theorem is the itemized receipt that every premise feeding that deposit is tagged deltaOnly, so the weakest-link grade cannot silently rise.
It sits beside the axiom-print block that audits costSelectionPackageNative_holds, the continuum residue wall, and the refutation of the prime-signed strengthened uniqueness target. No downstream consumers are wired yet; the declaration is a public-spine honesty certificate rather than a lemma used in further forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.