normalized_two_point_equiv_unique
plain-language theorem explainer
For a fixed empty configuration and marked point, any two normalized two-point recognition floors determine the same equivalence from the configuration space onto Bool. Absolute-floor and T0 workers cite this when collapsing two presentations of the Boolean floor to one canonical model. The argument is a two-line case split on exhaustiveness: both equivalences send empty to false and the mark to true.
Claim. Let $C$ be a configuration space with empty point $\emptyset$ and marked point $m\neq\emptyset$. Let $K_1,K_2$ be cost functions on $C$ and $e_1,e_2:C\simeq\mathbf{Bool}$ equivalences such that each quadruple $(C,m,K_i,e_i)$ is a normalized two-point recognition floor (every configuration is $\emptyset$ or $m$; consistency is emptiness; recognition cost is unit-normalized on the mark). Then $e_1=e_2$.
background
The Unified Forcing Chain module shows that T-1 through T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). The absolute floor (T-1) is the remaining precondition that the chain is even statable: a meta-language with a genuine distinction and a non-singleton universe.
A configuration space supplies an empty point, a join, a consistency predicate, and an independence relation. A cost function on that space obeys dichotomy (cost vanishes exactly on consistent configurations) and independent additivity. The 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 Bool showing that Bool is only the canonical representative, not a hidden extra assumption.
The structure fields used here include exhaustiveness (every configuration is empty or marked) and the forced values of the equivalence on those two points.
proof idea
Pointwise extensionality on the two equivalences. For an arbitrary configuration $\Gamma$, exhaustiveness from the first floor splits into $\Gamma=\emptyset$ or $\Gamma=m$. In the empty case both equivalences evaluate to the same Boolean by the empty-point clauses; in the marked case both evaluate to the same Boolean by the mark clauses. The two cost functions never enter the argument: uniqueness of the equivalence depends only on the shared empty/mark shape and the floor's forced Bool values.
why it matters
This uniqueness is the first half of the absolute-floor rigidity package. Downstream, the sibling result that any two normalized two-point recognition costs over the same two-point shape agree pointwise applies it (or its bridge twin) to pin the cost as well as the equivalence. Together they show that the Boolean floor is unique up to the shared empty/mark data, so T-1 does not smuggle a choice of presentation.
In the forcing chain this sits at T-1 (absolute floor) and feeds T0 (logic forced from cost minimization). Without unique equivalence-to-Bool, later steps that treat Bool as the canonical two-point model would be presentation-dependent. The module's stronger claim, complete inevitability rather than mere compatibility, needs exactly this kind of rigidity at the floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.