positiveRatioRealization
plain-language theorem explainer
Packages any comparison operator on positive reals that obeys the Aristotelian laws of logic as a setting-independent logic realization. Cited by the T4-to-T5 bridge and by the arithmetic-equivalence lemmas that identify the Boolean floor with continuous positive-ratio carriers. 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), produce a logic realization whose carrier is the strictly positive reals $\{x:\mathbb{R}\mid 0<x\}$ and whose comparison cost is induced by $C$.
background
The module exposes the public T-1 through T8 forcing spine, from the absolute distinguishability floor through D=3. This definition sits at the T4-to-T5 interface: T4 supplies a recognition witness on the discrete floor; T5 forces uniqueness of the canonical reciprocal cost J.
A comparison operator is a two-argument real-valued cost of comparing quantities. It satisfies the laws of logic when the four Aristotelian constraints hold together with scale invariance and non-triviality. A logic realization is a carrier equipped with comparison cost, zero, and the structural laws needed by Universal Forcing; the invariant target is the arithmetic object extracted from identity/step data, not the ambient carrier.
The upstream constructor embeds any such continuous positive-ratio comparison into that interface, taking carrier ${x:\mathbb{R}\mid 0<x}$ and cost $\mathbb{R}$.
proof idea
One-line wrapper that applies the upstream constructor ofPositiveRatioComparison to the given comparison operator and its laws-of-logic certificate. No extra proof obligations are discharged here; the carrier, cost, and structural fields are filled entirely by that constructor.
why it matters
This is the public bridge copy of the continuous positive-ratio realization used throughout the forcing spine. Downstream, floor_to_positive_ratio_arithmetic shows that the Boolean floor and every such positive-ratio realization force canonically equivalent Peano arithmetic (orbit equivalence), so positive ratios are an admissible realization rather than a definitional rewrite of the floor. The same object is packaged into T4_To_T5_Realization_Bridge and t4_to_t5_bridge_holds, which hand the floor and positive-ratio realizations to the T5 step (J-uniqueness: $J(x)=(x+x^{-1})/2-1$). Parallel copies live in UnifiedForcingChain, including the normalized-floor variant. Without this packaging, the T4-to-T5 arithmetic bridge has no continuous carrier to compare against the discrete floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.