floor_to_positive_ratio_arithmetic
plain-language theorem explainer
The Boolean absolute-floor realization and any continuous positive-ratio realization that obeys the laws of logic force canonically equivalent Peano arithmetic carriers. Anyone comparing discrete floor models with continuum ratio models of the forcing chain cites this bridge. The proof is a one-line transport: both orbits are identified with the same logic-natural numbers, then composed.
Claim. For any comparison operator $C:\mathbb{R}_{>0}\times\mathbb{R}_{>0}\to\mathbb{R}$ that satisfies the laws of logic (identity, non-contradiction, excluded middle, scale invariance, route independence), the Peano carrier of the arithmetic forced by the Boolean floor realization is equivalent, as a type, to the Peano carrier of the arithmetic forced by the continuous positive-ratio realization of $C$.
background
The Unified Forcing Chain module aims to derive T-1 through T8 as inevitabilities 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. The Boolean floor realization builds a logic realization from the two-point distinction false/true.
A comparison operator is a two-argument real-valued cost of comparing positive quantities. It satisfies the laws of logic when the four Aristotelian constraints hold together with scale invariance and non-triviality, so a one-argument cost on positive ratios is well-defined. The continuous positive-ratio realization turns any such operator into a logic realization in the same universal-forcing interface as the floor.
Universal forcing extracts an arithmetic object (with a Peano carrier) from any logic realization. The carriers here are identified with the realization orbits via orbitEquivLogicNat, so arithmetic equivalence reduces to orbit equivalence.
proof idea
One-line wrapper. Rewrite the goal as an equivalence of orbits of the two realizations (the Peano carriers are definitionally those orbits under arithmeticOf). Compose floorRealization.orbitEquivLogicNat with the inverse of (positiveRatioRealization C h).orbitEquivLogicNat. Both sides match the same logic-natural-number type, so the composite is the required carrier equivalence.
why it matters
This is the honest bridge between the discrete absolute floor (T-1) and continuum positive-ratio models used later in the chain. The doc-comment stresses that positive ratios are not definitionally the Boolean floor; they are an admissible realization whose forced arithmetic is canonically equivalent. Downstream, the TMinus1-to-T8 bridge reuses the same equivalence so later steps (T0 logic from cost, T5 unique $J$, T6 $\varphi$, T7 eight-tick, T8 $D=3$) can switch presentation without changing the forced Peano object.
Without this bridge, continuum ratio language and Boolean floor language would look like two competing foundations. With it, the Complete Inevitability Chain can treat them as interchangeable carriers of one arithmetic, keeping the stronger claim (every level forced, not merely compatible) intact across presentations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.