bool_normalized_two_point_floor_unique
plain-language theorem explainer
Any unit-normalized two-point recognition floor on Bool with marked state true is forced to be the canonical Boolean floor: the configuration equivalence is the identity, and the cost is exactly the 0/1 recognition-work cost. Foundation and forcing-chain authors cite this when locking the absolute floor representative before T0–T8. The proof is a one-line application of the abstract two-point uniqueness lemma against the known Boolean floor witness.
Claim. Let $C$ be a recognition-work cost on $\mathrm{Bool}$ and let $\phi:\mathrm{Bool}\simeq\mathrm{Bool}$ be an equivalence. If $(\mathrm{Bool},\mathrm{true},C,\phi)$ is a normalized two-point recognition floor (one empty/consistent point, one marked inconsistent point, unit-normalized cost, exhaustive two-point support), then $\phi=\mathrm{id}$ and $C(\Gamma)$ equals the canonical Boolean cost ($0$ on $\mathrm{false}$, $1$ on $\mathrm{true}$) for every $\Gamma$.
background
The module is the public T-1 through T8 forcing spine: T-1 is the absolute distinguishability floor, T0 the Boolean recognition-work split, then T1–T8 up through $\varphi$, the eight-tick cadence, and $D=3$. It stops before private operator/measurement layers.
A CostFunction on a configuration space obeys dichotomy (cost zero iff consistent) and independent additivity over joins that share no predicates. The concrete Boolean cost sends false to $0$ and true to $1$.
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 Bool showing that Bool is only the canonical representative. The sibling witness records that the standard Boolean data satisfy those axioms with mark true.
proof idea
One-line term proof. Apply the abstract uniqueness lemma for normalized two-point costs up to equivalence, feeding the hypothesis that the given data form a normalized two-point floor and the already-established witness that the canonical Boolean floor (identity equivalence, 0/1 cost) is itself such a floor. Uniqueness forces the equivalence to be refl and the cost to agree pointwise with the Boolean recognition cost.
why it matters
Locks the unique normalized 0/1 representative of the absolute Boolean floor before the rest of the spine. Downstream, absolute_bool_floor_unique_normalized_01 (here and in UnifiedForcingChain) quotes it to conclude that any absolute-floor witness plus a normalized two-point floor on Bool collapses to the same cost; the chain also re-exports this uniqueness statement itself.
That uniqueness is the T-1/T0 hinge of the forcing chain: without a unique Boolean recognition-work split, later steps (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) would not sit on a single floor. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.