canonical_support_quotient_map
plain-language theorem explainer
For any event type with a finite atomic support map, the support-forgetting quotient is the unique map that preserves support. Anyone building observation surfaces or the T5→T6 self-similarity bridge cites this certificate. The proof assembles the existing preservation lemma with a uniqueness lemma for support-preserving quotients.
Claim. Let $\mathrm{Event}$ and $\mathrm{Atom}$ be types with decidable equality on atoms, and let $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}\,\mathrm{Atom}$. The support-forgetting quotient $q$ associated to $\mathrm{support}$ is a canonical support quotient: it preserves support, and any other support-preserving map $q'$ agrees with $q$ on every event.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Mid-chain, events must be observed only through finite atomic support so that self-similarity (T6) can act on a discrete ledger rather than raw event data.
A support map sends each event to a finite set of atoms. The support-forgetting quotient collapses events that share the same support into a SupportEvent, keeping only the observable atomic footprint. The structure CanonicalSupportQuotientMap packages two properties: the quotient preserves support, and it is the unique map with that property among all candidates of the same type.
Upstream, supportQuotientEvent builds that quotient, and supportQuotientEvent_preserves_support already proves the preservation half. Uniqueness is supplied by a companion lemma that any other support-preserving quotient agrees pointwise with the canonical one.
proof idea
The theorem is a structure inhabitant for CanonicalSupportQuotientMap at the canonical quotient supportQuotientEvent support.
The preserves_support field is filled by direct application of supportQuotientEvent_preserves_support.
The unique field is a short tactic proof: introduce an arbitrary competitor quotient $q'$ that preserves support and an event $e$, then apply supportQuotient_unique_of_preserves_support to conclude $q',e$ equals the canonical image. No new algebra is done here; the certificate only wires the two lemmas into the structure.
why it matters
This certificate is the explicit bridge surface that lets later results treat support observation as canonical rather than ad hoc. Downstream, canonical_support_observation installs it as the quotient field of the finite-support observation certificate on SupportEvent.
That observation layer feeds the T5→T6 self-similarity bridge (T5_To_T6_SelfSimilarity_Bridge, discharged by t5_to_t6_bridge_holds). 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. Without a unique support-forgetting quotient, hierarchy dynamics would not have a well-defined observation surface on which closed-scale self-similarity can act.
In the forcing chain this is scaffolding for the T5–T6 step, not a physics constant derivation itself, but it closes the uniqueness gap that would otherwise leave the observation map non-canonical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.