seed_support_model
plain-language theorem explainer
Given two support-bearing seed events whose finite atom supports are disjoint, they form a seed support model: seed independence is exactly support disjointness. Anyone proving recognition-work additivity on the concrete support-event carrier cites this. The proof packs the disjointness hypothesis with the already-proved identification of independence and support disjointness.
Claim. Let $\mathrm{Atom}$ be a type with decidable equality. For seed events $s_0,s_1$ in the support-event carrier (each carrying a finite support $\mathrm{supp}(s_i)\subseteq\mathrm{Atom}$), if $\mathrm{supp}(s_0)\cap\mathrm{supp}(s_1)=\emptyset$, then $(s_0,s_1)$ satisfy the seed support-model certificate: the seeds are support-disjoint, and for every pair of events, disjoint supports imply the abstract configuration-space independence relation.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain, recognition-work additivity needs independent seed events. Abstract configuration spaces only expose an Independent predicate; they do not carry supports, so independence cannot be read off level tags alone.
SupportEvent is the concrete carrier that closes this gap: an event is a finite set of atoms, join is union, and the empty configuration is the empty set. The support map simply returns that finite set. In this carrier, configuration-space independence is definitionally support disjointness (the sibling lemma disjoint_support_implies_independent).
SeedEventSupportModel is the certificate that packages (i) disjointness of two designated seed supports and (ii) the general implication from support disjointness to abstract independence. Downstream recognition-work arguments then obtain seed independence from a geometric disjointness hypothesis rather than an extra axiom.
proof idea
Constructor packing, not a deep argument. The seed-disjointness field of the model is filled by the input hypothesis h. The compatibility field is discharged by introducing arbitrary events a,b with disjoint supports and applying the sibling theorem that, on the support-event carrier, disjoint supports are exactly configuration-space independence. No further case analysis or cost algebra is required.
why it matters
This is the concrete model witness that lets seed independence be derived rather than postulated. It is applied directly by canonical_level_seed_support_model, which instantiates the certificate on the canonical level-tagged seeds (level 0 and level 1 support events over $\mathbb{N}$). That canonical model feeds the T5-to-T6 self-similarity bridge (t5_to_t6_bridge_holds), the step that forces $\varphi$ as the unique self-similar fixed point once J-uniqueness (T5) is in hand.
In the forcing chain, T5 pins $J(x)=(x+x^{-1})/2-1$; T6 needs a discrete ledger with independent hierarchical seeds so self-similarity can act. Support-disjoint seeds supply the independence half of recognition-work additivity without smuggling an extra predicate into the abstract cost foundation. The declaration is fully proved scaffolding for that bridge, not an open hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.