SupportQuotientCostPreserving
plain-language theorem explainer
A Prop-valued certificate that a map from abstract events into the canonical support-event carrier preserves recognition cost pointwise. Anyone assembling support extraction or the T5→T6 self-similarity bridge cites it as the cost face of the quotient package. It is a single-field structure; uniqueness is immediate by propositional equality of the field.
Claim. Fix event type $E$, atom type $A$, a configuration-space structure on $E$, a cost function $\kappa$ on $E$, and a map $q:E\to\mathrm{SupportEvent}(A)$. The certificate asserts that for every event $e$, $\kappa(e)$ equals the canonical support-event cost of $q(e)$. Certificates for fixed data are propositionally unique.
background
The module builds the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Mid-chain, abstract events must be reduced to a concrete carrier on which independence is literally disjointness of finite supports.
That carrier is SupportEvent A: each event is a finite set of atoms, with empty support as the unit and join as union. It carries the canonical support cost (cardinality-based recognition cost on the support). A cost function $\kappa$ on a general event type $E$ is the abstract recognition cost coming from the cost-from-distinction layer.
Cost preservation through a quotient map $q:E\to\mathrm{SupportEvent}(A)$ means the abstract cost of $e$ equals the canonical support cost of its image. This is the cost face of the larger support-extraction package (join preservation and independence reflection are separate surfaces).
proof idea
Definitional structure, not a proved theorem. The single field is the universal quantification $\forall e,,\kappa.C,e=\mathrm{supportCost}.C,(q,e)$. The accompanying Subsingleton instance is a one-line rfl: any two inhabitants agree because they are records of the same Prop field. No upstream lemmas are applied at definition time; consumers discharge the field by direct equality or by prior cost-identification lemmas.
why it matters
This is the cost face of support extraction through the canonical carrier. Downstream, supportCardinalityCost_of_supportQuotient turns a cost-preserving quotient into a support-cardinality cost certificate for the extracted support map. SupportExtractionThroughQuotient packages it with join preservation and independence reflection; support_extraction_through_quotient builds that full certificate from the three surfaces.
The package feeds the T5→T6 self-similarity bridge: once events live on finite supports with cost identified to support cardinality, hierarchy dynamics and the forced scale ratio $\varphi$ can be stated without a primitive support map. In the forcing chain this sits between unique $J$ (T5) and $\varphi$ as the self-similar fixed point (T6), keeping the bridge free of smuggled hierarchy assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.