canonicalSeedLevelEvent_seed_composes
plain-language theorem explainer
At the canonical seed-post index (level 2), the seed event map equals the support-join of the level-0 and level-1 singleton events. Anyone wiring the seed-only recognition-work model cites this equality. The proof is a one-line simplification that unfolds the composite-event definition against the piecewise level map.
Claim. Let $E(k)$ be the canonical seed-level support event at natural level $k$, and let $\star$ be support-event composition (configuration join). With the canonical seed-post index equal to $2$, one has $E(2) = E(0) \star E(1)$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Near the seed end of that chain one needs a concrete support-event universe built from a bare distinction: two adjacent seed levels and their first local closure.
A support event carries a finite set of atoms. Composition is configuration join: supportCompose is ConfigSpace.join. The canonical seed-post index is fixed at $2$, because a local second-order hierarchy seeds at levels $0$ and $1$, and their first local closure lands at the next level. The piecewise map canonicalSeedLevelEvent sends $0$ and $1$ to singleton level supports, sends the post index $2$ to the composite of those two singletons, and treats higher levels as harmless singleton placeholders.
The composite itself is defined as the join of the level-$0$ and level-$1$ supports, so the equality claimed here is the coherence statement that the piecewise interpretation at the post index really is that join.
proof idea
Term-mode one-liner. Unfold canonicalSeedCompositeEvent by simp. By definition the left-hand side is the composite branch of canonicalSeedLevelEvent at canonical_seed_post_index ($=2$). The right-hand side applies supportCompose to the non-composite branches at $0$ and $1$, which are exactly the two singleton level supports joined in the composite definition. After that unfold the two sides match definitionally.
why it matters
This is a small coherence lemma on the canonical seed support universe forced by a bare distinction. Downstream, canonical_seed_recognition_work_model_of_support_events builds the seed-only recognition-work posting model used by the forcing bridge; its instance fields need that the level-$2$ event is the join of the two seed events, and this theorem supplies that equality under the seed-event interpretation.
In the forcing-chain narrative the lemma sits below T0–T8 proper: it packages the two-atom seed so that recognition work can be posted from seed disjointness alone, without a full multilevel ledger. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those enter later in the chain (T6–T8). It closes a definitional gap so the seed recognition-work model can be instantiated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.