aggregate_scalar_work_projection
plain-language theorem explainer
Any cost function on a configuration space of events, together with a support map whose disjoint supports imply independence, yields a canonical projection of those events onto the scalar work carrier. Cost is preserved, and joins of disjoint-support events map to ordinary addition of scalars. Cited by the T5-to-T6 self-similarity bridge and by the support-event and nonnegative-work specializations. Proof fills the certificate fields by reflexivity on cost and one join lemma.
Claim. Let $\mathrm{Event}$ carry a configuration-space structure and let $\kappa$ be a cost function on it. Fix a support map $\mathrm{support}:\mathrm{Event}\to\mathrm{Finset}\,\mathrm{Atom}$ such that disjoint supports imply configuration independence. Then there is an aggregate scalar work projection: cost is preserved under the projection, and the join of two support-disjoint events projects to the sum of their scalar costs, with target the canonical scalar work carrier.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The present lemma sits in the scaffolding that turns support-bearing recognition events into pure scalar work, the abstraction used when the chain moves from unique $J$ (T5) to self-similar scale $\varphi$ (T6).
A configuration space supplies empty config, join, consistency, and an independence relation (no shared predicates). A cost function $\kappa$ obeys dichotomy (cost zero iff consistent) and independent additivity. Support-disjoint independence is the compatibility hypothesis: if $\mathrm{support}(a)$ and $\mathrm{support}(b)$ are disjoint, then $a$ and $b$ are independent configurations.
The aggregate scalar projection certificate packages four facts: that support compatibility, that projection preserves $\kappa.C$, that disjoint-support joins project to scalar addition, and that the target is the canonical scalar work carrier. Upstream cost and config-space infrastructure (CostFromDistinction) supply the algebraic laws the join step needs.
proof idea
The proof is a short structure constructor. The support-independence field is the given hypothesis, passed through unchanged.
project_cost is reflexivity: by definition the first component of the aggregate projection of an event is exactly $\kappa.C,e$.
project_join_of_disjoint reduces to the lemma aggregateScalarWorkProjection_join after converting support-disjointness into configuration independence via disjoint_implies_independent from the support-compatibility structure.
target_canonical is filled by the constant canonical_scalar_work_carrier. No further case analysis or induction appears.
why it matters
This certificate is the quotient/abstraction step that lets the forcing chain treat support-bearing events as scalar work. Downstream, supportEvent_aggregate_scalar_projection instantiates it for finite-support events (cardinality cost), and canonical_scalar_work_self_projection shows the nonnegative scalar carrier projects to itself by identity.
Both feed the T5→T6 self-similarity bridge (T5_To_T6_SelfSimilarity_Bridge, discharged by t5_to_t6_bridge_holds). That bridge records that a closed observable framework with a realized hierarchy forces the scale ratio to be $\varphi$, routing through internal hierarchy dynamics rather than smuggling hierarchy fields into bare closed-framework data. In the primer landmarks this is exactly the T5 (unique $J$) to T6 ($\varphi$ forced) step of the complete inevitability chain.
Without a clean aggregate projection, scalar self-similarity would not apply uniformly to support-carrying ledger events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.