CanonicalSupportObservation
plain-language theorem explainer
Packages three certificates: SupportEvent Atom admits a finite-support observation, its support-forgetting quotient is the unique support-preserving map, and that quotient is pointwise the identity. Cited by the T5→T6 self-similarity bridge and the canonical distinction-atom universe. Definitional Prop structure; certificates are propositionally unique by a Subsingleton instance.
Claim. For any atom type $A$ with decidable equality, a canonical support-observation certificate asserts three facts about the carrier of support-bearing events $e$ (each carrying a finite support $\mathrm{supp}(e)\subseteq A$): (i) the support map is a finite-support observation surface; (ii) the support-forgetting quotient $q$ is the unique support-preserving quotient map into that carrier; (iii) $q(e)=e$ for every support event $e$.
background
The ambient module is the Unified Forcing Chain: T−1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Locally this declaration sits in the support/quotient layer that turns bare distinctions into finite atom carriers.
A SupportEvent is the concrete carrier whose only data is a finite support set; independence is just disjointness of supports, not an extra predicate. A finite-support observation is a thin certificate naming a map Event → Finset Atom as an explicit bridge surface (finiteness is already in the type). A canonical support-quotient map is a support-preserving map into SupportEvent that is unique among all such maps.
The package therefore says: on the support-event carrier itself, the observation is the identity support, the forgetting quotient is canonical, and it acts as the identity pointwise. That is the rigid base case for later atom-universe and self-similarity bridges.
proof idea
Definitional structure, not a proved theorem. The three fields are pure Prop data: the finite-support observation certificate, the canonical quotient-map certificate, and the pointwise identity equation on support events. No tactics run in the structure body.
A companion Subsingleton instance shows any two such packages are propositionally equal by rfl (all fields are Prop, so uniqueness is free). Existence is discharged downstream by canonical_support_observation, which fills the fields from supportEvent_finite_support_observation and canonical_support_quotient_map.
why it matters
Gives the rigid support-observation base used when the chain builds a finite atom universe from a bare distinction (CanonicalDistinctionAtomUniverse) and when it routes T5 J-uniqueness into the T6 self-similarity bridge (T5_To_T6_SelfSimilarity_Bridge). The existence theorem canonical_support_observation is the immediate consumer.
In the forcing chain, T5 pins $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. The support-event carrier is where independence becomes disjoint finite supports, so a canonical identity quotient is the clean starting point for hierarchy and scale-ratio arguments. Without this package the T5→T6 bridge would have to re-state observation and quotient uniqueness ad hoc.
No open scaffold: claim status is definitional; the existence side is already a proved theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.