supportEvent_independent_iff_support_disjoint
plain-language theorem explainer
On the canonical support-event carrier, configuration-space independence of two events is exactly disjointness of their finite atom supports. Anyone assembling support-induced ConfigSpace certificates or quotient independence maps cites this equivalence. The proof is pure definitional reflexivity: Independent is implemented as support-disjointness on this carrier.
Claim. Let $\mathrm{Atom}$ be a type with decidable equality. For support-events $a,b$ (each carrying a finite set of atoms), configuration-space independence of $a$ and $b$ holds if and only if $\mathrm{supp}(a)\cap\mathrm{supp}(b)=\emptyset$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration). Early in that chain, configurations must carry a notion of independence so that cost-from-distinction can treat composite states without double-counting shared structure.
A configuration space supplies an empty configuration, a binary join, consistency, and an independence relation ("no shared predicates"). The concrete carrier SupportEvent packages each event as a finite set of atoms: empty is the empty set, join is union. Its documentation states the design intent directly: independence is not an extra predicate; it is disjointness of finite supports.
supportMap simply reads that finite support. The present lemma records that, on this carrier, the abstract ConfigSpace independence predicate is definitionally the set-theoretic disjointness of those supports.
proof idea
One-line definitional proof: rfl. On SupportEvent, the ConfigSpace instance defines Independent a b to be exactly Disjoint (supportMap a) (supportMap b), so the biconditional is reflexivity of equality of propositions. No lemmas are invoked.
why it matters
This is the bridge that makes the abstract independence language of CostFromDistinction coincide with concrete support geometry on the canonical carrier. Downstream, canonical_support_induced_config_space installs it as the independent_iff field of the support-induced configuration-space certificate. The companion supportEvent_support_disjoint_independence uses the same identification to supply the support-disjointness compatibility structure.
Further parents include supportDisjointIndependence_of_supportQuotient (quotient maps that reflect support-event independence induce support-disjoint independence) and supportQuotientEvent_target_independent_of_disjoint (disjoint source supports become independence of quotient events). In the forcing-chain narrative this keeps T0-style cost logic and later ledger/recognition steps honest about when two events may be joined without shared atoms, without adding an independent axiom for independence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.