The Crossing Pell Family

Abstract

The crossing recurrence is an explicit family on the Pell conic of discriminant 48.

Theorem 1.1 (The crossing recurrence preserves its Pell invariant).

$$\forall n\in \mathbb{N},(2A_n+1{)}^2-48j_n^2=1$$

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

Source. Repository-derived.

Commentary.

Let A 0 = 3 and j 0 = 1. Recursively set A (n+1) = 7 A n + 24 j n + 3 and j (n+1) = 2 A n + 7 j n + 1. The resulting pairs begin (3,1), (48,14), and (675,195). Every pair satisfies (2 A n + 1)^2 - 48 (j n)^2 = 1.

Pinned Mathlib already defines the Pell sequence generated by seven and proves its universal Pell equation as Pell.pell_eqz. The Lean proof identifies these crossing coordinates with that sequence and applies the library theorem directly; it does not reprove the Pell invariant.

This closes only the displayed Pell-family clause of appendix E.56. It does not claim the constant word, trace formula, norm realization, crossing-form identities, no-smaller-leg lemma, or spectral accumulation limit from the rest of the source atom.

References

• Truth anchor: D5/S3/PrimeForms/PellFamilies/CrossingPellFamily.crossing_pell_invariant