supportJoinCompatible_of_supportQuotientMap
plain-language theorem explainer
If a map from an arbitrary event configuration space into the canonical support-event carrier preserves join, the support extracted from that map is join-compatible: support of a join equals the union of the two supports. Anyone lifting independence-as-disjoint-support from the quotient back to a general event system cites this. The argument is a short unfold-and-rewrite off the quotient map's join law.
Claim. Let $E$ be a configuration space and $A$ a type of atoms with decidable equality. Suppose $q:E\to\mathrm{SupportEvent}(A)$ preserves join: $q(a\ast b)=q(a)\ast q(b)$ for all $a,b\in E$. Then the extracted support map $s(e):=q(e).\mathrm{support}$ satisfies $s(a\ast b)=s(a)\cup s(b)$ for all $a,b$.
background
In the Unified Forcing Chain, configuration spaces carry an empty configuration and a binary join, together with consistency and independence structure (CostFromDistinction). The canonical model of independence is not an extra predicate: a SupportEvent over atoms $A$ is just a finite support set, join is union, and independence is disjointness of supports.
A support quotient map is a theorem-facing extraction $q:E\to\mathrm{SupportEvent}(A)$ that preserves join: quotienting after join equals joining after quotienting. Support-join compatibility for a raw support function $s:E\to\mathrm{Finset},A$ is the same algebraic law written on $s$: support of a join is the union of supports. The extracted support of $q$ is the composite that reads the finite set off $q(e)$.
This sits in the foundation layer that forces T0–T8 from the Recognition Composition Law, normalization, and calibration. The local need is to move support-disjoint independence from the canonical carrier back onto an arbitrary event system once a join-preserving quotient is given.
proof idea
Term-mode structure instance with a four-step tactic body for the single field support_join. Introduce events $a,b$; unfold the extracted support (support of $q(\cdot)$); rewrite the join of the images by the quotient map's preserves_join law; close by reflexivity of equality of finite sets. No auxiliary lemmas beyond that field of the quotient-map hypothesis.
why it matters
Parent consumer is support_extraction_through_quotient, which builds the full support-extraction compatibility certificate from a quotient map, independence reflection, and cost preservation. The doc on that parent states the goal: construct the certificate so an arbitrary event system inherits support-disjoint independence from its canonical support quotient.
Without join compatibility of the extracted support, the quotient cannot transport the canonical "independence = disjoint supports" reading. This lemma closes the join half of that bridge; the companion reflection lemma (noted in the next doc-comment in-file) closes the independence half. In the forcing chain it is scaffolding for ledger and recognition levels (T3–T4), where configuration join and independent postings must line up with cost structure, not a T5–T8 constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.