canonicalSeedLevelEvent_two

The module UnifiedForcingChain assembles the complete inevitability chain: from the absolute floor (T-1) through logic, MP, discreteness, ledger, recognition, unique $J$, $\varphi$, the eight-tick octave, and $D=3$, all forced from the Recognition Composition Law plus normalization and calibration.

Seed chronology sits under that chain. A level-event map assigns to each seed index a concrete event object. The post-seed index is the level-2 slot. The seed-composite event is the named object that packages seed events 0 and 1 together at that slot.

Upstream, the same module defines both the level-event map and the composite event; this lemma only identifies them at one index. Related canonical constructions elsewhere (arithmetic initial object, completed trace, dyadic protocols) follow the same pattern: fix a preferred representative and rewrite against it.

One-line wrapper. The tactic simp [canonicalSeedLevelEvent] unfolds the level-event definition; by construction its value at the post-seed index is definitionally the composite event, so the equality closes with no further lemmas.

Keeps seed-index rewriting mechanical inside Foundation.UnifiedForcingChain. The module's claim is that T0-T8 are forced from the cost foundation (RCL, $F(1)=0$, $F''(1)=1$); seed composite bookkeeping is part of stating the early chain cleanly before T5 $J$-uniqueness and T6 $\varphi$.

No downstream consumers are recorded yet (used_by empty), so the lemma is presently a local simp fact rather than a load-bearing step of T0-T8. It still earns its place as the explicit level-2 identification that later seed or ledger arguments can rewrite against without unfolding definitions by hand.