canonicalSeedLevelEvent
plain-language theorem explainer
Assigns each hierarchy level index a support-bearing event: levels 0 and 1 are singletons, level 2 is their join (the seed composite), and higher levels are singleton placeholders. Seed-recognition-work models and the forcing bridge cite this as the canonical level-to-event map. The body is a one-line case split on the canonical seed-post index 2.
Claim. For each $k \in \mathbb{N}$, the canonical seed-level event is the composite support of levels $0$ and $1$ when $k = 2$, and the singleton support $\{k\}$ otherwise.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Near the seed of a multilevel hierarchy, one needs a concrete carrier in which independence is just disjointness of finite supports.
A support event is a finite set of atoms. Level-tagged events send level $k$ to the singleton ${k}$, so distinct levels are disjoint by construction. The canonical seed-post index is $2$: the first local closure of seed levels $0$ and $1$. Their composite is the join with support ${0,1}$.
This definition packages that interpretation into a single map from level indices to support events, so later lemmas can treat seed posting and higher placeholders uniformly.
proof idea
Definition by case split: if $k$ equals the canonical seed-post index $2$, return the prebuilt composite of the level-$0$ and level-$1$ singletons; otherwise return the singleton support event at $k$. No proof obligations beyond the surrounding structure instances.
why it matters
Gives the level-to-event assignment used by the seed-only recognition-work model that the forcing bridge relies on ("only seed disjointness is required"). Downstream simp facts pin the values at $0$, $1$, and $2$, and the composition identity states that the level-$2$ event is exactly the join of the level-$0$ and level-$1$ events under this map.
In the T−1/T0 region of the chain, a bare distinction forces a two-atom support universe; this definition is the bookkeeping layer that turns that seed into a multilevel event assignment without inventing extra independence predicates. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those sit later in T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.