supportCompose
plain-language theorem explainer
Canonical composition of two support-bearing events is the configuration-space join: the event whose support is the union of the two finite supports. Anyone building seed-level recognition-work models or multilevel composition bridges cites this. The body is a one-line alias of ConfigSpace.join on SupportEvent.
Claim. For any atom type $A$ with decidable equality, and support-events $a,b$ (each a finite subset of $A$), the compose $a\circ b$ is the support-event whose support is $\mathrm{supp}(a)\cup\mathrm{supp}(b)$. Equivalently, compose is the binary join of the configuration-space structure on support-events.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). Near this declaration the development builds a concrete carrier for events so that independence is not an extra predicate but disjointness of finite supports.
A SupportEvent on an atom type $A$ is just a finite set $\mathrm{supp}\subseteq A$. The CostFromDistinction configuration-space class supplies an empty configuration and a binary join; on support-events the instance sets empty to $\emptyset$ and join to union of supports. Independence of two events is then literally $\mathrm{supp}(a)\cap\mathrm{supp}(b)=\emptyset$.
Compose is the named operation used when seed-level events are combined into composite recognition-work postings. Downstream seed models only need this join, not a richer monoidal structure.
proof idea
One-line definitional wrapper: supportCompose a b is definitionally ConfigSpace.join a b for the SupportEvent instance, which expands to the support-event whose support is the Finset union of the two supports. No tactics or lemmas are involved.
why it matters
This alias is the composition law fed into the canonical seed bridge inside the forcing chain. It builds canonicalSeedCompositeEvent as the join of level-0 and level-1 singleton support events (support ${0,1}$). The theorem canonicalSeedLevelEvent_seed_composes then records that the level-2 seed interpretation is exactly that compose. The larger result canonical_seed_recognition_work_model_of_support_events packages a SeedRecognitionWorkPostingModel whose composition operation is this join, so only seed disjointness is required for the forcing bridge.
In framework terms this sits under the cost-to-logic and ledger steps of the complete inevitability chain: events must compose before recognition work, multilevel composition, and the later T0–T8 forcing can be stated on a concrete carrier. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only supplies the monoidal glue those arguments use for seed supports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.