costSelectionPackageNativeSlim_holds
plain-language theorem explainer
The slim native cost-selection package is fully inhabited: uniqueness of the canonical cost under base, prime-pair, signed-unit, and zero-orbit axioms, plus non-vacuity and decoy exclusions, all without the all-prime axis field. Anyone citing the contracted δ-only deposit or the j-free minimality prereg needs this assembly. The proof is a pure structure inhabitant wiring already-proved uniqueness, witness, and exclusion lemmas.
Claim. The slim native cost-selection package holds: (i) every native cost $F$ on ratio orbits satisfying base two-calibration, prime-pair products, signed unit, and zero-orbit calibration is pointwise $\mathrm{crossEq}$-equivalent to the canonical selected cost; (ii) that canonical cost itself meets the slim hypotheses and matches the on-orbit cost; (iii) the constant-zero, linear, and zero-flat decoys are excluded from the slim class (zero-flat still passes the signed-strengthened layer without zero calibration).
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits. The full round-1 selection package forced the canonical cost (the discrete avatar of the J-cost $J(x)=(x+x^{-1})/2-1$) by a ledger that included an all-prime axis calibration family. The slim package is that same package with the all-prime field deleted from the price: uniqueness is asked only under base two-calibration, prime-pair products, signed unit, and zero-orbit calibration.
CostSelectionPackageNativeSlim packages six obligations: slim uniqueness (PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget), non-vacuity of the slim class, and three decoy exclusions (constant zero, linear, zero-flat), plus a witness that zero-flat still clears the signed-strengthened layer without zero calibration. Upstream, uniqueness is already proved: factorization needs only base and zero; pair and sign fields transfer to the factor character; a transport lemma recovers per-prime calibration; signed-admissible rigidity closes. The canonical selected native cost is the round-1 non-vacuity witness and inhabits the slim class via the slim/full equivalence.
proof idea
Term-mode structure inhabitant. Slim uniqueness is filled by PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved. Non-vacuity is the triple of the canonical selected native cost, its slim hypotheses (via slim_class_iff_full_class from the full hypotheses), and the existing crossEq-on-orbit identity. Constant-zero and linear exclusions are the slim decoy lemmas, each reducing to the corresponding not-native fact on the nested native layer. Zero-flat-passes-without-zero projects the signed-strengthened component of the zero-flat prime-signed-strengthened hypotheses; zero-flat exclusion is the dedicated slim exclusion lemma.
why it matters
This is the assembly step for the contracted deposit cost_selection_native_slim_holds, which tags the slim package as deltaOnly on the PublicSpine countable carrier, same grade as round 1 but with the all-prime calibration family removed from the ledger price. It also feeds nativeCostSelectionSlimPremiseLedger_all_deltaOnly, which certifies that every entry of the contracted premise ledger stays at the δ-only floor.
In framework terms this is the j-free minimality prereg (PREREG-jfree-minimality-20260724) closing toward T5 J-uniqueness: the Recognition Composition Law cost is forced without paying for a full prime-axis field. The slim uniqueness theorem already records that factorization plus pair-to-prime transport and signed rigidity recover the canonical cost. No open scaffold remains on this declaration; it is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.