Baker-Davenport bound, medium ratio

Open

diophantine_bd_medium_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 medium-ratio regime $2a\\le b\\le 8a$ , one has $b>130000$ . Second case of Lemma 2.1 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015).

Preamble

import Mathlib.Tactic

Formal statement

theorem diophantine_bd_medium_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)
    (hlo : 2 * a ≤ b) (hhi : b ≤ 8 * a) : 130000 < b := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Lemma 2.1, second bullet

View graph