supportEvent_finite_support_observation
plain-language theorem explainer
On the canonical support-bearing event type, the finite-support observation is exactly the projection to each event's finite atom set. Anyone assembling the canonical observation surface for the unified forcing chain cites this certificate. The proof is a one-line application of the generic finite-support observation constructor to that projection.
Claim. For any atom type $A$ with decidable equality, the support projection $\mathrm{supp}: E_A \to \mathrm{Finset}\, A$ on the support-bearing event carrier $E_A$ (events identified with finite subsets of $A$) is a finite-support observation: it is certified as an explicit bridge surface from events to finite atom supports.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain one needs a concrete event model in which independence is not an extra predicate but disjointness of finite supports.
A support-bearing event over atoms $A$ is simply a finite subset of $A$. Its support map is the identity projection onto that finite set. A finite-support observation is a named certificate that a given map from events to Finset of atoms is the observation surface; finiteness is already in the codomain type, so the certificate mainly makes the bridge explicit rather than implicit.
Upstream, any map into finite atom sets is already a finite-support observation by a trivial constructor. The present result specializes that constructor to the canonical support-bearing carrier and its support projection.
proof idea
One-line term wrapper. Apply the generic theorem that any map Event → Finset Atom is a finite-support observation, instantiating the map by the support projection of the support-bearing event carrier. No case analysis or arithmetic is required; the structure field is reflexivity of equality on supports.
why it matters
This pins the observation half of the canonical support-observation package used later in the same module. The parent theorem canonical_support_observation takes this certificate as its observation field and pairs it with a quotient map that is propositionally the identity on supports.
In the forcing chain, support-bearing events are the concrete model where ledger independence is disjoint finite supports, feeding discreteness and ledger steps (T2–T4) without extra predicates. The certificate keeps that model theorem-backed rather than informal, so downstream quotient and recognition-work constructions can cite a named observation surface instead of rebuilding the bridge ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.