AggregateScalarWorkProjection
plain-language theorem explainer
A Prop certificate that support-bearing recognition events project canonically onto the nonnegative scalar work carrier by cost, with disjoint-support joins mapping to scalar addition. Anyone building the T5–T6 self-similarity bridge or support-event aggregation cites it. It is a definitional structure (four fields) with a trivial Subsingleton instance, not a proved theorem.
Claim. Fix event type $E$ with a configuration-space structure, cost $\kappa$, atoms $A$, and support map $s:E\to\mathrm{Finset}\,A$. An aggregate scalar work projection is a proposition asserting: (i) disjoint supports imply configuration independence; (ii) the scalar projection of each $e$ has cost equal to $\kappa(e)$; (iii) if $s(a)\cap s(b)=\emptyset$, the projection of the join $a\vee b$ equals the nonnegative sum of the projections; (iv) the target carrier is the canonical scalar work carrier (join $=$ addition, empty $=$ zero, empty supports).
background
The module UnifiedForcingChain forces the full T-1 through T8 stack from the Recognition Composition Law plus normalization and calibration. Mid-chain one needs a clean quotient from support-bearing events down to a pure scalar work value, so that self-similarity and hierarchy dynamics see only additive costs.
A configuration space supplies empty configuration, join, and an independence relation. A cost function $\kappa$ assigns a real cost to each event. Support-disjoint independence says that whenever two events have disjoint atom supports, they are independent in the configuration sense. The canonical scalar work carrier is the nonnegative reals under addition: empty is zero, join is sum, every scalar has empty internal support, and cost is the scalar itself.
Upstream, recognition events (source, target, positive ratio) and aggregate costs (sums of weighted ratios, or exponential aggregates in $n$ dimensions) motivate treating total work as a scalar. This structure packages the projection axioms that make that abstraction rigorous.
proof idea
No proof body: the declaration is a four-field Prop structure. The fields are pure interface: support independence, cost preservation under projection, join-to-addition for disjoint supports, and canonicity of the scalar target. A companion Subsingleton instance proves any two certificates for the same data are propositionally equal by rfl (all fields are Props). Actual inhabitants are built later by aggregate_scalar_work_projection from a SupportDisjointIndependence hypothesis, and by specialized constructors for the canonical scalar carrier and support-event carriers.
why it matters
This certificate is the quotient/abstraction step that lets the forcing chain treat multi-atom events as pure scalar work when supports are disjoint. Downstream, aggregate_scalar_work_projection constructs instances from support compatibility; canonical_scalar_work_self_projection shows the scalar carrier projects to itself by identity; supportEvent_aggregate_scalar_projection and SupportEventAggregateProjection specialize to finite-support cardinality costs. The T5→T6 self-similarity bridge consumes this surface so hierarchy dynamics and $\varphi$-forcing see additive scalar postings rather than raw event geometry. In the primer landmarks, that bridge is exactly the passage from unique $J$ (T5) to $\varphi$ as the self-similar fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.