SupportQuotientPreservesSupport
plain-language theorem explainer
A support-preserving quotient is a map from events to support-events that recovers the given finite-support observation under the support projection. Anyone formalizing uniqueness or canonicity of support-forgetting quotients cites this certificate. It is a pure Prop structure (one field), with propositional uniqueness via a Subsingleton instance.
Claim. Fix types $\mathrm{Event}$ and $\mathrm{Atom}$ (with decidable equality on atoms), a support observation $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}(\mathrm{Atom})$, and a map $q:\mathrm{Event}\to\mathrm{SupportEvent}(\mathrm{Atom})$. The map $q$ preserves support when, for every event $e$, the support of $q(e)$ equals $\mathrm{support}(e)$.
background
In the Unified Forcing Chain module, T0–T8 are derived as forced consequences of the Recognition Composition Law plus normalization and calibration. Early in that development one needs a clean model of events whose only observable content is a finite set of atoms: independence is then just disjointness of supports.
SupportEvent is that carrier: a structure whose sole field is a finite set of atoms, equipped with empty configuration and join-by-union so it realizes a cost-from-distinction configuration space. The projection that reads off that finite set is the support map used here.
A finite-support observation on an arbitrary event type is any assignment of a finite atom set to each event. A quotient map into SupportEvent is support-preserving precisely when composing with the support map recovers that observation pointwise. That is the content of this Prop structure.
proof idea
No proof body: the declaration is a Prop-valued structure with a single field preserves_support, the universal equality of supports. Immediately below, a Subsingleton instance shows any two such certificates are propositionally equal by rfl (Prop fields, no data). Downstream theorems inhabit the structure by supplying that equality (e.g. the canonical quotient does so by construction).
why it matters
This certificate is the first half of the canonicity package for support-forgetting quotients in the forcing chain. CanonicalSupportQuotientMap packages it as the preserves-support leg of canonicity. The theorem supportQuotientEvent_preserves_support shows the canonical quotient induced by any finite-support observation satisfies it by construction, and finite_support_observation_recovers_canonical_quotient restates that recovery. Uniqueness then follows: supportQuotient_unique_of_preserves_support proves any support-preserving $q$ equals the canonical quotient pointwise.
In framework terms this sits under the ledger/recognition layer (T3–T4): events are reduced to finite atom supports so distinction cost and independence are purely set-theoretic. It does not itself force J, φ, the eight-tick octave, or D=3; it supplies the quotient interface those later steps rely on when events are coarsened to supports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.