seed_independent_of_support_model
plain-language theorem explainer
A seed support model (disjoint supports plus a compatibility map into ConfigSpace independence) immediately yields independence of the two seed events. Anyone assembling recognition-work additivity from a concrete support certificate cites this. The proof is a one-line unpack of the model's compatibility field on the seed pair.
Claim. Let $\mathrm{Event}$ carry a configuration-space structure, and let $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}(\mathrm{Atom})$. If a seed support model certifies that $\mathrm{support}(\mathrm{seed}_0)$ and $\mathrm{support}(\mathrm{seed}_1)$ are disjoint and that disjoint supports imply configuration-space independence, then $\mathrm{seed}_0$ and $\mathrm{seed}_1$ are independent.
background
In the Unified Forcing Chain, T0–T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). Recognition-work additivity at the seed level needs the two seed events to be independent in the abstract configuration space.
A configuration space supplies an empty config, a join, consistency, and an independence relation (no shared predicates). Abstract ConfigSpace does not expose supports, so independence cannot be read off level tags alone. The seed support model is the certificate that fills the gap: a map from events into finite atom sets, a proof that the two seeds have disjoint supports, and a compatibility theorem that disjoint supports imply independence.
Upstream, the concrete support-event carrier already equates disjoint supports with independence; the model packages that fact for arbitrary event carriers used later in the hierarchy.
proof idea
One-line wrapper. Apply the model's field disjoint_support_implies_independent to the pair (seed0, seed1), feeding the model's own seed_support_disjoint hypothesis. No extra algebra or case splits.
why it matters
This is the hinge from support geometry to the abstract independence used by recognition-work posting. Downstream, canonical_level_seed_independent obtains seed independence in the level-tagged carrier with no extra hypothesis, by feeding the canonical support model into this theorem. seed_recognition_work_model_of_support builds a full seed recognition-work posting model from the same certificate. That stack feeds the T5-to-T6 self-similarity bridge (t5_to_t6_bridge_holds), where unique $J$ plus internal hierarchy force $\varphi$ (forcing-chain landmarks T5 and T6). Without seed independence, recognition-work additivity and the closed-scale argument for $\varphi$ do not start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.