supportQuotientMap_of_support_observation
plain-language theorem explainer
Join-compatible support observations induce a canonical support quotient that preserves configuration join. Anyone wiring event supports into the T5–T6 self-similarity bridge cites this packaging lemma. The proof is a one-field structure constructor that applies the already-proved join-preservation fact for the support quotient event map.
Claim. Let $E$ be a configuration space of events and $A$ a type of atoms with decidable equality. Given a support map $s : E \to \mathrm{Finset}(A)$ such that $s(a \vee b) = s(a) \cup s(b)$ for every pair of events, the canonical support quotient $q_s : E \to \mathrm{SupportEvent}(A)$ preserves join: $q_s(a \vee b) = q_s(a) \vee q_s(b)$.
background
In the Unified Forcing Chain, configurations carry a commutative monoid join with empty unit (the ConfigSpace structure from CostFromDistinction). A support observation assigns to each event a finite set of atoms. Join-compatibility means support of a joined configuration is exactly the union of the two supports: the support map is a monoid homomorphism into the union monoid on finite sets.
A support quotient map is the theorem-facing interface: an event-to-support-event map that preserves join, so quotienting after join equals joining after quotienting. The canonical construction supportQuotientEvent builds that carrier map from any support observation; this lemma certifies it meets the interface once join-compatibility is assumed.
The ambient module forces T0–T8 from the Recognition Composition Law plus normalization and calibration. Support extraction sits in the ledger/recognition layer that feeds self-similarity arguments between unique $J$ (T5) and the forced golden ratio fixed point (T6).
proof idea
Term-mode structure construction. The goal is a SupportQuotientMap instance for the canonical map supportQuotientEvent support. The sole field is preserves_join, discharged by applying the upstream lemma supportQuotientEvent_preserves_join to the given SupportJoinCompatible certificate. No further case analysis or rewriting is required.
why it matters
Packages join-compatible support data as a first-class support quotient map so later bridge lemmas can treat support extraction abstractly. Downstream it is used by t5_to_t6_bridge_holds, which states that the T5-to-T6 self-similarity bridge is theorem-backed once $J$-uniqueness is available.
In the forcing chain, T5 pins $J(x)=(x+x^{-1})/2-1$ and T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. Clean support quotients keep configuration joins coherent when events are coarsened to atom supports, which is part of the internal hierarchy and closed-scale arguments that realize $\varphi$. Without this interface, the bridge would have to re-prove join preservation at every use site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.