canonicalSeedCompositeEvent
plain-language theorem explainer
Defines the canonical two-atom seed event as the join of the level-0 and level-1 singleton supports, yielding support set {0,1}. Anyone building the seed-level interpretation of the forcing chain cites this carrier. The body is a one-line application of support composition to the two level-tagged singletons.
Claim. The canonical seed composite event is the support-bearing event obtained by joining the level-$0$ singleton support $\{0\}$ with the level-$1$ singleton support $\{1\}$, so its support is the two-element set $\{0,1\}$.
background
In the Unified Forcing Chain module, T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Near the absolute floor, events are modeled as finite-support carriers so that independence is literally disjointness of supports, not an extra predicate.
A support event on atoms of type $\mathbb{N}$ is a structure whose only data is a finite set of atoms. The level-tagged event at index $k$ is the singleton ${k}$; distinct levels are therefore disjoint by construction. Composition of two support events is the configuration join: the union of their supports.
The seed story needs a distinguished composite that packages the bare distinction between the first two levels. That composite is the object defined here.
proof idea
Pure definitional abbreviation. Apply the canonical support-event compose (configuration join) to the level-0 singleton support event and the level-1 singleton support event. No tactics or lemmas beyond those two constructors; the resulting support is ${0}\cup{1}={0,1}$.
why it matters
This is the concrete two-atom seed that the canonical seed-level interpretation plugs in at the post-seed index (level 2). Downstream, the level-event map sends that index to this composite and leaves other levels as their own singletons; simp lemmas then record that the level-2 value equals the join of levels 0 and 1.
In the forcing chain this sits under the absolute-floor and T0 logic-from-cost layer: a bare distinction forces a two-atom support universe before discreteness, ledger, unique $J$, $\varphi$, the eight-tick octave, and $D=3$ are forced. Without a named composite of the first two level supports, the seed-composition theorems have nothing to point at.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.