work_extensive_scale_composition_eq_ledgerCompose
plain-language theorem explainer
Any binary operation on real scales that is work-extensive (composing two work values yields their sum) coincides pointwise with additive ledger composition. Cited when identifying the unique scale-composition law forced by extensivity of recognition work. The proof is a two-step rewrite: unfold the extensivity hypothesis, then match the definition of ledger sum.
Claim. Let $\mathrm{op}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be a binary operation on real scales. If $\mathrm{op}$ is work-extensive, meaning $\mathrm{op}(a,b)=a+b$ for all $a,b\in\mathbb{R}$, then $\mathrm{op}(a,b)$ equals the additive ledger composition of $a$ and $b$ for every pair of reals.
background
In the Unified Forcing Chain, T0–T8 are derived as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). Ledger structure appears at T3 via cost symmetry $J(x)=J(1/x)$, and scale composition is the real-valued operation that combines two ledger scales.
Additive ledger composition is the standard sum on $\mathbb{R}$: composing two scales returns $a+b$. Work-extensive scale composition is the theorem-facing hypothesis that replaces silently choosing addition: an operation $\mathrm{op}$ is work-extensive when composing two scale-as-work values produces the sum of those work values.
This lemma sits between that hypothesis and canonicity of scale composition. It records that work-extensivity already forces equality with the existing additive ledger law, so no other binary law on real work values is available once extensivity is imposed.
proof idea
Term-mode, essentially a one-line identification. Introduce arbitrary reals $a,b$. Rewrite $\mathrm{op},a,b$ by the work-extensivity field of the hypothesis, obtaining $a+b$. Reflexivity then matches the definition of additive ledger composition, which is exactly $a+b$. No further lemmas are required.
why it matters
Feeds directly into canonical_scale_composition, which packages work-extensivity together with equality to additive ledger composition into full canonicity of the scale law. Downstream that canonicity is the bridge from a physical extensivity assumption on recognition work to the unique ledger sum used throughout the forcing chain.
In the T0–T8 narrative this closes a small but sharp gap at the ledger/scale layer (T3–T6 vicinity): one does not postulate addition as composition; one proves that any work-extensive composition is forced to be that sum. That keeps the Complete Inevitability Chain honest about where addition enters, rather than smuggling it in as a definitional choice.
No open scaffold remains here; the claim is fully proved and only serves as a named bridge into canonicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.