nonnegativeWork_independent_of_support_disjoint
plain-language theorem explainer
Support-disjoint nonnegative work values are independent configurations in the cost-from-distinction configuration space. Anyone building the canonical scalar work carrier cites this bridge from support geometry to ConfigSpace independence. The proof is a one-line trivial discharge: on this carrier, independence is definitionally support disjointness.
Claim. If $a$ and $b$ are nonnegative real work values and their supports are disjoint, then $a$ and $b$ are independent configurations in the cost-from-distinction configuration space.
background
The Unified Forcing Chain derives T0–T8 as forced consequences of the Recognition Composition Law with normalization and calibration. This declaration sits in the scalar-work specialization of that chain: cost values live on nonnegative reals rather than an all-real model.
Nonnegative work is the subtype ${x:\mathbb{R}\mid 0\le x}$, the realizable domain of recognition-work costs. A configuration space supplies an empty configuration, a binary join, a consistency predicate, and an independence relation (no shared predicates). The support of a work value records which coordinates it occupies; disjoint supports mean the two values share no active coordinates.
Upstream, ConfigSpace is the abstract structure used throughout cost-from-distinction arguments. Independence there is the relation this theorem instantiates for the scalar carrier. Nearby aggregate and registry machinery is not required for the discharge itself.
proof idea
The goal is configuration independence of $a$ and $b$, given disjoint supports. On the nonnegative-work instance of the configuration-space structure, independence is definitionally (or immediately) that support-disjointness predicate. The single tactic trivial closes the goal; no named lemmas are applied. The unused hypothesis name underscores that the proof is pure definitional matching.
why it matters
This is local plumbing for the canonical scalar work carrier. Downstream, canonical_scalar_work_carrier packages empty-as-zero and join-as-add for nonnegative work, and canonical_scalar_work_self_projection shows the aggregate scalar carrier projects to itself by identity of scalar cost. Both need a clean independence relation so disjoint contributions join without shared predicates.
In the forcing chain the result supports the cost foundation under T0 (logic from cost minimization) and the ledger steps that later force unique $J$ and $\varphi$: additive joins of independent nonnegative work pieces are the scalar model those arguments run on. It does not itself force T5–T8, pin $\varphi$, or set $D=3$; it certifies the carrier those steps use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.