Large Pell indices force irregularity

Open

diophantine_pell_irregular

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

diophantine-equationsnumber-theory

Under the Pell-index data above, the fourth element exceeds the regular extension $d_+=a+b+c+2abc+2rst$ . Hence a quintuple-derived quadruple with large indices is irregular, licensing the Baker-Davenport bounds. From the analysis of A. Filipin and Y. Fujita as used in M. Cipu and Y. Fujita, Glas. Mat. 50 (2015).

Preamble

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

Formal statement

theorem diophantine_pell_irregular (a b c d r s t : Nat)
    (ha : 0 < a) (hab : a < b) (hbc : b < c) (hcd : c < d)
    (hr : a * b + 1 = r ^ 2) (hs : a * c + 1 = s ^ 2)
    (ht : b * c + 1 = t ^ 2)
    (m n : Nat) (z₀ x₀ z₁ y₁ : Int)
    (hm : 3 ≤ m) (hn : 2 ≤ n) (hmn : m ≤ 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)) :
    a + b + c + 2 * a * b * c + 2 * r * s * t < d := by
  sorry

Source

A. Filipin and Y. Fujita, Publ. Math. Debrecen 82 (2013); via M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Sections 3 and 6

View graph