bool_recognition_work_constraint
plain-language theorem explainer
On the two-point Boolean configuration space, the concrete recognition-work cost admits a master certificate of the recognition-work constraint: empty cost vanishes and cost is positive exactly on inconsistent states. Anyone citing T0 (logic as the zero/positive split of recognition work) or the T-1→T0 bridge needs this existence fact. The proof is a one-line application of the general recognition-work constraint theorem to the Boolean cost.
Claim. There exists a recognition-work constraint certificate on the Boolean configuration space: a cost function $C:\mathrm{Bool}\to\mathbb{R}_{\ge 0}$ satisfying dichotomy (zero cost iff consistent) and independent additivity, with empty configuration cost zero and positive cost exactly on inconsistent configurations.
background
This module isolates the pre-analytic start 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 works only with the Boolean floor.
A cost function on a configuration space is a nonnegative map $C$ obeying two bridge axioms: (D) dichotomy, $C(\Gamma)=0$ iff $\Gamma$ is consistent; (A) independent additivity over joins of configurations that share no predicates. The recognition-work constraint certificate packages such a $C$ with the immediate consequences that empty cost is zero and positivity tracks inconsistency.
On Bool the concrete cost is the indicator of the inconsistent point: $C(\mathrm{false})=0$, $C(\mathrm{true})=1$. The general recognition-work constraint theorem states that any cost function satisfying the two axioms yields a nonempty certificate.
proof idea
One-line term proof: apply the general recognition-work constraint theorem to the concrete Boolean cost boolRecognitionCost. That theorem builds the master certificate from any cost function obeying dichotomy and independent additivity; the Boolean cost already carries those proofs, so existence of RecognitionWorkConstraintCert Bool is immediate.
why it matters
This is the Boolean instance that discharges the recognition-work half of T0. Downstream, t0_holds cites it as the recognition_work field of T0_Logic_Forced (logic as the zero/positive split of recognition work). The same certificate is wired into tminus1_to_t0_bridge_holds and the UnifiedForcingChain copies (t0_holds, tminus1_to_t0_bridge, canonical_two_point_floor_normalization), so the absolute floor's two-point witness feeds a normalized T0 cost interface without ever invoking analytic $J$.
In the forcing chain this sits at the T-1→T0 step: before T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, or T8 $D=3$. It closes the pre-analytic bridge from absolute distinguishability to a certified recognition-work split on Bool.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.