canonical_scale_composition_of_recognition_work
plain-language theorem explainer
Recognition-work cost additivity forces any real scale-composition law that represents event composition to be the unique work-extensive operation, namely ledger composition. The T5-to-T6 self-similarity bridge cites this to pin how closed scales compose under the unique J-cost. Proof is a one-line term application of the general canonical-scale-composition theorem to work-extensivity extracted from the recognition-work model.
Claim. Let $Event$ be a configuration space with cost $\kappa$. Suppose each real $a$ is realized by an event of cost $a$, event composition represents a binary operation $op$ on reals, and these data form a recognition-work scale-composition model. Then $op$ is work-extensive, equals ledger composition on $\mathbb{R}$, and is the unique work-extensive scale composition.
background
The module builds the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law, normalization, calibration). Here the local concern is how real-valued recognition work composes when events are joined.
A configuration space supplies empty config, join, consistency, and independence. A cost function $\kappa$ obeys dichotomy (zero cost iff consistent) and independent additivity. The recognition-work scale-composition model packages three maps: each real work value $a$ is an event of cost $a$; event composition represents a real operation $op$; and the model axioms tie those together. Doc-comment on the model: if composition is configuration join on independent events, additivity forces $op(a,b)=a+b$.
Canonicality for a scale operation means three facts: work-extensivity, equality with ledgerCompose from the phi-forcing layer, and uniqueness among work-extensive ops. That ledger law is the discrete self-similar composition used when T5's unique $J$ feeds T6.
proof idea
One-line term proof. From the recognition-work model and cost $\kappa$, apply work_extensive_of_recognition_work_scale_model to obtain that $op$ is work-extensive. Feed that certificate into canonical_scale_composition, which returns the full ScaleCompositionCanonicality package: work-extensivity, pointwise equality with ledger composition, and uniqueness among work-extensive real operations. No extra case analysis; the model axioms already encode the additivity bridge.
why it matters
Sits on the T5-to-T6 bridge inside the unified forcing chain. Downstream, t5_to_t6_bridge_holds records that the self-similarity bridge is theorem-backed once T5 uniqueness is in hand; closed-scale composition must be the canonical ledger law so that the self-similar fixed point $\varphi$ is forced (T6 in the primer: $\varphi$ as the self-similar fixed point of the discrete ledger).
Without a unique work-extensive scale composition, competing real ops could realize different rung multiplications and the phi-ladder would not be forced. The doc-comment states the moral directly: recognition-work cost additivity gives the canonical scale composition, and the existing ledger composition is that law. This closes a foundation step between unique $J$ (T5, RCL plus calibration) and forced $\varphi$ (T6), rather than assuming how work values multiply across scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.