supportEvent_aggregate_scalar_projection
plain-language theorem explainer
For any atom type with decidable equality, the canonical support-event carrier satisfies the aggregate scalar work projection certificate: cost is finite-support cardinality, and disjoint-support joins project to scalar addition. Cited by anyone packaging the support-event model as a theorem-backed quotient to scalar work. The proof is a short term application of the generic aggregate projection lemma to the support-event cost and its disjoint-independence fact.
Claim. For every type $\mathrm{Atom}$ with decidable equality, the carrier of finite-support events on $\mathrm{Atom}$ (with cost equal to support cardinality and support map the underlying finite set) satisfies the aggregate scalar work projection property: support-disjointness gives event independence, and the canonical projection of each event to scalar work preserves cost.
background
The Unified Forcing Chain module derives T-1 through T8 as forced consequences of the Recognition Composition Law plus normalization and calibration. Inside that chain one needs concrete event carriers on which cost, independence, and aggregation are not extra axioms but structural facts.
A support event is a finite set of atoms. Join is union; the empty support is the unit. Independence is literally disjointness of supports, so the independence predicate is not an external side condition. The associated cost is support cardinality (finite-support counting).
The structure AggregateScalarWorkProjection is the quotient/abstraction certificate: support-bearing events project canonically to a scalar work carrier by cost, and disjoint-support joins project to ordinary scalar addition. Two fields matter: a support-disjoint independence witness, and the identity that the projected scalar equals the event cost.
proof idea
Term-mode one-liner. Instantiate the generic lemma aggregate_scalar_work_projection at the support-event cost function, feeding the already-proved fact that support-event independence is exactly support-disjointness. That lemma assembles the two fields of the projection certificate (independence plus cost-preserving projection). No further case analysis or arithmetic is done here.
why it matters
This pins the canonical support-event model as a theorem-backed surface for scalar aggregate work, not merely a definitional convenience. Downstream, canonical_support_event_aggregate_projection packages it with the support-induced configuration space into a single certificate: "the support-induced carrier and aggregate scalar projection are compatible theorem-backed surfaces of the same canonical support-event construction."
In the forcing chain this sits under the cost-foundation layer that feeds T0 (logic from cost) and the later ledger/recognition steps: once events project cleanly to scalar work by cardinality, aggregate bookkeeping and independence become forced rather than postulated. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those are later T6–T8 landmarks. It closes the support-event half of the aggregate-projection interface used by the canonical packaging theorem above.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.