BoolRecognitionCostFromFloor
plain-language theorem explainer
Packages the unit-normalized Boolean recognition-work cost forced by an absolute-floor witness on Bool: empty/consistent has cost 0, the marked inconsistent state has cost 1, and positivity is equivalent to inconsistency. Cited by the T-1→T0 bridge and the canonical two-point floor normalization in the unified forcing chain. As a Prop structure it is pure interface; the companion theorem fills the fields by reflexivity and case analysis.
Claim. Given an absolute-floor witness on $\mathrm{Bool}$, the Boolean recognition-work cost $C$ satisfies: $C(\mathsf{false})=0$, $C(\mathsf{true})=1$, every inconsistent configuration has $C(a)=1$, and $0<C(a)$ if and only if $a$ is inconsistent.
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 (inconsistent floor states cannot be selected at zero cost). The bridge is deliberately pre-analytic: from bare distinguishability to a Boolean recognition-work split.
An AbsoluteFloorWitness on a type $K$ asserts bare meta-level distinguishability (some $P\neq Q$) together with a nontrivial specification on $K$. A ConfigSpace supplies empty configuration, join, and an IsConsistent predicate. On $\mathrm{Bool}$ the empty/consistent pole is $\mathsf{false}$ and the marked inconsistent pole is $\mathsf{true}$; the sibling cost boolRecognitionCost is the discrete work functional on that two-point space.
Unit normalization here means fixing the scale so the unique marked inconsistency carries recognition work $1$, while the consistent empty configuration carries work $0$. That scale choice is what later certificates treat as the canonical two-point floor.
proof idea
No proof body: this is a Prop-valued structure (interface certificate), not a proved theorem. The four fields are the normalization and dichotomy axioms on boolRecognitionCost.C. The companion constructor bool_recognition_cost_from_floor discharges them by rfl on the zero/unit equations and by Boolean case analysis on the inconsistency clauses. Downstream bridge structures simply require an inhabitant of this Prop.
why it matters
This is the explicit scale-fix step that keeps the T-1→T0 edge non-vacuous. Downstream, TMinus1_To_T0_Bridge bundles a Boolean absolute-floor witness, a floor configuration, and this cost certificate so that the minimal T0 recognition-work interface is reached from bare distinguishability. In UnifiedForcingChain the same structure is re-exported and appears inside CanonicalTwoPointFloorNormalization, whose doc states that bare T-1 distinguishability does not by itself name false/true or the unit cost scale; this certificate is that orientation-and-normalization step.
It sits before the analytic forcing landmarks (T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). The module deliberately avoids the $J$-surface; the point is only the discrete pre-analytic bridge from absolute floor to Boolean recognition work. Parent consumers are the local and chain-level T-1→T0 bridges and the canonical two-point normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.