Pell-index setup for large quadruple solutions

Open

diophantine_pell_setup

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

diophantine-equationsnumber-theory

Let $a<b<c<d$ with all six pairwise products plus one square. Then there are indices $m\ge 3$ , $n\ge 2$ and initial data with $|z_0|=1$ solving the two Pell equations whose recurrences share the value $v_{2m}=w_{2n}$ , with $m\le 2n$ . Quoted from A. Filipin and Y. Fujita (see the part just before Theorem 2.1) in M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Section 3.

Preamble

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

Formal statement

theorem diophantine_pell_setup (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)
    (had : ∃ x : Nat, a * d + 1 = x ^ 2)
    (hbd : ∃ y : Nat, b * d + 1 = y ^ 2)
    (hcd2 : ∃ z : Nat, c * d + 1 = z ^ 2) :
    ∃ m n : Nat, ∃ z₀ x₀ z₁ y₁ : Int,
      3 ≤ m ∧ 2 ≤ n ∧ m ≤ 2 * n ∧ (z₀ = 1 ∨ z₀ = -1) ∧
      (a : Int) * z₀ ^ 2 - (c : Int) * x₀ ^ 2 = (a : Int) - c ∧
      (b : Int) * z₁ ^ 2 - (c : Int) * y₁ ^ 2 = (b : Int) - c ∧
      PellV (s : Int) (c : Int) z₀ x₀ (2 * m)
        = PellW (t : Int) (c : Int) z₁ y₁ (2 * n) := by
  sorry

Source

A. Filipin and Y. Fujita, Publ. Math. Debrecen 82 (2013), before Theorem 2.1; via M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Section 3

View graph