NonnegativeWork
plain-language theorem explainer
Nonnegative reals are the carrier type for recognition-work costs: every cost value is a real $x$ with $x \ge 0$. Anyone building scale-composition or scalar-work models in the forcing chain cites this domain. The declaration is a one-line subtype abbreviation, not a proved statement.
Claim. Write $\mathrm{NonnegativeWork}$ for the set of real numbers $x$ satisfying $0 \le x$. This is the intended domain of recognition-work (cost) values.
background
The Unified Forcing Chain module derives the full T0–T8 ladder from the Recognition Composition Law plus normalization and calibration. Costs live on configuration spaces; the cost functional returns a real that must be nonnegative by construction.
Earlier attempts to treat work as an unrestricted real fail the scale-closure bridge: geometric scale factors are positive, and recognition-work costs cannot go negative. The natural domain is therefore the closed half-line of nonnegative reals, packaged as a subtype so that nonnegativity is part of the type.
Downstream, this carrier supports the canonical cost that reads off the scalar itself, additive join of work values, and projections from arbitrary costed events onto a single nonnegative work coordinate.
proof idea
No proof. The declaration is a definitional abbreviation: the subtype ${x : \mathbb{R} \mid 0 \le x}$. Lean treats it as definitional equality with that subtype, so all subsequent lemmas about nonnegative work are ordinary subtype reasoning (projection to the real and the inequality witness).
why it matters
This type is the realizable replacement for an all-real work model inside the forcing chain. It feeds the canonical nonnegative-work cost (cost equals the scalar), the additive composition theorems, the scale-composition model, the canonical scalar-work carrier, and the aggregate scalar-work projection from any costed event.
Those objects sit under the cost-foundation half of the chain (T0 logic-from-cost through T5 unique $J$), where every cost value must stay nonnegative and compose under the Recognition Composition Law. Without a typed nonnegative carrier, the scale-closure bridge and the uniqueness statements for work composition cannot even be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.