ledgerCompose_canonical
plain-language theorem explainer
Addition of real scales is the unique work-extensive scale composition, certified by the canonicality structure. Anyone building the T5–T6 self-similarity bridge cites this to pin ledger composition as ordinary sum. The proof is a one-line application of the general canonicality theorem to the fact that ledger composition is work-extensive.
Claim. The binary operation $(a,b)\mapsto a+b$ on real scales satisfies the canonicality certificate: it is work-extensive, equals the ledger scale composition, and is the unique work-extensive scale composition.
background
In the Unified Forcing Chain, T0–T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Between T5 (unique $J$) and T6 ($\varphi$ forced by self-similarity), one needs a precise notion of how discrete ledger scales compose.
Ledger scale composition is defined as ordinary addition: $\mathrm{ledgerCompose}(a,b)=a+b$. Work-extensivity is the structural property that composing scales adds their work contributions. The structure ScaleCompositionCanonicality packages three facts for an operation $\mathrm{op}$: it is work-extensive, it equals ledger composition pointwise, and it is unique among work-extensive operations.
Upstream, ledgerCompose_work_extensive records that addition is work-extensive (by reflexivity of equality on the work identity). The general theorem canonical_scale_composition then lifts any work-extensive operation to a full canonicality certificate.
proof idea
One-line term proof. Apply canonical_scale_composition to the hypothesis ledgerCompose_work_extensive. That general theorem fills the three fields of the canonicality structure: it reuses the work-extensivity witness, proves pointwise equality with ledger composition via the uniqueness lemma for work-extensive ops, and records uniqueness among all such ops.
why it matters
This pins the ledger's scale algebra as ordinary addition and as the unique work-extensive choice. Downstream, t5_to_t6_bridge_holds uses it inside the T5-to-T6 self-similarity bridge: once $J$ is unique (T5), closed scale composition must be the canonical sum, which forces the self-similar fixed point $\varphi$ (T6 in the forcing chain).
In the module's stronger claim, every step from absolute floor through T8 is forced rather than merely compatible. Canonical scale composition is the algebraic hinge that lets discrete ledger hierarchy produce $\varphi$ without an extra composition axiom. It does not itself derive $\varphi$ or the eight-tick octave; those land later in the bridge and in T7–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.