CostSelectionPackageNative
plain-language theorem explainer
Packages four δ-native conditions that select the rational J-cost on ratio orbits: uniqueness under a countable calibration ledger, a non-empty witness agreeing with the canonical cost, and exclusion of the constant-zero and linear impostors. Cited by anyone tracking the free-side cost-selection deposit below the continuum spine. As a Prop-structure it has no proof body; inhabitance is discharged downstream.
Claim. The native cost-selection package is the conjunction of: (i) every cost $F$ on ratio orbits that satisfies the zero-calibrated, prime-signed, strengthened native ledger is pointwise cross-equivalent to the canonical $J(q)=((q+q^{-1})/2)-1$; (ii) some $F$ meets that ledger and agrees with canonical $J$ under cross-equivalence; (iii) the constant-zero map fails the ledger; (iv) the linear map fails the ledger.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the countable rational display used before any real completion. Cross-equivalence is the internal PRC relation that two orbits balance under cross-multiplication of signed orbits, matching rational equality of verifier displays.
The canonical cost on a ratio orbit is the algebraic $J$-object $J(q)=((q+q^{-1})/2)-1$, written entirely with orbit arithmetic (add, reciprocal, half, one). Recognition cost elsewhere in the monolith is this same $J$ (observer forcing, multiplicative recognizers, rung coarsening), so selecting $J$ on the countable carrier is the free-side half of cost selection.
The module sits under PublicSpine's statement-carrier convention: the package is the δ-native counterpart of the continuum CostSelectionPackage. Every ledger hypothesis is algebraic on RatioOrbit, with countable quantification over prime orbits; no completed orbit, trace closure, or continuity is consumed.
proof idea
No proof body: the declaration is a Prop-valued structure with four fields. Inhabitance is assembled downstream by costSelectionPackageNative_holds, which fills uniqueness from the proved native uniqueness target, non-vacuity from the canonical selected native cost plus its full hypotheses and crossEq agreement with onRatioOrbit, and the two exclusions from the sibling lemmas that constant-zero and linear fail the native hypotheses.
why it matters
This is the statement carrier for WIN-A on the free side of the meter: cost selection of $J$ on the δ-native countable carrier, tagged strictly below the continuum deposit at traceClosure. Downstream, costSelectionPackageNative_holds proves the package, and cost_selection_native_holds wraps it as a PublicSpine-tagged StrengthTag.deltaOnly assertion.
Framework role: it records conditional δ-native rigidity of the T5 $J$-cost. The Recognition Composition Law plus an explicit countable calibration ledger (base hypotheses, prime-pair products, signed unit, all prime axes, zero orbit) forces $J$ on every ratio orbit. Calibration cost remains; continuum completion cost is removed. Uniqueness is real because calibration lives on generators and RCL must still propagate it, but the honest reading is rigidity from extensive calibration data, not an economical selector. Parent-module refuted propagation targets already show that propagation step is not free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.