bool_normalized_two_point_floor
plain-language theorem explainer
The Boolean type with marked state true, unit recognition cost, and the identity equivalence is a normalized two-point recognition floor: one empty/consistent point, one marked/inconsistent point, exhaustive two-point config space, and unit-normalized cost. Anyone citing the T2–T3→T4 bridge or the canonical floor normalization uses this witness. The proof is pure case analysis on Bool plus definitional equalities.
Claim. The configuration space $\mathrm{Bool}$ with marked point $\mathsf{true}$, the Boolean recognition-work cost, and the identity equivalence $\mathrm{Bool}\simeq\mathrm{Bool}$ forms a normalized two-point recognition floor: $\mathsf{true}\neq\mathsf{false}$; every configuration is empty or marked; consistency is exactly emptiness; cost is $0$ on empty and $1$ on marked; and the equivalence sends empty to $\mathsf{false}$ and marked to $\mathsf{true}$.
background
The Unified Forcing Chain module aims to derive T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). The absolute floor (T-1) is the meta-language precondition: a non-singleton universe of distinctions so the chain is statable at all.
A normalized two-point recognition floor is the abstract Boolean floor: a config space with one empty/consistent point and one marked/inconsistent point, a unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ showing that $\mathrm{Bool}$ is only the canonical representative, not a hidden extra assumption. The Boolean recognition cost is the concrete cost function on $\mathrm{Bool}$ used at the T-1/T0 interface.
This theorem supplies the concrete inhabitant of that structure on $\mathrm{Bool}$ itself, with marked state $\mathsf{true}$ and the identity equivalence. Downstream uniqueness results then say any other normalized Boolean floor with the same orientation is propositionally this one.
proof idea
Tactic-mode field-by-field discharge of the structure. mark_ne_emp: assume $\mathsf{true}=\mathsf{false}$ and apply Bool.noConfusion. exhaustive: case-split on the configuration; each case is definitional equality to empty or mark. The remaining fields (consistent_iff_emp, cost_emp_zero, cost_mark_one, toBool_emp, toBool_mark) are all rfl against the Boolean recognition cost and the identity equivalence. No external lemmas beyond Bool's inductive structure.
why it matters
This is the concrete T-1/T0 floor witness that the rest of the forcing chain treats as canonical. It is consumed by canonical_two_point_floor_normalization, by the uniqueness theorem that any normalized Boolean floor with mark $\mathsf{true}$ agrees with this cost and the identity equivalence, and by the T2–T3→T4 bridge: T4 (Recognition) is obtained from discreteness plus the ledger by plugging this normalized floor in as the recognition substrate.
In the module's chain diagram, T4 is "Recognition ← Ledger + observables"; the Boolean floor is the minimal observable distinction. Without a proved normalized two-point floor, the T4 corollary of T2/T3 would have no concrete config space. The companion Subsingleton instance records that the normalization is unique at the audit level: any two inhabitants for the same parameters are propositionally equal.
Framework landmark: this sits at the absolute-floor end of the T-1→T8 inevitability chain, before J-uniqueness (T5), $\varphi$ (T6), eight-tick (T7), and $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.