canonical_distinction_atom_universe
plain-language theorem explainer
Certificate that a bare distinction yields a canonical two-atom Boolean universe: distinct atoms, disjoint seed supports, and an induced support configuration with injective atom selection. Absolute-floor closure and the T5→T6 self-similarity bridge cite it. Proof is a structure assembly: reflexivity for the Bool carrier, plus prior distinctness, disjointness, support-induction, and two-atom index injectivity lemmas.
Claim. There is a canonical finite atom-universe certificate from a bare distinction: the atom carrier equals $\mathrm{Bool}$, the two atoms are distinct ($\mathsf{false}\neq\mathsf{true}$), the seed support events of the two atoms are disjoint, and the induced support configuration space with its observation map has injective selected-atom index.
background
The Unified Forcing Chain module aims to force every step T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language distinction plus a non-singleton universe, so the chain is statable at all.
The canonical atom carrier is defined as $\mathrm{Bool}$. Upstream lemmas already record that the two atoms are distinct and that the seed support events (false-atom and true-atom) have disjoint support maps. A companion structure CanonicalDistinctionAtomUniverse packages the Boolean carrier equality, distinctness, seed disjointness, and the support-layer fields (induced config space, observation, injective selection index) into one Prop certificate.
This theorem is the inhabited instance of that certificate for the bare-distinction atom universe, before absolute-floor closure is threaded through.
proof idea
Structure-mode proof filling CanonicalDistinctionAtomUniverse field by field. The carrier equality canonicalDistinctionAtom = Bool is rfl (definitional). Distinctness and seed disjointness are the named upstream theorems on the canonical atoms. Support carrier and observation are obtained by applying the canonical support-induction and support-observation constructors to canonicalDistinctionAtom. Selected-atom-index injectivity is a short intro then twoAtomSelectionIndex_injective on the selection.
why it matters
Pins the Boolean two-atom support universe that the absolute-floor layer hands to the rest of the chain. Downstream, distinction_atom_universe_from_absolute_floor uses this shape so that a T-1 closure certificate supplies the same Boolean atom universe. The T5→T6 self-similarity bridge (and its holding theorem) also depend on it: once J is unique (T5), the discrete ledger needs a finite atom support to force the self-similar scale $\varphi$ (T6).
In the primer landmarks this sits at T-1 (absolute floor), before T0 logic-from-cost and well before T5 J-uniqueness and T6 $\varphi$. It does not itself force $\varphi$ or the eight-tick octave; it only certifies the bare distinction atom universe those later steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.