support_quotient_compatibility
plain-language theorem explainer
Given a support map on events whose cost equals support cardinality, and that is join-compatible and independent on disjoint supports, the canonical quotient into SupportEvent preserves support, joins, independence, and aggregate work. Anyone assembling the T5-to-T6 self-similarity bridge or extracting support through a quotient cites this. The proof is a structure pack: three source hypotheses plus five named quotient lemmas.
Claim. Let $\mathrm{Event}$ carry a configuration-space structure and let $\kappa$ be a cost on events. Fix a support map $s:\mathrm{Event}\to\mathrm{Finset}(\mathrm{Atom})$. Suppose (i) disjoint supports imply configuration independence, (ii) $s$ of a join equals the union of supports, and (iii) $\kappa(e)=|s(e)|$ for every event $e$. Then the canonical quotient map into the support-event carrier is compatible: it preserves support and joins, reflects disjoint-support independence, preserves aggregate scalar work, and lands on the canonical support aggregate.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. The present lemma sits in the support-extraction layer that feeds the T5→T6 bridge (unique $J$ to self-similar $\varphi$).
A configuration space supplies empty config, join, consistency, and an independence relation (no shared predicates). A cost function obeys dichotomy (zero cost iff consistent) and independent additivity. Support-disjoint independence says disjoint finite supports imply that independence. Join-compatibility says support of a join is the union of supports. Support-cardinality cost says event cost equals cardinality of support.
Support quotient compatibility packages those source surfaces with preservation under the canonical map into SupportEvent Atom: support, joins, independence on disjoint supports, and aggregate scalar projection all survive the quotient, and the target support is the canonical aggregate.
proof idea
Tactic-mode structure construction. The three input certificates are copied into the corresponding fields of the compatibility structure. The remaining five fields are discharged by named quotient lemmas: supportQuotientEvent_support for support preservation; supportQuotientEvent_preserves_join (using join-compatibility) for join preservation; supportQuotientEvent_target_independent_of_disjoint for target independence on disjoint supports; supportQuotientEvent_preserves_aggregate_projection (using cardinality cost) for aggregate work; and canonical_support_event_aggregate_projection for canonicity of the target support. No further case analysis.
why it matters
This certificate is the source-side half of support extraction: support_extraction_through_quotient builds the full extraction certificate from a quotient map, independence reflection, and cost preservation, using this result as the compatibility surface. Downstream it appears in t5_to_t6_bridge_holds and the T5_To_T6_SelfSimilarity_Bridge structure, which route unique $J$ (T5) into forced $\varphi$ (T6) via internal hierarchy dynamics and realized closed scale.
In the forcing chain, T5 pins $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. Support-cardinality cost and quotient compatibility ensure that ledger events can be reduced to finite atomic supports without losing additive work or independence, so the self-similarity argument sees a well-defined discrete carrier rather than an arbitrary config space. Without this pack, the T5→T6 bridge would lack a proved path from cost-on-events to canonical support events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.