Upper bound for the regular extension

Proved

diophantine_dplus_upper

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

diophantine-equationsnumber-theory

Let $ab+1=r^2$ , $ac+1=s^2$ , $bc+1=t^2$ with $0<a<b<c$ , and write $d_+=a+b+c+2abc+2rst$ . Then $d_+<4abc+4c$ . The proof follows Section 3 of B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2: squaring reduces the claim to $4(ab+1)(ac+1)(bc+1)\le(2abc+3c-a-b)^2$ , which after expansion follows from $c\ge a+b+2r$ (Jones dichotomy) by term-by-term comparison; strictness comes from $abc>1$ .

Preamble

import Mathlib.Tactic

Formal statement

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

Source

B. He, A. Togbe and V. Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, Section 3, Lemma 2 (upper bound)

View graph