normalized_two_point_cost_eq_indicator
plain-language theorem explainer
On any normalized two-point recognition floor, configuration cost equals the 0/1 indicator of the marked state under the Boolean equivalence. Foundation workers cite this to fix unit recognition work at the absolute floor before lifting toward J-cost and T5 uniqueness. The proof is a two-case rewrite from exhaustiveness of empty versus marked.
Claim. Let $C$ be a configuration space with empty point $\mathrm{emp}$ and marked point $m$, a cost $\mathcal{C}:C\to\mathbb{R}_{\ge 0}$, and an equivalence $\varphi:C\simeq\mathrm{Bool}$ forming a normalized two-point recognition floor. Then for every $\Gamma\in C$, $\mathcal{C}(\Gamma)=0$ if $\varphi(\Gamma)=\mathsf{false}$, and $\mathcal{C}(\Gamma)=1$ otherwise.
background
The module is the public T-1 through T8 forcing spine: absolute distinguishability floor, Boolean recognition-work split, cost-form Meta-Principle, discreteness, ledger, witness, J-uniqueness, phi, eight-tick, and $D=3$. It stops before private operator layers.
A configuration space carries an empty configuration, a join, and a consistency predicate. A cost function obeys dichotomy (cost vanishes iff the configuration is consistent) and independent additivity over joins of independent configurations.
A normalized two-point recognition floor is the abstract Boolean floor: exactly two points (empty and marked), unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ showing Bool is only the canonical representative. The structure records exhaustiveness, consistency of empty, Boolean labels of both points, cost zero on empty, and cost one on marked.
proof idea
The floor hypothesis supplies exhaustiveness: every configuration equals either the empty point or the marked point. Case-split on that disjunction for the given $\Gamma$.
Empty case: rewrite $\Gamma$ to emp, apply the floor's Boolean label of emp ($\mathsf{false}$) and its cost-zero field, then simplify the indicator. Marked case: rewrite to mark, apply the Boolean label of mark ($\mathsf{true}$) and the unit-cost field, then simplify. Pure case analysis on structure fields; no external lemmas.
why it matters
Theorem-level form of unit recognition work on the absolute floor, not a hidden definition of the Boolean representative. Feeds the sibling uniqueness result that any two normalized two-point costs over the same shape agree pointwise, and the carrier-independent absolute-floor form in UnifiedForcingChain (any absolute floor carrier with a normalized two-point floor has forced $0/1$ cost).
In the spine this anchors T-1 (absolute distinguishability) and T0 (Boolean recognition-work split), before T1's cost-form Meta-Principle and the climb to T5 $J$-uniqueness. Re-exports in UnifiedForcingChain expose it to the full T0–T8 chain. Without a forced unit cost at the floor, later normalizations of $J$ and the phi ladder would float by an arbitrary scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.