canonical_support_join_compatibility
plain-language theorem explainer
For any atom type with decidable equality, the canonical support-event carrier is join-compatible under the finite-support union law. Anyone auditing the T5-to-T6 self-similarity bridge cites this as the packaged certificate that join acts as support-map union. The proof plugs in the existing join-compatibility lemma and discharges the union identity by reflexivity.
Claim. For every atom type $A$ with decidable equality, support events on $A$ satisfy canonical support-join compatibility: the support map of a configuration-space join equals the union of the two supports, and that identity is exactly the built-in finite-support union law.
background
The Unified Forcing Chain module derives T0 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Mid-chain steps need a discrete configuration carrier whose joins behave like set-theoretic unions on finite supports, so cost and ledger structure stay compatible with hierarchy dynamics.
A support event is a configuration whose observable footprint is a finite set of atoms. Support-join compatibility says the support map intertwines configuration join with ordinary union of those finite sets. The sibling structure SupportJoinCompatibilityCanonicality packages two facts: the canonical support-event map is join-compatible, and the join law is precisely that built-in finite-support union.
Upstream, supportEvent_support_join_compatible already proves the first half: "join is finite-support union" on the canonical support map. Several cost notions in the stack (observer J-cost, multiplicative-recognizer cost, PRC quotient cost) ultimately read off support or ratio data, so this carrier law is the discrete substrate those costs sit on.
proof idea
Short structure inhabitant, not a deep argument. The canonical_join field is filled by applying the upstream theorem that the canonical support-event support map is join-compatible. The union_law field is a one-line tactic proof: introduce the two support events and close by rfl, because configuration-space join is definitionally finite-support union on this carrier.
why it matters
This certificate is consumed by t5_to_t6_bridge_holds, which states that the T5-to-T6 self-similarity bridge is theorem-backed once J-uniqueness is in hand. In the forcing chain, T5 pins the unique cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. The bridge needs a canonical discrete carrier whose joins preserve support, so hierarchy and closed-scale arguments can talk about unions without extra hypotheses.
Without this packaging, the T5-to-T6 step would still depend on an ad-hoc join law rather than a named canonicality Prop. It does not itself prove $\varphi$ or eight-tick structure; it only locks the support-join substrate those later landmarks use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.