boolRecognitionCost
plain-language theorem explainer
The Boolean floor carries a recognition-work cost that is 0 on the empty/false state and 1 on the marked/true state. Anyone citing the T-1 absolute floor or the T0 logic-from-cost step uses this as the concrete CostFunction instance on Bool. The structure fields are discharged by exhaustive case analysis on the two Boolean values, with independent additivity failing only when both sides are true.
Claim. On the Boolean configuration space, the recognition-work cost is the function $C(\Gamma)=0$ if $\Gamma=\mathsf{false}$ and $C(\Gamma)=1$ otherwise. It is nonnegative, vanishes if and only if the configuration is the empty (consistent) state, and is additive under join of independent configurations.
background
The Unified Forcing Chain module derives T-1 through T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. The absolute floor (T-1) is the meta-language precondition: a non-singleton universe that can state a distinction at all. The Boolean type is the minimal such floor: two states, empty versus marked.
A configuration space supplies an empty configuration, a binary join, consistency, and an independence relation. A cost function on that space is a map $C$ to nonnegative reals obeying dichotomy (zero cost iff consistent) and independent additivity (cost adds under join of configurations that share no predicates). Those two axioms are the recognition-work bridge from CostFromDistinction.
Here the configuration type is simply $\mathsf{Bool}$, with false as empty and true as the single marked distinction. The cost is the indicator of the marked state. Downstream bridges transport this same cost onto forced quotients and ledger shadows.
proof idea
The definition packages three structure fields. Nonnegativity is immediate: both branches are $0$ or $1$. Dichotomy rewrites the zero-cost predicate as equality with false and splits on the Boolean. Additivity splits on both arguments; the three joins involving at least one false reduce by the join table and arithmetic. The remaining case (true joined with true) is excluded by the independence hypothesis, which would require true to equal false, discharged by Bool.noConfusion.
why it matters
This is the concrete T-1 floor cost that seeds the complete inevitability chain. DistinctionToT4 builds forcedQuotientRecognitionCost by composing this cost with the forced-quotient Boolean coordinate, and proves the transport identity by reflexivity. LedgerFloorT0Bridge uses it to identify the T0 floor as a surjective two-state truncation of the extensive recognition ledger: rank-1 unit-weight cost is literally this Boolean cost after booleanTruncation, and the Phase-2 certificate packages that bridge for the T-1-to-T8 audit.
In the forcing ladder, T0 (logic forced by cost minimization) sits on this floor: consistency is the cheap state. Without a verified CostFunction instance on Bool, the absolute-floor precondition and the ledger-to-floor shadow would remain informal. The definition is pure scaffolding for those bridges, not a deep uniqueness claim; uniqueness of $J$ arrives only at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.