CostSelectionPackageNativeSlim
plain-language theorem explainer
The slim native cost-selection package is a six-field Prop bundling uniqueness of the Recognition J-cost under a reduced ledger (base axioms, prime-pair products, signed unit, zero-orbit calibration), non-vacuity of that class, and decoy exclusions for constant-zero, linear, and zero-flat costs. Anyone citing the contracted δ-native rigidity deposit (PREREG-jfree-minimality) would reference it. It is a pure structure definition; the holding theorem is separate.
Claim. The slim native cost-selection package is the conjunction of: (1) uniqueness: every $F$ on ratio orbits satisfying the slim hypotheses (signed-strengthened native cost plus zero-orbit calibration) is cross-multiplication-equivalent pointwise to the canonical $J(q)=((q+q^{-1})/2)-1$; (2) non-vacuity: some $F$ meets those hypotheses and agrees with $J$; (3) the constant-zero and linear costs fail the slim class; (4) the zero-flat cost satisfies the signed-strengthened class without zero calibration, yet fails once zero calibration is required.
background
In the Primitive Recognition Calculus, costs act on ratio orbits: pairs (signed numerator, nonzero distinction-orbit denominator). Two ratio orbits are identified by cross-multiplication equivalence when the scaled numerators balance as signed orbits; that is the internal rational equality on the countable carrier.
The canonical cost is the ratio-orbit object $J(q)=((q+q^{-1})/2)-1$, not yet the real-analytic uniqueness theorem. The slim hypothesis class is the round-1 minted ledger with the all-prime axis field deleted: base axioms (reciprocity, normalization invariance, nonzero Recognition Composition Law, unit-zero, two-calibration), plus prime-pair products, signed unit, and zero-orbit calibration of the doubled trace.
The uniqueness target then says every $F$ in that slim class is crossEq-pointwise equal to $J$. Decoys include the constant-zero map and the linear cost $q-1$; the zero-flat cost is the layer-discrimination witness that passes without the zero field and fails with it.
proof idea
No proof body: this is a Prop-structure (definition). It packages six named fields whose mathematical content is fixed by the referenced hypothesis and uniqueness targets, the decoy cost maps, and the signed-strengthened class. Discharge of the package is deferred to the sibling holding theorem, which fills each field from prior uniqueness, witness, and exclusion lemmas.
why it matters
This is the contracted deposit interface for native J-selection after deleting the all-prime axis field from the calibration ledger. Downstream, the holding theorem instantiates every field, and the PublicSpine-tagged theorem records the same grade as round 1 (δ-only, countable carrier) at lower premise cost: finite generator data on 2 and -1, pair products, and the zero orbit.
In the Recognition forcing chain this is the native, countable-carrier face of T5 J-uniqueness: $J(x)=(x+x^{-1})/2-1$ forced under the Recognition Composition Law and calibration. The zero-flat pair shows the zero-orbit field is doing real work, not decorative. Honest reading stays conditional δ-native rigidity on the countable carrier under the classical proof shell disclosed by the axiom audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.