boolConfigSpace
plain-language theorem explainer
Booleans form the minimal configuration space for the absolute floor: false is empty and consistent, join is disjunction, and independence means at least one side is empty. Anyone citing the T-1→T0 bridge (floor forces a cost/consistency interface) uses this instance. The laws are discharged by exhaustive case analysis on Bool plus reflexivity.
Claim. The type $\mathrm{Bool}$ carries a configuration-space structure: empty configuration $\mathrm{emp}=\mathsf{false}$; join $\Gamma_1\vee\Gamma_2$; consistency means $\Gamma=\mathsf{false}$; independence means $\Gamma_1=\mathsf{false}$ or $\Gamma_2=\mathsf{false}$. Join is a commutative monoid with identity $\mathsf{false}$, independence is symmetric, empty is independent of every configuration, and the consistency/independence interaction axioms hold.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). It bottoms out at T-1, the absolute floor: meta-language proposition distinguishability and a non-singleton universe of discourse, recorded as a closure certificate. Below the Law of Logic, one still needs an object-level configuration interface on which cost and consistency can act.
A configuration space (from CostFromDistinction) is an abstract type with empty cell emp, binary join, a consistency predicate, and an independence relation (no shared predicates). The laws require join to be a commutative monoid with emp as identity, independence symmetric with emp independent of everything, and standard interaction between join, consistency, and independence.
The local bridge section states that the minimal object-level space supplied by the absolute floor is Boolean: empty/consistent versus marked-inconsistent, with independent joins those that do not double-count two inconsistencies in one Boolean cell.
proof idea
The instance fills the four structure fields on Bool and proves the ConfigSpace axioms by direct computation. Empty-consistency is reflexivity. Independence symmetry swaps the two disjuncts. Empty-independence is the left disjunct with reflexivity. Commutativity, associativity, and left-unit for join are three nested cases on the Boolean arguments, each closing by rfl. The two join/independence/consistency interaction lemmas likewise case-split both arguments and simplify; the inconsistent cases are impossible under the hypotheses.
why it matters
This instance is the concrete carrier that lets T-1 speak the CostFromDistinction language. Downstream, the TMinus1ToT1Bridge re-exports the same Boolean floor and builds recognition-work cost on it, so that T0 (logic forced by cost minimization: consistency is cheap) has a minimal model rather than an assumed logical substrate.
In the forcing chain diagram, T-1 is the precondition of statability; T0 is the first forced layer. Without a verified ConfigSpace on the two-point type, the claim that the absolute floor supplies a cost/consistency interface would be schematic. The Boolean choice matches the floor narrative: one bit of distinction (consistent vs marked-inconsistent), no extra structure.
It does not yet force unique J, φ, eight-tick, or D=3; those sit at T5–T8. It only anchors the bottom of the chain so later cost lemmas have a place to land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.