absolute_bool_floor_unique_normalized_01
plain-language theorem explainer
Any absolute floor witness on the Boolean configuration space, equipped with a normalized two-point recognition-work cost and an equivalence to Bool, forces that equivalence to be the identity and the cost to equal the canonical Boolean recognition cost. Researchers tracing the T-1 absolute floor into the public forcing spine cite this uniqueness. The proof is a one-line application of the specialized two-point uniqueness lemma.
Claim. Let $F$ be an absolute floor witness on $\mathrm{Bool}$. Let $C$ be a cost function on $\mathrm{Bool}$ and let $\varphi:\mathrm{Bool}\simeq\mathrm{Bool}$ be an equivalence such that $(\mathrm{true},C,\varphi)$ is a normalized two-point recognition floor. Then $\varphi$ equals the identity equivalence, and $C(\Gamma)$ equals the canonical Boolean recognition cost for every configuration $\Gamma$.
background
The module publishes the theory-only T-1 through T8 forcing spine. T-1 is the absolute distinguishability floor; T0 is the Boolean recognition-work split; later steps reach J-uniqueness, $\varphi$, the eight-tick octave, and $D=3$.
An absolute floor witness on a universe $K$ asserts bare distinguishability: there exist distinct propositions and a nontrivial specification of $K$. A cost function on a configuration space satisfies dichotomy (cost vanishes exactly on consistent configurations) and independent additivity over joins that share no predicates.
A normalized two-point recognition floor is the abstract Boolean floor: one empty/consistent point, one marked inconsistent point, a unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ showing that $\mathrm{Bool}$ is only the canonical representative. The canonical Boolean recognition cost is the fixed $0/1$ cost used by the T-1 to T1 bridge.
proof idea
One-line term proof. It applies the sibling uniqueness lemma for the Boolean normalized two-point floor directly to the given normalized-floor hypothesis, yielding both the identity equivalence and pointwise equality of costs with the canonical Boolean recognition cost.
why it matters
The result is re-exported into the unified forcing chain, whose doc-comment records that the absolute Boolean floor has a unique normalized $0/1$ recognition-work representative, namely the canonical Boolean recognition cost. It locks the T-1 absolute floor to a single cost representative before the spine continues through T0 (logic forced), T1 (meta-principle), T2 (two-state discreteness), and onward to T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, and T8 $D=3$. Without this uniqueness the later cost-form and reciprocal steps would float relative to an arbitrary Boolean labeling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.