References:

• Wikipedia, Lucas_sequence
• Wikipedia, Wall–Sun–Sun prime
• Wikipedia, Wieferich prime

def LucasSequence.U (P Q : ℤ) : ℕ → ℤ

The Lucas sequence of the first kind $U_0(P, Q) = 0$, $U_1(P, Q)=1$, $U_{n+2}(P, Q)=PU_{n+1}(P, Q)-QU_n(P, Q)$

Equations

• LucasSequence.U P Q 0 = 0
• LucasSequence.U P Q 1 = 1
• LucasSequence.U P Q n.succ.succ = P * LucasSequence.U P Q (n + 1) - Q * LucasSequence.U P Q n

def LucasSequence.V (P Q : ℤ) : ℕ → ℤ

The Lucas sequence of the second kind $V_0(P, Q) = 0$, $V_1(P, Q)=P$, $V_{n+2}(P, Q)=PV_{n+1}(P, Q)-QV_n(P, Q)$

Equations

• LucasSequence.V P Q 0 = 2
• LucasSequence.V P Q 1 = P
• LucasSequence.V P Q n.succ.succ = P * LucasSequence.V P Q (n + 1) - Q * LucasSequence.V P Q n

def lucasNumber : ℕ → ℤ

The Lucas numbers $L_0 = 2$, $L_1=1$, $L_{n+2} = L_{n+1}+L_n$

Equations

• lucasNumber = LucasSequence.V 1 (-1)

structure IsWallSunSunPrime (p : ℕ) : Prop

Wall–Sun–Sun prime A prime $p$ is a Wall–Sun–Sun prime if and only if $L_p \equiv 1 \pmod{p^2}$, where $L_p$ is the $p$-th Lucas number.

• prime : Nat.Prime p
• lucasNumber_modeq : lucasNumber p ≡ 1 [ZMOD ↑p ^ 2]

structure IsLucasWieferichPrime (a b p : ℕ) : Prop

Lucas–Wieferich prime A Lucas–Wieferich prime associated with $(a,b)$ is a prime $p$ such $U_{p-\varepsilon}(a,b) \equiv 0 \pmod{p^2}$ where $U(a,b)$ is the Lucas sequence of the first kind and $\varepsilon$ is the Legendre symbol $\left({\tfrac {a^{2}-4b}{p}}\right)$

• prime : Nat.Prime p
• modeq : LucasSequence.U (↑a) (↑b) (↑p - jacobiSym (↑p) (a ^ 2 - 4 * b)).toNat ≡ 0 [ZMOD ↑p ^ 2]