positiveRatioRealization
plain-language theorem explainer
Any comparison operator on positive reals that obeys the laws of logic packages as a setting-independent Law-of-Logic realization on the positive-ratio carrier. Authors of the T4-to-T5 bridge and the floor-to-ratio arithmetic equivalence cite this packaging. The body is a one-line wrapper around the positive-ratio embedding constructor.
Claim. Given a comparison operator $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ that satisfies the laws of logic (identity, non-contradiction, excluded middle, scale invariance, and route independence), there is an associated Law-of-Logic realization whose carrier is $\{x\in\mathbb{R}:x>0\}$ with real-valued comparison cost.
background
The Unified Forcing Chain module aims to force the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration. Logic itself (T0) is derived from cost minimization rather than assumed, and later steps extract a unique cost $J$, the golden ratio $\varphi$, the eight-tick octave, and $D=3$.
A comparison operator is a two-argument real cost of comparing quantities. It satisfies the laws of logic when the Aristotelian constraints hold together with scale invariance and route independence, so the derived one-argument cost on positive ratios is well-posed and non-vacuous. A Law-of-Logic realization is the setting-independent interface: a carrier, a cost type, a distinguished identity element, and a comparison map, from which Universal Forcing later extracts an arithmetic object (orbits / Peano carrier).
Upstream, ofPositiveRatioComparison embeds any such continuous positive-ratio comparison into that interface by taking the carrier to be strictly positive reals and the cost to be $\mathbb{R}$.
proof idea
One-line wrapper: the definition applies the upstream constructor that builds a Law-of-Logic realization from a comparison operator and a proof that it satisfies the laws of logic. No extra obligations are discharged here; carrier, cost, zero, and compare fields are those fixed by the positive-ratio embedding.
why it matters
This packaging is the continuous side of the honest T4-to-T5 bridge. Downstream, floor_to_positive_ratio_arithmetic and its normalized variant produce a canonical equivalence between the Peano carriers forced by the Boolean floor realization and by every positive-ratio realization built here: positive ratios are not definitionally the Boolean floor, but they force the same arithmetic object.
The T4-to-T5 realization bridge structure records both a nonempty floor realization and a family of positive-ratio realizations (this definition) under the hypothesis that recognition is forced. That bridge is the handoff from ledger/observables (T4) into uniqueness of $J$ (T5) in the forcing chain. Without a uniform realization interface, the continuous and discrete sides of the chain could not be compared inside Universal Forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.