supportDisjointIndependence_of_supportQuotient
plain-language theorem explainer
If a map from events to support-events reflects independence, the support extracted from that map is support-disjoint independent: disjoint finite supports force configuration independence. Used when building support-extraction certificates through a quotient. The proof is a short term construction: reverse the SupportEvent independence–disjointness equivalence, then apply the reflection hypothesis.
Claim. Let $\mathrm{Event}$ carry a configuration-space structure and let $q:\mathrm{Event}\to\mathrm{SupportEvent}(\mathrm{Atom})$. Suppose $q$ reflects independence: whenever $q(a)$ and $q(b)$ are independent as support-events, $a$ and $b$ are independent as configurations. Then the extracted support map $a\mapsto q(a).\mathrm{support}$ satisfies support-disjoint independence: $\mathrm{Disjoint}(\mathrm{supp}(a),\mathrm{supp}(b))$ implies configuration independence of $a$ and $b$.
background
In the Unified Forcing Chain, configuration spaces (from CostFromDistinction) package empty config, join, consistency, and an independence relation. Cost and logic are forced from distinction structure; independence is the "no shared predicates" relation that keeps joins cost-additive.
SupportEvent Atom is the canonical carrier: a finite Finset Atom support, with join as union. There independence is not an extra predicate; it is literally disjointness of supports. The lemma supportEvent_independent_iff_support_disjoint records that equivalence.
SupportQuotientReflectsIndependence is the remaining bridge for an arbitrary event system: if the images under $q$ are independent, the sources are independent. SupportDisjointIndependence is the dual surface on a support map: disjoint supports must imply configuration independence. supportFromQuotient q pulls the finite support out of $q(a)$.
proof idea
Term-mode structure construction filling disjoint_implies_independent. Given events $a,b$ with disjoint extracted supports, apply supportEvent_independent_iff_support_disjoint (right-to-left) to $q(a)$ and $q(b)$ to obtain SupportEvent independence. Then apply hreflect.reflects_independence to push independence back to the source events. No further lemmas; the certificate is exactly that one implication chain.
why it matters
Feeds support_extraction_through_quotient, which "construct[s] the support-extraction compatibility certificate from quotient-map, independence-reflection, and cost-preservation surfaces." That certificate is part of the foundation layer that lets arbitrary event systems inherit the canonical support model used in the cost-from-distinction development.
In the module's Complete Inevitability Chain (T-1 through T8 from the Recognition Composition Law plus normalization and calibration), support and independence structure underwrite how cost sees non-interacting configurations. This lemma closes the independence half of quotient extraction: reflection of SupportEvent independence is enough to get support-disjoint independence on the extracted map, so the quotient path does not invent a new independence notion.
No open scaffold: claim status is proved. It is local plumbing inside Foundation.UnifiedForcingChain rather than a named T$k$ landmark, but it stabilizes the support model that the forcing chain relies on when configurations are presented via quotients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.