No quintuple starts with a two-gap

Open

diophantine_no_consecutive_gap_two

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

diophantine-equationsnumber-theory

Let $a<b<c<d<e$ be a Diophantine quintuple. Then $b-a\\ge 3\$ . Pairs at distance 1 are impossible elementarily, and Y. Fujita (The extensibility of Diophantine pairs ${k-1,k+1}$, J. Number Theory 128 (2008)) showed that a pair at distance 2 never extends to a quintuple. Used in M. Cipu and Y. Fujita, Glas. Mat. 50 (2015) to license the gap lemma in the proof of Theorem 1.1.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_no_consecutive_gap_two (f : Fin 5 → Nat)
    (hq : Quintuple f) (ho : Ordered f) : 3 ≤ f 1 - f 0 := by sorry

Source

Y. Fujita, J. Number Theory 128 (2008), 322-353; via M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), proof of Theorem 1.1 ([14])

View graph