CanonicalDistinctionAtomUniverse
plain-language theorem explainer
A propositional certificate that the bare-distinction atom universe is Boolean: two distinct atoms, disjoint seed supports, support-induced configuration space, and injective Boolean indexing of any selected pair. Foundation authors cite it when wiring absolute-floor witnesses into the support-event layer of the forcing chain. It is a structure of six Prop fields, not a proved theorem; uniqueness is by Subsingleton (allEq by rfl).
Claim. A certificate that the canonical distinction-atom carrier equals $\mathrm{Bool}$, that $\mathsf{false}\neq\mathsf{true}$ on that carrier, that the two seed support events have disjoint finite supports, that the carrier carries the support-induced configuration space (independence $=$ support disjointness) and the canonical support observation, and that every selection of two distinct atoms admits an injective Boolean index map on the selected pair.
background
The Unified Forcing Chain module aims to force T-1 through T8 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 the chain is even statable.
A SupportEvent is a finite-support event on an atom type; independence is not an extra predicate but disjointness of those supports. SupportInducedConfigSpace packages that equivalence and the aggregate-projection interface. CanonicalSupportObservation adds the finite-support observation and the identity support-forgetting quotient on that carrier.
TwoAtomSelection picks any two distinct atoms and supplies the canonical Boolean index on that two-point subcarrier. The present structure freezes the canonical atom type to Bool and records that the seed false/true supports are disjoint, so the Boolean floor is a concrete two-atom support universe for everything downstream.
proof idea
No proof body: this is a structure (Prop bundle) with six named fields. Inhabitants are built fieldwise elsewhere. The companion theorem canonical_distinction_atom_universe fills them by rfl on the atom type, the distinctness and seed-disjointness lemmas for the canonical Boolean atoms, the canonical support-induced config-space and support-observation constructors, and the general injectivity of the two-atom selection index. A Subsingleton instance proves any two certificates are equal by rfl, so the certificate is propositionally unique once inhabited.
why it matters
This is the finite-atom universe certificate that turns a bare distinction into the Boolean support carrier used by the cost-from-distinction layer. Downstream, canonical_distinction_atom_universe inhabits it; DistinctionAtomUniverseFromAbsoluteFloor ties absolute-floor closure certificates to the same Boolean two-atom support universe ("supplies the Boolean two-atom support universe used by the downstream support-event layer"). The T5-to-T6 self-similarity bridge also depends on this package as part of the internal hierarchy route from unique $J$ to $\varphi$.
In the forcing chain it sits under T-1/T0: without a non-singleton Boolean atom floor and disjoint seed supports, ledger discreteness, recognition observables, and the later $\varphi$ and eight-tick steps have no carrier. It does not itself force $J$, $\varphi$, or $D=3$; it only certifies the atom universe those steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.