canonical_level_seed_support_model
plain-language theorem explainer
The level-0 and level-1 singleton support events form a seed support model: their atom sets are disjoint, and any support-disjoint pair is ConfigSpace-independent. Anyone building recognition-work additivity or the T5→T6 self-similarity bridge cites this certificate. The proof is a one-line application of the generic SupportEvent seed model to the level-tagged seeds and their disjointness lemma.
Claim. On the concrete carrier of finite-support events over atoms $\mathbb{N}$, with support map $e \mapsto e.\mathrm{support}$, the pair of level-tagged seeds $e_0=\{0\}$ and $e_1=\{1\}$ satisfies the seed support model: $\mathrm{supp}(e_0)\cap\mathrm{supp}(e_1)=\emptyset$, and whenever two events have disjoint supports they are independent in the configuration-space sense.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Near T5→T6 one needs seed independence so recognition-work additivity can fire on a discrete ledger hierarchy.
Abstract ConfigSpace does not expose supports, so independence cannot be read off level indices alone. SeedEventSupportModel is the certificate that supplies a concrete support map into a finite atom set and proves that disjoint supports imply the abstract independence relation.
SupportEvent Atom is the canonical carrier: an event is just a finite set of atoms, join is union, and independence is support disjointness. The level-tagged seeds are levelSupportEvent k := ⟨{k}⟩, so distinct levels are disjoint by construction. The companion lemma records that levels 0 and 1 are disjoint.
proof idea
Term-mode one-liner. Instantiate the generic constructor SupportEvent.seed_support_model at the two canonical seeds levelSupportEvent 0 and levelSupportEvent 1, feeding the already-proved fact levelSupportEvent_seed_disjoint. That constructor packages the two structure fields: seed supports are disjoint, and any support-disjoint pair is ConfigSpace.Independent. No extra case analysis.
why it matters
This is the concrete model that discharges seed independence without an extra hypothesis. Downstream, canonical_level_seed_independent is exactly seed_independent_of_support_model applied to this certificate: levels 0 and 1 are independent in the ConfigSpace sense.
That independence feeds recognition-work additivity on the discrete ledger, which is part of the internal hierarchy dynamics used by the T5→T6 self-similarity bridge. The bridge structure T5_To_T6_SelfSimilarity_Bridge and the theorem t5_to_t6_bridge_holds sit on that path: once J is unique (T5), a realized closed hierarchy forces the scale ratio φ (T6).
In the forcing chain this is scaffolding for the T5→T6 step, not a physics constant derivation itself. It closes the gap that abstract ConfigSpace left open: independence is now a theorem of the level-tagged support geometry, not an assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.