ledgerCompose_work_extensive
plain-language theorem explainer
The ledger scale-composition map on reals is work-extensive: composing two scale values yields the sum of their work values. Anyone citing the canonicality of ledger composition, or the T3–T6 ledger/φ forcing steps, needs this instance. The proof is a one-line definitional check: the operation is literally addition.
Claim. The binary operation $\mathrm{ledgerCompose}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfies work-extensive scale composition: for all $a,b\in\mathbb{R}$, $\mathrm{ledgerCompose}(a,b)=a+b$. Equivalently, it is an instance of the structure requiring that composition of two scale/work values produces the sum of those work values.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). Ledger structure sits at T3 (cost symmetry $J(x)=J(1/x)$) and feeds T4–T6 (recognition, unique $J$, and $\varphi$ from self-similarity on a discrete ledger).
Work-extensive scale composition is the theorem-facing interface that replaces silently taking addition as the ledger operation: a binary op on reals is work-extensive when $\mathrm{op}(a,b)=a+b$ for all real scale/work values $a,b$. Upstream, ledgerCompose is defined exactly as that sum. Related scale notions (phi-powers, action scaling) appear elsewhere but are not needed here; only the real binary op matters.
This instance packages the definitional fact so later uniqueness/canonicity theorems can quantify over the structure rather than hard-code addition.
proof idea
Term-mode instance construction for WorkExtensiveScaleComposition on PhiForcingDerived.ledgerCompose. The single field work_extensive is proved by introducing $a,b$ and closing with rfl: by definition ledgerCompose a b is a + b, so the required equality holds definitionally. No lemmas are applied.
why it matters
Feeds ledgerCompose_canonical, which states that the existing ledger composition is the canonical scale composition via canonical_scale_composition applied to this instance. That canonicity step is how the chain avoids an ad hoc choice of addition when forcing ledger structure (T3) and the self-similar fixed point $\varphi$ (T6) on discrete scales.
In the forcing narrative, work-extensivity is the observable content of composing recognition-work values: total work adds under composition. Pinning the concrete op to that law lets uniqueness results treat ledger composition as forced rather than stipulated. No open scaffold remains here; the claim is fully proved and only definitional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.