Rickert-type upper bound for the Pell index

Open

diophantine_rickert_bound

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

diophantine-equationsnumber-theory

With the Pell-index data and the threshold hypothesis, the index satisfies the explicit logarithmic upper bound in the formal statement. Lemma 3.3 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015) (via their Theorem 2.2 and Lemma 3.1).

Preamble

import Definitions.Def_diophantine_pell
import Mathlib.Analysis.SpecialFunctions.Log.Basic
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_rickert_bound (a b c a' : Nat)
    (m n : Nat) (z₀ x₀ z₁ y₁ : Int) (s t : Nat)
    (ha : 0 < a) (hab : a < b) (hbc : b < c)
    (ha' : a' = Nat.max (b - a) a)
    (hs : a * c + 1 = s ^ 2) (ht : b * c + 1 = t ^ 2)
    (hm : 3 ≤ m) (hn : 2 ≤ n) (hz0 : (z₀ = 1 ∨ z₀ = -1))
    (hsol1 : (a : Int) * z₀ ^ 2 - (c : Int) * x₀ ^ 2 = (a : Int) - c)
    (hsol2 : (b : Int) * z₁ ^ 2 - (c : Int) * y₁ ^ 2 = (b : Int) - c)
    (hcommon : PellV (s : Int) (c : Int) z₀ x₀ (2 * m)
      = PellW (t : Int) (c : Int) z₁ y₁ (2 * n))
    (hthr : (3706 / 10000 : ℝ) * (a' : ℝ) * (b : ℝ) * ((b : ℝ) - (a : ℝ)) ^ 2
      / (a : ℝ) ≤ (c : ℝ)) :
    (n : ℝ) < 4
      * Real.log (84060000000000 * Real.sqrt (a : ℝ) * Real.sqrt (a' : ℝ)
        * (b : ℝ) ^ 2 * (c : ℝ))
      * Real.log (1643 / 1000 * Real.sqrt (a : ℝ) * Real.sqrt (b : ℝ)
        / ((b : ℝ) - (a : ℝ)) * (c : ℝ))
      / (Real.log (4 * (b : ℝ) * (c : ℝ))
        * Real.log (2699 / 10000 * (a : ℝ) / (a' : ℝ) / (b : ℝ)
          / ((b : ℝ) - (a : ℝ)) ^ 2 * (c : ℝ))) := by
  sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Section 3, Lemma 3.3

View graph