SupportJoinCompatible
plain-language theorem explainer
A support map on a configuration space is join-compatible when the support of a joined pair equals the set-union of the two supports. Anyone building finite-support extraction, quotient carriers, or independence certificates cites this interface. It is a one-field Prop structure; certificates are propositionally unique by subsingleton.
Claim. Fix types $E$ (events) and $A$ (atoms) with decidable equality on $A$, and equip $E$ with a configuration-space structure (empty config, binary join, consistency, independence). A map $\mathrm{supp}: E \to \mathrm{Finset}\, A$ is join-compatible when for all $a,b \in E$, $\mathrm{supp}(a \ast b) = \mathrm{supp}(a) \cup \mathrm{supp}(b)$, where $\ast$ is configuration join.
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). Early in that chain, configurations carry cost; later steps extract finite atomic support so ledger and discreteness arguments can talk about which atoms participate in an event.
A configuration space supplies an empty configuration, a binary join forming a commutative monoid, a consistency predicate, and an independence relation (no shared predicates). Support maps send each event to a finite set of atoms. Join-compatibility says that joining configurations does not invent or drop atoms: support of the join is exactly the union of the supports.
Upstream, the configuration-space class is the ambient algebra. Downstream work uses a canonical support carrier (SupportEvent) whose built-in support map is finite-set union on join, and quotient maps that extract support through that carrier.
proof idea
Definitional: a Prop-valued structure with a single field asserting equality of the support of a join with the union of supports. No proof body beyond the field. A companion instance shows any two such certificates are equal by reflexivity (Subsingleton), so uniqueness is propositional identity of the Prop, not a separate uniqueness theorem about the map.
why it matters
This interface is the join half of the support-compatibility surface used throughout the forcing chain's support-extraction layer. Downstream, the canonical support carrier is shown join-compatible by reflexivity; uniqueness says any join-compatible structure on that carrier agrees with built-in union; quotient maps that preserve join induce join-compatibility on the extracted support; and the full support-quotient compatibility certificate packages join-compatibility with independence and cost data.
In framework terms it sits under the cost-to-ledger path (T2 discreteness, T3 ledger): finite support must respect monoidal join so double-entry and independence remain well-defined after coarsening or quotienting. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it is scaffolding for those later steps' event algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.