canonical_scalar_work_self_projection
plain-language theorem explainer
The canonical nonnegative scalar-work carrier is an aggregate scalar projection of itself: disjoint-support joins add costs, and projection recovers cost by identity. Anyone wiring the T5→T6 self-similarity bridge cites this as the base scalar case. The proof is a direct term application of the general projection constructor with the nonnegative-work support-independence fact.
Claim. Let events be nonnegative reals $\{x\in\mathbb{R}:x\ge 0\}$, atoms the unit type, $\kappa$ the canonical nonnegative work cost, and $\mathrm{supp}$ the canonical support map. Then the aggregate scalar-work projection certificate holds: support-disjoint events are cost-independent, and for every event $e$ the scalar projection recovers $\kappa(e)$ exactly.
background
Module UnifiedForcingChain forces the full T-1…T8 inevitability ladder from the Recognition Composition Law plus normalization and calibration. Near T5–T6 one needs a clean scalar work carrier so that hierarchy and closed-scale arguments can treat cost as ordinary nonnegative addition.
NonnegativeWork is the subtype ${x:\mathbb{R}\mid 0\le x}$, the realizable domain of recognition-work values (geometric scales stay positive). AggregateScalarWorkProjection is the quotient certificate: support-bearing events project canonically to that scalar carrier by cost, and disjoint-support joins project to scalar addition. Its two fields are support-independence (disjoint supports imply cost independence) and cost preservation under projection.
Upstream, aggregate_scalar_work_projection builds any such certificate from a cost function plus a SupportDisjointIndependence witness. The present theorem specializes that constructor to the canonical nonnegative-work cost and support.
proof idea
Term-mode one-liner. Apply the general constructor aggregate_scalar_work_projection to canonicalNonnegativeWorkCost, supplying the packaged independence hypothesis ⟨nonnegativeWork_independent_of_support_disjoint⟩. The constructor fills both structure fields (support independence and project-cost identity), so no further case analysis is needed.
why it matters
This pins the base scalar case of aggregate work: the carrier projects to itself by identity of scalar cost. Downstream it is consumed by T5_To_T6_SelfSimilarity_Bridge and the theorem t5_to_t6_bridge_holds, which route T5 J-uniqueness into T6 φ-forcing via internal hierarchy dynamics and realized closed scale. Without a certified scalar projection, the self-similarity bridge would lack a cost-additive normal form on which φ can be forced as the unique scale ratio. In the primer chain this sits between T5 (unique $J(x)=(x+x^{-1})/2-1$) and T6 (φ as self-similar fixed point), keeping the complete inevitability claim free of a hidden scalar-work gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.