supportQuotientEvent
plain-language theorem explainer
Maps an arbitrary event to the canonical support-only carrier by retaining solely its finite atom support. Anyone reducing event structure to support cardinality or independence-as-disjointness cites this. The body is a one-line structure constructor packing the support finset.
Claim. Given event type $E$, atom type $A$, and support map $\mathrm{supp}: E \to \mathrm{Finset}\, A$, the support quotient of $e \in E$ is the support-event whose only data is the finset $\mathrm{supp}(e)$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. A recurring reduction is to forget all event structure except which atoms participate.
SupportEvent is the canonical carrier: a single field support : Finset Atom. Independence is not an extra predicate; it is disjointness of those finsets. Join is union, and the empty configuration is the empty finset. Cost-from-distinction instances live naturally on this carrier.
Upstream, several Event notions appear (directed postings with ratios, finite distinction predicates on Fin (N+1), etc.). This definition abstracts over any such source type once a support map to atoms is fixed, sending each source event to its support-only image.
proof idea
Definitional one-liner: construct the SupportEvent whose support field is exactly support e. No lemmas, no tactics; pure structure introduction.
why it matters
This is the canonical support-forgetting quotient map used throughout the support-observation layer of the forcing chain. Downstream, canonical_support_quotient_map packages it as the identity-style quotient; finite_support_observation_recovers_canonical_quotient shows any finite-support observation recovers this map; and SupportQuotientCompatibility certifies that joins, independence, and aggregate scalar work survive the quotient.
Preservation lemmas (supportQuotientEvent_preserves_support, _preserves_join, _preserves_aggregate_projection) and the identification of support-cardinality cost after quotienting all apply this constructor. In the T0–T2 region (logic and discreteness from cost), reducing to finite supports is how continuous or over-structured event models are forced down to discrete ledger data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.