supportQuotientEvent_preserves_join
plain-language theorem explainer
Whenever a support assignment on a configuration space is union-compatible with join, the support quotient map preserves join: the quotient of a join equals the join of the quotients. Cited by anyone assembling a SupportQuotientMap or a support-quotient compatibility certificate. Proof is a short term rewrite: unfold the quotient carrier and apply the union-compatibility field.
Claim. Let $E$ be a configuration space and $A$ a type of atoms with decidable equality. Fix $\mathrm{supp}:E\to\mathrm{Finset}(A)$. If $\mathrm{supp}$ is join-compatible, meaning $\mathrm{supp}(a\vee b)=\mathrm{supp}(a)\cup\mathrm{supp}(b)$ for all $a,b\in E$, then the support quotient $q$ (sending each event to the carrier whose support is $\mathrm{supp}$ of that event) satisfies $q(a\vee b)=q(a)\vee q(b)$.
background
In the Unified Forcing Chain module, T0–T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Configuration spaces supply the abstract algebra of events: empty configuration, binary join, consistency, and independence. Cost is read off distinctions among configurations.
A concrete model replaces abstract independence by disjointness of finite atomic supports. The carrier SupportEvent is just a finite set of atoms; join on that carrier is union. A map $\mathrm{supp}:E\to\mathrm{Finset}(A)$ is join-compatible when support of a join equals the union of the supports (the structure SupportJoinCompatible). The support quotient packages each source event as that finite-support carrier.
Upstream, ConfigSpace fixes the monoid laws for join and the meaning of independence; the join-compatibility hypothesis is exactly the bridge that lets source-side join become carrier-side union.
proof idea
Term-mode, two steps. First change rewrites the goal into an equality of SupportEvent constructors: left side is the support of the joined source event, right side is the union of the two source supports (the join on the quotient carrier). Then a single rewrite by the field support_join of the join-compatibility hypothesis closes the goal. No induction or case split.
why it matters
This is the join half of the support-quotient homomorphism. Downstream, supportQuotientMap_of_support_observation installs it as the preserves_join field of a SupportQuotientMap, and support_quotient_compatibility bundles it with the independence and cost surfaces into a full compatibility certificate.
In the forcing chain, independence of configurations is realized as disjointness of supports. Preserving join under the quotient is required so that cost and consistency statements on the source descend to the support carrier, where independence is literally set-disjointness. That carrier is the concrete model used when logic and ledger structure are forced from cost (T0–T4 region of the chain). Without join preservation the quotient would not be a configuration-space morphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.