supportEvent_support_join_unique
plain-language theorem explainer
On the canonical support-event carrier, any certificate that the support map respects configuration join recovers ordinary finite-set union. Cost-from-distinction and ledger-forcing arguments cite this when they need the join law without unpacking the compatibility structure. The proof is a one-line field projection from the join-compatibility hypothesis.
Claim. Let $A$ be a type of atoms with decidable equality, and let support-events over $A$ carry the standard configuration-space structure (empty support; join by union of supports). If the support map on these events is join-compatible, then for all support-events $a,b$, $\mathrm{supp}(a \vee b) = \mathrm{supp}(a) \cup \mathrm{supp}(b)$.
background
In the Unified Forcing Chain module, T-1 through T8 are derived as inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration). Early in that chain, configurations are abstract objects with empty element, binary join, consistency, and independence.
A configuration space supplies emp and a binary join, with independence meant to capture "no shared predicates." The concrete carrier SupportEvent realizes that idea by packaging a finite set of atoms: independence is just disjointness of supports, and join is defined by set union. The support map simply reads off that finite set.
Join-compatibility is the Prop-structure asserting that a chosen support function intertwines with configuration join via union: support of a join equals the union of the two supports. On the canonical carrier this is the built-in law; the present lemma records that any such certificate agrees with that law.
proof idea
One-line term proof: project the support_join field of the given join-compatibility hypothesis. No rewriting or case analysis is required; the universal quantification over pairs of support-events is exactly that field.
why it matters
The forcing chain treats independence as a cost-relevant structural fact, not an extra predicate. Support-events are the canonical model where that reduction is literal (disjoint finite supports). Canonicality of join-compatibility on this carrier means downstream ledger and discreteness arguments can invoke the union law from any compatibility certificate without re-proving it.
The module's stronger claim is a complete inevitability chain from absolute floor through T8 (unique $J$, $\varphi$, eight-tick octave, $D=3$). This lemma sits in the support-geometry scaffolding that makes independence and join cost-interpretable before those later steps. No downstream users are wired yet in the graph; it is a local uniqueness/canonicality fact for the support carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.