disjoint_support_implies_independent
plain-language theorem explainer
In the concrete support-event carrier, two events are configuration-space independent exactly when their finite atom supports are disjoint. Anyone building seed independence for recognition-work additivity cites this identification. The proof is pure definitional equality: the ConfigSpace instance on support-events takes Independent to be support disjointness, so the hypothesis is already the goal.
Claim. Let $a$ and $b$ be support-bearing events over an atom type. If the finite supports of $a$ and $b$ are disjoint, then $a$ and $b$ are independent in the configuration-space sense (no shared atoms under the support map).
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). Configuration spaces supply the abstract algebra of events: empty configuration, binary join, consistency, and an independence relation meaning the two configurations share no predicates.
SupportEvent is the canonical concrete carrier: each event is a finite set of atoms, join is union, and the empty event is the empty set. In this model independence is not an extra predicate; it is ordinary Finset disjointness of supports. The support map simply reads off that finite set.
Upstream, ConfigSpace packages the monoid and independence laws used throughout cost-from-distinction arguments. Downstream seed machinery needs a bridge from concrete support disjointness to the abstract Independent relation so that recognition-work additivity can fire on seed pairs.
proof idea
One-line term proof. The ConfigSpace instance on SupportEvent defines Independent as disjointness of the two supports under supportMap. The hypothesis is therefore definitionally the goal, and the proof is just that hypothesis (no tactics, no intermediate lemmas).
why it matters
This lemma is the compatibility hinge inside SeedEventSupportModel: abstract ConfigSpace does not expose supports, so independence cannot be read off level separation alone. The model supplies a support map and requires that disjoint supports imply Independent; this theorem discharges that field on the concrete carrier.
It is used by seed_support_model (build the model from raw seed disjointness), seed_independent_of_support_model (extract Independent for recognition-work additivity), and seed_support_model_of_canonical_equiv (transport along canonical seed equivalence). In the forcing chain this underwrites the seed-independence step that lets recognition work add across independent distinctions, feeding the cost foundation that forces T0 (logic from cost) onward through T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.