floorRealization
plain-language theorem explainer
The Boolean two-point set, with the named distinction false ≠ true, is packaged as a concrete Law-of-Logic realization. Workers on the T4→T5 bridge and the floor-to-positive-ratio arithmetic equivalence cite this object as the canonical discrete floor. Construction is a one-line application of the universal instantiation theorem for named distinctions.
Claim. Let $\mathsf{Bool}$ be the two-element carrier with distinguished points $\mathsf{false}\neq\mathsf{true}$. The floor realization is the Law-of-Logic realization on carrier $\mathsf{Bool}$ with cost type $\mathbb{N}$, identity and comparison data induced by that named distinction via universal instantiation from distinction.
background
The module exposes the public T-1 through T8 forcing spine, from the absolute distinguishability floor through D=3. A Law-of-Logic realization is a carrier equipped with a comparison cost, an identity element, a step/generator action, and the structural laws demanded by the Universal Forcing program. The invariant target is not the ambient carrier; it is the arithmetic object extracted from the identity/step data.
Universal instantiation states that any carrier with a named distinction $x\neq y$ is already a Law-of-Logic realization on that carrier (cost type $\mathbb{N}$). The Boolean floor is the minimal discrete instance of that pattern: two points, one inequality, decidable equality. Upstream, the same construction appears in the unified forcing chain as the Boolean recognition floor.
proof idea
One-line definitional wrapper. Apply the universal instantiation constructor to carrier $\mathsf{Bool}$, points $\mathsf{false}$ and $\mathsf{true}$, and the decidable proof $\mathsf{false}\neq\mathsf{true}$ (discharged by decide). No further rewriting or case analysis; the structure fields (carrier, cost, zero, compare, identity) are filled by that constructor.
why it matters
This is the concrete Boolean recognition floor used throughout the public T-1–T8 spine. Downstream it supplies the floor side of the T4→T5 realization bridge (recognition witness on the discrete floor to uniqueness of the canonical reciprocal cost J), and it is the left-hand realization in the floor-to-positive-ratio arithmetic equivalence: the floor and every continuous positive-ratio realization force the same Peano arithmetic object up to canonical equivalence of orbits.
In the forcing chain this sits at the T2/T4 discrete-floor layer that feeds T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). The same definition is re-exported in the unified forcing chain, and the normalized-floor variant is definitionally equal to it. Without a named floor realization the T4→T5 bridge structure cannot be inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.