finite_support_observation
plain-language theorem explainer
Any map from events to finite atom sets is automatically a finite-support observation certificate: finiteness is already in the Finset codomain. Bridge builders on the T5→T6 self-similarity path cite it to name an explicit observation surface rather than leave support implicit. The proof is pure reflexivity on the support field.
Claim. For types $E$ (events) and $A$ (atoms) with decidable equality on $A$, and any map $s : E \to \mathrm{Finset}\, A$, the pair $(E,A,s)$ carries a finite-support observation certificate: for every event $e$, $s(e)=s(e)$. Finiteness is inherited from the codomain.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Between T5 (unique cost $J(x)=(x+x^{-1})/2-1$) and T6 ($\varphi$ as the self-similar fixed point), the chain needs explicit observation surfaces on discrete ledgers so hierarchy dynamics can force the scale ratio.
A finite-support observation is a named Prop certificate around a map $E\to\mathrm{Finset}, A$. Because the codomain is already finite sets of atoms, the only content of the certificate is the tautology that the supplied support equals itself. The structure exists so later bridges can require an explicit surface instead of an implicit Finset-valued field.
Related event types in the stack (rung-coarsen postings, finite distinction events on $\mathrm{Fin}(N+1)$, support events) all supply such maps; this theorem is the generic constructor for any of them.
proof idea
Term-mode structure instance with a one-tactic field proof. Introduce an arbitrary event $e$ and close observes_finite_support by reflexivity: the support map applied to $e$ equals itself. No upstream lemmas are invoked; the result is definitional from the Finset-valued signature.
why it matters
Parent uses are immediate: the canonical support map on SupportEvent and any quotient into support events obtain theorem-backed certificates by applying this constructor. Those certificates feed the T5→T6 self-similarity bridge, which records that a closed observable framework with a realized hierarchy forces the scale ratio to be $\varphi$ (forcing-chain landmark T6), while keeping the obstruction explicit that bare closed-observable fields alone do not force hierarchy data.
Without a named finite-support surface, the bridge would smuggle an implicit Finset assumption. This trivial certificate is the bookkeeping step that keeps the Complete Inevitability Chain honest between unique $J$ and forced $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.