SeedEventSupportModel
plain-language theorem explainer
Support-disjointness certificate for a pair of seed events in an abstract configuration space. It packages a finite-atom support map with the rule that disjoint supports imply the space's independence relation. Anyone deriving seed independence for recognition-work additivity (without treating independence as a free predicate) cites this. Pure structure definition: two Prop fields, no proof body.
Claim. A support-disjointness model for seed events $e_0,e_1$ on a configuration space of events is a map $\mathrm{supp}$ from events to finite sets of atoms such that $\mathrm{supp}(e_0)\cap\mathrm{supp}(e_1)=\emptyset$, and such that for all events $a,b$, if $\mathrm{supp}(a)$ and $\mathrm{supp}(b)$ are disjoint then $a$ and $b$ are independent in the configuration-space sense.
background
The Unified Forcing Chain module aims to force the full T0–T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). Early steps need a configuration space: empty config, join, consistency, and an independence relation meaning “no shared predicates.” Independence is abstract; the class does not expose supports, so level separation alone cannot derive it.
Recognition-work additivity for seed postings needs the two seeds to be independent. This structure is the certificate that bridges the gap: equip events with a map into finite atom sets, require the seeds’ supports to be disjoint, and require that disjoint supports always imply the abstract independence relation. Downstream, seed independence is then a corollary of support disjointness rather than an extra axiom.
Upstream, the configuration-space class supplies Independent and the monoid laws on join; concrete carriers (support-bearing events, level-tagged seeds) instantiate the support map. Cosmology-side events (source/target/ratio postings) are a related but separate carrier; here the atoms are the finite support labels.
proof idea
Definitional structure, not a theorem. The body is two fields only: (1) the seeds have disjoint supports under the given map; (2) a universal implication from support-disjointness of any pair to configuration-space independence. No tactics, no lemmas applied at this site. Instantiations (e.g. on the concrete support-event carrier) fill the fields by exhibiting disjointness and proving the implication from the carrier’s independence definition.
why it matters
Closes the gap between abstract independence and concrete support geometry so recognition-work additivity can be forced rather than assumed. Downstream: seed independence is read off any such model; a recognition-work posting model is built from a support certificate; concrete and canonical-level seed models inhabit the structure; equivalence-to-canonical plus a compatibility map also produce an instance. The T5→T6 self-similarity bridge sits further up the same chain: hierarchy dynamics and additive posting need independent seed composition, which this certificate underwrites. In the forcing ladder this is scaffolding for the T5 (unique J) to T6 (φ as self-similar fixed point) passage, not a T-step itself. Landmark link: without forced seed independence, self-similar ledger composition (and thus φ) cannot be derived cleanly from cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.