RatGt
plain-language theorem explainer
Defines the decidable predicate that a rational p/q sits strictly above an element x of the golden ring ℤ[φ], via positivity of the integer witness p − q·x. Anyone proving certified upper brackets on φ-ladder rungs (φ, φ⁵, φ⁸) cites it. The body is a one-line reduction to the existing sign predicate IsPos on a negated ratWitness.
Claim. For integers $p,q$ and $x\in\mathbb{Z}[\varphi]$, the predicate $\mathrm{RatGt}(p,q,x)$ asserts that the rational $p/q$ lies strictly above $x$ (when $q>0$ over $\mathbb{R}$). Equivalently it is the constructive positivity statement $0 < p - q\cdot x$ in $\mathbb{Z}[\varphi]$, obtained by applying the golden-ring positivity test to the witness of $-p$, $q$, and $-x$.
background
The module LadderRatioBounds certifies dimensionless φ-ladder ratios entirely inside the golden ring ℤ[φ], without continuum arithmetic. Elements are pairs $(a,b)$ for $a+b\varphi$ with multiplication folded by $\varphi^2=\varphi+1$. The RS mass law places spectrum rungs on exact powers $\varphi^k$; this file makes those powers and their rational brackets kernel-decidable (sigma0).
The witness map sends $(p,q,x)$ to $q\cdot x-p\in\mathbb{Z}[\varphi]$. Its sibling lower predicate asserts $0<q\cdot x-p$ (i.e. $p/q<x$). Positivity on ℤ[φ] is the constructive predicate IsPos: for $x=a+b\varphi$ one tests the pair $(2a+b,b)$ against the $\sqrt{5}$-irrationality comparison of integer squares, so every concrete instance closes by decide inside {propext, Quot.sound}.
The dual upper predicate is obtained by sign flip: positivity of the witness for $(-p,q,-x)$ is exactly $0<p-q\cdot x$.
proof idea
Pure definitional wrapper. Unfold to IsPos applied to ratWitness of $(-p)$, $q$, and $-x$. Because IsPos is already a DecidablePred on GoldenInt, the derived instance for this predicate is immediate by unfold and infer_instance. No separate lemma is needed; the arithmetic content lives in ratWitness and the √5 sign test behind IsPos.
why it matters
Upper halves of every certified ladder bracket are instances of this predicate: φ < 1618034/1000000, φ⁵ < 11.10, φ⁸ < 46.979, and the bundled theorem that pins φ, φ⁵, and the octave rung φ⁸ inside explicit rational intervals by choice-free integer arithmetic. Downstream, GoldenIntReal.ratGt_toReal lifts the sigma0 predicate (for $q>0$) to the genuine real inequality $\mathrm{toReal}(x)<p/q$, feeding the T5 display bridge that identifies the sigma0 cost ladder with classical J-cost on the φ-ladder. In the forcing chain this supports T6 (φ as self-similar fixed point) and the mass-ratio binding thread: dimensionless rung gaps stay certified before any Classical.choice evaluation into ℝ. MassRatioBinding also consumes it for spectrum ratio bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.