deltaOnly_ne_traceClosure
plain-language theorem explainer
The δ-only strength tag is unequal to the trace-closure tag on Primitive Recognition Calculus claims. K1 auditors and anyone classifying PRC claim strength cite this as a basic tag-separation fact. The proof is a one-line decidability check on the finite inductive type of strength tags.
Claim. The strength tag marking claims forced by distinction and finite repetition alone is not equal to the strength tag marking claims that use completed orbits or completed stable trace families.
background
In the Primitive Recognition Calculus strength layer, every claim carries a StrengthTag recording how much structure the argument uses. The constructors form a ladder: δ-only (distinction plus finite repetition), trace-closure (completed orbits or stable trace families), choice (witness selection), power-comprehension, and classical extension.
K1 is the audit that keeps these tags honest: a claim tagged δ-only must not silently rely on trace completion, choice, or classical reasoning. The present fact is the first pairwise separation on that ladder: the δ-only constructor is definitionally distinct from the trace-closure constructor.
The module sits in Foundation and imports only Mathlib; the tags themselves are a pure inductive enumeration with no analytic content.
proof idea
One-line wrapper: decide. Lean’s decidable equality for a finite inductive type discharges StrengthTag.deltaOnly ≠ StrengthTag.traceClosure by constructor discrimination. No lemmas are invoked.
why it matters
This is a K1 audit sanity check, not a physics derivation. It locks the first rung of the strength ladder so downstream classifiers cannot collapse δ-only claims into trace-closure claims by tag confusion. Sibling facts (e.g. choice ≠ δ-only) complete the pairwise separations. No forcing-chain landmark (T5–T8, RCL, φ, eight-tick) depends on it; it is bookkeeping that keeps PRC claim-strength metadata sound. Currently unused by other declarations, but required for any honest K1 audit of strength tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.