Numerical contradiction in the small-ratio case

Proved

diophantine_case1_combine

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

diophantine-equationsnumber-theory

In the notation of the Cipu-Fujita proof that no Diophantine quintuple has $b<2a$ : let $b>21000$ , $d>5.8284b^3$ , and let $n$ satisfy the gap lower bound $n>0.6035b$ and the Rickert upper bound $n<4\log(8.406\\cdot 10^{13}b^3d)\\log(0.8215\\sqrt b d)/(\\log(4bd)\\log(1.0796d/b^3))\$ . These four conditions are jointly impossible: the upper bound decreases in $d$ , hence is at most its value at $d=5.8284b^3$ , which is in turn below $0.6035b$ for $b>21000$ . This is the final numerical contradiction of Case 1 ( $b<2a$ ) of Theorem 1.1 of M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015). Its analytic inputs (the two bounds on $n$ ) are separate problems.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case1_combine (b d n : Nat)
    (hb : 21000 < b)
    (hd : (58284 / 10000 : ℝ) * (b : ℝ) ^ 3 < (d : ℝ))
    (hlower : (6035 / 10000 : ℝ) * (b : ℝ) < (n : ℝ))
    (hupper : (n : ℝ) < 4 * Real.log (84060000000000 * (b : ℝ) ^ 3 * (d : ℝ))
      * Real.log ((8215 / 10000) * Real.sqrt (b : ℝ) * (d : ℝ))
      / (Real.log (4 * (b : ℝ) * (d : ℝ))
        * Real.log ((10796 / 10000) * (d : ℝ) / (b : ℝ) ^ 3))) :
    False := by sorry

Source

M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015), 25-34, proof of Theorem 1.1, case b < 2a (final numerical contradiction)

View graph