bool_floor_config_from_witness
plain-language theorem explainer
Any absolute-floor witness on the Boolean universe yields the concrete two-point configuration interface used by the T-1→T0 bridge: empty/consistent is false, marked is true, join is OR, and the floor is nontrivial. Bridge and normalization theorems cite this conversion so the abstract witness is not left implicit. The proof is short case analysis on Bool plus the bare-distinguishability lemma from AbsoluteFloorClosure.
Claim. Let $F$ be an absolute-floor witness on the Boolean type (meta-language distinction plus a nontrivial specification of $\mathrm{Bool}$). Then $F$ supplies the Boolean floor configuration interface: the floor is nontrivial; every state is either $\mathsf{false}$ or $\mathsf{true}$; $\mathsf{false}\neq\mathsf{true}$; the empty configuration is $\mathsf{false}$; join is Boolean OR; consistency is equivalent to $\mathsf{false}$; and joining with empty acts as the left unit.
background
In the Unified Forcing Chain, T-1 is the absolute floor: a meta-language that can distinguish propositions and a non-singleton universe of discourse. An AbsoluteFloorWitness on a type $K$ packages meta-distinction plus a nontrivial specification of $K$. For $K=\mathrm{Bool}$, that witness is the starting certificate for logic (T0).
T0 is not assumed. It is forced by cost minimization once a concrete Boolean ledger interface exists: empty/consistent versus marked, with join and consistency predicates. The structure proved here records exactly that conversion from the abstract Boolean absolute-floor witness into the empty/marked configuration interface used by the T0 bridge, rather than hiding the conversion in a global ConfigSpace Bool instance.
Upstream, bare distinguishability of an absolute floor already gives $\exists x,y:K,, x\neq y$. On Bool the remaining interface equations are definitional identities of the two-point type and the cost-from-distinction configuration operations.
proof idea
Construct the configuration interface fieldwise.
Nontriviality is bare_distinguishability_of_absolute_floor applied to the given Boolean absolute-floor witness, yielding two distinct Booleans.
Dichotomy is pure case split on $\Gamma:\mathrm{Bool}$: each case is reflexivity into the corresponding disjunct. Distinctness of false and true is decide. Emptiness equaling false, join equaling OR, and consistency equaling false are definitional (rfl). The empty-join left unit is again a two-case split on Bool with rfl in each branch.
No analytic cost identities are needed; the work is interface normalization on the two-point type.
why it matters
This is the explicit T-1→T0 handoff on the Boolean route. Downstream, tminus1_to_t0_bridge and tminus1_to_t0_bridge_holds install this configuration (with the matching recognition-cost normalization) as the minimal T0 cost interface. The same conversion feeds canonical_two_point_floor_normalization, distinction_atom_universe_from_absolute_floor, and boolean_floor_atom_route_equivalence, which identify the Boolean floor with the two-point atom universe out of the T-1 certificate.
In the forcing chain primer, T-1 is the absolute floor and T0 is logic forced by cost (consistency is cheap). Without this lemma the bridge would smuggle the empty/marked Boolean ledger into global instances. With it, the Complete Inevitability Chain can start from a named absolute-floor witness and reach T0 without hidden configuration choices. It does not itself derive J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8); those sit further down the chain once the cost foundation is in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.