distinction_atom_universe_from_absolute_floor
plain-language theorem explainer
From any absolute-floor closure certificate one obtains the canonical Boolean two-atom support universe used by the support-event layer. Anyone assembling the T-1 entry of the unified forcing chain cites this packing. The proof is a short term construction: it reuses the certificate's Boolean witness, builds the floor configuration, records bare distinguishability, and installs the canonical two-atom carrier with injective index.
Claim. Given an absolute-floor closure certificate $C$ (self-bootstrap route, nontrivial-specification equivalence, and a Boolean absolute-floor witness), there exists a distinction-atom universe package for $C$: the Boolean witness of $C$, a Boolean floor configuration from that witness, bare nontriviality $\exists a,b:\mathrm{Bool},\, a\neq b$, and the canonical two-atom distinction universe with injective atom index.
background
The Unified Forcing Chain module aims to force every level T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language with Prop-level distinction and a non-singleton universe, so the rest of the chain is even statable.
An AbsoluteFloorClosureCert packages three pieces: a self-bootstrap certificate, the equivalence between bare distinguishability and nontrivial specification on any nonempty type, and a Boolean absolute-floor witness. Bare distinguishability of that witness is already a theorem: any absolute-floor witness on a nonempty type yields $\exists x,y$ with $x\neq y$.
The structure being inhabited here is the bridge from that certificate to the downstream support-event layer. It records the Boolean witness, a concrete Boolean floor configuration interface, nontriviality of the Boolean floor, and the canonical distinction-atom universe (the two-point carrier with empty/configuration atom versus marked atom).
proof idea
Term-mode field packing, not a deep argument. The Boolean witness is taken directly from the closure certificate. The floor configuration is bool_floor_config_from_witness applied to that witness. Nontriviality is bare_distinguishability_of_absolute_floor on the same witness. The atom universe is the module's canonical distinction-atom universe, and injectivity of the atom index is the injectivity lemma for the canonical two-atom selection. No new arithmetic or cost identities are proved.
why it matters
This is the T-1 packing step that turns the absolute-floor certificate into the Boolean atom-support universe the rest of the chain expects. Downstream, boolean_floor_atom_route_equivalence uses it to identify the Boolean floor route with the Boolean atom-support route as the same two-point construction (false empty/configuration atom, true marked atom).
It also sits on the dependency path into the T5-to-T6 self-similarity bridge material (t5_to_t6_bridge_holds, T5_To_T6_SelfSimilarity_Bridge), which routes unique $J$ into the forcing of $\varphi$ as the self-similar scale. In the primer landmarks this is the floor under T0 (logic from cost) and the later T5 $J$-uniqueness / T6 $\varphi$ steps: without a certified two-atom Boolean carrier, the support-event and hierarchy layers have nothing discrete to stand on.
No open scaffold remains here; the claim is fully proved and only packages already-established floor facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.