NormalizedTwoPointRecognitionFloor
plain-language theorem explainer
Abstract Prop-bundle for a two-point recognition floor: one empty consistent state, one marked unit-cost state, and an equivalence to Bool. Cited by absolute-floor uniqueness and T0 logic-from-cost results in the T−1→T8 bridge. Definitional structure of seven field obligations; instances are built by discharging those fields, not by a separate proof term.
Claim. A configuration type $Config$ with empty point $e$, marked point $m$, cost $C$, and equivalence $\phi:Config\simeq\mathbf{Bool}$ is a normalized two-point recognition floor when $m\neq e$; every $\Gamma$ equals $e$ or $m$; consistency holds iff $\Gamma=e$; $C(e)=0$ and $C(m)=1$; and $\phi(e)=\mathsf{false}$, $\phi(m)=\mathsf{true}$.
background
In the Unified Forcing Chain, T−1 (absolute floor) is the precondition that a meta-language can state a non-singleton distinction at all. Configurations carry an empty point and a consistency predicate; a cost function assigns recognition work. The Boolean case (false empty, true marked, indicator cost) is the concrete model.
This structure abstracts that model. It packages the two-point shape, unit normalization of cost, and an explicit equivalence to Bool so that Bool is only the canonical representative, not a hidden extra assumption. Downstream uniqueness theorems then show any such floor is equivalent to the Boolean one.
The local setting is the complete inevitability chain from the Recognition Composition Law plus normalization and calibration: every step T0–T8 is forced from cost, once the absolute floor is available.
proof idea
No proof body: this is a Prop-valued structure. An instance is a record of seven obligations (mark ≠ empty; exhaustive two-point cover; consistency iff empty; cost 0 on empty and 1 on mark; equivalence sends empty→false and mark→true). Concrete instances (e.g. the Boolean floor with identity equivalence) discharge each field by direct case analysis on Bool or by the definition of the indicator cost.
why it matters
This is the abstract interface for the absolute floor inside the T−1→T8 bridge. Downstream results use it to prove: the Boolean floor is a normalized two-point floor; any such floor has cost equal to the 0/1 indicator pulled back along the Bool equivalence; the equivalence is unique for fixed empty/mark; costs agree pointwise up to that equivalence; and on Bool with mark true the data collapse to the identity equivalence and the canonical Boolean recognition cost.
In framework terms it underwrites T−1 (absolute floor) and the start of T0 (logic from cost minimization: consistency is the cheap empty state). Without a normalized two-point shape, the claim that Bool is forced rather than assumed cannot be stated. It does not itself force φ, the eight-tick octave, or D=3; those sit later in the chain (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.