supportQuotientEvent_preserves_support
plain-language theorem explainer
The canonical support-forgetting quotient of events recovers the original finite-support observation on every event. Anyone assembling finite-support quotients inside the unified forcing chain cites this certificate. The proof is a one-field structure instance that applies the pointwise support identity for that canonical map.
Claim. Let $E$ be a type of events and $A$ a type of atoms with decidable equality. Given any support observation $\mathrm{supp}: E\to\mathrm{Finset}\,A$, the canonical support quotient map $q:E\to\mathrm{SupportEvent}(A)$ satisfies $\mathrm{supportMap}(q(e))=\mathrm{supp}(e)$ for every $e\in E$.
background
This lives in the Unified Forcing Chain module, which derives the absolute floor and T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The local machinery here is about finite-support observations: each event is observed only through the finite set of atoms it touches.
A support quotient map sends events to support-events (events reduced to their atom support). The structure SupportQuotientPreservesSupport packages the recovery condition: composing the quotient with the support projection must reproduce the original observation pointwise. The canonical such map is built directly from the supplied support function.
Upstream, support-events and related quotient constructions appear across the primitive recognition calculus and ledger/event layers; this lemma is the preservation certificate for the canonical choice of quotient in that family.
proof idea
Term-mode structure instance. The goal is an inhabitant of the preservation structure for the pair (support, canonical quotient). The single field preserves_support is filled by the already-proved pointwise identity that the canonical support quotient recovers support on every event. No case split or induction is required.
why it matters
This is the preservation half of the canonical support-quotient package. Downstream, canonical_support_quotient_map installs this certificate as the preserves_support field of the full canonical-map structure, and finite_support_observation_recovers_canonical_quotient re-exports the same fact under a finite-support-observation hypothesis ("the canonical quotient induced by a finite-support observation recovers exactly that observation").
In the forcing chain, finite-support observations are the discrete, ledger-compatible way events are seen. Guaranteeing that the canonical quotient does not lose or invent support is a bookkeeping lemma on the path from cost foundation through discreteness and ledger structure (T2–T4 territory), not a new physical force law. It keeps observation quotients honest before coarser identification results are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.