bool_recognition_cost_from_floor
plain-language theorem explainer
Given any absolute-floor witness on Bool, the Boolean recognition-work cost is unit-normalized: empty/consistent costs 0, the unique marked inconsistent state costs 1, and positivity matches inconsistency. Cited by anyone assembling the T-1→T0 bridge or the canonical two-point floor. Proof is mostly reflexivity plus case analysis on Bool, reusing the CostFunction dichotomy lemmas.
Claim. If $floor$ is an absolute-floor witness on $\mathrm{Bool}$, then the Boolean recognition-work cost $C$ satisfies $C(\mathsf{false})=0$, $C(\mathsf{true})=1$, every inconsistent Boolean configuration has unit cost, $C(\Gamma)>0$ iff $\Gamma$ is inconsistent, and $C(\Gamma)=0$ iff $\Gamma$ is consistent.
background
The Unified Forcing Chain module aims to force T0–T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). The chain begins at T-1: an absolute floor, the meta-language precondition that distinction is possible at all.
An AbsoluteFloorWitness on a type $K$ records bare distinguishability: some pair of unequal propositions, plus a nontrivial specification of $K$. On $\mathrm{Bool}$ this is the two-point universe of discourse. A CostFunction on a configuration space obeys dichotomy (cost zero iff consistent) and independent additivity.
BoolRecognitionCostFromFloor packages the scale choice for the Boolean floor: empty/consistent has zero cost, the unique marked inconsistent state has unit cost $C(\mathsf{true})=1$, and inconsistency is exactly unit cost. That normalization is no longer buried inside the definition of the Boolean cost; it is an explicit bridge hypothesis from T-1 into T0 (logic from cost minimization).
proof idea
The proof builds the BoolRecognitionCostFromFloor record field by field. zero_empty and unit_marked are definitional equalities (rfl) against the Boolean recognition cost. inconsistent_unit is a short case split on $\Gamma:\mathrm{Bool}$: the consistent case is absurd from the inconsistency hypothesis; the inconsistent case is reflexivity of unit cost. Positivity-iff-inconsistency is the general CostFunction.cost_pos_iff_inconsistent lemma applied to the Boolean cost; zero-iff-consistency is that cost's built-in dichotomy axiom.
why it matters
This theorem is the normalization step that lets the absolute floor supply a genuine T0 cost interface rather than a hand-picked Boolean cost. Downstream it is plugged into tminus1_to_t0_bridge and tminus1_to_t0_bridge_holds (both in this module and in TMinus1ToT1Bridge), and into canonical_two_point_floor_normalization, which packages config, unit cost, and recognition-work as the abstract two-point floor.
In the forcing chain this is the T-1→T0 hinge: absolute floor (meta-language distinction) yields logic as cost minimization, with consistency cheap and inconsistency unit-priced. Without an explicit unit normalization, later calibration of $J$ (T5) and the $\varphi$ fixed point (T6) would smuggle a scale choice. The result is fully proved; it closes the Boolean-floor half of the bridge rather than leaving a scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.