ratLt_toReal
plain-language theorem explainer
The decidable integer predicate that a rational p/q sits strictly below a golden integer x is exactly the real inequality p/q < toReal(x), once q > 0. Anyone transporting sigma0 ladder or mass-ratio brackets into classical ℝ cites this bridge. The proof rewrites the positivity witness through the evaluation map and finishes by linear arithmetic over ℝ.
Claim. Let $p,q\in\mathbb{Z}$ with $q>0$, and let $x\in\mathbb{Z}[\varphi]$. If the sigma0 predicate $\mathrm{RatLt}(p,q,x)$ holds (i.e. $q\cdot x-p$ is positive in the golden ring), then $\frac{p}{q}<\mathrm{toReal}(x)$ in $\mathbb{R}$.
background
This lives in the GoldenIntReal display bridge: the sigma1 module that evaluates the golden ring $\mathbb{Z}[\varphi]$ into $\mathbb{R}$ once, after T6 has already forced $\varphi$ inside $\mathbb{Z}[\varphi]$ at sigma0. Elements are pairs $\langle a,b\rangle$ for $a+b\varphi$, and $\mathrm{toReal}(\langle a,b\rangle)=a+b\cdot\varphi_{\mathbb{R}}$ with $\varphi_{\mathbb{R}}$ the classical golden ratio from PhiForcing.
The ladder-ratio layer supplies two decidable integer predicates. $\mathrm{RatLt},p,q,x$ means $\mathrm{IsPos}(q\cdot x-p)$, i.e. the rational $p/q$ lies strictly below $x$ when $q>0$. Its companion $\mathrm{RatGt}$ is the dual upper bracket. The sign bridge $\mathrm{isPos_iff_toReal_pos}$ identifies the integer positivity predicate with ordinary real positivity of the evaluation, so sigma0 order facts become real order facts without a private surrogate order.
The witness identity $\mathrm{toReal}(q\cdot x-p)=q\cdot\mathrm{toReal}(x)-p$ is the algebraic link that turns the integer certificate into an affine real inequality.
proof idea
Unpack $\mathrm{RatLt}$ as $\mathrm{IsPos}$ of the bracket witness $q\cdot x-p$. Apply the sign bridge $\mathrm{isPos_iff_toReal_pos}$ to obtain $0<\mathrm{toReal}(q\cdot x-p)$. Rewrite that evaluation via $\mathrm{toReal_ratWitness}$ to $0<q\cdot\mathrm{toReal}(x)-p$. Cast $q>0$ to $\mathbb{R}$, convert the target $p/q<\mathrm{toReal}(x)$ by $\mathrm{div_lt_iff}_0$, and close with $\mathrm{nlinarith}$.
why it matters
This is the lower-bracket half of the continuum tax for rational comparisons against golden integers. Downstream, $\mathrm{ladder_ratio_real_brackets}$ uses it (with the dual upper map) to read the sigma0 brackets on $\varphi$, $\varphi^5$, and $\varphi^8$ as genuine real inequalities on the classical golden ratio; those powers sit on the RS phi-ladder (T6 fixed point, eight-tick octave context).
In MassRatioBindingReal it feeds $\mathrm{muE_window_between_rungs}$ ($\varphi^{11}<R<\varphi^{12}$), $\mathrm{muE_sq_between}$, and $\mathrm{muE_pow88_lt}$, which are the sigma1 readings of the electron mass-ratio window certificates. Without this lemma the sigma0 deviation arithmetic stays trapped in $\mathbb{Z}[\varphi]$ and cannot speak to classical real bounds used in the mass formula and alpha-band display. It does not itself force $\varphi$ or derive the mass ladder; it only transports already-proved integer brackets across the display boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.