supportQuotientEvent_preserves_aggregate_projection
plain-language theorem explainer
When event cost equals support cardinality, the aggregate scalar work of an event equals that of its image under the support quotient into the canonical support-event model. Anyone building support-quotient compatibility certificates cites this equality. The proof is a short term argument: unwrap both projections to cost, apply the cardinality law, and finish by reflexivity on the support finset.
Claim. Let $E$ be a configuration space of events with cost $\kappa$, and let $\mathrm{supp}: E \to \mathrm{Finset}(A)$ be a support map. If $\kappa(e)=|\mathrm{supp}(e)|$ for every event $e$, then the aggregate scalar work projection of $e$ under $\kappa$ equals the aggregate scalar work projection of the support-quotiented event $\langle\mathrm{supp}(e)\rangle$ under the canonical support-cardinality cost on support-events.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Locally this sits in the cost-from-distinction layer: a configuration space carries empty config, join, consistency, and independence; a cost function obeys dichotomy (zero cost iff consistent) and independent additivity.
A support-cardinality cost is the special case where $\kappa(e)$ equals the cardinality of a finite atomic support. The canonical model is the support-event carrier: each event is just a finite set of atoms, join is union, and independence is disjointness of supports. The support quotient sends a general event to that carrier by reading off its support finset.
Aggregate scalar work projection packages the scalar cost of an event as the work quantity used downstream when comparing source systems to the support-event model. The theorem says that, once cost is pure support cardinality, this scalar is invariant under the quotient.
proof idea
Term-mode proof by subtype extensionality on the projected scalar. Rewrite both sides via the lemma that aggregate scalar work projection recovers the underlying cost value. On the source side, replace $\kappa(e)$ by $|\mathrm{supp}(e)|$ using the support-cardinality hypothesis. The right-hand side is already the cardinality of the support of the quotiented event, which is definitionally the same finset, so reflexivity closes the equality.
why it matters
This is one of the three source-side surfaces assembled by support_quotient_compatibility, whose doc-comment states it builds the certificate that a support-bearing event system maps canonically to support-events while preserving support, joins, disjoint-support independence, and aggregate scalar work. Without cost-projection agreement, the quotient would only match combinatorial structure, not recognition work.
In the forcing chain this keeps the cost foundation aligned when events are reduced to pure support data: the same work numbers feed ledger and recognition steps (T3–T4) and the unique $J$ forcing (T5) that pins $J(x)=(x+x^{-1})/2-1$. It is a proved bridge lemma, not scaffolding; it closes the work half of support-quotient compatibility so later T0–T8 arguments can treat support-events as faithful cost models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.