bool_recognition_work_constraint
plain-language theorem explainer
The Boolean configuration space admits a recognition-work constraint certificate: a cost on Bool with zero empty cost and positive cost exactly on inconsistent configurations. Anyone citing the T-1 to T0 bridge or the claim that logic is forced by cost will use this. The proof is a one-line application of the general recognition-work constraint theorem to the Boolean recognition cost.
Claim. There exists a recognition-work constraint certificate on the Boolean configuration space: a cost function $\kappa$ on $\mathrm{Bool}$ such that the empty configuration has zero cost, cost is positive if and only if the configuration is inconsistent, and the remaining certificate fields (calibration witness and independent additivity) hold.
background
The Unified Forcing Chain module derives T0 through T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). The local step is the T-1 to T0 segment: the absolute floor supplies a Boolean witness, and T0 asserts that logic is the zero/positive split of recognition work rather than a pre-given structure.
A cost function on a configuration space satisfies two bridge axioms: dichotomy (cost is zero iff the configuration is consistent) and independent additivity (cost adds over joins of configurations that share no predicates). The recognition-work constraint certificate packages such a cost with its immediate consequences: empty cost zero, positivity exactly on inconsistency, and a non-vacuous calibration witness.
Upstream, the general recognition-work constraint theorem states that any cost function yields a nonempty certificate. Here the configuration type is Bool, with the Boolean recognition cost already constructed on the pre-analytic floor.
proof idea
One-line term wrapper. Apply the general recognition-work constraint theorem to the Boolean recognition cost already defined on the Bool configuration space. That theorem builds the master certificate from any cost function satisfying dichotomy and independent additivity, so inhabitation of the certificate type on Bool is immediate.
why it matters
This is the Boolean-floor instance that makes T0 statable. Downstream, t0_holds packages it as the recognition-work field of T0_Logic_Forced, with consistency cheap (zero) and contradiction expensive (positive). The same certificate is threaded through the T-1 to T0 bridge and the canonical two-point floor normalization.
In the forcing chain, T0 is the claim that logic emerges from cost minimization: consistent configurations cost zero, inconsistent ones cost positively. Without a concrete certificate on the Boolean floor, the absolute-floor precondition cannot hand off to Meta-Principle and the later T1-T8 steps. The module doc places this beneath the Meta-Principle as the foundation that dissolves the assumption of pre-given logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.