floorRealizationFromNormalized_eq
plain-language theorem explainer
On the Boolean two-point floor with the standard unit recognition cost and the identity equivalence, the realization built from a normalized-floor witness equals the canonical Boolean logic realization. Foundation authors cite this when routing T-1 through a supplied normalized floor rather than a hard-coded Bool construction. The proof is pure definitional equality (rfl).
Claim. If $h$ is a normalized two-point recognition floor on $\mathrm{Bool}$ with marked point $\mathsf{true}$, the standard Boolean recognition-work cost ($0$ on $\mathsf{false}$, $1$ on $\mathsf{true}$), and the identity equivalence $\mathrm{Bool}\simeq\mathrm{Bool}$, then the logic realization constructed from $h$ equals the canonical Boolean floor realization.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 spine from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language distinction that makes the chain statable at all.
A normalized two-point recognition floor is the abstract Boolean floor: one empty/consistent configuration, one marked inconsistent point, a unit-normalized recognition-work cost, and an equivalence to $\mathrm{Bool}$ showing Bool is only the canonical representative. The concrete Boolean cost sends false to 0 and true to 1.
The canonical floor realization is the logic realization obtained by instantiating distinction on Bool with empty false and mark true. The normalized constructor builds the same object from an explicit normalized-floor witness, so callers can supply the floor proof rather than bake Bool into the API.
proof idea
One-line definitional equality. Both sides reduce to the same term (the distinction-based logic realization on Bool with false empty and true marked), so rfl closes the goal. No lemmas are applied beyond unfolding the definitions of the normalized constructor and the canonical realization.
why it matters
This sits at the T-1 entry of the complete inevitability chain: absolute floor before T0 (logic from cost) and the rest of T0-T8. It records that the normalized-floor API is not a second realization, only a different packaging of the same Boolean floor. Downstream code can therefore accept a normalized-floor hypothesis without changing the forced logic object that feeds T0 and the cost-minimization story. No used-by edges are recorded yet; the lemma is infrastructure for callers that prefer the normalized interface over the hard-coded Bool path. It does not itself force T0-T8; it only identifies two presentations of the floor realization that those steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.