falseAtomSupportEvent
plain-language theorem explainer
Defines the seed support event whose finite support is the singleton {false} on the canonical two-atom carrier Bool. Anyone building the Boolean atom-universe route from the absolute floor cites this as the unmarked atom's event. The body is a one-line structure constructor packing that singleton finset.
Claim. Let the canonical distinction atom type be $\mathrm{Bool}$. The false-atom seed support event is the support-bearing event whose support is the finite set $\{\mathsf{false}\}$.
background
The Unified Forcing Chain module aims to force T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). At T-1, a bare meta-language distinction plus a non-singleton universe yields an absolute floor; the Boolean route realizes that floor as a two-point atom carrier.
canonicalDistinctionAtom is defined to be Bool. A SupportEvent on an atom type is a concrete carrier with a finite support : Finset Atom. Independence of events is not an extra predicate: it is disjointness of those finite supports. Config space structure joins events by union of supports and takes the empty support as the empty configuration.
This definition is the unmarked seed on that carrier: the event whose support is exactly the false atom. Its twin is the true-atom seed (support ${\mathsf{true}}$).
proof idea
One-line definitional constructor. The structure SupportEvent has a single field support; the term is the anonymous constructor packing the singleton finset {false} on canonicalDistinctionAtom (i.e. Bool). No lemmas are applied.
why it matters
This seed is half of the two-point support model that makes the Boolean atom-universe route concrete. Downstream, canonicalDistinctionAtom_seed_disjoint proves the false and true seed supports are disjoint, which is the independence fact the support model was built to express. CanonicalDistinctionAtomUniverse packages that disjointness with the Boolean carrier identity and atom distinctness into a finite-atom-universe certificate from a bare distinction. BooleanFloorAtomRouteEquivalence then equates the Boolean floor-configuration route from T-1 with this atom-support route: false is the empty/configuration atom and true is the marked atom. In the forcing chain this sits at T-1 (absolute floor), before T0 logic-from-cost and the rest of T1-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.