boolRecognitionCost
plain-language theorem explainer
Compatibility alias that re-exports the Boolean recognition-work cost on the two-point floor: C(false)=0 and C(true)=1, packaged as a CostFunction Bool. Anyone citing the public T-1–T8 spine, the T0 Boolean split, or ledger-to-floor transport uses this name. The body is a one-line abbrev redirect to the TMinus1ToT1Bridge definition.
Claim. The Boolean recognition cost is the cost function $C:\mathrm{Bool}\to\mathbb{R}_{\ge 0}$ given by $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$, satisfying dichotomy (zero cost iff the configuration is consistent) and independent additivity on the Boolean configuration space.
background
The module exposes the public theory-only T-1 through T8 forcing spine, from the absolute distinguishability floor (T-1) through the Boolean recognition-work split (T0) and cost-form Meta-Principle (T1) up to $D=3$ (T8). It stops before private operator and measurement layers.
A cost function on a configuration space is a map $C$ to non-negative reals obeying two recognition-work axioms: (D) dichotomy, cost is zero iff the configuration is consistent; (A) independent additivity over joins of configurations that share no predicates. The Boolean floor is the two-point space that realises T0.
Upstream, the concrete Boolean cost is already defined on the first bridge as $C(a)=0$ when $a=\mathsf{false}$ and $1$ otherwise, with non-negativity and dichotomy discharged by case analysis. This abbrev simply surfaces that object under the public T-1–T8 namespace.
proof idea
One-line abbrev wrapper: the declaration equals TMinus1ToT1Bridge.boolRecognitionCost and carries no extra proof obligations. The underlying definition builds a CostFunction Bool with $C$ the indicator of $\mathsf{true}$, proves non-negativity by cases on Bool with norm_num, and discharges dichotomy the same way. No new lemmas are applied here.
why it matters
This name is the public handle for the T0 Boolean recognition-work cost on the forcing spine. Downstream, the forced quotient recognition cost is defined by transporting this Boolean cost along the forced-quotient Boolean equivalence; the transport theorem states that equality is definitional. Ledger-floor bridges use it to identify rank-1 ledger cost with Boolean truncation ($C = $ Boolean cost $\circ$ boolean truncation) and to certify that the T0 floor is a surjective cost-and-join shadow of the extensive ledger under unit weight.
In the primer chain it anchors T0 (Boolean recognition-work split) and feeds T1 (cost-form Meta-Principle) before J-uniqueness (T5) and $\varphi$ forcing (T6). It does not itself force uniqueness of $J$ or the eight-tick octave; those sit later on the spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.