SupportEventAggregateProjection
plain-language theorem explainer
Packages two compatible certificates for the canonical support-event model: independence equals disjoint finite support, and scalar aggregate work is the finite-support cost projection. Anyone building quotient or T5–T6 bridge arguments cites this bundle. It is a pure Prop structure (definitional packaging), with propositional uniqueness via Subsingleton.
Claim. For a type of atoms with decidable equality, a support-event aggregate-projection certificate is a proposition asserting both: (i) the configuration space on finite-support events has independence exactly when supports are disjoint; and (ii) the map from those events to scalar aggregate work is the canonical cost projection (cost preserved, and disjoint-support joins project to scalar addition).
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. Mid-chain one needs a concrete event carrier where independence is not an extra predicate but geometry of supports.
A support-event is a finite set of atoms; join is union and the empty support is the unit. The support-induced configuration-space certificate states that two events are independent if and only if their supports are disjoint, and that this supplies the aggregate-projection compatibility interface.
The aggregate scalar-work projection certificate is the quotient/abstraction layer: support-bearing events project to a scalar work carrier by cost, with projection preserving cost and sending disjoint-support joins to addition. This structure simply asserts both certificates together for the same atom type.
proof idea
No proof body: this is a Prop-valued structure definition bundling two fields. The first field is the support-induced configuration-space certificate; the second is the aggregate scalar-work projection specialized to support-events, their support cost, and their support map. A companion Subsingleton instance shows any two such certificates are propositionally equal by reflexivity, so the bundle is unique up to proof irrelevance. Inhabitation is deferred to the canonical constructor theorem.
why it matters
This is the packaging step that makes the canonical support-event model a single theorem-backed surface rather than two loose lemmas. Downstream, the canonical constructor fills both fields from the support-induced and support-event scalar-projection theorems. Support-quotient compatibility then uses the bundle to assert that a general support-bearing event system maps to support-events while preserving support, joins, independence, and aggregate work.
Further along the chain, the T5→T6 self-similarity bridge routes hierarchy dynamics toward φ as the forced scale ratio (T5 J-uniqueness, T6 φ fixed point). Having a unique, support-induced aggregate projection keeps the discrete ledger and cost-additive joins aligned before self-similarity is imposed, so no hidden independence axiom is smuggled into the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.