levelSupportEvent_seed_disjoint
plain-language theorem explainer
Canonical level-0 and level-1 seed events carry disjoint finite supports ({0} versus {1}). Anyone assembling the seed-event support model, transferring disjointness along canonical equivalence, or closing the T5-to-T6 self-similarity bridge cites this fact. The argument is a short Finset membership chase: unfold the singletons and obtain a numeric contradiction.
Claim. The supports of the canonical level-tagged seed events at levels $0$ and $1$ are disjoint: if $e_k$ denotes the support event whose atom set is the singleton $\{k\}$, then $\mathrm{supp}(e_0)\cap\mathrm{supp}(e_1)=\emptyset$.
background
In the Unified Forcing Chain module, every step from the absolute floor through T0–T8 is derived from the Recognition Composition Law plus normalization and calibration. Independence of seed data is not an extra predicate: it is realized as disjointness of finite supports on a concrete carrier.
A SupportEvent over atoms is a structure whose only field is a finite set of atoms. Joining events is union of supports; the empty configuration is the empty set. The projection that reads out the support turns independence into ordinary Finset disjointness.
The level-tagged seed constructor sends each natural index $k$ to the singleton support ${k}$. Distinct level indices are therefore disjoint by construction. The present lemma records the base case needed for the two-seed model: levels $0$ and $1$.
proof idea
Rewrite disjointness via Finset.disjoint_left, so it suffices to show no atom lies in both supports. Introduce a candidate atom $x$ with membership hypotheses in each support. Unfolding the level-tagged constructor and the support projection reduces both hypotheses to $x\in{0}$ and $x\in{1}$. The resulting numeric contradiction is discharged by omega.
why it matters
This is the concrete disjointness fact that installs the canonical two-seed support model: the downstream theorem packages levels $0$ and $1$ as a SeedEventSupportModel over SupportEvent ℕ. From there, any event type whose seeds are equivalent to the canonical pair inherits support disjointness (seed_support_disjoint_of_canonical_equiv).
That inheritance is part of the scaffolding for the T5-to-T6 bridge: unique $J$ (T5) plus a self-similar discrete hierarchy forces $\varphi$ as the fixed point (T6). The bridge theorem lists this seed infrastructure among the ingredients that make the self-similarity step theorem-backed rather than axiomatic. In the forcing chain, T6 is the step that pins $\varphi$; clean seed independence is the combinatorial precondition for treating successive hierarchy levels as non-interfering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.