supportFromQuotient
plain-language theorem explainer
Given any map from an event type into the canonical support-event carrier, this definition postcomposes with the carrier's support projection to yield a plain Event → Finset Atom support map. Downstream lemmas cite it to transfer join-compatibility, independence, and cardinality-cost properties from the quotient. The body is a one-line lambda applying SupportEvent.supportMap.
Claim. For types $\mathrm{Event}$ and $\mathrm{Atom}$ (with decidable equality on atoms) and any map $q : \mathrm{Event} \to \mathrm{SupportEvent}(\mathrm{Atom})$ into the canonical finite-support carrier, define $\mathrm{supp}_q(e) := \mathrm{support}(q(e)) \in \mathrm{Finset}\,\mathrm{Atom}$.
background
The Unified Forcing Chain module aims to force the full T0–T8 ladder from the Recognition Composition Law plus normalization and calibration. Mid-chain, events must carry finite atomic supports so that independence is literally disjointness and cost can be read as support cardinality.
SupportEvent Atom is the canonical carrier: a structure whose only field is a Finset Atom. Its ConfigSpace instance joins by union and takes the empty set as the unit. Independence is not an extra predicate; it is disjointness of those finite supports.
A quotient map $q : \mathrm{Event} \to \mathrm{SupportEvent},\mathrm{Atom}$ is the device that realizes an abstract event system inside that carrier. Once $q$ is in hand, the concrete support of an event is just the support field of its image. This definition packages that extraction so later theorems can talk about an ordinary Event → Finset Atom map rather than the quotient itself.
proof idea
Pure definitional wrapper: the map sends each event $e$ to SupportEvent.supportMap (q e), i.e. the support field of the image under $q$. No lemmas are invoked; equality is definitional.
why it matters
This extraction is the hinge between quotient-level hypotheses and the support-map interface used by the forcing chain. Downstream, finite_support_observation_from_quotient builds a theorem-backed finite-support observation by postcomposing with it; supportJoinCompatible_of_supportQuotientMap, supportDisjointIndependence_of_supportQuotient, and supportCardinalityCost_of_supportQuotient lift join preservation, independence reflection, and cost preservation from $q$ to the extracted map. Those pieces assemble into SupportExtractionThroughQuotient, which replaces a primitive support map by a theorem-backed extraction through the canonical carrier.
That package feeds the T5→T6 self-similarity bridge: once supports and costs are extracted cleanly, hierarchy dynamics can force the scale ratio $\varphi$ (T6) from J-uniqueness (T5). Without a uniform support extraction, the discrete-ledger self-similarity step would have to assume a bare support map rather than derive it from the quotient model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.