canonicalDistinctionAtom
plain-language theorem explainer
The carrier for a bare distinction is fixed as the two-point type, identified with the Booleans. Anyone building the absolute-floor (T-1) atom universe or the Boolean floor route cites this as the canonical support. It is a one-line type synonym, not a derived theorem.
Claim. The canonical atom type forced by a bare distinction is the two-element type, taken to be $\mathrm{Bool}=\{\mathsf{false},\mathsf{true}\}$.
background
The Unified Forcing Chain module aims to force the full ladder T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). The absolute floor (T-1) is the precondition that the meta-language can state a distinction at all: a non-singleton universe together with a Prop-level distinction.
A bare distinction needs a minimal support carrier with exactly two atoms (empty/unmarked versus marked). Downstream certificates package that carrier as a finite atom universe with distinct seeds and disjoint support events. Naming that carrier once keeps the Boolean floor route and the atom-support route aligned on the same two-point construction.
proof idea
Pure definition: the canonical distinction atom type is declared equal to Bool. No lemmas, tactics, or obligations. Downstream facts (decidable equality, false ≠ true, two-atom selection) inherit immediately from the Boolean instance.
why it matters
This is the named two-atom support for T-1 in the complete inevitability chain. It feeds CanonicalDistinctionAtomUniverse and the theorem that the canonical atom universe exists, the decidable-equality instance, distinctness of the two atoms, canonicalTwoAtomSelection, and the seed support events for false and true. BooleanFloorAtomRouteEquivalence uses it to identify the Boolean floor configuration route with the Boolean atom-support route: false as the empty/configuration atom and true as the marked atom. Without a fixed carrier, the absolute-floor certificates cannot close the gap between meta-language distinction and the cost-forced logic step T0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.