bool_normalized_two_point_floor
plain-language theorem explainer
The Boolean configuration space with marked state true, unit cost (0 on false, 1 on true), and the identity equivalence is a normalized two-point recognition floor. Anyone citing the T2–T4 bridge or the canonical Boolean floor will use this witness. The proof discharges the structure fields by Bool case analysis and definitional equalities.
Claim. The type $\mathrm{Bool}$ with marked point $\mathsf{true}$, recognition cost $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$, and the identity equivalence $\mathrm{Bool}\simeq\mathrm{Bool}$, satisfies the normalized two-point recognition floor axioms: the mark is not empty, every configuration is empty or marked, consistency holds exactly at the empty point, costs are unit-normalized, and the equivalence sends empty to $\mathsf{false}$ and mark to $\mathsf{true}$.
background
This module is the public T-1 through T8 forcing spine. Early steps fix an absolute distinguishability floor (T-1), a Boolean recognition-work split (T0), and the cost-form Meta-Principle (T1); T2 then asserts two-state discreteness of that floor.
A normalized two-point recognition floor is the abstract package of that Boolean picture: one empty/consistent configuration, one marked inconsistent configuration, a unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ showing that $\mathrm{Bool}$ is only the canonical representative. The concrete cost used here is the Boolean recognition-work cost: $C(a)=0$ if $a=\mathsf{false}$ and $1$ otherwise.
The empty point of the Boolean config space is $\mathsf{false}$; the marked point is $\mathsf{true}$. The identity equivalence makes the representative explicit rather than an extra hidden assumption.
proof idea
Structure introduction with one tactic block per field. mark_ne_emp rewrites the assumed equality true = false and closes by Bool.noConfusion. exhaustive cases on the Boolean configuration and returns rfl on each branch. The remaining fields (consistent_iff_emp, cost_emp_zero, cost_mark_one, toBool_emp, toBool_mark) are pure definitional equalities closed by rfl. No external lemmas beyond Bool elimination are required.
why it matters
This is the concrete witness that the Boolean floor is a normalized two-point recognition floor, the bridge object between discreteness (T2) and recognition on the floor (T4). Downstream, bool_normalized_two_point_floor_unique upgrades the witness to uniqueness of cost and equivalence; canonical_two_point_floor_normalization packages it as the canonical normalization; and both t2_t3_to_t4_bridge_holds and t4_corollary_of_t2_t3 plug it in as normalized_floor so that T4 follows from T2 and T3.
In the forcing chain this sits at the T2–T4 interface: two-state discreteness plus ledger bookkeeping yield a recognition witness on the discrete floor, before T5 forces the reciprocal cost $J$ and T6 forces $\varphi$. It is pure foundation scaffolding for the public spine, not an operator-layer claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.