canonicalSeedLevelEvent_zero
plain-language theorem explainer
At level 0 the canonical seed event is just the singleton support on {0}. Anyone wiring the seed hierarchy into the forcing chain cites this to collapse the special-case definition at the base index. The proof is a one-line simp unfolding the seed-event definition against the fixed post index 2.
Claim. The canonical seed-level support event at index $0$ equals the ordinary level-tagged singleton support event on $\{0\}$. Equivalently, because the canonical seed-posting index is $2$, the special composite branch of the seed-event map is not taken at $k=0$.
background
The module UnifiedForcingChain aims to force the full T-1 through T8 stack from the Recognition Composition Law plus normalization and calibration, so every structural layer is an inevitability rather than an assumption.
Support events tag discrete levels by finite supports on $\mathbb{N}$. The ordinary level event at $k$ is the singleton ${k}$, so distinct levels are disjoint by construction. The canonical seed-posting index is fixed at $2$: levels $0$ and $1$ are the adjacent seeds of a local second-order hierarchy, and their first local closure is posted at the next level.
The seed-event map therefore branches only at that post index: at $k=2$ it returns the composite of the two seed supports; elsewhere it falls back to the plain singleton level event. Level $0$ is one of those fallback cases.
proof idea
One-line wrapper. Unfold canonicalSeedLevelEvent and canonical_seed_post_index. The definition is an if-then on equality with the post index $2$; since $0 \neq 2$, simp reduces the left-hand side to levelSupportEvent 0, matching the goal.
why it matters
Inside the Complete Inevitability Chain, seed levels $0$ and $1$ are the base of the local hierarchy whose composite posts at level $2$. This simp lemma pins the base case so later reasoning about seed supports, disjointness, and composite posting can treat level $0$ as an ordinary singleton without reopening the definition.
No downstream consumers are recorded yet; the lemma is infrastructure for the seed-event layer that sits under the T0–T8 forcing narrative (logic from cost, discreteness, ledger symmetry, unique $J$, $\varphi$, eight-tick, $D=3$). It does not itself advance a numbered T-step, but it keeps the seed bookkeeping definitionally clean for those arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.