Infinitude of Wall–Sun–Sun primes

The question

exists_isWallSunSunPrime. A prime $p$ is a Wall–Sun–Sun prime if and only if $L_{p} \equiv 1 (mod p^{2})$ , where $L_{p}$ is the $p$ -th Lucas number. It is conjectured that there is at least one Wall–Sun–Sun prime.

infinite_isWallSunSunPrime. A prime $p$ is a Wall–Sun–Sun prime if and only if $L_{p} \equiv 1 (mod p^{2})$ , where $L_{p}$ is the $p$ -th Lucas number. It is conjectured that there are infinitely many Wall-Sun-Sun primes.

infinite_isWallSunSunPrime_of_disc_eq. Let $K$ be a real quadratic field of discriminant $D$ and let $ε$ be a fundamental unit of $K$ . Following [EJ10, Remark 2.2.8], an odd prime $p ∤ D$ is a Wall–Sun–Sun prime for $K$ if, in $O_{K}$ , $ε^{p - 1} \equiv 1 (mod p^{2})$ when $(\frac{D}{p}) = 1$ , and $ε^{2 p + 2} \equiv 1 (mod p^{2})$ when $(\frac{D}{p}) = - 1$ . Both exponents are even, so the condition does not depend on the choice of $ε$ , and it is equivalent to asking the same congruence for every unit of $K$ . For $K = Q (5)$ and $ε = \frac{1 + 5}{2}$ these are the classical Wall–Sun–Sun primes other than $2$ and $5$ [EJ10, Proposition 2.2.6].

It is conjectured that for every fundamental discriminant $D \neq = 1$ there are infinitely many Wall–Sun–Sun primes with discriminant $D$ (Wikipedia; [EJ10, §4.1] gives the heuristic for $Q (5)$ ). It is stated here for $D > 0$ only. Wikipedia's sentence also covers $D < 0$ , but [EJ10] gives the definition above only for real quadratic fields, and its literal extension to imaginary quadratic fields is degenerate: there every unit is a root of unity of order dividing $4$ or $6$ , and that order divides the relevant exponent $p - 1$ or $2 p + 2$ for every odd prime $p ∤ D$ .

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.WallSunSun (3 statements).

theorem exists_isWallSunSunPrime : ∃ p, IsWallSunSunPrime p

theorem infinite_isWallSunSunPrime : {p : ℕ | IsWallSunSunPrime p}.Infinite

theorem infinite_isWallSunSunPrime_of_disc_eq {K : Type*} [Field K] [NumberField K]
    [IsQuadraticExtension ℚ K] [IsTotallyReal K] {D : ℤ} (hD : discr K = D) :
    {p : ℕ | p.Prime ∧ Odd p ∧ ¬ (p : ℤ) ∣ D ∧ ∀ ε : (𝓞 K)ˣ,
      (p : 𝓞 K) ^ 2 ∣ (ε : 𝓞 K) ^ (if J(D | p) = 1 then p - 1 else 2 * p + 2) - 1}.Infinite

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Wikipedia
[EJ10] A.-S. Elsenhans and J. Jahnel, *The Fibonacci sequence modulo $p^{2}$ – An investigation by computer for $p < 1 0^{14}$ *, arXiv:1006.0824

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.

Current state

The problem