costSelectionPackageNative_holds
plain-language theorem explainer
Assembles the full native cost-selection package on the δ-native ratio-orbit carrier: uniqueness of any cost meeting the zero-calibrated prime-signed strengthened ledger, a non-vacuous canonical witness equal to the on-orbit J cost, and exclusion of the constant-zero and linear candidates. Cited by the WIN-A free-side deposit that tags native J-selection strictly below the continuum spine. Proof is a four-field structure term wiring prior uniqueness, witness, and exclusion lemmas.
Claim. The native cost-selection package holds: (i) every native cost $F$ on ratio orbits that satisfies the zero-calibrated, prime-signed, strengthened hypothesis ledger is pointwise cross-equivalent to the canonical on-orbit cost; (ii) there exists an explicit $F$ inhabiting that ledger and agreeing with the canonical cost on every orbit; (iii) the constant-zero map fails the ledger; (iv) the linear map fails the ledger.
background
In the Primitive Recognition Calculus, costs live on the countable carrier of ratio orbits rather than on a continuum of positive reals. The native package is the δ-native counterpart of the public-spine cost-selection package: it packages uniqueness, non-vacuity, and exclusion of degenerate candidates under a single Prop.
The uniqueness target asserts that any $F$ meeting the itemized ledger (base native hypotheses, prime-pair products, signed unit, all prime axes, and the zero orbit) is crossEq-pointwise the canonical onRatioOrbit cost, i.e. the discrete avatar of $J(x)=(x+x^{-1})/2-1$. The non-vacuity clause demands an explicit witness in that class that does not drift from the canonical cost.
The canonical selected native cost sends the unit orbit to the literal zero representative and otherwise follows the on-orbit J formula; upstream lemmas already show it satisfies the full strengthened hypotheses and is crossEq to the canonical cost on every orbit. Constant-zero and linear maps are the standard vacuous/degenerate competitors excluded from the ledger.
proof idea
Term-mode structure construction with four fields. Uniqueness is discharged by the already-proved native uniqueness target for the zero-calibrated prime-signed strengthened class. Non-vacuity is the existential triple of the canonical selected native cost, its full-hypothesis certificate, and the pointwise crossEq lemma against the on-orbit cost. The two exclusion fields are the prior lemmas that constant-zero and linear maps fail the strengthened native hypotheses. No new calculation occurs here; the package is pure assembly of those four results.
why it matters
This is the free-side (δ-native) deposit of J-cost selection, the discrete half of the T5 uniqueness landmark. Downstream, cost_selection_native_holds wraps it as a PublicSpine.Tagged StrengthTag.deltaOnly package, the WIN-A deposit sitting strictly below the continuum cost_selection_holds at traceClosure. The premise-ledger theorem then records that every ledger entry is uniformly at the δ-only floor.
In the Recognition framework this pins the countable-carrier selection of $J$ before continuum closure: the same functional equation and fixed-point story that force $\phi$ and the eight-tick octave begin here with a non-vacuous, non-degenerate native cost class. It closes the prereg native mint for cost selection and feeds the public spine strength accounting that separates δ-only from continuum deposits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.