canonical_scale_composition
plain-language theorem explainer
Any binary operation on real scales that is work-extensive (op a b = a + b) is the unique canonical scale composition, identical to ledgerCompose. Cited when closing the T5–T6 self-similarity bridge and when certifying that recognition-work additivity forces the ledger composition law. The proof packages two prior lemmas: equality to ledgerCompose and uniqueness among work-extensive ops.
Claim. Let $\mathrm{op}:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfy work-extensivity: $\mathrm{op}(a,b)=a+b$ for all $a,b\in\mathbb{R}$. Then $\mathrm{op}$ is canonical as a scale composition: it equals the ledger composition operation, and it is the unique work-extensive binary operation on scales.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Scale composition sits between the ledger (T3) and the self-similarity step that forces $\varphi$ (T6).
Work-extensive scale composition is the structure asserting that composing two real scale/work values yields the sum of those work values: $\mathrm{op},a,b=a+b$. It is the theorem-facing replacement for silently taking addition as ledger composition. Canonicality packages three facts: the operation is work-extensive; it equals ledgerCompose from the $\varphi$-forcing derived layer; and it is unique among all work-extensive operations.
Upstream, recognition-work and J-cost models treat cost of events as additive under composition. The present statement abstracts that additivity to pure real arithmetic so later bridges need only the work-extensive hypothesis.
proof idea
Tactic-mode structure construction. The work_extensive field is the given hypothesis. Equality to ledger composition is discharged by the lemma work_extensive_scale_composition_eq_ledgerCompose applied to $h$. Uniqueness is a short intro on a rival operation $\mathrm{op}'$ with the same work-extensivity, then work_extensive_scale_composition_unique h h'. No new arithmetic is proved here; the theorem is the certificate assembler.
why it matters
This certificate is the hinge from work additivity to a unique scale law. Downstream, canonical_scale_composition_of_recognition_work lifts recognition-work cost additivity to the same canonical operation; ledgerCompose_canonical specializes the result to the existing ledger compose map. Both feed t5_to_t6_bridge_holds, which states that the T5-to-T6 self-similarity bridge is theorem-backed once J-uniqueness is available.
In the forcing chain, T5 pins $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger. Canonical scale composition is what makes “closed scale under composition” a well-defined, unique operation rather than a modeling choice, so hierarchy dynamics can force $\varphi$ without an extra axiom choosing addition.
No open scaffold remains on this declaration: claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.