supportQuotientEvent_support
plain-language theorem explainer
Quotienting an event down to its finite atom support leaves that support unchanged: the support map of the quotient equals the original support function. Anyone wiring support-based independence into the cost-from-distinction layer cites this. The proof is pure definitional equality (rfl).
Claim. For types $\mathrm{Event}$ and $\mathrm{Atom}$ with decidable equality on atoms, and any support assignment $\mathrm{support} : \mathrm{Event} \to \mathrm{Finset}\,\mathrm{Atom}$, every event $e$ satisfies $\mathrm{supportMap}(\mathrm{quotient}(e)) = \mathrm{support}(e)$, where the quotient retains only the finite support of $e$.
background
In the Unified Forcing Chain, events are reduced to a canonical carrier SupportEvent: a structure whose only data is a finite set of atoms. Independence is then disjointness of those supports, not an extra predicate. The support map simply reads off that finite set.
The support quotient sends an arbitrary event type equipped with a support function to this carrier by packing support e into a SupportEvent. The module's larger program forces T0–T8 from the Recognition Composition Law, normalization, and calibration; support geometry is the concrete model used when cost-from-distinction needs join and independence surfaces.
Upstream, the quotient is defined as $\langle \mathrm{support}, e \rangle$, and the support map is the field projection. This lemma records that those two definitions compose to the identity on supports.
proof idea
One-line term proof by rfl. Unfolding the quotient yields the structure whose support field is exactly support e; applying the support map recovers that field, so both sides are definitionally equal.
why it matters
Feeds supportQuotientEvent_preserves_support, which packages the same fact as a SupportQuotientPreservesSupport certificate (preserves_support := supportQuotientEvent_support support). That certificate, together with join-compatibility and support-disjoint independence, is assembled by support_quotient_compatibility into the full support-quotient compatibility surface for cost-from-distinction.
In the forcing chain this is plumbing, not a T-step: it guarantees that reducing events to finite supports does not invent or drop atoms, so ledger-style independence (disjoint supports) and join-as-union remain faithful after quotienting. Without it, the canonical support model could not be substituted for a general event type while keeping cost and independence aligned with the RCL foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.