SupportEvent
plain-language theorem explainer
SupportEvent packages a finite set of atoms as an event carrier for the cost-from-distinction configuration space. Independence is literally disjointness of supports; join is union; the empty support is the unit and the only consistent configuration. Downstream seed models, Boolean floor/atom route equivalence, and canonical distinction-atom certificates all instantiate this carrier. The instance is pure Finset algebra: union monoid laws plus empty-set characterizations of consistency.
Claim. For any type of atoms $A$ with decidable equality, a support event is a pair consisting of a finite subset $\mathrm{supp}\subseteq A$. The empty support is the unit configuration; the join of two events is the union of their supports; a configuration is consistent precisely when its support is empty; two events are independent precisely when their supports are disjoint. These data satisfy the configuration-space axioms (commutative monoid under join, symmetry of independence, empty independent of everything, and the join/independence consistency laws).
background
The Unified Forcing Chain module aims to derive the full T-1 through T8 ladder from the Recognition Composition Law and cost normalization, starting from an absolute floor of bare distinction. Early in that chain one needs a concrete configuration space on which cost, consistency, and independence are not free predicates but geometric facts about supports.
Upstream, ConfigSpace (CostFromDistinction) is the abstract interface: empty configuration, binary join, consistency predicate, and independence relation, with join a commutative monoid and independence symmetric with empty independent of all. Recognition geometry separately treats configurations as the world's latent states and events as what recognizers actually receive. SupportEvent is the bridge: events are finite atom supports, so independence collapses to Finset disjointness.
The Boolean and natural-number seed models later in the module use this carrier to turn a bare two-point distinction into level-tagged support events whose joins and disjointness feed the atom-universe and Boolean-floor routes.
proof idea
The structure itself is a single field: a Finset of atoms. The ConfigSpace instance is definitional on the operations (empty set, union, emptiness as consistency, Disjoint as independence) and then discharges the laws by Finset algebra. Commutativity and associativity of join are Finset.union_comm / union_assoc after unpacking constructors. Empty-join and empty-independence are simp. Symmetry of independence is Disjoint.symm. The two consistency-of-join laws reduce emptiness of a union to emptiness of each factor, or push membership through mem_union and the empty-set characterization eq_empty_iff_forall_notMem.
why it matters
This is the canonical concrete model that makes independence geometric rather than axiomatic inside the forcing chain. Downstream it is the carrier for canonical seed level and composite events, the level-tagged seed support model, seed-disjointness of false/true atom supports, CanonicalDistinctionAtomUniverse, and BooleanFloorAtomRouteEquivalence (the identification of the Boolean floor route with the Boolean atom-support route). Those objects sit under T-1 (absolute floor) and the T0 logic-from-cost step: once supports are Finsets, cost minimization and consistency-is-cheap become statements about empty versus nonempty finite sets. Without this carrier the seed and atom-universe certificates would have to re-prove monoid and independence laws ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.