absolute_bool_floor_unique_normalized_01
plain-language theorem explainer
Any absolute Boolean floor with a normalized two-point recognition-work cost has a unique 0/1 representative: the Bool self-equivalence must be the identity, and the cost must equal the canonical Boolean recognition cost on every configuration. Cited by anyone closing the T-1 absolute-floor step of the unified forcing chain. Proof is a one-line application of the general Boolean two-point normalization uniqueness lemma.
Claim. Let an absolute-floor witness on $\mathrm{Bool}$ be given, together with a cost function $C$ on $\mathrm{Bool}$ and an equivalence $e:\mathrm{Bool}\simeq\mathrm{Bool}$. If $(\mathrm{Bool},\mathrm{true},C,e)$ is a normalized two-point recognition floor (exactly one empty/consistent point, one marked inconsistent point, unit-normalized recognition work), then $e$ is the identity equivalence and $C(\Gamma)$ equals the canonical Boolean recognition cost for every configuration $\Gamma$.
background
The Unified Forcing Chain module proves that T0–T8 are forced inevitabilities from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). The chain opens at T-1: an absolute floor, recorded as meta-language Prop distinction plus a non-singleton universe of discourse.
An absolute-floor witness on a carrier $K$ asserts that the meta-language distinguishes at least two propositions and that $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 normalized two-point recognition floor is the abstract Boolean floor: one empty/consistent point, one marked inconsistent point, unit-normalized recognition work, and an equivalence showing that $\mathrm{Bool}$ is only the canonical representative, not a hidden extra assumption.
The canonical Boolean recognition cost assigns work $0$ to the empty/consistent configuration and work $1$ to the marked inconsistent one.
proof idea
One-line term proof. Apply the general uniqueness lemma for normalized two-point floors on $\mathrm{Bool}$ (the sibling that forces any such floor to the identity equivalence and the canonical Boolean recognition cost) directly to the normalized-floor hypothesis. The absolute-floor witness is ambient context only and is not inspected in the body.
why it matters
Pins the T-1 Boolean absolute floor to a unique normalized $0/1$ recognition-work representative, closing uniqueness before T0 (logic from cost minimization) is forced. Downstream, the T-1-to-T8 bridge re-exports this statement as part of the bridge from the absolute floor through the full forcing chain. Without it, multiple inequivalent recognition-work normalizations could sit at the Boolean base, weakening the claim that the chain is forced from a single axiom bundle. The companion general-form result (any absolute-floor carrier with a normalized two-point floor and an equivalence to $\mathrm{Bool}$) is the carrier-independent version of the same uniqueness. Framework landmark: T-1 absolute floor in the T-1→T8 sequence of UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.