Pell recurrence sequences for quintuple analysis

Definition

diophantine_pell

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

diophantine-equationsnumber-theory

The second-order linear recurrences parametrizing solutions of the generalized Pell systems $az^2-cx^2=a-c$ and $bz^2-cy^2=b-c$ arising from a Diophantine quadruple: $v_0=z_0$ , $v_1=sz_0+cx_0$ , $v_{m+2}=2sv_{m+1}-v_m$ and similarly $w$ with $t$ . Over integers. These are (3.3)--(3.4) of M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015), following A. Filipin and Y. Fujita, Publ. Math. Debrecen 82 (2013). Common values $v_{2m}=w_{2n}$ index the large solutions.

Definition code

namespace DiophantineDescent

/-- Forward recurrence for solutions of `a*z^2 - c*x^2 = a - c`:
`v 0 = z0`, `v 1 = s*z0 + c*x0`, `v (m+2) = 2*s*v (m+1) - v m`.
Over integers; see (3.3) of Cipu-Fujita. -/
def PellV (s c z0 x0 : Int) : Nat → Int
  | 0 => z0
  | 1 => s * z0 + c * x0
  | (n + 2) => 2 * s * PellV s c z0 x0 (n + 1) - PellV s c z0 x0 n

/-- Forward recurrence for solutions of `b*z^2 - c*y^2 = b - c`:
`w 0 = z1`, `w 1 = t*z1 + c*y1`, `w (n+2) = 2*t*w (n+1) - w n`.
See (3.4) of Cipu-Fujita. -/
def PellW (t c z1 y1 : Int) : Nat → Int
  | 0 => z1
  | 1 => t * z1 + c * y1
  | (n + 2) => 2 * t * PellW t c z1 y1 (n + 1) - PellW t c z1 y1 n

end DiophantineDescent

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), Section 3, equations (3.3)-(3.4); via A. Filipin and Y. Fujita, Publ. Math. Debrecen 82 (2013)

View graph