SupportInducedConfigSpace
plain-language theorem explainer
A Prop-structure certifying that, on finite-support events over a decidable atom type, configuration independence is exactly disjointness of supports, and that this supplies the support-disjoint independence interface. Downstream aggregate-projection and T5→T6 bridge certificates cite it as the carrier-side independence law. Definitional packaging only; uniqueness is propositional (Subsingleton by rfl).
Claim. Fix an atom type $A$ with decidable equality. A support-induced configuration-space certificate is a proposition asserting: (i) for all finite-support events $a,b$ on $A$, configuration independence of $a$ and $b$ holds if and only if $\mathrm{supp}(a)\cap\mathrm{supp}(b)=\emptyset$; (ii) the same support map therefore satisfies the support-disjoint independence interface (disjoint supports imply independence).
background
The module builds the complete inevitability chain T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). Early links force logic, discreteness, and a ledger; later links force unique $J$, then $\varphi$, the eight-tick period, and $D=3$.
A configuration space (from CostFromDistinction) is an abstract carrier with empty config, binary join, consistency, and an independence relation meaning "no shared predicates," with join a commutative monoid. SupportEvent is the concrete model: each event is a finite set of atoms, empty is $\emptyset$, join is union. In that model independence is not an extra predicate; it is disjointness of finite supports.
SupportDisjointIndependence packages the one-way law that disjoint supports imply ConfigSpace independence, the interface needed so aggregate scalar projections stay compatible with independence.
proof idea
Definitional structure, not a proved theorem. The two fields are Prop obligations: a biconditional equating ConfigSpace.Independent on SupportEvent to Disjoint of support maps, and a bundled SupportDisjointIndependence witness for that same support map. No tactics discharge content here; inhabitants are supplied later (notably by the canonical certificate theorem). A companion Subsingleton instance shows any two such certificates are propositionally equal via rfl, so the interface is unique up to proof irrelevance.
why it matters
Pins the carrier-side meaning of independence before cost aggregation and self-similarity enter. The canonical certificate theorem builds an inhabitant; SupportEventAggregateProjection requires this structure plus a finite-support cardinality projection to scalar aggregate work. CanonicalDistinctionAtomUniverse uses the same support language for Boolean seed atoms and disjoint seed events.
On the forcing chain, T5_To_T6_SelfSimilarity_Bridge routes unique $J$ (T5) into the $\varphi$ fixed point (T6) through hierarchy dynamics; this certificate keeps independence geometric (disjoint support) so self-similar scale ratios are not smuggled past the config monoid laws. It is scaffolding for the RCL-driven chain rather than a landmark theorem itself, but without it the support model cannot feed T6 cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.