normalized_two_point_equiv_unique
plain-language theorem explainer
For fixed empty and marked states, any two normalized two-point recognition floors on the same configuration space induce the same equivalence to Bool. Cited when pinning the Boolean representative of the discrete recognition floor. Proof is a one-line pointwise case split on exhaustiveness: every configuration is empty or marked, and both floors send those points to the same Booleans.
Claim. Let $C$ be a configuration space with empty configuration $\mathrm{emp}$ and fixed marked state $m \neq \mathrm{emp}$. Suppose $c_1,c_2$ are cost functions and $\phi_1,\phi_2:C\simeq\mathbf{Bool}$ each make $(C,m,c_i,\phi_i)$ a normalized two-point recognition floor (two-point exhaustive shape, unit-normalized recognition-work cost, equivalence to $\mathbf{Bool}$). Then $\phi_1=\phi_2$.
background
This module is the public T-1 through T8 forcing spine: absolute distinguishability floor, Boolean recognition-work split, cost-form Meta-Principle, two-state discreteness, ledger bookkeeping, reciprocal cost uniqueness (T5), $\varphi$ from self-similarity (T6), eight-tick cadence (T7), and $D=3$ (T8).
A configuration space carries an empty configuration, a join, a consistency predicate, and independence. A cost function on it obeys dichotomy (cost zero iff consistent) and independent additivity. A normalized two-point recognition floor packages the abstract Boolean floor: one empty/consistent point, one marked inconsistent point, a unit-normalized recognition-work cost, and an equivalence to $\mathbf{Bool}$ showing Bool is only the canonical representative. Exhaustiveness says every configuration equals emp or the mark.
The theorem sits at the T2 layer (two-state discreteness of the floor): once empty and mark are fixed, the Bool labeling cannot vary between two such floors.
proof idea
Term-mode proof by pointwise extensionality of equivalences. Fix an arbitrary configuration $\Gamma$. Exhaustiveness of the first floor splits $\Gamma=\mathrm{emp}$ or $\Gamma=m$. In the empty case, rewrite both equivalences by their toBool_emp fields; in the marked case, rewrite by both toBool_mark fields. The two sides agree, so the equivalences are identical. No external lemmas beyond the structure fields of the normalized floor.
why it matters
Uniqueness of the Bool equivalence is the first half of uniqueness for the normalized two-point floor. It is consumed immediately by normalized_two_point_cost_unique_up_to_equiv (in this bridge and in UnifiedForcingChain), which upgrades equivalence uniqueness to pointwise agreement of the two recognition costs on the same two-point shape.
In the forcing spine this locks T2: the discrete floor is not merely two-point, but canonically labeled once empty and mark are chosen. That canonical labeling is what later steps treat as the Boolean recognition-work split (T0/T1) before T5 forces the reciprocal cost $J(x)=(x+x^{-1})/2-1$ and T6 forces $\varphi$. Without unique equivalence-to-Bool, cost uniqueness up to equivalence would not even be well-posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.