support_extraction_through_quotient
plain-language theorem explainer
Given a join-preserving quotient from an abstract event system into the canonical support-event carrier, together with independence reflection and cost preservation, one obtains the full support-extraction compatibility certificate. Anyone assembling the T5→T6 self-similarity bridge cites this packaging step. The proof is a structure constructor that reuses the three input surfaces and discharges the remaining fields by named lemmas.
Claim. Let $\mathrm{Event}$ be a configuration space and $\kappa$ a cost function on it. Let $q:\mathrm{Event}\to\mathrm{SupportEvent}(\mathrm{Atom})$ preserve join, reflect independence (if $q(a)$ and $q(b)$ are independent then so are $a$ and $b$), and preserve cost ($\kappa(e)=C_{\mathrm{support}}(q(e))$). Then $q$ yields a full support-extraction certificate: join compatibility, support-disjoint independence on the source, cardinality cost, and quotient compatibility all hold.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Support extraction is the bridge that lets an arbitrary event system inherit the canonical model in which independence is literally disjointness of finite supports.
A SupportEvent is a finite set of atoms; join is union and independence is disjoint support. A support quotient map $q$ is a join homomorphism into that carrier. Independence reflection says independence of images pulls back to the source. Cost preservation says source cost equals the canonical support cost after $q$.
The target structure SupportExtractionThroughQuotient packages those three surfaces plus the derived properties (join compatibility, support-disjoint independence, cardinality cost, quotient compatibility) needed so that support extraction is theorem-backed rather than a primitive map.
proof idea
Term-mode structure construction. The three input hypotheses are copied into quotient_map, reflects_independence, and cost_preserving. The remaining fields are filled by specialized lemmas: supportJoinCompatible_of_supportQuotientMap from the join-preserving map; supportDisjointIndependence_of_supportQuotient from independence reflection; supportCardinalityCost_of_supportQuotient from cost preservation; and support_quotient_compatibility assembled from those three derived facts together with $\kappa$. No new arithmetic is proved here; it is pure certificate assembly.
why it matters
This declaration sits on the path from unique $J$ (T5) to forced $\varphi$ (T6). Downstream, T5_To_T6_SelfSimilarity_Bridge and t5_to_t6_bridge_holds need a theorem-backed support extraction so the self-similarity hierarchy can be realized on concrete event data without smuggling a primitive support map.
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 extraction is the bookkeeping that lets cost and independence pass through a quotient into the canonical support carrier, so the hierarchy-dynamics arguments that force the scale ratio $\varphi$ apply to general event systems.
It closes a packaging gap rather than an open mathematical question: once the three surface certificates exist, the full extraction certificate is automatic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.