SupportJoinCompatibilityCanonicality
plain-language theorem explainer
Packages two properties of the canonical support-event carrier: its support map is join-compatible, and that law is exactly finite-support union under configuration join. Anyone citing the T5→T6 self-similarity bridge or the canonical support-join certificate needs this Prop bundle. It is a pure structure definition (no proof body); uniqueness is recorded by a Subsingleton instance.
Claim. For a type of atoms $A$ with decidable equality, a support-join canonicality certificate asserts: (i) the support map on support-events over $A$ is join-compatible (support of a join equals the union of supports); (ii) for all support-events $a,b$, the support of their configuration join equals $\mathrm{supp}(a)\cup\mathrm{supp}(b)$.
background
In the Unified Forcing Chain, T0–T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). Configuration spaces supply an empty configuration and a binary join; independence is the absence of shared predicates.
SupportEvent is the concrete carrier whose data is a finite set of atoms. Join is union of supports and the empty event is the empty support, so independence is literally disjointness of finite supports rather than an extra predicate.
SupportJoinCompatible is the Prop that a support map intertwines join with set-union: $\mathrm{supp}(a\ast b)=\mathrm{supp}(a)\cup\mathrm{supp}(b)$. The present structure specializes that interface to the canonical support-event model and records that the law is exactly the built-in Finset union.
proof idea
No proof: this is a structure (Prop bundle) with two fields. The first field is an instance of join-compatibility for SupportEvent with its support map. The second field is the pointwise identity that support of configuration join equals Finset union of the two supports. A companion Subsingleton instance proves any two such certificates are propositionally equal by rfl on the fields. The inhabiting theorem canonical_support_join_compatibility fills the fields from the support-event join lemma and a direct intro on the union identity.
why it matters
This certificate pins the canonical model in which join of configurations is support-union, so independence and additive posting talk about disjoint finite supports without extra axioms. Downstream, canonical_support_join_compatibility inhabits the structure, and T5_To_T6_SelfSimilarity_Bridge consumes that layer when routing T5 (unique $J$) into T6 (φ forced by self-similarity on a discrete ledger). In the forcing chain, T6 needs a realized hierarchy with self-similar scale ratio; a clean support-join law is part of making hierarchy and additive posting well-defined on the ledger side rather than smuggled assumptions. It does not itself prove uniqueness of $J$ or force φ; it only freezes the support geometry those steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.