SupportQuotientCompatibility
plain-language theorem explainer
A Prop-valued certificate that a support-bearing event system maps canonically onto the finite-support carrier, preserving support sets, joins, disjoint-support independence, and aggregate scalar work. Anyone routing cost data through the support quotient before the T5–T6 self-similarity bridge cites it. As a structure of eight fields plus a Subsingleton instance, uniqueness is propositional identity.
Claim. Fix event type $E$, atom type $A$ with decidable equality, a configuration-space structure on $E$, a cost $\kappa$ on $E$, and a support map $\mathrm{supp}: E \to \mathrm{Finset}\, A$. A support-quotient compatibility certificate asserts: (i) disjoint supports imply configuration independence; (ii) $\mathrm{supp}(a \vee b) = \mathrm{supp}(a) \cup \mathrm{supp}(b)$; (iii) $\kappa(e) = |\mathrm{supp}(e)|$; (iv) the quotient map $q$ into the canonical support-event carrier preserves support and join; (v) disjoint source supports map to independent quotient events; (vi) aggregate scalar work is invariant under $q$; (vii) the target carrier is the canonical support-event aggregate projection. Any two such certificates are propositionally equal.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Mid-chain, event systems must be reduced to a concrete carrier before self-similarity (T6) can be forced from unique $J$ (T5).
A configuration space supplies empty config, binary join, consistency, and an independence relation. The canonical support-event carrier is simply a finite set of atoms: join is union, and independence is exactly disjointness of supports. Three source-side surfaces package the needed hypotheses: disjoint supports imply independence; support of a join is the union of supports; and cost equals support cardinality.
Aggregate scalar work projection extracts a real work total from an event via its cost. The support-event aggregate-projection certificate says the target carrier realizes independence as disjoint support and projects work by cardinality. The quotient map sends each source event to the support-event whose support equals the source support.
proof idea
This is a definitional Prop structure, not a proved theorem. The eight fields are the certificate contents: three source-side compatibility surfaces (disjoint-independence, join-compatibility, cardinality cost), four preservation/transport statements for the quotient (support, join, target independence from disjointness, aggregate work), and canonicity of the target support-event aggregate projection.
The accompanying Subsingleton instance is a one-line proof that any two inhabitants are equal by reflexivity of equality on Prop-valued structures (all fields are propositions). Construction of an inhabitant is deferred to the companion theorem that assembles the certificate from the three source-side surfaces.
why it matters
Without a certified quotient into the canonical support carrier, support data remains a primitive map rather than a theorem-backed extraction. Downstream, SupportExtractionThroughQuotient packages a full extraction compatibility from a quotient map into SupportEvent, replacing primitive support with this certified route. The constructor theorem builds an inhabitant from the three source-side surfaces alone.
The T5-to-T6 self-similarity bridge cites this layer: unique $J$ (T5: $J(x)=(x+x^{-1})/2-1$) forces $\varphi$ only after hierarchy dynamics sit on a closed observable framework whose event geometry has been reduced through support. The certificate keeps that reduction honest: joins, independence, and scalar work survive the quotient, so no hidden cost distortion enters the $\varphi$-forcing step of the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.