Baker-Davenport bound, small ratio

Open

diophantine_bd_small_ratio

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

diophantine-equationsnumber-theory

Let $a<b<c<d$ be positive integers with all six pairwise products plus one square (a Diophantine quadruple), and let $r,s,t$ witness the triple squares. If the quadruple is irregular, i.e. $d>d_+=a+b+c+2abc+2rst$ , then: in the small-ratio regime $b<2a$ , one has $b>21000$ . This is the first case of Lemma 2.1 of M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015) (computations from A. Filipin, Y. Fujita and A. Togbe, Glas. Mat. 49 (2014), via the Baker-Davenport reduction method). It supplies the $b>2000$ hypothesis needed for Rickert-type estimates, and contradicts the $b<200$ (resp. $b<97000\$ ) conclusions of the Case 1 (resp. Case 2) analyses.

Preamble

import Mathlib.Tactic

Formal statement

theorem diophantine_bd_small_ratio (a b c d r s t : Nat)
    (ha : 0 < a) (hab : a < b) (hbc : b < c) (hcd : c < d)
    (hr : a * b + 1 = r ^ 2) (hs : a * c + 1 = s ^ 2) (ht : b * c + 1 = t ^ 2)
    (had : ∃ x : Nat, a * d + 1 = x ^ 2) (hbd : ∃ y : Nat, b * d + 1 = y ^ 2)
    (hcd2 : ∃ z : Nat, c * d + 1 = z ^ 2)
    (hirr : a + b + c + 2 * a * b * c + 2 * r * s * t < d)
    (hlt : b < 2 * a) : 21000 < b := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Lemma 2.1, first bullet; computations from [13, Theorem 1.2]

View graph