seed_support_model_of_canonical_equiv
plain-language theorem explainer
Canonical seed-event equivalence (seed supports equal to the singleton level tags {0} and {1}) together with a compatibility rule that disjoint supports imply ConfigSpace independence yields a SeedEventSupportModel. The T5-to-T6 self-similarity bridge cites this certificate. The proof is a two-field structure pack: disjointness from the canonical-equivalence lemma, independence from the supplied compatibility hypothesis.
Claim. Let $E$ be a configuration space with support map $\mathrm{supp}: E \to \mathrm{Finset}\,\mathbb{N}$ and seed events $s_0,s_1\in E$. Suppose $s_0,s_1$ are canonically equivalent: $\mathrm{supp}(s_0)=\{0\}$ and $\mathrm{supp}(s_1)=\{1\}$. Suppose also that whenever $\mathrm{supp}(a)\cap\mathrm{supp}(b)=\emptyset$, the configurations $a,b$ are independent in the ConfigSpace sense. Then $(E,\mathrm{supp},s_0,s_1)$ forms a seed-event support model: the seed supports are disjoint, and disjoint supports imply independence.
background
The module UnifiedForcingChain builds the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Mid-chain, seed events need a concrete support model so that recognition-work additivity can use independence of the two seeds.
A ConfigSpace is an abstract configuration type with empty config, join, consistency, and an Independent relation (no shared predicates). Abstract ConfigSpace does not expose supports, so independence cannot be read off level separation alone. SeedEventSupportModel supplies a support map into a finite atom set and a theorem that disjoint supports imply Independent; seed independence used by recognition-work additivity is then derived from support disjointness.
SeedEventsEquivalentToCanonical certifies that the hierarchy's seeds are the canonical level-tagged supports: seed 0 maps to ${0}$ and seed 1 to ${1}$. That forces the two seed supports to be disjoint singletons.
proof idea
The goal is the structure SeedEventSupportModel, which has two fields. The first field, seed_support_disjoint, is discharged by the upstream lemma seed_support_disjoint_of_canonical_equiv applied to the canonical-equivalence hypothesis $h$: supports ${0}$ and ${1}$ are disjoint. The second field, disjoint_support_implies_independent, is exactly the supplied compatibility hypothesis compat, plugged in by definitional equality. No further tactic work; it is a two-line structure constructor.
why it matters
This certificate is the concrete support model that lets seed independence be derived rather than postulated. Downstream it is consumed by t5_to_t6_bridge_holds, whose doc-comment states that the T5-to-T6 self-similarity bridge is theorem-backed. That bridge sits between T5 (unique J-cost $J(x)=(x+x^{-1})/2-1$) and T6 ($\varphi$ forced as the self-similar fixed point of the discrete ledger). Without a seed support model, recognition-work posting on the two seeds cannot invoke additivity from disjoint supports, and the internal-hierarchy route to $\varphi$ loses its independence premise. In the forcing chain this is scaffolding glue inside the T5→T6 step, not a new physical law, but it closes the gap between canonical level tags and the abstract Independent relation of ConfigSpace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.