normalized_two_point_floor_unique
plain-language theorem explainer
Any two witnesses that the same configuration data form a normalized two-point recognition floor are propositionally equal. Foundation authors cite this when treating the Boolean floor as a unique abstract object rather than a choice of proof. The argument is a one-line Subsingleton elimination: the floor predicate is a Prop, so proof irrelevance finishes it.
Claim. Fix a configuration space $Config$ with empty configuration, a marked point $mark$, a recognition cost $C$, and an equivalence $Config \simeq \mathrm{Bool}$. If $h_1$ and $h_2$ are any two proofs that $(Config, mark, C, \simeq)$ is a normalized two-point recognition floor (exactly two points, unit-normalized cost, Boolean representative), then $h_1 = h_2$.
background
The module is the public T-1 through T8 forcing spine: absolute distinguishability floor, Boolean recognition-work split, cost-form Meta-Principle, discreteness, ledger, reciprocal cost uniqueness, $\varphi$, eight-tick cadence, and $D=3$. It stops before private operator layers.
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: one empty/consistent point, one marked inconsistent point, unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ showing Bool is only the canonical representative, not a privileged ontology.
Upstream cost and config machinery (CostFromDistinction, projector and multiplicative recognizer costs) supply the ambient types; this lemma only concerns uniqueness of floor witnesses once those data are fixed.
proof idea
One-line term proof: Subsingleton.elim _ _. The floor is declared as a Prop-valued structure, so any two inhabitants are equal by Lean's proof irrelevance (the Subsingleton instance on Prop). No field-by-field rewriting or cost algebra is required; the equality is purely propositional uniqueness of witnesses for fixed Config, mark, cost, and toBoolEquiv.
why it matters
Re-exported into UnifiedForcingChain.normalized_two_point_floor_unique with the same statement: two normalized two-point recognition floors over the same orientation, cost, and equivalence are propositionally equal. That chain is the public T0–T8 spine; T0 is the Boolean recognition-work split, and uniqueness of the floor witness keeps later steps (T2 two-state discreteness, T5 J-uniqueness, T6 $\varphi$) from depending on a choice of proof object.
Without this, every downstream bridge that assumes "the" normalized floor would carry an extra equality obligation. It does not itself force the $0/1$ indicator cost (a sibling theorem does that); it only locks the floor predicate as a unique certificate so the forcing spine can treat the Boolean representative as canonical without hidden definitional choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.