Lower bound for the regular extension

Proved

diophantine_dplus_lower

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 $a,b>0$ , and write $d_+=a+b+c+2abc+2rst$ for the regular extension. Then $4abc+c<d_+\$ : since $(rst)^2=(ab+1)(ac+1)(bc+1)>(abc)^2$ , we get $rst>abc$ , and the claim follows by linear arithmetic. This is the first inequality of Lemma 2 of B. He, A. Togbe and V. Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, Section 3.

Preamble

import Mathlib.Tactic

Formal statement

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

Source

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

View graph