normalized_two_point_floor_unique
plain-language theorem explainer
Any two normalized two-point recognition floors sharing the same configuration space, marked point, cost, and Bool equivalence are propositionally equal. Absolute-floor and T-1 arguments cite this to treat the Boolean floor as unique rather than choice-dependent. The proof is one-line subsingleton elimination on a Prop structure.
Claim. Let $C$ be a configuration space, $m \in C$ a marked point, $c$ a cost function on $C$, and $e : C \simeq \mathrm{Bool}$ an equivalence. If $h_1$ and $h_2$ are both witnesses that $(C,m,c,e)$ is a normalized two-point recognition floor (one empty/consistent point, one marked inconsistent point, unit recognition-work cost, exhaustive two-point support), then $h_1 = h_2$.
background
The module UnifiedForcingChain aims to force the full T-1 through T8 ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language Prop distinction plus a non-singleton universe, realized concretely as a two-point recognition floor.
A configuration space supplies an empty configuration, a join, consistency, and independence. A cost function on it obeys dichotomy (cost zero iff consistent) and independent additivity. The structure NormalizedTwoPointRecognitionFloor packages the abstract Boolean floor: the mark is not empty, every configuration is empty or marked, consistency is exactly emptiness, the cost is the unit 0/1 recognition-work indicator pulled back along an equivalence to Bool. Bool is only the canonical representative, not an extra assumption.
Uniqueness of such a floor, for fixed orientation, cost, and equivalence, is what this theorem records.
proof idea
One-line term proof: Subsingleton.elim. The floor structure is a Prop, so any two inhabitants are equal by the subsingleton instance on propositions (proof irrelevance). No field-by-field case analysis is required.
why it matters
This pins uniqueness of the normalized two-point floor so downstream code can treat the absolute Boolean floor as a single object. It is re-exported and used in TMinus1ToT8Bridge under the same name, feeding the bridge from the absolute floor into the T0–T8 inevitability chain.
In the module's stronger claim, T-1 (absolute floor) is the precondition that the chain is statable at all; uniqueness prevents hidden choice of representative when logic is later forced from cost minimization (T0) and the rest of the ladder (unique J, φ, eight-tick, D=3) is derived. The companion fact that cost on such a floor is the pulled-back 0/1 indicator is the theorem-level form of unit recognition work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.