floorRealizationFromNormalized
plain-language theorem explainer
From a normalized Boolean two-point recognition floor, extract the Law-of-Logic realization consumed by Universal Forcing. Anyone working the T4-to-T5 bridge cites this: the floor is no longer a free hard-coded artifact but the explicit source of the realization. The body is a one-line call of the distinction-to-realization constructor on Bool with points false and true.
Claim. Given a normalized two-point recognition floor on $\mathrm{Bool}$ with marked point $\mathsf{true}$, the Boolean recognition-work cost, and the identity equivalence $\mathrm{Bool}\simeq\mathrm{Bool}$, return the associated Law-of-Logic realization (carrier, comparison cost, identity element, and step data).
background
The Unified Forcing Chain module aims to force every level T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). T4 supplies a recognition floor; T5 needs a continuous positive-ratio surface on which unique $J$ is proved. The bridge between them is a shared Law-of-Logic realization whose extracted arithmetic is independent of the ambient carrier.
A normalized two-point recognition floor is the abstract Boolean floor: one empty/consistent point, 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. A Law-of-Logic realization packages a carrier, a comparison cost, an identity element, and a step/generator action with the structural laws Universal Forcing needs; the invariant target is the arithmetic object extracted from the identity/step data, not the ambient type.
Upstream, the distinction-to-realization constructor builds such a realization from any two-point distinction. Canonical arithmetic on a realization is the initial Peano object, realization-independent at the structural level.
proof idea
One-line wrapper. Ignore the floor hypothesis in the term (it is present only so callers must supply a normalized-floor proof) and apply the distinction-to-realization constructor to carrier $\mathrm{Bool}$ with distinguished points $\mathsf{false}$ and $\mathsf{true}$, discharging distinctness by decide. Definitionally this is the same object as the hard-coded Boolean floor realization; the eq lemma records that by rfl.
why it matters
This definition is the projection step that makes the T4-to-T5 bridge certificate honest: the realization is the image of T4's normalized floor, not an extra assumption. Downstream, the equality lemma shows it coincides with the canonical Boolean realization; the positive-ratio arithmetic comparison shows the floor realization and every continuous positive-ratio realization force the same Peano carrier; and both T4_To_T5_Realization_Bridge and t4_to_t5_bridge_holds package this object as the floor side of the bridge.
In the forcing chain, T5 is unique $J$ (the cost $J(x)=(x+x^{-1})/2-1$) under d'Alembert, normalization, and calibration. The bridge certificate states that the pre-analytic recognition floor yields a setting-independent realization, the continuous positive-ratio surface used by T5 is an admissible realization of the same interface, and Universal Forcing identifies their extracted arithmetic so the RCL theorem applies on the continuous side. Without this projection, T4 and T5 would sit on disconnected carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.