CanonicalSupportQuotientMap
plain-language theorem explainer
A Prop-structure certifying that a map from events to support-bearing events is the unique support-forgetting quotient for a given finite-support observation. Anyone assembling canonical support packages or the T5→T6 self-similarity bridge cites it. The certificate bundles support preservation with pointwise uniqueness; a Subsingleton instance makes any two such certificates definitionally equal.
Claim. Fix event and atom types (atoms with decidable equality), a support assignment $\mathrm{supp}:\mathrm{Event}\to\mathrm{Finset}(\mathrm{Atom})$, and a map $q:\mathrm{Event}\to\mathrm{SupportEvent}(\mathrm{Atom})$. Then $q$ is the canonical support-forgetting quotient when (i) the support of $q(e)$ equals $\mathrm{supp}(e)$ for every event $e$, and (ii) every other map $q'$ with the same support-preservation property satisfies $q'(e)=q(e)$ for all $e$.
background
The module UnifiedForcingChain derives the full T-1 through T8 chain as forced consequences of the Recognition Composition Law plus normalization and calibration. Mid-chain, events must be reduced to their finite atomic supports so that independence is literally disjointness of supports, not an extra predicate.
A support-event is a carrier whose only data is a finite set of atoms; join is union and the empty configuration is the empty set. A support-preserving quotient is any map $q$ from raw events into that carrier such that reading off the support of $q(e)$ recovers the supplied support observation on $e$. The present structure strengthens that preservation certificate by demanding uniqueness among all such maps.
This sits just above the preservation-only certificate and just below the packaged canonical support observation used later in the forcing chain.
proof idea
Definitional, not a proved theorem: the structure is a Prop bundling two fields. The first field is exactly the support-preservation certificate (composing $q$ with the support projection recovers the given support). The second field is a uniqueness quantifier: any other support-preserving map agrees with $q$ pointwise.
An accompanying Subsingleton instance shows that for fixed data any two inhabitants are equal; the proof is rfl on the Prop fields. The actual existence of such a $q$ is discharged downstream by the theorem that builds the support-forgetting map from a support assignment and fills both fields.
why it matters
Canonical support reduction is the bookkeeping layer that lets the forcing chain treat independence as disjoint finite supports. Downstream, the theorem canonical_support_quotient_map inhabits this structure for the concrete support-forgetting map, and CanonicalSupportObservation packages the observation together with the induced identity quotient on the support-event carrier.
That package feeds the T5→T6 self-similarity bridge: once J is unique (T5), hierarchy dynamics on a closed observable framework force the scale ratio to be $\varphi$ (T6). Without a unique support-forgetting quotient, the discrete ledger side of self-similarity would not be pinned to a single carrier. The structure therefore closes a definitional gap between raw events and the support geometry used in the $\varphi$-forcing step of the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.