cost_selection_native_holds
plain-language theorem explainer
The native cost-selection package is deposited on the public spine at δ-only strength: on the countable ratio-orbit carrier, every cost meeting the full native ledger is cross-equivalent to the canonical on-ratio-orbit cost, a witness exists, and the zero cost is excluded. Cite this for the free-side WIN-A deposit of J-selection below the continuum meter. The proof is a one-line term that tags the already-proved package.
Claim. The native cost-selection package holds as a $\delta$-only strength-tagged claim: (i) every native cost $F$ on the ratio-orbit carrier that satisfies the full itemized ledger (base hypotheses, prime-pair products, signed unit, all prime axes, and zero orbit) is pointwise cross-equivalent to the canonical on-ratio-orbit cost; (ii) some explicit $F$ inhabits that ledger and agrees with the canonical cost; (iii) the constant-zero cost fails the ledger.
background
Recognition Science forces a unique cost functional $J$ on positive ratios (forcing chain T5: $J(x)=(x+x^{-1})/2-1$). The continuum side of that selection is already packaged on the public spine; this module builds the $\delta$-native counterpart on the countable ratio-orbit carrier, free of classical real analysis.
The native package is a three-clause proposition: uniqueness of any ledger-satisfying native cost up to cross-equivalence with the canonical on-ratio-orbit map; non-vacuity via an explicit witness that meets the full strengthened prime-signed zero-calibrated hypotheses and matches the canonical cost; and exclusion of the constant-zero native cost. Public-spine tagging refuses untagged theorem badges: a claim is exposed only with a strength tag. The $\delta$-only tag marks choice-free certificates over $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$, strictly below continuum deposits.
Upstream, the untagged package is already assembled from the proved uniqueness target and the canonical selected native cost as witness.
proof idea
One-line term proof. The constructor for a strength-tagged claim needs only a proof of the underlying proposition. Supply the already-proved native package theorem (uniqueness target, canonical witness with full hypotheses and cross-equivalence, and zero-cost exclusion) as the holds field under the $\delta$-only tag. No new algebra is done here.
why it matters
This is the WIN-A deposit for cost selection on the free side of the meter: J-selection on the $\delta$-native countable carrier, tagged strictly below the continuum deposit at trace closure. It is the public-spine entry point for the native half of T5-style J-uniqueness inside Primitive Recognition Calculus.
Downstream, the native cost-selection premise ledger uses this tagged claim so that every ledger entry can be checked to sit at the $\delta$-only floor (weakest link of the deposit is $\delta$-only). Without the tag, the public surface would refuse the theorem badge. The package itself closes the preregistered native mint: uniqueness, non-vacuity, and zero exclusion on the free carrier, keeping the continuum side separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.