canonical_nonnegative_work_scale_composition_model
plain-language theorem explainer
The nonnegative reals under addition form a recognition-work scale-composition model: each work value is represented by itself under the canonical cost, and addition is both the event composition and the work operation. Anyone building the T5–T6 scale-closure bridge cites this as the concrete carrier. The proof is pure definitional equality (rfl/trivial on each field).
Claim. There exists a recognition-work model on nonnegative work values $\{x\in\mathbb{R}:x\ge 0\}$ in which the canonical cost of the identity embedding of $a$ equals $a$, addition of work values represents scale composition, event composition coincides with the work join, and independent pairs compose without extra cost.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Between unique $J$ (T5) and forced $\varphi$ (T6) one needs a scale-closure bridge: geometric scales must close under a composition that is realized by recognition work.
Recognition costs take values in nonnegative reals, written $\mathrm{NonnegativeWork}={x:\mathbb{R}\mid 0\le x}$. The structure RecognitionWorkNonnegativeScaleCompositionModel packages the realizable domain for that bridge: costs are nonnegative and geometric scales are positive (the all-real model is impossible). Its fields demand that every work value is hit by the cost of a representing event, that work composition is represented by event composition, that compose equals the work join, and that independent pairs add without interaction.
The canonical instance takes events to be the work values themselves, the cost to be the canonical nonnegative-work cost, the representing map to be the identity, and both composition operations to be nonnegative-work addition.
proof idea
Four field obligations, each discharged by a one-line tactic proof. work_value is intro a; rfl (identity embedding has cost equal to the underlying real by definition of the canonical cost). composition_represents and compose_eq_join are likewise rfl once both sides are nonnegative-work addition. independent is trivial on the independence predicate for this carrier. No external lemmas are invoked; the model is definitionally the additive monoid of nonnegative reals.
why it matters
This is the concrete carrier that lets scale closure talk about recognition work rather than an abstract Prop. Downstream, canonical_nonnegative_work_additive reads off extensivity $(a\oplus b)_1=a_1+b_1$ from the model; canonical_nonnegative_work_closure_iff_ledger equates the nonnegative-work closure predicate with ordinary ledger composition, so geometric scale sequences can be checked in either language. Both feed t5_to_t6_bridge_holds, which packages the T5-to-T6 self-similarity bridge (unique $J$ plus realized closed scales force $\varphi$). In the forcing chain this sits between T5 (J-uniqueness via d'Alembert, normalization, calibration) and T6 ($\varphi$ as the self-similar fixed point on the discrete ledger).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.