Fujita regularity of {a,b,c,d} (explicit d_+ equation)

Open

diophantine_quintuple_fujita_regular

by xuanji · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $a<b<c<d<e$ be a Diophantine quintuple. There exist nonnegative integers $r,s,t$ such that

r^2=ab+1,\quad s^2=ac+1,\quad t^2=bc+1,

and

d=a+b+c+2abc+2rst.

Thus the first four entries form a regular Diophantine quadruple. This is the Fujita regularity theorem used throughout the source paper; combined with elementary square-product estimates it supplies the lower bound $d>4abc$ . Formalization note: the regular-extension formula uses explicit natural-number square witnesses.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_quintuple_fujita_regular (f : Fin 5 → Nat)
    (hq : Quintuple f) (ho : Ordered f) :
    ∃ r s t : Nat, f 0 * f 1 + 1 = r ^ 2 ∧ f 0 * f 2 + 1 = s ^ 2 ∧
      f 1 * f 2 + 1 = t ^ 2 ∧
      f 3 = f 0 + f 1 + f 2 + 2 * f 0 * f 1 * f 2 + 2 * r * s * t := by sorry

Source

Bo He, Alain Togbe, Volker Ziegler, arXiv:1610.04020v2, Theorem thm:fujita (Y. Fujita, Any Diophantine quintuple contains a regular Diophantine quadruple, J. Number Theory 129 (2009), 1678–1697): if {a,b,c,d,e} is a quintuple with a<b<c<d<e then the quadruple {a,b,c,d} is regular. Used in Lemma lem:acb as `By Fujita's result, the quadruple {a,b,c,d} is regular' and `we have d = d_+ > 4abc'. Source text: https://arxiv.org/abs/1610.04020v2.

View graph