nonnegative_work_composition_unique
plain-language theorem explainer
Any two binary operations on nonnegative work that both realize recognition-work composition for the same cost function and event embedding must coincide pointwise. Scale-closure and ledger-bridge arguments cite this uniqueness. The proof reduces both operations to ordinary addition of the underlying reals via the model's extensivity lemma, then uses subtype equality.
Claim. Let $\kappa$ be a cost function on a configuration space of events. Fix an embedding of nonnegative work values into events and a binary event composition. If $\oplus$ and $\oplus'$ are two binary operations on nonnegative work $\{x\in\mathbb{R}:x\ge 0\}$ that both satisfy the recognition-work nonnegative scale composition model axioms relative to $\kappa$, the embedding, and event composition, then $\oplus(a,b)=\oplus'(a,b)$ for all nonnegative work values $a,b$.
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the cost foundation (Recognition Composition Law plus normalization and calibration). Nonnegative work is the subtype ${x:\mathbb{R}\mid 0\le x}$: the actual codomain of recognition costs.
A configuration space supplies empty config, join, consistency, and independence. A cost function $\kappa$ on it obeys dichotomy (cost zero iff consistent) and independent additivity. The recognition-work nonnegative scale composition model packages the realizable bridge: each nonnegative work value is hit by $\kappa$ on a designated event, and the abstract work operation is represented by event composition. This replaces an impossible all-real model; costs are nonnegative and geometric scales are positive.
Upstream, CostFunction and ConfigSpace fix the recognition-work axioms; the model structure records the representation equalities needed for scale closure.
proof idea
Term-mode, two steps after introducing $a,b$. Apply subtype extensionality so it suffices to equate the underlying reals. Rewrite both $\mathrm{op},a,b$ and $\mathrm{op}',a,b$ by the lemma that any recognition-work model is extensive: the model's operation equals ordinary addition of the real components. The two rewrites yield the same sum, hence the subtypes agree. No case split; uniqueness is inheritance from uniqueness of real addition once extensivity is available for both models.
why it matters
Uniqueness of nonnegative work composition is the algebraic hygiene step for the scale-closure bridge inside the complete inevitability chain. Once recognition-work costs live on the nonnegative reals and event composition represents work composition, there is only one candidate binary operation: addition. That pins the monoid structure used when lifting cost additivity toward ledger and $\varphi$-ladder constructions (T3–T6 in the forcing chain).
The module's stronger claim is that T0–T8 are forced from RCL plus normalization and calibration; this lemma ensures the work monoid is not an extra choice. No downstream uses are recorded yet in the graph, so it presently serves as a local uniqueness fact for subsequent canonical-addition and scale-bridge declarations in the same file rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.