supportCardinalityCost_of_supportQuotient
plain-language theorem explainer
If event cost agrees with canonical support-event cost after quotienting into the finite-support carrier, then cost equals cardinality of the extracted support. Cited when assembling support-extraction certificates from quotient maps in the cost foundation. One-line term proof: apply the quotient-cost specialization to the cost-preservation field.
Claim. Let $\kappa$ be a cost function on a configuration space of events, and let $q$ send events into the canonical support-event carrier over atoms. If $\kappa$ is cost-preserving through $q$ (for every event $e$, $\kappa(e)$ equals the support cost of $q(e)$), then $\kappa$ is support-cardinality cost for the support map extracted from $q$: $\kappa(e)=|\mathrm{supp}(e)|$ for all $e$.
background
In the Unified Forcing Chain module, T0–T8 are derived as inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration). Configuration spaces carry empty config, join, consistency, and independence; a cost function satisfies dichotomy (zero cost iff consistent) and independent additivity.
The canonical support-event carrier packages each event as a finite set of atoms. Independence is then just disjointness of supports, and the canonical cost on that carrier is support cardinality. A quotient map $q$ into that carrier is cost-preserving when source cost equals canonical support cost after $q$.
Support-cardinality cost is the property that event cost equals the cardinality of a designated finite support map. The extracted support map from a quotient is the support field of $q(e)$. This lemma bridges cost preservation through $q$ to that cardinality identity.
proof idea
One-line term proof. Unpack the cost-preservation field of the quotient certificate (source cost equals canonical support-event cost after $q$), then apply the existing specialization that turns quotient cost agreement into support-cardinality cost for the extracted support map. No extra case analysis or induction.
why it matters
Feeds the parent theorem that builds the full support-extraction compatibility certificate from a quotient map, independence reflection, and cost preservation. That certificate replaces a primitive support map by theorem-backed extraction through the canonical support carrier, keeping the cost foundation aligned with finite-support discreteness in the forcing chain.
In the module narrative this sits under the cost-to-structure path that forces logic, discreteness, and ledger structure (T0–T4) before unique $J$, $\varphi$, the eight-tick octave, and $D=3$. Without cost equaling support cardinality after quotienting, independence-as-disjointness would not match the numeric cost used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.