Local Periodicity of Pell Recurrences

Abstract

Pell-unit and unimodular recurrences are pure-periodic under every prime-power observation.

Theorem 1.1 (Pell recurrences are periodic modulo every prime power).

$$\begin{gathered} \forall D,x,y\in \mathbb{Z},s,t:\mathrm{Fin}\left(2\right)\to \mathbb{Z}, \\ G:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{Z}\right),p,k\in \mathbb{N},\mathrm{Prime}\left(p\right) \\ \Rightarrow \mathrm{let}q=p^k,R=(M\mapsto \mathrm{mod}\left(M,q\right)), \\ r=(v\mapsto (i\mapsto \mathrm{mod}\left(v_i,q\right))),U=Matrix2\left(x,Dy,y,x\right), \\ u=(n\mapsto R{\left(U\right)}^{n}r\left(s\right)),z=(n\mapsto R{\left(G\right)}^{n}r\left(t\right)) \\ ((x^2-D{y}^2=1\vee x^2-D{y}^2=-1)\Rightarrow \exists T\in \mathbb{N},0<T\wedge \forall n\in \mathbb{N},u_{n+T}=u_n)\wedge \\ ((\det \left(G\right)=1\vee \det \left(G\right)=-1)\Rightarrow \exists T\in \mathbb{N},0<T\wedge \forall n\in \mathbb{N},z_{n+T}=z_n). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/PellFamilies/LocalPellPeriodicity.pell_unit_and_unimodular_recurrences_are_locally_periodic (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a prime p and an exponent k. The observer modulus is q = p^k. The displayed reduction maps act entrywise on integral two-by-two matrices and two-coordinate integer states.

For an integral Pell unit x + y sqrt(D), multiplication on its two coordinates is the explicit matrix with rows (x, Dy) and (y, x). Its determinant is x^2 - D y^2, so norm one or minus one makes its reduction invertible. The first implication therefore gives a positive pure period for its observed orbit.

The second implication treats an arbitrary integral unimodular two-coordinate recurrence independently. Reduction preserves the unit determinant, and the reduced matrix belongs to a finite unit group. Its positive finite order is a period from time zero for every reduced seed.

References

• Truth anchor: D5/S3/PrimeForms/PellFamilies/LocalPellPeriodicity.pell_unit_and_unimodular_recurrences_are_locally_periodic
• Dependency: D5/S3/PrimeForms/PellFamilies/CrossingPellFamily
• Dependency: D5/S3/PrimeForms/PellFamilies/SqrtTwentyOnePellTower