canonicalTwoAtomSelection
plain-language theorem explainer
The Boolean carrier supplies a concrete two-atom selection: false and true as the ordered pair of distinct atoms. Anyone wiring the T-1 absolute-floor support universe to the two-point selection interface cites this default instance. It is a structure instance that plugs the Boolean atoms into the selection fields and reuses the Boolean distinctness fact.
Claim. On the canonical distinction-atom type (identified with $\mathsf{Bool}$), the ordered pair $(\mathsf{false}, \mathsf{true})$ is a two-atom selection: the two chosen atoms are distinct.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language Prop distinction plus a non-singleton universe, so that the rest of the chain is even statable.
Upstream, the canonical distinction-atom type is defined to be $\mathsf{Bool}$, and a short decide-proof records that $\mathsf{false} \neq \mathsf{true}$ on that type. A two-atom selection is the structure that packages any carrier with a chosen ordered pair of distinct atoms; its doc states that any such choice "canonically identify their carrier with the Boolean two-atom carrier, at the level of the selected two-point subcarrier."
This definition is the canonical inhabitant of that structure on the Boolean atom type itself.
proof idea
Pure structure instance, not a tactic proof. Set the first selected atom to $\mathsf{false}$, the second to $\mathsf{true}$, and discharge the inequality field by the already-proved Boolean distinctness lemma on the canonical atom type. No further rewriting or cost algebra is involved.
why it matters
T-1 needs a concrete two-atom support universe before the support-event and floor-configuration layers can run. Downstream, the structure "Distinction atom universe from absolute floor" packages the Boolean absolute-floor witness and floor config; the theorem of the same name builds that package from an absolute-floor closure certificate. This selection is the default Boolean two-point choice those constructions rely on when they identify the floor carrier with $\mathsf{Bool}$.
In the forcing chain it sits at the absolute-floor end (T-1), before T0 logic-from-cost and the later J-uniqueness / $\varphi$ / eight-tick / $D=3$ steps. It does not itself force physics constants; it only freezes the two-atom indexing used by the floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.