Numerical contradiction in the medium-ratio case

Proved

diophantine_case2_combine

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

diophantine-equationsnumber-theory

Case 2 ( $2a\\le b\\le 3a$ ) of Theorem 1.1 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015): the gap lower bound, Rickert upper bound and $b>130000$ are jointly impossible. Analytic inputs are separate problems.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case2_combine (b d n : Nat)
    (hb : 130000 < b)
    (hd : (3317 / 1000 : ℝ) * (b : ℝ) ^ 3 < (d : ℝ))
    (hlower : (4553 / 10000 : ℝ) * (b : ℝ) < (n : ℝ))
    (hupper : (n : ℝ) < 4 * Real.log (42030000000000 * (b : ℝ) ^ 3 * (d : ℝ))
      * Real.log ((23236 / 10000) * (d : ℝ))
      / (Real.log (4 * (b : ℝ) * (d : ℝ))
        * Real.log ((3036 / 10000) * (d : ℝ) / (b : ℝ) ^ 3))) :
    False := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), proof of Theorem 1.1, case 2a <= b <= 3a (final numerical contradiction)

View graph