boolConfigSpace
plain-language theorem explainer
The Boolean type carries a configuration-space structure: empty is false, join is disjunction, consistency means false, and independence means at least one operand is false. Anyone citing the T-1→T0 bridge or the minimal recognition-work floor uses this instance. The laws are discharged by exhaustive case analysis on Bool together with reflexivity.
Claim. The type $\mathrm{Bool}$ is a configuration space: the empty configuration is $\mathsf{false}$; join is logical or; a configuration is consistent precisely when it equals $\mathsf{false}$; two configurations are independent when at least one is $\mathsf{false}$. Join is a commutative monoid with empty as identity, independence is symmetric, empty is independent of every configuration, and the consistency/independence join laws hold.
background
The module isolates the first three levels of the forcing chain: T-1 (absolute floor of distinguishability), T0 (minimal recognition-work cost interface), and T1 (cost-form Meta-Principle). It deliberately avoids the analytic $J$-cost surface and only builds the pre-analytic bridge from the absolute floor to the Boolean recognition-work split.
A configuration space (from CostFromDistinction) is an abstract type with empty configuration, binary join, a consistency predicate, and an independence relation. The laws require join to be a commutative monoid with empty as identity, independence to be symmetric with empty independent of everything, and consistency to interact correctly with independent joins.
The surrounding prose states that the minimal object-level configuration space supplied by the absolute floor is Boolean: false is empty/consistent, true is marked inconsistent. Independent joins are those in which two independent inconsistencies are not double-counted in the same Boolean cell.
proof idea
Direct instance construction. Empty is false; join is Boolean or; consistency is equality to false; independence is the disjunction that at least one argument is false.
emp_consistent is reflexivity. independent_symm swaps the two disjuncts. emp_independent always takes the left disjunct (false is empty). Commutativity, associativity, and left-identity of join are proved by exhaustive cases on the Boolean arguments, each reducing by rfl. The two consistency-of-join laws likewise case-split on both Booleans and finish with simp.
why it matters
This instance is the concrete Boolean floor that turns the closed absolute-floor certificate (T-1) into a usable ConfigSpace, so the recognition-work cost interface (T0) can be stated without importing analytic $J$. Downstream, UnifiedForcingChain re-exports the same Boolean ConfigSpace as the start of the forcing chain bridge from T-1 into T0.
In the Recognition Science forcing chain, T-1 is the absolute floor of distinguishability; this declaration supplies the minimal object-level carrier on which recognition work is measured before any continuous cost surface appears. Sibling declarations (boolRecognitionCost, the T-1→T0 bridge, T0_Logic_Forced) sit on top of this instance. It does not yet force $J$, $\varphi$, the eight-tick octave, or $D=3$; those enter only at later chain steps (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.