BoolFloorConfigFromWitness
plain-language theorem explainer
Packages the conversion of an absolute Boolean floor witness into the concrete empty/marked Boolean configuration interface used by the T0 bridge. Anyone citing the T-1→T0 step or the two-point floor normalization needs this certificate. It is a pure Prop structure: seven named interface equations, no proof body.
Claim. Given an absolute-floor witness on $\mathrm{Bool}$, the following hold as a configuration interface: there exist distinct Booleans; every Boolean is $false$ or $true$; $false \neq true$; the empty configuration is $false$; join is Boolean OR; a configuration is consistent iff it equals $false$; and $false$ is a left identity for join.
background
The module isolates the first three rungs of the forcing chain without importing the analytic $J$-cost surface: T-1 (absolute floor of distinguishability), T0 (minimal recognition-work cost interface), and T1 (cost-form Meta-Principle). The absolute-floor witness on a type $K$ asserts bare distinguishability: some pair of propositions differs, and $K$ admits a nontrivial specification.
A configuration space supplies an empty configuration, a binary join, a consistency predicate, and independence laws so that join is a commutative monoid with empty as identity. On $\mathrm{Bool}$ the intended reading is the two-point ledger: $false$ is the empty/consistent state and $true$ is the marked/inconsistent state, with join as OR.
This structure makes that reading explicit relative to a given Boolean absolute-floor witness, rather than leaving the conversion implicit in a global $\mathrm{ConfigSpace},\mathrm{Bool}$ instance.
proof idea
No proof: this is a Prop-valued structure definition. Its seven fields are the interface obligations. The companion theorem bool_floor_config_from_witness later discharges them from an AbsoluteFloorWitness Bool, using bare distinguishability of the absolute floor for nontriviality and ordinary Boolean case analysis for dichotomy, distinctness, empty/join/consistency identities.
why it matters
This is the explicit T-1→T0 configuration hinge in the public bridge module. Downstream, TMinus1_To_T0_Bridge requires a field of this type together with the matching Boolean recognition-cost certificate and a recognition-work constraint, so that T-1 supplies the minimal T0 interface. The unified forcing chain reuses the same structure for Boolean-floor/atom-route equivalence and for canonical two-point floor normalization: bare distinguishability does not by itself name $false$/$true$, Boolean join, or unit cost; this certificate orients the floor as empty/marked before cost normalization. It sits before T5–T8 ($J$-uniqueness, $\varphi$, eight-tick octave, $D=3$) and does not touch the analytic $J$ surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.