SupportQuotientMap
plain-language theorem explainer
A support quotient map is a join-preserving map from an abstract event configuration space into the canonical finite-support carrier. Anyone building support extraction or the Boolean-floor route cites it as the interface that replaces a primitive support observation by a theorem-backed quotient. The declaration is a one-field Prop structure; uniqueness is immediate (subsingleton by reflexivity).
Claim. Fix types $E$ (events) and $A$ (atoms), with $E$ a configuration space (empty config and binary join) and $A$ decidably equal. A map $q : E \to \mathrm{SupportEvent}(A)$ is a support quotient map when it preserves join: for all $a,b \in E$, $q(a \vee b) = q(a) \vee q(b)$, where join on the right is union of finite supports. Any two such proofs of the property are definitionally equal.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 forced from the cost foundation (Recognition Composition Law plus normalization and calibration). Early in that chain one needs a clean way to read off finite atomic support from abstract events without treating support as a primitive axiom.
A configuration space supplies an empty configuration and a binary join, with consistency and independence structure used elsewhere for cost-from-distinction. The canonical carrier SupportEvent A is a finite set of atoms; its join is union, so independence is literally disjointness of supports rather than an extra predicate.
The map $q$ is the theorem-facing extraction surface: events are sent into that canonical carrier, and the only law demanded here is that quotienting after join equals joining after quotienting.
proof idea
No mathematical proof body: the declaration is a Prop-valued structure with a single field preserves_join. Inhabitants are certificates that a given $q$ commutes with join. The accompanying instance shows the type of such certificates is a subsingleton: any two proofs are equal by rfl, so the interface is propositionally unique for fixed $E$, $A$, and $q$.
why it matters
This interface is the join half of support extraction through the canonical carrier. Downstream, SupportExtractionThroughQuotient packages it with independence reflection and cost preservation; support_extraction_through_quotient builds that full certificate from a quotient map. Join preservation alone yields support-join compatibility for the extracted support map, and conversely a join-compatible support observation induces a support quotient map via the canonical quotient event.
It also appears on the Boolean-floor / atom-universe equivalence route out of the T-1 absolute-floor certificate, and is referenced on the T5-to-T6 self-similarity bridge path in the forcing chain. In framework terms it keeps support extraction theorem-backed rather than axiomatic while the chain moves from unique $J$ (T5) toward $\varphi$ as the self-similar fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.