levelSupportEvent
plain-language theorem explainer
Maps each natural number k to the support event whose finite support is the singleton {k}. Downstream seed-independence and composite-seed constructions cite it as the canonical level tagging. The body is a one-line structure constructor; disjointness of distinct levels is immediate from set theory.
Claim. For each natural number $k$, the canonical level-tagged support event is the support-bearing event with finite support $\{k\}$. Distinct level indices therefore have disjoint supports by construction.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration, rather than treating later steps as merely compatible.
A SupportEvent on an atom type is a concrete carrier with a finite support set. Independence is not an extra predicate: it is disjointness of those supports. The configuration space instance takes the empty support as the unit and union of supports as join.
Level tagging needs a family of events indexed by $\mathbb{N}$ so that seed levels 0 and 1 (and their composite) can be placed in this carrier. The canonical choice is the singleton support at the level index itself.
proof idea
Definitional one-liner: package the Finset singleton ${k}$ as a SupportEvent ℕ. No lemmas are applied; the structure field is filled directly. Downstream proofs then obtain independence from Finset disjointness of distinct singletons.
why it matters
This is the canonical level tagging used throughout the seed-support fragment of the forcing chain. It feeds canonical_level_seed_support_model and, via that model, canonical_level_seed_independent, which states that seed independence holds without an extra independence hypothesis.
It also builds canonicalSeedCompositeEvent (join of levels 0 and 1, support ${0,1}$) and canonicalSeedLevelEvent (levels 0 and 1 as singletons, level 2 as the composite, higher levels as their own singletons). Simp lemmas identify the zero and one cases with this definition.
In framework terms it is scaffolding for the cost-from-distinction configuration layer under T0–T4 (logic, MP, discreteness, ledger, recognition), not a T5–T8 identity theorem itself. It makes “independent seeds” mean disjoint supports in the canonical model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.