aggregateScalarWorkProjection_join
plain-language theorem explainer
Independent configuration joins project to ordinary addition of scalar recognition work. Anyone assembling the aggregate scalar-work certificate in the unified forcing chain cites this identity. The argument is a one-step subtype unwrap that hands the goal to the cost function's independent-additivity axiom.
Claim. Let $\mathcal{E}$ be a configuration space with cost function $\kappa$. For independent configurations $a,b\in\mathcal{E}$, the aggregate scalar work projection of the join equals the nonnegative sum of the projections of the factors: $\pi_\kappa(a\ast b)=\pi_\kappa(a)\oplus\pi_\kappa(b)$.
background
A configuration space (CostFromDistinction) is an abstract type with empty config, binary join, a consistency predicate, and an independence relation meaning the factors share no predicates. Join is a commutative monoid with empty as identity; independence is symmetric and empty is independent of everything.
A cost function $\kappa$ on that space takes nonnegative real values and obeys two bridge axioms: dichotomy (cost is zero iff the config is consistent) and independent additivity ($\kappa(a\ast b)=\kappa(a)+\kappa(b)$ whenever $a$ and $b$ are independent). Aggregate scalar work projection packages $\kappa.C$ as a nonnegative subtype; nonnegative work addition is the corresponding subtype sum.
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration, starting from the absolute floor and logic-from-cost.
proof idea
Term-mode proof in three micro-steps. First apply subtype extensionality so equality of projected works becomes equality of underlying reals. A change rewrites the goal to $\kappa.C(a\ast b)=\kappa.C(a)+\kappa.C(b)$. That is exactly the independent-additivity field of the cost function, applied to $a$, $b$, and the given independence hypothesis. No further lemmas are needed.
why it matters
Downstream parent is the certificate constructor aggregate_scalar_work_projection, whose doc-comment reads: construct the aggregate scalar projection certificate from support compatibility. This join law is the monoid-homomorphism clause that certificate needs: under support-disjoint independence, projected work of a join is the sum of projected works.
In the forcing chain that packages recognition cost into a scalar work layer above the absolute floor and T0 (logic from cost minimization). Without join-to-sum compatibility, aggregate projection would not respect independent composition, and the work/Hamiltonian lift from the cost foundation would fail at the first binary step. It does not itself touch T5 J-uniqueness or later $\varphi$/octave steps; it only secures additivity of the scalar work packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.