SupportExtractionThroughQuotient
plain-language theorem explainer
Packages full support-extraction compatibility for an event system that quotients into the canonical support-event carrier. Anyone proving that a primitive support map can be replaced by a theorem-backed extraction through finite atomic supports will cite this bundle. It is a pure Prop structure: seven named surfaces (join preservation, independence reflection, cost preservation, and the three extracted-support properties plus overall quotient compatibility) with a Subsingleton instance, so certificates are unique up to proof irrelevance.
Claim. Fix event type $E$, atom type $A$ (with decidable equality), a configuration-space structure on $E$, a cost $\kappa$ on $E$, and a map $q:E\to\mathrm{SupportEvent}(A)$. The predicate $\mathrm{SupportExtractionThroughQuotient}(E,A,\kappa,q)$ asserts: $q$ preserves joins; $q$ reflects target independence back to source independence; $\kappa$ agrees with canonical support cost after $q$; the extracted support $e\mapsto(q\,e).\mathrm{support}$ is join-compatible (support of a join is the union), supplies support-disjoint independence, and carries support-cardinality cost; hence the event system quotients compatibly into $\mathrm{SupportEvent}(A)$.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Mid-chain, event systems must carry finite atomic supports so that independence is disjointness of supports and cost is support cardinality. The canonical carrier is $\mathrm{SupportEvent}(A)$: a structure whose only data is a finite set of atoms, with empty support as unit and join as union.
A support quotient map $q:E\to\mathrm{SupportEvent}(A)$ is required to preserve joins. Independence reflection says that if $q(a)$ and $q(b)$ are independent in the target, then $a$ and $b$ are independent in the source. Cost preservation equates source cost $\kappa.C(e)$ with the canonical support cost of $q(e)$. From $q$ one extracts an ordinary support map $\mathrm{supportFromQuotient},q$, and the remaining surfaces demand that this extracted map be join-compatible, realize support-disjoint independence, and realize support-cardinality cost.
The module’s stronger claim is complete inevitability rather than mere compatibility; this structure is the bookkeeping interface that lets an arbitrary configuration space inherit the canonical support geometry instead of postulating a primitive support map.
proof idea
No proof obligation: the declaration is a Prop-valued structure bundling seven fields. Each field is itself a named certificate structure (join-preserving quotient map, independence reflection, cost preservation, join compatibility of the extracted support, support-disjoint independence, support-cardinality cost, and overall quotient compatibility). A companion Subsingleton instance discharges uniqueness by rfl on the two inhabitants, since all fields are propositions. The actual construction lives in the downstream theorem support_extraction_through_quotient, which builds the bundle from the three input surfaces (quotient map, reflection, cost preservation) and derives the extracted-support fields.
why it matters
Replaces a primitive support map by a theorem-backed extraction through the canonical support carrier, which is required before self-similarity and the $\varphi$ fixed point can be stated on discrete ledgers. Downstream, support_extraction_through_quotient constructs inhabitants of this structure from the three quotient surfaces; the T5→T6 self-similarity bridge consumes that infrastructure when routing unique $J$ into hierarchy dynamics that force the scale ratio $\varphi$ (forcing-chain landmarks T5 and T6). Without quotient compatibility, support-disjoint independence and cardinality cost would remain external hypotheses rather than inherited geometry. The structure therefore closes a scaffolding gap between Cost-from-Distinction configuration spaces and the discrete ledger layer used later in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.