TwoAtomSelection
plain-language theorem explainer
A two-atom selection is a pair of distinct elements of an arbitrary atom type, packaged with the inequality witness. It is the data needed to identify any chosen two-point subcarrier with the Boolean carrier. Downstream Boolean index maps and injectivity lemmas cite it. The declaration is a plain structure definition, not a proved theorem.
Claim. For any type $A$, a two-atom selection consists of elements $a_0, a_1 \in A$ together with a proof that $a_0 \neq a_1$. Any such pair identifies the selected two-point subcarrier of $A$ with the Boolean two-atom carrier via the canonical index map.
background
The module Unified Forcing Chain aims to derive the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration. At the absolute-floor end (T-1), the meta-language must already support a non-singleton universe of distinctions: at least two distinct atoms so that Boolean logic and cost can be stated at all.
A two-atom selection is the minimal data for that step on an arbitrary carrier type Atom. It does not assert that the whole type is Boolean; it only names two unequal points. The companion index map sends false to the first atom and true to the second, so the selected subcarrier is identified with Bool at the level of those two points.
This sits under the absolute-floor and T0 logic-from-cost layer: once two distinct atoms exist, Boolean configurations and recognition cost on them become available, and the forcing chain can begin.
proof idea
No proof body: this is a structure definition. The fields are the two atoms and the inequality atom0 ≠ atom1. Downstream definitions fill the fields (e.g. false and true on the canonical distinction atom) and prove injectivity of the induced Boolean index by case analysis on Bool.
why it matters
This structure is the shared interface for every place the forcing chain needs "exactly two named distinct atoms." It is inhabited by canonicalTwoAtomSelection on the canonical distinction atom (Boolean false/true). The index map twoAtomSelectionIndex and the theorem that it is injective both take a TwoAtomSelection as input, so any later argument that a selected pair is Boolean-indexed goes through this type.
CanonicalDistinctionAtomUniverse packages the stronger certificate that the canonical atom carrier is Bool with distinct seeds; the two-atom selection is the lighter, carrier-agnostic fragment used before that full identification. In the T-1 absolute-floor story, non-singleton distinction is the precondition that makes the rest of T0-T8 statable. The structure does not itself force D=3, φ, or the eight-tick octave; it only supplies the two-point seed those later steps presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.