CanonicalScalarWorkCarrier
plain-language theorem explainer
Packages the algebraic laws that make nonnegative scalar work a commutative monoid under join-as-addition, with empty support, universal independence, and cost equal to the scalar value. Cited by the T5→T6 self-similarity bridge and by the aggregate scalar-work projection that quotients support-bearing events down to pure cost. The declaration is a Prop structure (certificate interface), not a proved theorem; uniqueness is immediate by subsingleton.
Claim. A canonical scalar work carrier is a package of identities on nonnegative work values $W = \{x \in \mathbb{R} : x \ge 0\}$: empty configuration equals $0$; join equals addition; every support is empty (hence pairwise disjoint); disjoint support implies independence, so all pairs are independent; join is commutative and associative with empty as left identity; the canonical cost of $a$ is its underlying real $a_1$; and cost is additive under join.
background
The Unified Forcing Chain module aims to force every landmark T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Mid-chain, recognition events live in a configuration space: empty config, binary join, consistency, and an independence relation (no shared predicates). Cost is a real-valued functional on that space.
Nonnegative work is the subtype ${x:\mathbb{R}\mid x\ge 0}$, the actual range of recognition costs. The scalar carrier treats pure work values as configurations whose internal support is empty, so independence is automatic and join collapses to ordinary addition. The canonical cost simply reads off the underlying real.
Upstream, ConfigSpace supplies the abstract monoid-and-independence interface that these fields instantiate. Related cost and arithmetic canons elsewhere in the stack play the same role for measures and Peano structure; here the target is the additive work monoid used by later bridges.
proof idea
No proof body: this is a structure (Prop bundle) listing eleven field obligations. Each field is a pure equational or relational statement about empty, join, support, independence, and the canonical cost on nonnegative work. A separate theorem canonical_scalar_work_carrier discharges every field by reflexivity or trivial rewriting. Propositional uniqueness is recorded by a Subsingleton instance whose proof is rfl.
why it matters
This certificate is the pure-cost endpoint of the configuration hierarchy. Downstream, AggregateScalarWorkProjection uses it as the quotient target: support-bearing recognition events project by cost onto the scalar carrier, and disjoint-support joins project to scalar addition. The inhabitant canonical_scalar_work_carrier supplies the concrete witness.
It also appears in the T5→T6 self-similarity bridge, which routes unique $J$ (T5: $J(x)=(x+x^{-1})/2-1$) into the forced golden ratio $\varphi$ (T6) via hierarchy dynamics and additive posting. Having a clean additive scalar monoid with cost-equals-value keeps the self-similarity and additive-posting hypotheses from smuggling extra structure. In the forcing chain this is scaffolding for the cost-to-scale step, not a T-step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.