RatLt
plain-language theorem explainer
Decidable integer predicate that a rational p/q lies strictly below an element of the golden ring ℤ[φ]. Anyone proving certified φ-ladder brackets at sigma0 cites it. Defined by constructive positivity of the witness q·x − p; no continuum, floats, or classical choice.
Claim. For integers $p,q$ and $x=a+b\varphi\in\mathbb{Z}[\varphi]$, the rational $p/q$ lies strictly below $x$ when the witness $q\cdot x-p\in\mathbb{Z}[\varphi]$ is constructively positive. When $q>0$, this is the choice-free integer encoding of the real inequality $p/q<x$.
background
The module LadderRatioBounds certifies forced φ-ladder ratios entirely inside ℤ[φ], so both decide and #eval close the brackets without Real.sqrt, Float, or native_decide. The RS mass law places spectrum rungs on the φ-ladder: states separated by rung gap k stand in exact ratio φ^k. φ itself is the T6 fixed point; φ^5 and φ^8 (the octave) are the representative rungs treated here.
GoldenInt is the ring of pairs (a,b) for a+b·φ with multiplication folded through φ²=φ+1. Constructive positivity IsPos on x asks that the paired form (s+b√5)/2 with s=2a+b be positive, decided by comparing integer squares s² and 5t² (a tie is impossible by √5-irrationality). The witness ratWitness p q x is the element q·x−p = ⟨q·a−p, q·b⟩ whose sign decides p/q ⋚ x.
Because IsPos is a decidable, choice-free predicate, every concrete instance of this lower-bound predicate reduces by kernel computation inside {propext, Quot.sound}. The real reading is deferred to GoldenIntReal (sigma1).
proof idea
One-line definitional wrapper: the predicate is exactly IsPos applied to ratWitness p q x. Unfolding gives positivity of ⟨q·a−p, q·b⟩, which is the integer form of 0 < q·x − p. No tactics, no lemmas beyond the already-decidable IsPos instance on GoldenInt.
why it matters
This is the lower half of the sigma0 bracket apparatus. Concrete lower bounds phi_lower, phi5_lower, and phi8_lower are instances closed by decide; the dual RatGt supplies the matching uppers. Their conjunction is ladder_ratio_brackets, the delta-forced bundle pinning φ, φ^5, and the octave rung φ^8 inside explicit rational intervals (e.g. 1618033/1000000 < φ).
On the real side, ratLt_toReal (via toReal_ratWitness) translates each sigma0 lower bound into a genuine real inequality p/q < toReal x when q>0. That bridge feeds the T5 display path in GoldenIntReal: the sigma0 cost ladder evaluates to classical J-cost on the φ-ladder and its cosh form. Framework landmarks: T5 J-uniqueness, T6 φ as forced ratio, T7 eight-tick octave (φ^8). Verdict target remains sigma0 DELTA_FORCED.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.