nonnegative_work_extensive_of_recognition_work_model
plain-language theorem explainer
Any recognition-work model on nonnegative work values forces the binary composition of those values to be ordinary addition. Anyone building the T5–T6 scale-closure or uniqueness-of-composition arguments cites this. The proof equates the cost of the composed event to the sum of costs via independent additivity of κ, then finishes by linear arithmetic.
Claim. Let $E$ be a configuration space with cost function $\kappa$. Fix a representation of nonnegative work values by events, an event composition, and a binary operation $\oplus$ on nonnegative work, such that the data form a recognition-work nonnegative scale-composition model. Then for all nonnegative work values $a,b$, the underlying real of $a \oplus b$ equals $a + b$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration). The present lemma sits in the nonnegative-work layer that replaces an impossible all-real composition model: recognition costs are nonnegative, so the domain is {x : ℝ // 0 ≤ x}.
A configuration space supplies empty config, join, consistency, and independence. A cost function $\kappa$ obeys dichotomy (cost zero iff consistent) and independent additivity: cost of a join of independent configs is the sum of costs. The recognition-work model packages: each nonnegative work value is realized by an event of that cost; composition of work values is represented by event composition; event composition agrees with join on independent pairs; and the represented pairs are independent.
Upstream, CostFunction is exactly the recognition-work bridge with axioms (D) and (A). That additivity is what pins the numerical composition law here.
proof idea
Fix nonnegative work values $a,b$. Start from the model’s work-value identity for $a \oplus b$. Rewrite the left-hand side using the two representation axioms: composition of work is represented by event composition, and that composition equals the config-space join. Independent additivity of $\kappa$ on the pair of work-events (independence is part of the model) then yields $\kappa(\mathrm{join}) = \kappa(\mathrm{workEvent},a) + \kappa(\mathrm{workEvent},b)$. Substitute the work-value identities for $a$ and $b$, and close with linarith. No external lemmas beyond the model fields and $\kappa$.additivity.
why it matters
This is the extensivity step that turns abstract recognition-work composition into ordinary addition on values. Downstream it discharges canonical_nonnegative_work_additive (the canonical model is additive), feeds nonnegative_work_composition_unique (any two such ops agree), and equates the nonnegative scale-closure predicate with ledger composition in scaleClosureAtWithNonnegative_iff_ledgerCompose.
That scale-closure package is consumed by t5_to_t6_bridge_holds, the theorem-backed T5→T6 self-similarity bridge. In the forcing chain, T5 is unique $J$ and T6 forces $\varphi$ as the self-similar fixed point; without additive nonnegative work, the closed-scale route to $\varphi$ does not connect. The lemma is therefore a small but load-bearing link between cost additivity and the $\varphi$-forcing half of the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.