ratGt_toReal
plain-language theorem explainer
The integer-level certificate RatGt p q x (with q > 0) is exactly the real strict inequality toReal(x) < p/q under the GoldenInt evaluation map. Anyone transporting sigma0 rational brackets on φ-ladder elements into classical ℝ inequalities cites this. The proof rewrites the positivity witness via the sign bridge and the affine evaluation of the bracket, then finishes by linear arithmetic over ℝ.
Claim. Let $x = a + b\varphi$ be an element of the golden integers $\mathbb{Z}[\varphi]$, and let $p,q\in\mathbb{Z}$ with $q>0$. If the sigma0 rational-greater certificate $\mathrm{RatGt}(p,q,x)$ holds, then under the evaluation $x\mapsto a+b\varphi_{\mathbb{R}}$ one has $\mathrm{toReal}(x) < p/q$ in $\mathbb{R}$.
background
This module is the sigma1 display bridge from the golden ring $\mathbb{Z}[\varphi]$ into $\mathbb{R}$. Elements are pairs $\langle a,b\rangle$ for $a+b\varphi$, and toReal sends them to $a + b\cdot\varphi_{\mathbb{R}}$ with the classical golden ratio from PhiForcing. The derivation of T6 (φ forced as the unique positive golden root) lives entirely in $\mathbb{Z}[\varphi]$ at sigma0; only the continuum display costs classical choice.
RatGt p q x is the decidable integer certificate that the bracket witness is positive in the sigma0 sense. The companion lemma toReal_ratWitness evaluates that witness to the affine form $q\cdot\mathrm{toReal}(x)-p$. The sign bridge isPos_iff_toReal_pos identifies the integer positivity predicate with genuine real positivity of the evaluation, so sigma0 order facts become real order facts without a private surrogate order.
Upstream, toReal_neg supplies additivity of negation under evaluation. Together these make rational brackets on golden integers readable as ordinary real inequalities $x < p/q$.
proof idea
Start from the hypothesis RatGt p q x, which packages integer positivity of a bracket witness. Apply isPos_iff_toReal_pos to obtain a real positivity statement. Rewrite that witness with toReal_ratWitness and toReal_neg, so positivity becomes a statement about $\pm(q\cdot\mathrm{toReal}(x)-p)$. Cast $q>0$ to $\mathbb{R}$, rewrite the target via lt_div_iff₀, push casts, and close with nlinarith. The argument is a short tactic chain: sign bridge, affine evaluation, then real linear arithmetic.
why it matters
This is the one-line transport that turns sigma0 rational brackets into classical real inequalities on φ and the φ-ladder. Downstream, ladder_ratio_real_brackets uses it to display forced brackets on φ, φ⁵, and φ⁸ as genuine real bounds (the arithmetic was already decided at sigma0). The mass-ratio binding layer depends on it heavily: muE_window_between_rungs reads the electron window as $φ^{11}<R<φ^{12}$, muE_sq_between as $φ^{21}<R^2<φ^{23}$, and muE_pow63_gt as $φ^{698}<R^{63}$.
In the Recognition framework this sits on the T6 display path: φ is forced inside $\mathbb{Z}[\varphi]$, and only here is that force shown to match the continuum golden ratio used in mass-ladder and rung-window statements. It does not re-derive uniqueness of φ; it only exports already-proved integer certificates into ℝ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.