normalized_two_point_cost_unique_up_to_equiv
plain-language theorem explainer
On any two-point configuration space, two normalized recognition floors that share the same marked state force identical Bool equivalences and identical pointwise costs. Absolute-floor and T0 uniqueness arguments cite this to pin the recognition-work functional before logic is forced. The proof equates the equivalences first, then rewrites both costs as the same indicator of the marked point.
Claim. Let $\mathrm{Config}$ be a configuration space with marked point $m$, and let $C_1,C_2$ be cost functions each equipped with an equivalence $\mathrm{Config}\simeq\mathrm{Bool}$ making $(\mathrm{Config},m,C_i,e_i)$ a normalized two-point recognition floor (exhaustive empty/marked dichotomy, unit cost on the mark, zero on empty). Then $e_1=e_2$ and $C_1(\Gamma)=C_2(\Gamma)$ for every configuration $\Gamma$.
background
The module builds the complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. T-1 is the absolute floor: a meta-language distinction plus a non-singleton universe, realized here as a two-point recognition floor rather than an ad hoc Boolean assumption.
A configuration space supplies an empty point, a join, consistency, and independence. A cost function obeys dichotomy (cost zero iff consistent) and independent additivity. The structure NormalizedTwoPointRecognitionFloor packages the abstract Boolean floor: one empty/consistent point, one marked inconsistent point, unit-normalized recognition-work cost, and an equivalence to Bool showing Bool is only the canonical representative.
The local claim is uniqueness of that package once the marked point is fixed: no second normalized cost or second labeling can coexist on the same two-point shape.
proof idea
Term-mode, two steps. First apply normalized_two_point_equiv_unique to the two floor hypotheses to obtain equality of the Bool equivalences. Split the conjunction: the first conjunct is that equality. For the second, introduce an arbitrary configuration $\Gamma$ and rewrite both costs via normalized_two_point_cost_eq_indicator, which expresses each normalized floor cost as the indicator of the marked point under its equivalence; transport along the already-proved equivalence equality to finish.
why it matters
This is the uniqueness engine for the absolute floor (T-1) inside the unified forcing chain. Downstream, absolute_floor_unique_normalized_01 lifts it to any absolute-floor carrier, and bool_normalized_two_point_floor_unique specializes to the canonical Boolean floor: equivalence is Equiv.refl Bool and cost agrees with boolRecognitionCost. The bridge module re-exports both forms for the T-1 to T8 pipeline.
Without pointwise uniqueness, T0 (logic from cost minimization) would not know which recognition-work functional it is minimizing. The result closes the "Bool is only a representative" gap stated in the floor structure doc: the two-point shape, not a preferred encoding, determines the cost. It sits at the base of the stronger claim that every level T0-T8 is forced from the cost foundation rather than merely compatible with it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.