canonicalNonnegativeWorkCost
plain-language theorem explainer
Canonical cost on nonnegative work events: the cost equals the work value itself. Anyone assembling the scale-composition model, scalar-work carrier, or the T5-to-T6 self-similarity bridge cites this as the concrete CostFunction on {x : ℝ // 0 ≤ x}. The instance is discharged by subtype nonnegativity plus definitional equality for dichotomy and additivity.
Claim. Let $W = \{x \in \mathbb{R} : x \ge 0\}$. The map $C : W \to \mathbb{R}$ given by $C(a) = a$ is a cost function on $W$: it is nonnegative, satisfies dichotomy (zero cost characterises consistency), and is additive under independent join.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalisation and calibration. Cost is the primitive: configurations carry a nonnegative real measuring recognition work.
A CostFunction on a configuration space is a map $C$ with three axioms: nonnegativity; dichotomy (D), zero cost iff the configuration is consistent; and independent additivity (A), $C$ additive under join of configurations that share no predicates. The domain here is nonnegative work values $W = {x \in \mathbb{R} : 0 \le x}$, the realizable replacement for an all-real model (costs are nonnegative; geometric scales are positive).
This definition packages $W$ itself as the configuration space of scalar work, so the cost is the identity on the underlying real. Downstream results treat it as the canonical recognition-work representation for scale composition and ledger closure.
proof idea
Structure instance, not a deep proof. The cost field is the subtype projection $a \mapsto a.1$. Nonnegativity is the subtype witness $a.2$. Dichotomy and additivity are rfl: once the ConfigSpace operations on $W$ are set so that consistency is zero-cost and join is addition, both axioms hold definitionally.
why it matters
This is the concrete cost carrier that makes the nonnegative recognition-work model inhabit the CostFunction interface. Downstream it is fed into the scale-composition model (canonical_nonnegative_work_scale_composition_model), additivity of composition on values, and the equivalence of nonnegative-work closure with additive ledger composition. It also underwrites the canonical scalar-work carrier (join = addition, empty = zero, cost = scalar value) and the self-projection of that carrier.
In the forcing chain it is a dependency of the T5-to-T6 self-similarity bridge: unique $J$ (T5) must pass through a realizable nonnegative work model before $\varphi$ is forced as the discrete self-similar fixed point (T6). Without a canonical cost on $W$, the scale-closure side of that bridge has no inhabiting instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.