boolRecognitionCost
plain-language theorem explainer
Concrete recognition-work cost on the two-state Boolean floor: zero on the empty (consistent) state and one on the marked state. Anyone identifying the T0 floor with a Boolean truncation of a ledger or forced quotient cites this object. The CostFunction fields are discharged by exhaustive case analysis on Bool with elementary arithmetic.
Claim. The Boolean recognition-work cost is the cost function $C:\{\bot,\top\}\to\mathbb{R}$ with $C(\bot)=0$ and $C(\top)=1$, satisfying non-negativity, dichotomy (cost vanishes if and only if the configuration is consistent), and independent additivity under join.
background
This module isolates the pre-analytic bridge from T-1 (absolute floor of distinguishability) through T0 (minimal recognition-work cost interface) to T1, deliberately without importing the analytic $J$-cost surface.
A configuration space supplies an empty configuration, a binary join, a consistency predicate, and an independence relation, with join a commutative monoid. A cost function on such a space is a map $C$ to the non-negative reals obeying dichotomy (zero cost characterises consistency) and independent additivity (cost adds over joins of configurations that share no predicates).
Here the configuration type is Bool: false plays the empty/consistent role and true the marked/inconsistent role. Join is Boolean OR. The cost is the indicator of the marked state.
proof idea
Structure construction, not a deep theorem. The cost map is the piecewise constant $C(a)=0$ if $a=\mathsf{false}$ else $1$. Non-negativity and dichotomy are each a two-case split on the Boolean argument plus norm_num. Additivity splits on both arguments: the three joins involving at least one false reduce by rewriting the join equation and arithmetic; the double-true case is impossible under the independence hypothesis, discharged by Bool.noConfusion.
why it matters
This is the concrete T0 cost that the whole early forcing spine transports. Downstream, the forced-quotient recognition cost is defined by pulling this Boolean cost back along the forced-quotient Boolean equivalence, and the transport identity is definitional. The ledger-floor T0 bridge and the Phase-2 identification certificate specialise to it: on a single primitive distinction with unit weight, rank-one ledger cost is literally this Boolean cost composed with Boolean truncation of multiplicity. The T-1-to-T0 bridge certificates in this same module package the floor-to-Boolean identification around it. Framework role: it is the minimal recognition-work split before any analytic $J$, phi, or eight-tick structure appears (those enter only at T5–T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.