canonical_support_event_aggregate_projection
plain-language theorem explainer
For any atom type with decidable equality, the canonical support-event construction carries both a support-induced configuration space and a scalar aggregate-work projection by finite-support cardinality. Anyone assembling the T5–T6 self-similarity bridge or support-quotient compatibility cites this packing certificate. The proof is a two-field term constructor wiring the two already-proved surfaces.
Claim. For every type $\mathrm{Atom}$ with decidable equality, the canonical support-event carrier admits a joint certificate: independence is exactly disjoint finite support, and projection to scalar aggregate work is by finite-support cardinality (via the support cost and support map).
background
The Unified Forcing Chain module aims to force the full T0–T8 ladder from the Recognition Composition Law plus normalization and calibration. Mid-chain, events must be reduced to finite atomic supports so that cost aggregates and independence relations become combinatorial.
A support-induced configuration space asserts that two events are independent precisely when their supports are disjoint, and that this disjointness yields the independence law used by the cost foundation. Separately, an aggregate scalar-work projection says that total work on a support-event is the scalar obtained from finite-support cardinality under the support cost and support map.
SupportEventAggregateProjection packages those two surfaces as a single Prop-valued certificate on the same canonical support-event construction. Upstream, canonical_support_induced_config_space already supplies the independence half, and supportEvent_aggregate_scalar_projection supplies the cardinality projection half.
proof idea
Term-mode structure inhabitant. The support_induced field is filled by canonical_support_induced_config_space Atom (itself built from the disjoint-support independence lemmas). The aggregate_projection field is filled by supportEvent_aggregate_scalar_projection Atom, which applies the generic aggregate_scalar_work_projection to SupportEvent.supportCost. No further rewriting or case analysis.
why it matters
This certificate is the joint surface that later steps treat as one object rather than two parallel lemmas. Downstream, support_quotient_compatibility builds the support-quotient compatibility certificate from source-side compatibility surfaces, of which this packing is the aggregate-projection half. It also feeds t5_to_t6_bridge_holds, the theorem-backed T5-to-T6 self-similarity bridge: once J is unique (T5), discrete ledger self-similarity forces $\varphi$ (T6), and support-event aggregation is part of the hierarchy/closed-scale scaffolding that bridge uses.
In the forcing chain, T5 is J-uniqueness via the RCL functional equation; T6 pins $\varphi$ as the self-similar fixed point. Packaging support-induced independence with cardinality projection keeps the discrete ledger side of that bridge theorem-backed rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.