canonicalDistinctionAtom_distinct

The Unified Forcing Chain module aims to force T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). The absolute floor (T-1) is the meta-language precondition: a bare distinction plus a non-singleton universe so the chain is even statable.

The canonical distinction atom type is defined as $\mathrm{Bool}$. It is the minimal two-point carrier forced by a bare distinction: the two atoms that seed support events and ledger configurations. Downstream constructions package this type into a universe structure and into an explicit two-atom selection (atom0 = false, atom1 = true).

This lemma is the elementary distinctness fact for those two atoms. Without it, the absolute-floor seed cannot certify a genuine distinction, and the two-atom selection cannot satisfy its inequality field.

One-line decidability proof. After the type synonym canonicalDistinctionAtom := Bool, the goal is ordinary false ≠ true on Bool, which decide discharges by the decidable equality instance.

This is the atomic non-degeneracy step under T-1 (absolute floor) in the complete inevitability chain. It feeds canonical_distinction_atom_universe, which packages atom type, distinctness, seed disjointness, and support carrier into the canonical atom universe from a bare distinction. It also supplies the atom_ne field of canonicalTwoAtomSelection, the Boolean two-atom selection used to index the seed support.

In the forcing narrative, everything above T-1 (logic from cost, MP, discreteness, ledger, unique J, φ, eight-tick, D = 3) presupposes that the meta-language can host a real distinction. This lemma is the Lean witness that the canonical two atoms are not collapsed. It does not itself force φ or the octave; it only closes the distinctness obligation those later packages inherit.