Jones gap dichotomy for Diophantine triples

Proved

diophantine_jones_lemma

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

diophantine-equationsnumber-theory

Let $a<b<c$ with $ab+1=r^2$ , $ac+1\$ square and $bc+1\$ square. Then either $c=a+b+2r$ (the Euler case) or $c>4ab$ . This is Lemma 4 of B. W. Jones, A second variation on a problem of Diophantus and Davenport, Fibonacci Quart. 16 (1978), restated as Lemma 1 in Section 3 of B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2. The non-Euler case is the platform theorem diophantine_triple_non_euler_lower_bound; the Euler case is definitional.

Preamble

import Mathlib.Tactic

Formal statement

theorem diophantine_jones_lemma (a b c r : Nat)
    (ha : 0 < a) (hab : a < b) (hbc : b < c)
    (hr : a * b + 1 = r ^ 2)
    (hs : ∃ s : Nat, a * c + 1 = s ^ 2)
    (ht : ∃ t : Nat, b * c + 1 = t ^ 2) :
    c = a + b + 2 * r ∨ 4 * a * b < c := by sorry

Source

B. W. Jones, A second variation on a problem of Diophantus and Davenport, Fibonacci Quart. 16 (1978), 155-165, Lemma 4; via B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2, Section 3, Lemma 1

View graph