canonicalSeedLevelEvent_one
plain-language theorem explainer
At seed level 1, the canonical seed-level event equals the singleton level-support event. Anyone assembling the seed hierarchy inside the unified forcing chain cites this identity. The proof is a one-line simp that unfolds the case split against the fixed seed-post index 2.
Claim. The canonical seed-level event at index $1$ equals the level-support event at index $1$. Since the canonical seed-posting index is $2$, the defining case distinction selects the singleton support $\{1\}$ rather than the composite seed event.
background
The module UnifiedForcingChain aims to force the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration, so every layer is an inevitability rather than a compatibility claim.
A level-support event tags a natural number $k$ by the singleton support ${k}$, so distinct levels are disjoint by construction. The canonical seed-level event reuses that singleton for every index except the seed-post index: levels $0$ and $1$ stay singletons, their first local closure is posted at level $2$ as a composite, and higher indices keep harmless singleton placeholders.
The seed-post index itself is fixed at $2$, the first level after the adjacent seeds $0$ and $1$ in a local second-order hierarchy.
proof idea
One-line wrapper. Unfold the definition of the canonical seed-level event together with the fact that the seed-post index equals $2$. The guard $k=2$ fails at $k=1$, so the else branch returns the ordinary level-support event at $1$, and simp closes the equality.
why it matters
Inside the Complete Inevitability Chain, seed levels $0$ and $1$ must be interpreted as concrete support events before their composite can be posted at level $2$. This simp lemma pins the level-$1$ case of that interpretation, keeping the seed hierarchy definitionally aligned with singleton supports away from the post index.
No downstream theorem currently depends on it in the graph, so it functions as local definitional hygiene for the seed layer that underwrites the absolute-floor and T0 entry of the forcing chain. It does not itself touch J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$, but it keeps the discrete support language those later steps inherit free of off-by-one case errors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.