floorRealization
plain-language theorem explainer
The Boolean two-point floor (false versus true) is packaged as a concrete Law-of-Logic realization. Anyone bridging T4 recognition to T5 J-uniqueness cites this as the canonical discrete carrier from which arithmetic is extracted. Construction is a one-line call to the universal instantiation-from-distinction map, with decidable inequality of the two Booleans.
Claim. Let the floor realization be the Law-of-Logic realization obtained by applying the universal distinction constructor to the Boolean carrier with distinguished points $\mathsf{false}$ and $\mathsf{true}$ (whose inequality is decidable). The result is a concrete realization of type $\mathrm{LogicRealization}$ at universe levels $0,0$.
background
The Unified Forcing Chain module aims to show that every step from the absolute floor through T0–T8 is forced by the cost foundation (Recognition Composition Law plus normalization and calibration), rather than merely compatible with it. T−1 records that a meta-language Prop distinction and a non-singleton universe make the chain statable; T0 then forces logic from cost minimization.
A Law-of-Logic realization is a structure supplying a carrier, a cost type with zero, a comparison map, an identity element, and the step/generator data needed by Universal Forcing. The invariant target is not the ambient carrier itself but the arithmetic object extracted from the identity/step orbit.
The Boolean recognition floor is the minimal two-point distinction: two values that are not equal. Instantiating a realization from that distinction turns the absolute floor into a usable Law-of-Logic object rather than a free hard-coded artifact.
proof idea
One-line definitional wrapper. Apply UniversalInstantiationFromDistinction.logicRealizationOfDistinction to the carrier Bool, the two points false and true, and a decidability proof of false ≠ true obtained by decide. No further algebraic work; the constructor builds the full realization structure from that primitive distinction.
why it matters
This definition is the concrete T4-side carrier used by the T4-to-T5 realization bridge. Downstream, floor_to_positive_ratio_arithmetic exhibits a Peano-carrier equivalence between the arithmetic extracted from this floor realization and that of any continuous positive-ratio realization satisfying the laws of logic; the bridge structure packages nonempty floor recognition, floor distinction, this realization, and the positive-ratio family.
In the forcing chain, T4 (recognition from ledger plus observables) must hand a genuine realization to T5 (unique J from d'Alembert, normalization, and calibration). Packaging the Boolean floor this way makes the handoff definitional rather than an external assumption. The companion equality floorRealizationFromNormalized_eq records that the normalized-floor path lands on the same object, so callers who supply a normalized two-point floor proof still recover this canonical realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.