Linear-log endgame for the small-ratio case

Proved

diophantine_case1_endgame

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

diophantine-equationsnumber-theory

For $b>21000$ , $37.3+83.2\\log b\\le 0.6035b\$ . The difference grows (its derivative exceeds $0.6035-83.2/21000>0$ via $\\log x\\le x-1$ ) and is positive at $b=21000$ (using $\\log 21000<10$ ). This closes the numerical endgame of Case 1 ( $b<2a$ ) of Theorem 1.1 of M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015).

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case1_endgame (b : Nat) (hb : 21000 < b) :
    37.3 + 83.2 * Real.log (b : ℝ) ≤ (6035 / 10000) * (b : ℝ) := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), proof of Theorem 1.1, case b < 2a (endgame)

View graph