finite_support_observation_from_quotient
plain-language theorem explainer
Any map from events into support-bearing events induces a finite-support observation by reading off the image support. Builders of the T5-to-T6 self-similarity bridge cite this to certify that quotient-style event maps carry a theorem-backed observation surface rather than an implicit one. The proof is a one-line application of the generic finite-support observation constructor.
Claim. Let $E$ be an event type and $A$ an atom type with decidable equality. Given any map $q : E \to \mathrm{SupportEvent}(A)$, the composite $e \mapsto q(e).\mathrm{support}$ (a map $E \to \mathrm{Finset}\, A$) is a finite-support observation of $E$ on atoms $A$.
background
In the Unified Forcing Chain module, T0–T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. The T5→T6 step needs a discrete, support-bearing observation surface so that self-similarity of the ledger can force the golden ratio φ.
A SupportEvent on atoms $A$ is a concrete carrier whose only data is a finite set of atoms. Independence is then ordinary disjointness of supports, not an extra predicate. A finite-support observation is a certificate that a chosen map $E \to \mathrm{Finset}, A$ is the observation surface in use; finiteness is built into the codomain, and the certificate is propositionally unique for fixed data.
The construction supportFromQuotient postcomposes a quotient map $q : E \to \mathrm{SupportEvent}(A)$ with the support projection, yielding the Finset-valued observation that this theorem certifies.
proof idea
One-line wrapper: apply the generic constructor finite_support_observation to the composite support map supportFromQuotient q. The only field of the certificate is reflexivity of that support map, so no further lemmas are required.
why it matters
This lemma sits on the T5→T6 bridge inside the complete inevitability chain. Downstream it is consumed by the structure T5_To_T6_SelfSimilarity_Bridge and the theorem t5_to_t6_bridge_holds, which record that a closed observable framework with a realized hierarchy forces the scale ratio to be φ (primer landmark T6), once T5 J-uniqueness is available.
Without an explicit finite-support observation surface, the hierarchy-dynamics arguments would smuggle an implicit observation map. Certifying that every quotient into support-bearing events induces such a surface keeps the bridge free of hidden assumptions and ties discrete ledger observations to the self-similarity that pins φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.