bool_recognition_cost_from_floor
plain-language theorem explainer
Given any absolute-floor witness on the Boolean universe, the Boolean recognition-work cost is unit-normalized: zero on the empty/consistent state, one on the marked inconsistent state, and positive exactly when the configuration is inconsistent. Cited by the T-1→T0 bridge and the canonical two-point floor normalization in the forcing chain. Proof is a short record construction: two fields by definitional equality, inconsistency by Bool case split, positivity by the general cost dichotomy lemma.
Claim. Let $F$ be an absolute-floor witness on the Boolean universe. Then the Boolean recognition-work cost $C$ is unit-normalized on $F$: $C(\mathsf{false})=0$, $C(\mathsf{true})=1$, every inconsistent Boolean configuration has cost $1$, and for every Boolean configuration $a$ one has $0 < C(a)$ if and only if $a$ is inconsistent.
background
This 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 local goal is the pre-analytic bridge from the absolute floor to the Boolean recognition-work split.
An absolute-floor witness on a universe $K$ asserts bare distinguishability: there exist unequal propositions, and $K$ admits a nontrivial specification. A cost function on a configuration space satisfies dichotomy (cost zero iff the configuration is consistent) and independent additivity over joins that share no predicates. The Boolean recognition cost is the concrete two-point instance of that interface.
The structure being inhabited here packages unit normalization of that Boolean cost relative to a given Boolean floor witness: zero on the empty state, unit on the marked inconsistent state, and the positivity dichotomy.
proof idea
Construct the four fields of the unit-normalization structure directly. Zero-on-empty and unit-on-marked are definitional (rfl). For the inconsistent-unit clause, introduce a Boolean $a$ assumed inconsistent and case-split: the false branch yields an immediate contradiction with the consistency hypothesis; the true branch is definitional equality to $1$. The positivity dichotomy is a one-line application of the general lemma that any cost function is positive precisely on inconsistent configurations, specialized to the Boolean recognition cost.
why it matters
This is the cost half of the T-1→T0 bridge: once the Boolean floor is in hand, the minimal recognition-work interface is unit-normalized and ready for T1 (the cost-form Meta-Principle). Downstream, tminus1_to_t0_bridge and its holding instance install this cost as floor_cost; the unified forcing chain re-exports the same fact and feeds it into canonical_two_point_floor_normalization, which packages config plus cost plus the recognition-work constraint as the canonical normalized two-point floor. That normalization is what the chain's T-1→T0 bridge record carries forward. The result sits strictly before analytic $J$-uniqueness (T5) and the $\phi$ fixed point (T6); it only forces the discrete Boolean cost skeleton on which later rungs build.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.