supportQuotientEvent_target_independent_of_disjoint
plain-language theorem explainer
Disjoint atom supports on two source events lift to ConfigSpace independence of their support-quotient images. Anyone assembling support-quotient compatibility for the cost foundation cites this bridge. The proof is a one-line reverse application of the iff between support-event independence and support disjointness.
Claim. Let $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}(\mathrm{Atom})$ with $\mathrm{Atom}$ decidably equal. If $\mathrm{support}(a)$ is disjoint from $\mathrm{support}(b)$, then the support-quotient configurations of $a$ and $b$ are independent in the configuration-space sense (they share no predicates).
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). Configuration spaces package empty config, join, consistency, and an independence relation meaning "no shared predicates," with join a commutative monoid and independence symmetric.
Support maps each event to a finite set of atoms. The support quotient collapses events to configurations keyed by that support. Independence of two such quotient events is the ConfigSpace relation used when cost aggregates over joined configurations without double-counting shared structure.
Upstream, support-event independence is characterized exactly by disjointness of the underlying supports. Recognition events elsewhere carry source/target and a positive ratio with doubled J-cost, but here only the support geometry matters.
proof idea
One-line term proof. Apply the reverse direction of supportEvent_independent_iff_support_disjoint to the pair of support-quotient events of $a$ and $b$, feeding the hypothesis that $\mathrm{support}(a)$ and $\mathrm{support}(b)$ are disjoint. No further case analysis or rewriting.
why it matters
Feeds support_quotient_compatibility, which builds the support-quotient compatibility certificate from three source-side surfaces (independence, join compatibility, and the related cost surfaces). That certificate lets cost and independence pass through the quotient to SupportEvent, so aggregate scalar projections agree after coarsening.
In the forcing chain this is plumbing under the cost foundation that forces T0 (logic from cost minimization) onward through T5 J-uniqueness and T6 $\varphi$. Without independence lifting across the support quotient, joined configurations could silently share atoms and corrupt the cost accounting that drives the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.