FiniteSupportObservation
plain-language theorem explainer
A Prop-valued certificate that a map from events to finite sets of atoms is an explicit finite-support observation surface. Finiteness is free from the Finset codomain; the structure only names the map as a bridge interface. Cited by support-quotient lemmas and the T5-to-T6 self-similarity bridge. Definitional: one tautological field, with propositional uniqueness via Subsingleton.
Claim. Fix types $E$ (events) and $A$ (atoms) with decidable equality on $A$, and a map $s : E \to \mathrm{Finset}\, A$. A finite-support observation for $(E,A,s)$ is a proposition whose sole content is the identity $s(e)=s(e)$ for every event $e$. Equivalently: any supplied finite-support map is already such an observation; certificates are unique up to equality of proofs.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 forced from the Recognition Composition Law plus normalization and calibration. Mid-chain, events must expose which atoms they touch so that support-forgetting quotients and hierarchy data can be stated without smuggling infinite support.
Upstream, recognition events appear in several guises: directed postings source → target with positive ratio (cosmology rung coarsening), and finite distinction events on Fin(N+1) in the primitive recognition calculus. Here the carrier is abstract: any Event type equipped with a map into Finset Atom. Because the codomain is finite sets, every value is already a finite support; the structure does not re-prove finiteness.
The certificate is an explicit bridge surface. Downstream packages (canonical support observation on SupportEvent, quotient-induced observations) consume it so that T5→T6 self-similarity can route through realized hierarchy data rather than bare closed-observable fields.
proof idea
Not a proof: a Prop-structure with one field, the reflexive equality support e = support e for all events. Any map Event → Finset Atom therefore inhabits the type (see the companion constructor that fills the field by intro). A Subsingleton instance follows by rfl on the unique field, so certificates are propositionally unique for fixed data.
why it matters
Gives the named observation interface used by CanonicalSupportObservation (canonical package on SupportEvent with identity support-forgetting quotient), by the constructors that turn any Finset-valued map or any quotient into SupportEvent into a finite-support observation, and by the recovery lemma that the induced quotient preserves the original support.
In the forcing chain this sits under the T5→T6 self-similarity bridge: that bridge records that closed observable frameworks alone do not force hierarchy fields, and needs realized support/hierarchy data. Naming finite support as an explicit certificate keeps the φ-forcing step (T6: self-similar fixed point of the discrete ledger) free of hidden infinite-support assumptions. Landmark context: T5 J-uniqueness and T6 φ from self-similarity on the discrete ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.