nonnegativeWork_support_disjoint
plain-language theorem explainer
Any two nonnegative scalar work values have disjoint supports, because each support is the empty set of unit coordinates. The result is cited when building the canonical scalar work carrier, which needs configuration independence from support disjointness. The proof is a one-line simplification of the support definition.
Claim. For any two nonnegative real work values $a,b \in \{x \in \mathbb{R} : x \ge 0\}$, the supports $\mathrm{supp}(a)$ and $\mathrm{supp}(b)$ are disjoint as finite sets. (Each support is empty, since scalar work is already an aggregate quantity with no internal coordinates.)
background
In the Unified Forcing Chain, cost values live on nonnegative reals: recognition-work costs cannot be negative, so the domain is the subtype ${x:\mathbb{R}\mid x\ge 0}$ rather than all of $\mathbb{R}$. That subtype is the realizable replacement for an impossible all-real work model and is the domain needed for scale-closure bridges.
Scalar work is already an aggregate quantity. Its support is defined as the empty finite set on the unit type: there are no internal support coordinates to track. Disjointness of supports is the configuration-independence condition used when two work values are joined in a carrier structure.
The ambient module forces T0–T8 from the Recognition Composition Law plus normalization and calibration. This lemma sits in the scalar-work infrastructure that feeds the carrier certificate, not in the T5–T8 uniqueness steps themselves.
proof idea
One-line tactic proof. Unfold the support definition: both supports equal $\emptyset$ as finite sets on $\mathrm{PUnit}$. Empty sets are disjoint, so simp on that definition closes the goal immediately. No external lemmas are required beyond the definitional equality.
why it matters
Feeds canonical_scalar_work_carrier, the certificate that scalar nonnegative work is a valid work carrier (empty joins to zero, join is addition). The next doc-comment states the design intent: "In the canonical scalar work carrier, support disjointness gives configuration independence."
Within the forcing chain this is plumbing, not a T-step: it makes the scalar carrier honest about configuration independence so later cost composition can treat work values as pure aggregates. It does not itself force $\varphi$, the eight-tick octave, or $D=3$, but it keeps the work model aligned with the cost foundation (nonnegative $J$-values) used throughout T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.