canonical_scalar_work_carrier
plain-language theorem explainer
Nonnegative scalar work values form a canonical commutative additive work carrier: empty is zero, join is addition, supports are empty (hence independent), and cost equals the scalar itself. Cited by anyone assembling the aggregate scalar-work projection or the T5-to-T6 self-similarity bridge. The proof discharges the structure fields by reflexivity plus the monoid and additivity lemmas already proved for configuration space and nonnegative work cost.
Claim. The nonnegative work values, with empty configuration as zero and join as addition, satisfy the canonical scalar work-carrier axioms: empty equals zero work; join equals scalar addition; every support is empty; independence holds for all pairs via support-disjointness; join is commutative and associative with empty as identity; and the cost equals the scalar value and is additive on independent pairs.
background
The Unified Forcing Chain module derives T0 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. Inside that chain one needs a concrete work carrier on which cost is literally the scalar value, so that later projections and self-similarity arguments can treat work additively without residual support structure.
A configuration space (from CostFromDistinction) is a commutative monoid of configurations with empty unit, a join, a consistency predicate, and an independence relation. Nonnegative work is the subtype of nonnegative reals used as scalar work events. The canonical cost on those events is the projection $C(a)=a$ itself (canonicalNonnegativeWorkCost), already known to be nonnegative and additive once independence is granted.
The structure CanonicalScalarWorkCarrier packages exactly the claim that this scalar setup is a commutative additive work carrier: join is addition, zero is empty, supports are empty (so all pairs are independent), and cost equals the scalar value.
proof idea
Structure-field discharge, mostly reflexivity. emp_eq_zero, join_eq_add, support_empty, and cost_eq_value are definitional (rfl). support_disjoint and independent_of_support are the preexisting lemmas nonnegativeWork_support_disjoint and nonnegativeWork_independent_of_support_disjoint; all_independent is nonnegativeWork_universal_independence. join_comm, join_assoc, and emp_join are the ConfigSpace monoid laws. cost_additive applies canonicalNonnegativeWorkCost.additivity at the universal-independence hypothesis for the two arguments.
why it matters
This certificate is the concrete scalar instance that later forcing steps treat as the work carrier. Downstream, aggregate_scalar_work_projection builds the aggregate scalar projection certificate from support compatibility on top of it. The same carrier feeds T5_To_T6_SelfSimilarity_Bridge and the theorem t5_to_t6_bridge_holds, which route T5 J-uniqueness into the self-similarity that forces $\varphi$ (T6 in the forcing chain).
In the primer landmarks this sits between T5 (unique $J(x)=\cosh(\log x)-1$) and T6 ($\varphi$ as the self-similar fixed point). Without a proved scalar work carrier, the hierarchy-dynamics bridges would have no additive cost object on which closed-scale self-similarity can act. The declaration closes that scaffolding gap inside the complete inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.