twoAtomSelectionIndex
plain-language theorem explainer
Given any pair of distinct atoms, the canonical Boolean index sends false to the first atom and true to the second. Anyone building the absolute-floor two-atom carrier or proving that selected atoms are Bool-indexed will cite it. The body is a pure pattern match on Bool; no proof content.
Claim. For a type of atoms and a selection of two distinct atoms $a_0 \neq a_1$, the canonical index map $\iota:\{\mathsf{false},\mathsf{true}\}\to\mathrm{Atom}$ is defined by $\iota(\mathsf{false})=a_0$ and $\iota(\mathsf{true})=a_1$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are forced from the Recognition Composition Law plus normalization and calibration. At the absolute-floor end (T-1), a non-singleton universe and a meta-language distinction supply a Boolean two-point carrier before logic and cost are derived.
A two-atom selection packages any chosen pair of distinct atoms $a_0\neq a_1$ on a carrier type. The structure's purpose is to identify that selected two-point subcarrier with the Boolean two-atom carrier, without yet forcing the whole universe to be Bool.
This index map is the concrete identification: Bool labels the selected pair. Downstream certificates (canonical distinction atom universe, absolute-floor Boolean witness) use that labeling to wire support events and floor configurations onto the two seed atoms.
proof idea
Definition by cases on Bool: false maps to the selection's first atom, true to the second. No lemmas, no tactics; the equation compiler discharges the match.
why it matters
This is the indexing glue between an arbitrary two-atom selection and the Boolean carrier used at the absolute floor. It feeds the injectivity theorem that the selected atoms are exactly Bool-indexed, and it is referenced when building CanonicalDistinctionAtomUniverse (canonical atom carrier is Boolean) and DistinctionAtomUniverseFromAbsoluteFloor (absolute-floor closure supplies the Boolean two-atom support universe for the support-event layer).
In the forcing chain this sits under T-1: the absolute floor needs a concrete two-point distinction before T0 (logic from cost) and the rest of T0-T8 run. Without a canonical Bool index on the selected pair, the Boolean floor witness and seed support events have no carrier map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.