Envelope for the Rickert bound at minimal d, medium ratio

Proved

diophantine_case2_d0bound

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

diophantine-equationsnumber-theory

With $d_0=3.317b^3$ ( $b>130000$ ), the Case-2 Rickert fraction at $d_0$ is at most $2568+3705\\log b\$ . From the proof of Theorem 1.1 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), case $2a\le b\le 3a\878.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case2_d0bound (b : Nat) (hb : 130000 < b) :
    4 * Real.log ((42030000000000 * (b:ℝ)^3) * ((3317/1000) * (b:ℝ)^3))
    * Real.log ((23236/10000) * ((3317/1000) * (b:ℝ)^3))
    / (Real.log ((4 * (b:ℝ)) * ((3317/1000) * (b:ℝ)^3))
      * Real.log (((3036/10000) / (b:ℝ)^3) * ((3317/1000) * (b:ℝ)^3)))
    ≤ 2568 + 3705 * Real.log (b:ℝ) := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), proof of Theorem 1.1, case 2a <= b <= 3a (d-elimination bound)

View graph