Crude envelope for the Rickert bound at minimal d

Proved

diophantine_case1_d0bound

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

diophantine-equationsnumber-theory

With $d_0=5.8284b^3$ ( $b>21000$ ), the Rickert-type fraction $F(d_0)=4\\log(C_1d_0)\\log(C_2d_0)/(\\log(C_3d_0)\\log(C_4d_0))$ is at most $37.3+83.2\\log b\$ . Each logarithm is bounded by smooth-factor estimates using only $\\log 2,\\log 3,\\log 5\$ rigged from Mathlib sharp bounds, and the ratio is controlled by a max-of-ratios envelope. From the proof of Theorem 1.1 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), case $b<2a\$ : this bounds the decreasing upper bound at the smallest admissible $d\878.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case1_d0bound (b : Nat) (hb : 21000 < b) :
    4 * Real.log ((84060000000000 * (b:ℝ)^3) * ((58284/10000) * (b:ℝ)^3))
    * Real.log (((8215/10000) * Real.sqrt (b:ℝ)) * ((58284/10000) * (b:ℝ)^3))
    / (Real.log ((4 * (b:ℝ)) * ((58284/10000) * (b:ℝ)^3))
      * Real.log (((10796/10000) / (b:ℝ)^3) * ((58284/10000) * (b:ℝ)^3)))
    ≤ 37.3 + 83.2 * Real.log (b:ℝ) := by sorry

Source

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

View graph