NormalizedTwoPointRecognitionFloor
plain-language theorem explainer
A normalized two-point recognition floor packages the abstract Boolean floor: a two-point configuration space with empty/consistent and marked/inconsistent states, unit-normalized recognition cost (0 on empty, 1 on mark), and an equivalence to Bool. Downstream uniqueness theorems cite it to show Bool is only the canonical representative. As a structure of propositions it is pure interface, not a proved claim.
Claim. A tuple $(Config, mark, C, \phi)$ is a normalized two-point recognition floor when: $mark \neq emp$; every configuration is either $emp$ or $mark$; consistency holds exactly on $emp$; $C(emp)=0$ and $C(mark)=1$; and the equivalence $\phi: Config \simeq \mathrm{Bool}$ sends $emp \mapsto \mathsf{false}$ and $mark \mapsto \mathsf{true}$.
background
The module is the public T-1 through T8 forcing spine: absolute distinguishability floor, Boolean recognition-work split, cost-form Meta-Principle, then discreteness, ledger, J-uniqueness, $\varphi$, eight-tick, and $D=3$. This structure sits at the T-1/T0 interface, abstracting the Boolean floor before uniqueness and cost-forcing theorems.
A configuration space (from CostFromDistinction) carries an empty configuration $emp$, a join monoid, a consistency predicate, and independence. A cost function assigns recognition work $C$ to configurations. The Boolean floor is the concrete two-point case: empty/consistent versus marked/inconsistent, with unit cost on the mark.
The doc-comment states the intent directly: 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.
proof idea
No proof body: this is a structure of propositions (a definitional interface). Inhabitants are built by supplying the seven fields. The canonical instance is bool_normalized_two_point_floor, which takes Config = Bool, mark = true, the Boolean recognition cost, and the identity equivalence, discharging each field by Bool case analysis and reflexivity.
why it matters
This interface is the abstract T-1/T0 floor used throughout the bridge. Downstream theorems that inhabit or exploit it include: bool_normalized_two_point_floor (Bool is an instance); normalized_two_point_cost_eq_indicator (cost is the 0/1 indicator pulled back along the Bool equivalence, the theorem-level form of unit recognition work); normalized_two_point_equiv_unique and normalized_two_point_cost_unique_up_to_equiv (equivalence and cost uniqueness for fixed empty/mark); bool_normalized_two_point_floor_unique and absolute_bool_floor_unique_normalized_01 (any normalized Boolean floor with mark true is the canonical one). The same uniqueness statement is re-exported in UnifiedForcingChain, so the structure anchors the absolute floor before T5 J-uniqueness and the rest of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.