twoAtomSelectionIndex_injective
plain-language theorem explainer
Any selection of two distinct atoms induces an injective map from Bool onto those atoms (false to the first, true to the second). Foundation workers building the absolute-floor atom universe cite this to treat the Boolean carrier as a faithful index of a bare distinction. The proof is exhaustive case analysis on the two Boolean inputs, using distinctness of the selected atoms.
Claim. Let $A$ be any type and let $a_0, a_1 \in A$ with $a_0 \neq a_1$. The map $i:\{\mathrm{false},\mathrm{true}\}\to A$ defined by $i(\mathrm{false})=a_0$ and $i(\mathrm{true})=a_1$ is injective.
background
The module Unified Forcing Chain derives the full T-1 through T8 ladder as inevitabilities from the Recognition Composition Law plus normalization and calibration. T-1 (absolute floor) is the meta-language precondition: a non-singleton universe in which a bare distinction can be stated at all.
A two-atom selection packages any pair of distinct elements $a_0\neq a_1$ of a carrier type $A$. The associated index map sends the Boolean false to $a_0$ and true to $a_1$, so the selected two-point subcarrier is identified with the Boolean two-atom carrier. The structure's only nontrivial field is the inequality $a_0\neq a_1$.
This injectivity lemma is the elementary set-theoretic fact that makes that identification faithful on the domain side: distinct Booleans land on distinct atoms.
proof idea
Introduce two Booleans $a,b$ with $i(a)=i(b)$. Case-split on both. The diagonal cases (both false, both true) are reflexivity. The off-diagonal cases reduce to $a_0=a_1$ or $a_1=a_0$, each contradicted by the selection's distinctness hypothesis (once directly, once via symmetry of equality). No external lemmas are required beyond that field.
why it matters
The lemma sits inside the T-1 absolute-floor layer of the complete inevitability chain. Downstream it is used by the canonical distinction-atom universe (the seed-only support-event recognition-work model that needs only seed disjointness) and by the certificate that an absolute-floor closure supplies the canonical Boolean atom universe.
Without injectivity, the Boolean index would not be a faithful naming of the two selected atoms, and the bridge from a bare meta-language distinction to a two-point carrier would fail. The result is pure foundation scaffolding for the forcing chain; it does not itself touch J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$, but it is a prerequisite for stating those later steps on a discrete atom universe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.