supportEvent_support_disjoint_independence
plain-language theorem explainer
For the canonical finite-support event carrier, disjoint supports imply configuration-space independence. Anyone building support-induced configuration certificates or scalar work projections on SupportEvent cites this. The proof is a one-line reverse application of the independent-iff-disjoint-support biconditional.
Claim. For any type of atoms $A$ with decidable equality, the carrier of finite-support events on $A$ satisfies support-disjointness compatibility: whenever two events $a,b$ have disjoint supports, they are independent in the configuration-space sense (no shared predicates under join).
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain, configurations must carry a notion of independence so that cost can be assigned without double-counting shared structure.
A configuration space supplies an empty configuration, a binary join, consistency, and an independence relation. Support-disjointness compatibility is the bridge that says: if events expose finite supports in an atom type, then set-theoretic disjointness of those supports is enough to conclude configuration independence.
The canonical carrier is the support-event type: each event is just a finite set of atoms, join is union, and the empty event is the empty set. In that model, independence is not an extra predicate; it is literally disjointness of supports. The sibling biconditional records both directions of that identification.
proof idea
Construct the support-disjointness compatibility certificate by filling its single field. Introduce two events and a disjointness hypothesis on their supports, then apply the reverse direction of the already-proved biconditional that configuration independence holds if and only if the supports are disjoint. No further case analysis is required.
why it matters
This certificate is the independence half of the canonical support-induced configuration-space package. The parent theorem canonical_support_induced_config_space assembles the full certificate by pairing the independent-iff-disjoint biconditional with this one-sided implication. A second consumer is the aggregate scalar-work projection for support events, which needs the same independence discipline when collapsing finite-support cardinality to scalar work.
In the forcing chain this sits under the cost-from-distinction foundation that feeds T0 (logic from cost) and the later ledger and recognition steps. It does not itself force φ, the eight-tick octave, or D=3; it only locks the canonical event model so those later steps can treat independence as support geometry rather than an ad-hoc relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.