aggregateScalarWorkProjection
plain-language theorem explainer
Any event in a costed configuration space projects to its nonnegative recognition-work cost as a subtype of the reals. Cost-foundation and ledger arguments cite this when lifting bare event costs into the scalar work carrier used by aggregate projection certificates. The body is a one-line subtype constructor pairing the cost value with the cost function's nonnegativity proof.
Claim. Given a configuration space of events equipped with a cost function $\kappa$ (nonnegative, zero iff consistent, additive on independent joins), the aggregate scalar-work projection of an event $e$ is the pair $(\kappa(e),\, 0 \le \kappa(e))$ in $\{x \in \mathbb{R} \mid 0 \le x\}$.
background
The Unified Forcing Chain module derives T0–T8 as forced consequences of the Recognition Composition Law with normalization and calibration. A configuration space supplies empty config, join, consistency, and independence. A cost function on that space satisfies dichotomy (cost zero iff consistent) and independent additivity, with values in the nonnegative reals.
Nonnegative work is the subtype ${x:\mathbb{R}\mid 0\le x}$, the intended domain of recognition-work values (as opposed to an all-real model). Upstream cost constructions (observer J-cost, multiplicative-recognizer cost, rung-coarsen totals) already land in nonnegative reals; the CostFunction structure packages the map $C$ with an explicit nonnegativity certificate at every configuration.
This definition is the thin bridge that turns those two pieces into a single scalar-work element, so later join and quotient lemmas can treat costs as monoid elements rather than bare reals with side conditions.
proof idea
One-line definition: form the subtype element $\langle \kappa.C, e,, \kappa.\mathrm{nonneg}, e \rangle$. No lemmas fire. The CostFunction structure already guarantees $0 \le C(e)$ for every event, so the subtype constructor typechecks immediately.
why it matters
Feeds the AggregateScalarWorkProjection certificate: support-bearing events project canonically to the scalar work carrier by cost, and disjoint-support joins project to scalar addition. Immediate dependents are the cost-preservation identity (projection recovers $C$ by reflexivity) and the join-to-addition law under independence.
Further downstream, SupportQuotientCompatibility and the support-quotient preservation theorem require this projection so that quotienting events by support still agrees on aggregate scalar work. In the forcing chain this is the scalar carrier step that lets recognition work behave as an additive quantity once independence is supplied by disjoint supports, linking the cost foundation to ledger and recognition structure (T3–T4). It does not itself force J-uniqueness or $\varphi$ (T5–T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.