WorkExtensiveScaleComposition
plain-language theorem explainer
A binary operation on real scale/work values is work-extensive when it equals ordinary addition on every pair. Anyone proving that ledger composition is canonical, or that scale-closure is independent of the chosen op, cites this Prop interface. It is a one-field structure packaging the equation op(a,b)=a+b, the theorem-facing stand-in for silently hard-coding addition.
Claim. A binary operation $\mathrm{op}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ is work-extensive when $\mathrm{op}(a,b)=a+b$ for all $a,b\in\mathbb{R}$. Equivalently: composing two scale-as-work values yields the sum of their work values.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law, normalization, calibration). In that setting, scales live on the $\varphi$-ladder and are treated as real work values; composing two independent events must induce a real binary operation on those values.
Upstream, a cost function on a configuration space satisfies dichotomy (zero cost iff consistency) and independent additivity: cost of a join of predicate-disjoint configurations is the sum of costs. The Recognition Composition Law is the multiplicative d'Alembert equation on the analytic cost $F$. When scale is identified with recognition work, additivity of cost forces the induced real operation to be addition.
This structure is the explicit, theorem-facing packaging of that extensivity requirement. It replaces an earlier habit of silently taking ledger composition to be $+$.
proof idea
Definitional Prop-structure, not a proved theorem. A single field work_extensive asserts $\forall a,b,,\mathrm{op}(a,b)=a+b$. Inhabitants are built by supplying a proof of that equation (often rfl when op is definitionally addition, as for the standard ledger compose). Downstream lemmas then consume the structure as a hypothesis.
why it matters
Sits on the T5→T6 self-similarity bridge path: scale composition must be fixed before self-similar fixed-point forcing of $\varphi$ (T6) can be stated without a hidden choice of operation. Downstream, it is the hypothesis of canonical scale composition (any work-extensive op is canonical), of the uniqueness and equality-to-ledger-compose theorems, and of the iff relating scale-closure predicates under a general op versus ledger compose. The standard ledger compose is shown to inhabit it by reflexivity. It also receives the implication from recognition-work scale models: cost additivity on independent event join forces this Prop. In short, it makes the "addition is the only extensive scale compose" step auditable rather than ambient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.