canonicalDistinctionAtom_seed_disjoint
plain-language theorem explainer
The seed supports of the two Boolean atoms are disjoint finite sets: the false-atom support is {false} and the true-atom support is {true}. Anyone assembling the canonical two-atom universe from a bare distinction cites this. The proof unfolds the seed events and support map, then obtains a Boolean contradiction from membership in both singletons.
Claim. The finite supports of the two canonical seed events are disjoint: $\mathrm{supp}(\{false\}) \cap \mathrm{supp}(\{true\}) = \emptyset$ as subsets of the Boolean atom carrier.
background
In the Unified Forcing Chain, independence of events is not an extra predicate: it is disjointness of finite supports. A support event is a carrier whose only data is a finite set of atoms; the support map simply reads that set. Recognition-work cost on this model is support cardinality.
The canonical distinction atom is the Boolean two-point type. Its seed events are the singleton supports ${false}$ and ${true}$. These seeds are the minimal non-empty configurations that witness a bare distinction at the absolute floor (T-1), before logic, discreteness, and the rest of T0–T8 are forced from the Recognition Composition Law.
The module's stronger claim is that every level T-1 through T8 is forced from cost plus normalization and calibration. Disjoint seed supports are the concrete independence fact needed to treat the Boolean carrier as a two-atom universe rather than a collapsed singleton.
proof idea
Term/tactic hybrid on Finset disjointness. Rewrite with Finset.disjoint_left, so it suffices that no atom lies in both supports. Introduce a hypothetical common element and simplify using the definitions of the false and true seed events and of the support map; both membership hypotheses collapse to equalities with false and true respectively. Substitute one equality into the other and finish by Bool.noConfusion, which rules out false = true.
why it matters
Feeds canonical_distinction_atom_universe, which packages the canonical atom type, distinctness of the two atoms, this seed-disjointness fact, and the induced support configuration space into a single structure: "the canonical atom universe from a bare distinction."
That structure is the concrete two-atom model at the absolute floor of the forcing chain. Without disjoint seeds, independence would have to be postulated separately; with it, the Boolean carrier is already a genuine two-point distinction. In the module narrative this sits under T-1 (absolute floor from meta-language Prop distinction plus a non-singleton universe) and underwrites the later claim that T0 logic and the rest of T0–T8 are forced from cost rather than assumed.
No open scaffold remains here: the theorem is fully proved and only records a Boolean singleton fact needed by the universe constructor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.