ScaleCompositionCanonicality
plain-language theorem explainer
A Prop-valued certificate that a binary operation on real scales is the unique work-extensive scale composition. It packages three facts: the operation is work-extensive (op a b = a + b), it equals ledgerCompose, and any other work-extensive operation agrees with it pointwise. Downstream T5→T6 bridge material and the canonical_scale_composition theorems cite it. As a structure definition there is no proof body beyond field packing.
Claim. For a binary operation $\mathrm{op}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, a scale-composition canonicality certificate is a proposition asserting: (i) $\mathrm{op}$ is work-extensive, i.e. $\mathrm{op}(a,b)=a+b$ for all real $a,b$; (ii) $\mathrm{op}$ coincides with ledger composition $\mathrm{op}(a,b)=a+b$; (iii) $\mathrm{op}$ is unique among all work-extensive binary operations on $\mathbb{R}$.
background
The Unified Forcing Chain module aims to derive T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Between unique $J$ (T5) and forced $\varphi$ (T6) one needs a clean notion of how real scale/work values compose on the ledger.
Work-extensive scale composition is the theorem-facing replacement for silently choosing addition: an operation $\mathrm{op}$ satisfies $\mathrm{op}(a,b)=a+b$ for all reals. The derived ledger composition ledgerCompose is exactly that sum. The present structure packages the claim that any such extensive operation is identical to ledger composition and is unique in that class.
This sits in the scale/self-similarity layer that feeds the T5→T6 bridge: closed observable frameworks with realized hierarchy data force the scale ratio to be $\varphi$, and additive posting of scales is part of that hierarchy data.
proof idea
No mathematical proof: this is a structure definition (a bundled Prop). The three fields are pure data: a WorkExtensiveScaleComposition witness, a pointwise equality to ledgerCompose, and a uniqueness quantifier over other work-extensive operations. A companion Subsingleton instance shows any two certificates for fixed op are propositionally equal by rfl. Actual content is discharged later by canonical_scale_composition, which fills the fields from a work-extensivity hypothesis via work_extensive_scale_composition_eq_ledgerCompose.
why it matters
Canonical scale composition is the additive glue between discrete ledger postings and the self-similar $\varphi$-ladder. Downstream, canonical_scale_composition and canonical_scale_composition_of_recognition_work produce instances from work-extensivity or recognition-work cost additivity; ledgerCompose_canonical records that the existing sum operation is already canonical. The T5→T6 self-similarity bridge structure uses this layer so that hierarchy dynamics (ratio self-similarity and additive posting) are not smuggled past T5 $J$-uniqueness. In the forcing chain this supports T6: $\varphi$ as the self-similar fixed point of discrete ledger scaling, after T5 pins $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.