SupportDisjointIndependence
plain-language theorem explainer
Packages the compatibility hypothesis that disjoint finite atom-supports on events imply ConfigSpace independence. Downstream aggregate scalar-work projections and support-quotient extractions cite it as the bridge from geometric support to algebraic independence. It is a Prop-structure certificate, propositionally unique (Subsingleton) for fixed data.
Claim. Let $E$ be a configuration space of events and let $\mathrm{supp}: E\to\mathrm{Finset}(A)$ assign each event a finite set of atoms. The support-disjoint independence certificate asserts: for all events $a,b\in E$, if $\mathrm{supp}(a)$ and $\mathrm{supp}(b)$ are disjoint, then $a$ and $b$ are independent configurations (no shared predicates under the configuration-space join).
background
The ambient module is the Unified Forcing Chain: T-1 through T8 forced from the cost foundation (Recognition Composition Law, normalization, calibration). Locally one works with configuration spaces from CostFromDistinction: a type of configurations with empty config, binary join, consistency, and an Independent relation meaning no shared predicates. Join is a commutative monoid; independence is symmetric and the empty config is independent of everything.
A support map sends each event to a finite set of atoms. Disjoint supports are the geometric stand-in for non-interference. The canonical carrier SupportEvent makes independence exactly equal to disjoint finite support; the present structure abstracts that one-direction implication so arbitrary event systems can carry the same certificate.
Upstream, ConfigSpace supplies Independent and the monoid laws. Cosmology Event (source/target/ratio postings) and related rung machinery motivate support-bearing recognition events, but the certificate itself is carrier-agnostic.
proof idea
Definitional Prop-structure: a single field disjoint_implies_independent stating the universal implication from Finset.Disjoint of supports to ConfigSpace.Independent. No proof obligations beyond inhabiting that field at use sites.
A companion Subsingleton instance records propositional uniqueness for fixed Event, Atom, ConfigSpace instance, and support map: any two certificates are equal by rfl (Prop fields). Concrete inhabitants are built later (e.g. on SupportEvent by unfolding Independent as disjoint support).
why it matters
This is the hinge between support geometry and cost algebra in the forcing chain. AggregateScalarWorkProjection requires it so that support-disjoint joins project to scalar addition of work; the constructor aggregate_scalar_work_projection takes the certificate as input. SupportInducedConfigSpace strengthens the same idea to an iff on the canonical SupportEvent carrier.
Downstream quotient machinery (supportDisjointIndependence_of_supportQuotient, SupportExtractionThroughQuotient, SupportQuotientCompatibility) lifts or reflects the certificate through maps into SupportEvent, replacing a primitive support map by theorem-backed extraction. That keeps the scalar-work projection available after coarsening or quotienting events.
In the T0–T8 narrative it is scaffolding for ledger/recognition levels where cost must factor over independent sub-configurations: without disjoint-support independence, aggregate work would not split cleanly along the phi-ladder bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.