nonnegativeWorkSupport
plain-language theorem explainer
Scalar nonnegative work values carry empty internal support: their support finset is always empty. Anyone building the canonical scalar work carrier or proving support-disjoint independence cites this. The definition is a constant empty finset on the unit type, encoding that aggregate work has no configuration coordinates.
Claim. For every nonnegative work value $w \in \{x \in \mathbb{R} : x \ge 0\}$, the internal support of $w$ is the empty finite set of unit points: $\mathrm{supp}(w) = \emptyset \subseteq \mathbf{1}$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. In that setting, cost values live on nonnegative reals: nonnegative work is the subtype ${x:\mathbb{R}\mid x\ge 0}$, the realizable domain of recognition-work costs (geometric scales stay positive).
Config-space machinery from CostFromDistinction treats configurations with supports and independence under disjoint support. Scalar work is already an aggregate quantity, so it has no internal support coordinates to track. This definition supplies that empty support map, so later lemmas can treat every pair of scalar works as support-disjoint by construction.
proof idea
Pure definitional assignment: ignore the work argument and return the empty finset on PUnit. No lemmas or tactics; the body is the constant empty set. Downstream proofs (e.g. support-disjointness) simply unfold this definition and simplify.
why it matters
Feeds the canonical scalar work carrier (join as addition, empty support, cost equal to the scalar) and the self-projection theorem that the carrier projects to itself by identity of scalar cost. Direct consumers include the theorems that any two scalar works have disjoint supports and that disjoint support yields configuration independence (both trivial once support is empty).
That carrier infrastructure sits under the T5→T6 self-similarity bridge: unique $J$ (T5: $J(x)=(x+x^{-1})/2-1$) plus realized hierarchy forces $\varphi$ as the self-similar ratio (T6). Empty scalar support is the bookkeeping that lets aggregate work compose additively without smuggling configuration dependence into the $\varphi$ layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.