canonical_support_observation
plain-language theorem explainer
For any decidable atom type, the SupportEvent carrier admits a canonical finite-support observation whose support-forgetting quotient is the identity. Anyone assembling the distinction-to-atom-universe certificate or the T5→T6 self-similarity bridge cites this package. The proof plugs in the existing SupportEvent observation and quotient map, then discharges identity by case analysis on the event.
Claim. For every type $A$ with decidable equality, the carrier of finite-support events on $A$ admits a canonical support-observation package: there is a finite-support observation along the support map $e \mapsto e.\mathrm{support}$, and the induced support-forgetting quotient map is the identity on events (up to definitional equality of supports).
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration. Early steps need a concrete event model in which independence is not an extra predicate but disjointness of finite supports.
SupportEvent A is that model: each event is just a finite set of atoms. The support map sends an event to its underlying Finset. A finite-support observation packages the data that observations factor through finite supports; a canonical support-quotient map is the support-forgetting quotient built from that map.
CanonicalSupportObservation A bundles both pieces and requires that the quotient act as the identity on the SupportEvent carrier. Upstream, canonical_support_quotient_map already builds the quotient for an arbitrary support function, and supportEvent_finite_support_observation supplies the observation instance for this carrier.
proof idea
Term-mode construction of the structure fields, with a short tactic proof for the identity law.
- Set
observationto the preexistingsupportEvent_finite_support_observation Atom. - Set
quotientby applyingcanonical_support_quotient_maptoSupportEvent.supportMap. - For
quotient_eq_id, introduce an evente, case-split on the single-field structureSupportEvent, and close byrfl(the support-forgetting quotient is definitionally the identity on this carrier).
why it matters
This certificate is the support-side half of building a canonical atom universe from a bare distinction. Downstream, canonical_distinction_atom_universe uses the induced config space from this observation package ("The canonical atom universe from a bare distinction").
It also feeds the T5→T6 bridge infrastructure: t5_to_t6_bridge_holds and the structure T5_To_T6_SelfSimilarity_Bridge sit later in the same forcing chain. In the primer landmarks, T5 is J-uniqueness and T6 forces φ as the self-similar fixed point; a clean support/observation model is part of making the discrete ledger and hierarchy data available without smuggling extra assumptions.
Within the module's stronger claim (complete inevitability of T-1..T8 from cost), this is scaffolding glue rather than a numbered T-step: it locks the canonical SupportEvent model so later bridges can quote a single observation package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.