supportEvent_support_join_compatible
plain-language theorem explainer
On the canonical support-bearing event carrier, configuration join is finite-support union, so the support map is join-compatible by definition. Anyone treating independence as disjointness of finite supports, or building cost-from-distinction configuration spaces, would cite this certificate. The proof is pure definitional reflexivity after introducing the two events.
Claim. For any atom type $A$ with decidable equality, let events be pairs carrying a finite support $S \subseteq A$. With configuration join defined by $a \vee b := S_a \cup S_b$ and support map $\mathrm{supp}(e)=S_e$, one has $\mathrm{supp}(a \vee b) = \mathrm{supp}(a) \cup \mathrm{supp}(b)$ for all events $a,b$.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration, rather than treating later steps as mere compatibility. Early in that development one needs a concrete event carrier on which independence is not an extra predicate but disjointness of finite supports.
A support-event is exactly a finite set of atoms. Its configuration-space structure takes the empty set as the unit and set-union as join. Join-compatibility of a support map is the Prop that support of a join equals the union of the supports; that is the algebraic interface later uniqueness and canonicity results quantify over.
Upstream, the same module supplies the support-event carrier and the join-compatibility structure; the present theorem simply instantiates the interface on that carrier.
proof idea
Term/tactic proof with no external lemmas. Introduce the two events $a,b$. After unfolding the configuration-space join on support-events (union of the underlying finite sets) and the support map (the support field), both sides of the required equality are definitionally the same Finset union, so rfl closes the goal.
why it matters
This is the concrete witness that the canonical support carrier satisfies the join-compatibility interface used throughout the cost-from-distinction layer of the forcing chain. Downstream, canonical_support_join_compatibility packages it as the canonical certificate and pairs it with the built-in union law: any join-compatible structure on this carrier agrees with finite-support union.
In the broader RS picture the lemma is scaffolding for T0–T4 style configuration and ledger reasoning (independence as disjoint supports, additive cost on joins), not a direct T5–T8 constant derivation. It keeps the absolute-floor and logic-from-cost story on a single, definitionally clean model rather than an abstract axiomatized support map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.