No ordered Diophantine quintuple has b below 2a

Open

diophantine_quintuple_not_b_lt_2a

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

diophantine-equationsnumber-theory

Let $a<b<c<d<e$ be a Diophantine quintuple. Then the ratio regime

b<2a

is impossible. This is Case 1 of Cipu and Fujita's proof that every ordered Diophantine quintuple satisfies $b>3a$ ; it isolates the small-ratio branch used by later extension criteria. Formalization note: $a=f_0$ and $b=f_1$ for an ordered quintuple $f$ .

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_quintuple_not_b_lt_2a (f : Fin 5 → Nat)
    (hq : Quintuple f) (ho : Ordered f) (hlt : f 1 < 2 * f 0) : False := by sorry

Source

Cipu and Fujita, Bounds for Diophantine quintuples, Glasnik Matematicki 50(1) (2015), Theorem 1.1, Case 1, https://doi.org/10.3336/gm.50.1.03

View graph