nativeCostSelectionSlimPremiseLedger_all_deltaOnly
plain-language theorem explainer
Every entry of the contracted slim premise ledger carries the δ-only strength tag. Auditors of the native cost-selection deposit cite this to confirm the ledger never leaves the δ-only floor. The argument is a finite membership case-split on the four ledger cells, each tagged δ-only by construction.
Claim. For every strength claim $c$ belonging to the contracted slim premise ledger of native cost selection, the strength tag of $c$ equals $\delta$-only.
background
In the Primitive Recognition Calculus, native cost selection packages are deposited against a premise ledger: a finite list of strength claims, each carrying a label, a strength tag, and a prose statement. Tags grade how much structure is assumed; deltaOnly is the floor grade used for countable-carrier PublicSpine deposits.
The slim package contracts the earlier round-1 ledger by dropping the all-prime calibration family as independent price. Upstream, all_prime_axis_field_redundant shows every slim inhabitant is automatically calibrated on every native prime axis, and character_pair_two_calibration_forces_prime_calibration supplies the transport: prime-pair products plus base two-point calibration force prime-axis calibration. The slim deposit itself is cost_selection_native_slim_holds, graded δ-only.
nativeCostSelectionSlimPremiseLedger is the contracted list backing that deposit. Its first cell records the base PRC native-cost hypotheses (reciprocity, normalization invariance, canonical RCL on nonzero orbits, unit-zero, two-calibration) with necessity witnessed by the two-adic axis-twist refutation.
proof idea
Introduce an arbitrary ledger member $c$ and its membership hypothesis. Unfold the ledger definition and reduce list membership to a four-way disjunction (List.mem_cons / not_mem_nil). Case-split on the four constructors; in each branch substitute the concrete claim and close by reflexivity on the tag field, which is definitionally StrengthTag.deltaOnly. No external lemmas are required beyond the ledger def.
why it matters
This is a headline receipt in the axiom-audit block that closes the PRC native-cost minimality module. It certifies that the contracted premise ledger for the slim deposit stays uniformly at the δ-only floor, matching the grade of cost_selection_native_slim_holds and costSelectionPackageNativeSlim_holds.
In the Recognition forcing chain, native cost uniqueness is the J-uniqueness step (T5): $J(x)=(x+x^{-1})/2-1$ is forced by the Recognition Composition Law on ratio orbits. The slim package recovers that uniqueness under zero-calibrated signed-strengthened hypotheses, after the signed-strengthened target without zero-field was refuted by the zero-flat countermodel. Keeping the premise ledger δ-only documents that the contraction did not silently raise the strength grade when the all-prime family was removed as redundant.
No downstream theorems currently depend on this receipt; it is an audit invariant for the slim ledger itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.