nonnegativeWorkConfigSpace
plain-language theorem explainer
Nonnegative real work values form a configuration space: empty is zero, join is addition, consistency means zero work, and independence holds automatically. Anyone wiring cost-from-distinction models onto the actual domain of recognition costs cites this carrier. The instance discharges monoid and consistency laws by ordinary real arithmetic and nonnegativity.
Claim. The subtype $\{x\in\mathbb{R}:x\ge 0\}$ carries a configuration-space structure: empty configuration $0$, join by addition, consistency predicate $a=0$, and independence the constantly-true relation. Join is a commutative monoid with identity $0$; the empty configuration is consistent and independent of every configuration; and consistency of a join of independent parts forces each part consistent (and conversely, inconsistency of a left summand forces the join inconsistent).
background
The Unified Forcing Chain module aims to derive the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). Early steps need concrete configuration carriers on which cost-from-distinction can act.
A configuration space (CostFromDistinction.ConfigSpace) is an abstract type with empty configuration, binary join, a consistency predicate, and an independence relation, obeying commutative-monoid laws for join, symmetry of independence, and the usual consistency/independence interaction rules.
NonnegativeWork is the subtype of nonnegative reals: the realizable domain of recognition-work costs (as opposed to an impossible all-real model). Geometric scales are positive and costs are nonnegative, so this is the carrier needed for scale-closure bridges. The present instance equips that subtype with the canonical configuration-space structure used by later cost and logic-forcing constructions.
proof idea
Field-by-field instance construction. Empty is the subtype pair $\langle 0,_\rangle$. Join is the preexisting nonnegative addition map. Consistency is equality of the underlying real to zero; independence is constantly True, so its symmetry and empty-independence goals are trivial.
Monoid laws (join commutative, associative, empty identity) reduce via Subtype.ext and simp with add_comm / add_assoc on the underlying reals. Consistency of a join of consistent parts is $0+0=0$. The nontrivial direction uses nonnegativity of both summands: if the join is consistent (sum zero) and the left summand is assumed inconsistent (nonzero), nlinarith plus le_antisymm forces the left value to zero, contradicting inconsistency.
why it matters
In the forcing chain, T0 (logic forced from cost minimization: consistency is cheap) and the absolute-floor layer need a honest event carrier whose values are actual nonnegative work, not an abstract placeholder. This instance is that carrier: cost can be read off as the value itself (the following canonical cost definition), join is additive work, and only the zero-work event is consistent.
It sits among the bool-floor and recognition-cost siblings that seed T0_Logic_Forced and the analytic-cost refinement. No downstream users are recorded yet in the graph, so its role is infrastructural: close the gap between the abstract ConfigSpace API and the real-valued work domain demanded by RCL, J-cost, and the later T5–T6 uniqueness/self-similarity steps. Without a nonnegative carrier, scale-closure and cost-minimization arguments cannot be stated on the physical domain of the theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.