BoolFloorConfigFromWitness
plain-language theorem explainer
Packages the conversion of a Boolean absolute-floor witness into the concrete empty/marked configuration interface used by the T0 bridge. Anyone citing the T-1→T0 step, two-point floor normalization, or Boolean atom-route equivalence needs this certificate. It is a pure Prop structure: seven named interface laws, no proof obligations inside the declaration itself.
Claim. Given an absolute-floor witness on $\mathrm{Bool}$, the following hold as a single interface certificate: the floor is nontrivial ($\exists a,b\in\{\mathsf{false},\mathsf{true}\}$ with $a\neq b$); every state is $\mathsf{false}$ or $\mathsf{true}$; $\mathsf{false}\neq\mathsf{true}$; the empty configuration is $\mathsf{false}$; join is Boolean disjunction; consistency holds iff the state is $\mathsf{false}$; and joining $\mathsf{false}$ on the left is neutral.
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 that can distinguish propositions together with a non-singleton universe of discourse. An absolute-floor witness on a type $K$ records bare distinguishability ($\exists P,Q:\mathrm{Prop},,P\neq Q$) and a nontrivial specification of $K$.
Separately, a configuration space is the abstract ledger interface used to build recognition cost: an empty configuration, a binary join, a consistency predicate, and independence. On $\mathrm{Bool}$ the intended reading is empty/consistent versus marked, with join as disjunction of marks.
This structure sits exactly at the handoff: it does not re-prove that a Boolean absolute floor exists; it names the concrete laws that turn such a witness into the Boolean ConfigSpace interface the T0 (logic-from-cost) bridge consumes, rather than leaving that orientation implicit in a global instance.
proof idea
No proof body: the declaration is a Prop-valued structure (interface certificate). Each field is a named law relating the absolute Boolean floor to the configuration-space operations on $\mathrm{Bool}$. Downstream theorems discharge the fields by Boolean case analysis and by bare distinguishability extracted from the absolute-floor witness (e.g. nontriviality from the floor's meta-distinguishability). The companion constructor theorem builds an inhabitant field-by-field; this structure only states what must be shown.
why it matters
T0 claims logic is forced by cost minimization (consistency is cheap). That step needs a concrete two-point ledger, not a bare existence of distinction. This certificate is the explicit conversion from T-1's Boolean absolute-floor witness into empty/marked join and consistency laws.
It is required by the T-1→T0 bridge (which bundles floor witness, this config interface, Boolean recognition cost, and a recognition-work constraint with $C(\mathsf{false})=0$), by canonical two-point floor normalization (orienting bare distinguishability as false/true with unit marked cost), and by Boolean floor/atom-route equivalence (identifying the floor route with the two-point atom-universe route). In the forcing chain it is scaffolding for the first forced step after the absolute floor, before MP, discreteness, ledger symmetry, unique $J$, $\varphi$, eight-tick, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.