nonnegativeWorkAdd
plain-language theorem explainer
Canonical addition on nonnegative recognition-work values: the sum of two costs is again a nonnegative cost. Anyone building the scalar work carrier, aggregate event projections, or the T5-to-T6 self-similarity bridge cites it. The body is a one-line subtype constructor using Mathlib nonnegativity of sums.
Claim. If $a,b$ are nonnegative real work values (i.e. $a,b\in\mathbb{R}$ with $a\ge 0$ and $b\ge 0$), then $a+b$ is again a nonnegative work value.
background
The module UnifiedForcingChain aims to force the full T0–T8 chain from the Recognition Composition Law plus normalization and calibration. Near this declaration the development isolates the actual domain of cost values: recognition work is nonnegative, so the all-real model is replaced by a subtype of $\mathbb{R}$.
NonnegativeWork is the subtype ${x:\mathbb{R}\mid 0\le x}$. It is the carrier for the canonical scalar work model used in scale-closure and ledger composition. Addition must stay inside that subtype; that is exactly what this definition supplies.
Downstream, join of independent events is projected to scalar addition on this carrier, and the same operation appears as the composition law in the nonnegative recognition-work scale model that bridges unique $J$ (T5) to forced $\varphi$ (T6).
proof idea
One-line definition, not a tactic proof. Unpack the two subtype witnesses $(a_1,a_2)$ and $(b_1,b_2)$, form the real sum $a_1+b_1$, and re-pack with Mathlib's add_nonneg applied to the two nonnegativity certificates. No further lemmas are needed.
why it matters
This is the join operation of the canonical scalar work carrier: empty work is zero, join is addition, and every scalar is independent because internal support is empty. It is wired into CanonicalScalarWorkCarrier, canonical_nonnegative_work_scale_composition_model, and the additivity theorem that the first component of the sum is ordinary real addition.
It also feeds the aggregate projection story: independent event joins project to this addition (aggregateScalarWorkProjection_join), and the closure predicate built from it is equivalent to additive ledger composition. The T5-to-T6 self-similarity bridge uses the same carrier, so the operation sits on the path from unique $J$ (T5) to forced $\varphi$ (T6) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.