canonical_nonnegative_work_additive
plain-language theorem explainer
In the canonical nonnegative-work cost model, composition of two work values is ordinary real addition on the underlying carriers. Anyone wiring scale-closure or ledger extensivity into the T0–T8 forcing chain cites this. The proof is a direct specialization of the general recognition-work extensivity lemma to the canonical cost and its scale-composition model.
Claim. Let $\mathrm{NonnegWork} = \{x \in \mathbb{R} : x \ge 0\}$. For the canonical addition $\oplus$ on this type, every pair $a,b$ satisfies $\pi(a \oplus b) = \pi(a) + \pi(b)$, where $\pi$ projects to the underlying real.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). Work values live in the subtype of nonnegative reals: recognition costs cannot be negative, so the all-real model is unrealizable and this is the correct domain for the scale-closure bridge.
The canonical cost on that subtype is the identity projection: the cost of a work event is its real value. Canonical composition is subtype addition, preserving nonnegativity. Upstream, a general lemma states that any recognition-work model (cost function plus scale-composition data) forces composition on values to be ordinary addition. A companion theorem already certifies that the canonical cost, identity scale map, and subtype addition form such a model.
proof idea
One-line specialization. Feed the general extensivity theorem nonnegative_work_extensive_of_recognition_work_model the canonical cost function (cost equals the underlying real) and the already-proved certificate that this cost, the identity scale map, and subtype addition constitute a recognition-work nonnegative scale-composition model. The general lemma then returns exactly the claim that the underlying real of the composed pair is the sum of the underlying reals.
why it matters
Work-extensivity is the ledger-side content of cost additivity: independent recognition events accumulate cost by sum, matching the T3 ledger step (cost symmetry and additive bookkeeping) inside the complete inevitability chain. The declaration pins that property for the canonical nonnegative model used throughout the scale-closure bridge, so later uniqueness and forcing arguments can treat addition as the forced composition law rather than an extra axiom.
Immediately below in the module, work-extensive composition certificates are shown propositionally unique for a fixed operation, and work-extensivity is used to force the existing additive ledger composition. No downstream dependents are recorded yet; the result is infrastructure for those uniqueness and forcing steps rather than a cited leaf of T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.