choice_ne_deltaOnly
plain-language theorem explainer
The strength tags marking a Primitive Recognition Calculus claim as choice-based versus δ-only are unequal constructors. K1 audit and stratification lemmas cite this to keep forced-by-distinction claims separate from witness-selection claims. The proof is a one-line decidability discharge on the finite inductive type of strength tags.
Claim. In the strength classification of Primitive Recognition Calculus claims, the tag for selection of witnesses from stable families is not equal to the tag for claims forced by distinction and finite repetition alone: $\mathsf{choice} \neq \delta\text{-only}$.
background
Primitive Recognition Calculus (PRC) attaches a strength tag to each claim so that later forcing and audit steps can track which logical resources were used. The inductive type of tags includes at least: δ-only (forced by distinction and finite repetition alone), trace closure (completed orbit or stable trace families), choice (selection of witnesses from stable families), power comprehension (controlled subtrace- or power-class formation), and a classical/excluded-middle extension.
The local module records K1 audit sanity facts: pairwise inequalities among these constructors. The present statement isolates choice from δ-only, so a claim that truly needs witness selection cannot be mislabeled as pure distinction-and-repetition strength.
proof idea
One-line decidability proof. StrengthTag is a finite inductive type with distinct constructors; Lean’s decide closes constructor inequality by computation on the decidable equality instance. No lemmas or case splits are required beyond that.
why it matters
Inside the Foundation layer, strength tags police what may be called forced versus what still depends on choice or classical extras. Keeping choice strictly above δ-only supports the Recognition Science forcing chain: early steps (distinction, finite repetition, J-cost uniqueness, φ fixed point) must not silently import witness selection. Downstream K1 audits and any stratification of PRC claims into δ-only versus choice-using strata rely on this inequality as a trivial but necessary sanity gate. It does not itself force physics constants; it only keeps the logical ledger honest before those steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.