DistinctionAtomUniverseFromAbsoluteFloor
plain-language theorem explainer
From any absolute-floor closure certificate one obtains a Boolean two-atom support universe: a nontrivial Boolean floor configuration together with the canonical distinction-atom carrier, injectively indexed by Bool. Foundation authors cite it when wiring T-1 into the support-event and atom-route layers. It is a Prop-valued certificate structure (definitional packaging), not a derived theorem.
Claim. Given an absolute-floor closure certificate $C$, the following hold simultaneously: $C$ supplies a Boolean absolute-floor witness $W$; $W$ yields a concrete Boolean floor configuration (empty/marked dichotomy with $\mathsf{emp}=\mathsf{false}$); the Boolean floor is nontrivial ($\exists a,b:\mathsf{Bool},\,a\neq b$); the canonical distinction-atom universe is available (carrier $\mathsf{Bool}$, distinct atoms, disjoint seed supports); and the canonical two-atom selection indexes atoms injectively by $\mathsf{Bool}$.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language with distinguishable propositions and a non-singleton universe of discourse, so the chain is statable at all.
An absolute-floor closure certificate jointly packages self-bootstrap, the equivalence between bare nontriviality and a nontrivial specification, and a Boolean absolute-floor witness. That witness asserts meta-level distinguishability of propositions and a nonempty nontrivial specification on Bool. The sibling BoolFloorConfigFromWitness converts the abstract witness into the empty/marked Boolean ledger interface used by the T0 bridge (dichotomy, false ≠ true, empty config is false).
CanonicalDistinctionAtomUniverse records the finite two-atom support carrier: atom type is Boolean, the two atoms are distinct, and the seed support events for false and true are disjoint. This structure is the certificate that the absolute floor already supplies that two-atom universe for the downstream support-event layer.
proof idea
No proof body: this is a Prop-valued structure definition packing five fields. Inhabitation is supplied elsewhere by distinction_atom_universe_from_absolute_floor, which fills bool_witness from the closure certificate, builds bool_floor_config via bool_floor_config_from_witness, and discharges nontriviality and the canonical atom-universe fields from the Boolean floor and two-atom selection lemmas. A companion Subsingleton instance shows any two such certificates are definitionally equal (allEq by rfl), so the packaging is propositionally unique once the closure is fixed.
why it matters
This is the T-1 packaging step that turns absolute-floor closure into the Boolean two-atom support universe used by the support-event layer. Downstream, distinction_atom_universe_from_absolute_floor constructs an instance from any closure certificate, and BooleanFloorAtomRouteEquivalence equates the Boolean floor route with the Boolean atom-support route (false as empty/configuration atom, true as marked atom). The T5-to-T6 self-similarity bridge also depends on this atom-universe route as part of the unified chain.
In the forcing ladder it sits at T-1 (absolute floor from meta-language distinction plus non-singleton universe), before T0 logic-from-cost and the later J-uniqueness (T5), phi (T6), eight-tick (T7), and D=3 (T8) steps. It does not itself force phi or the cost functional; it only certifies that the absolute floor already yields the two-point atom carrier the rest of the chain needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.