aggregateScalarWorkProjection_cost
plain-language theorem explainer
The aggregate scalar-work projection of an event equals that event's recognition cost by definition. Anyone working with costed configuration spaces and nonnegative work packages cites this equality. The proof is pure reflexivity: the projection is the pair of the cost value with its nonnegativity witness.
Claim. For any configuration space of events equipped with a cost function $\kappa$, and for every event $e$, the underlying real of the aggregate scalar-work projection of $e$ equals $\kappa(e)$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Early in that chain one needs a clean bridge from abstract configuration cost to a scalar nonnegative work quantity.
A configuration space supplies empty config, join, consistency, and independence. A cost function $\kappa$ on such a space obeys dichotomy (cost zero iff consistent) and independent additivity. The aggregate scalar-work projection packages $\kappa(e)$ with the nonnegativity proof into a NonnegativeWork value, so downstream lemmas can treat recognition work as a single scalar object rather than a raw real plus side conditions.
Upstream, the projection definition is exactly $\langle \kappa.C, e,, \kappa.\mathrm{nonneg}, e\rangle$. This theorem records the first-component identity that definition forces.
proof idea
One-line term proof by rfl. Unfolding the aggregate scalar-work projection yields the subtype pair whose first field is definitionally $\kappa.C, e$, so equality holds by construction with no further lemmas.
why it matters
Feeds supportQuotientEvent_preserves_aggregate_projection, which shows that after quotienting events by support cardinality the aggregate projection still agrees. That step keeps scalar work stable under coarsening of the event space, a prerequisite for comparing costs across discrete ledger presentations in the forcing chain.
In the broader T0–T8 story, cost is the primitive that forces logic, discreteness, ledger structure, unique $J$, and eventually $\varphi$. A definitional bridge from event cost to nonnegative scalar work is bookkeeping, but without it the later quotient and independence arguments cannot state that projected work is preserved. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.