Gap lemma for close Diophantine pairs

Proved

diophantine_gap_lemma

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $ab+1=r^2$ with $0<a<b$ and $b-a>2$ . Then $a+b-2r\ge 1\$ : indeed, if $a+b\le 2r$ then $(a+b)^2\le 4r^2=4ab+4$ , so $(b-a)^2\le 4\$ and $b-a\le 2—a contradiction. This is the integer form of Lemma 3.5 of M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015), applied in the proof of Theorem 1.1 to control$ a^{1/2}(b-a)^{-1}—type error terms.

Preamble

import Mathlib.Tactic

Formal statement

theorem diophantine_gap_lemma (a b r : Nat) (hab : a < b)
    (hr : a * b + 1 = r ^ 2) (hgap : 2 < b - a) :
    2 * r + 1 ≤ a + b := by sorry

Source

M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015), 25-34, Lemma 3.5

View graph