Infinitude of Wall–Sun–Sun primes

Reference: Wikipedia

@[simp]

theorem QuadraticAlgebra.discr_rat_of_modEq_one {d : ℤ} [Fact (Squarefree d)] [Fact (d ≠ 1)] (hd₄ : d ≡ 1 [ZMOD 4]) : NumberField.discr (QuadraticAlgebra ℚ (↑d) 0) = d

The discriminant of ℚ[√d] for d ≥ 2 squarefree congruent to 1 mod 4 is d.

@[simp]

theorem QuadraticAlgebra.discr_rat_of_not_modEq_one {d : ℤ} [Fact (Squarefree d)] [Fact (d ≠ 1)] (hd₄ : ¬d ≡ 1 [ZMOD 4]) : NumberField.discr (QuadraticAlgebra ℚ (↑d) 0) = 4 * d

The discriminant of ℚ[√d] for d ≥ 2 squarefree not congruent to 1 mod 4 is 4 * d.

theorem Algebra.exists_quadraticAlgebra_of_isQuadraticExtension (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsQuadraticExtension K L] : ∃ (a : K) (b : K), Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b)

A quadratic algebra L over a field K is isomorphic to the explicit quadratic algebra QuadraticAlgebra K a b for some a b : K.

theorem Algebra.isQuadraticExtension_iff_exists_quadraticAlgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : IsQuadraticExtension K L ↔ ∃ (a : K) (b : K), Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b)

An algebra L is quadratic over a field K iff it is isomorphic to the explicit quadratic algebra QuadraticAlgebra K a b for some a b : K.

theorem NumberField.exists_quadraticAlgebra_of_isQuadraticExtension (K : Type u_1) [Field K] [NumberField K] [Algebra.IsQuadraticExtension ℚ K] : ∃ (d : ℤ), d ≠ 1 ∧ Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ (↑d) 0)

A quadratic number field K is isomorphic to the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

theorem NumberField.isQuadraticExtension_iff_exists_quadraticAlgebra {K : Type u_1} [Field K] [NumberField K] : Algebra.IsQuadraticExtension ℚ K ↔ ∃ (d : ℤ), d ≠ 1 ∧ Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ (↑d) 0)

A number field K is quadratic iff it is isomorphic to the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

def NumberField.IsFundamentalDiscr (D : ℤ) : Prop

Fundamental discriminants are those integers D that appear as discriminants of quadratic fields.

D is a fundamental discriminant if it is either of the form 4m for m congruent to 2 or 3 mod 4 squarefree, or if it congruent to 1 mod 4 and squarefree.

Equations

• NumberField.IsFundamentalDiscr D = (4 ∣ D ∧ ¬D / 4 ≡ 1 [ZMOD 4] ∧ Squarefree (D / 4) ∨ D ≠ 1 ∧ D ≡ 1 [ZMOD 4] ∧ Squarefree D)

theorem NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra {D : ℤ} : IsFundamentalDiscr D ↔ ∃ (d : ℤ) (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D

An integer D is a fundamental discriminant iff it is the discriminant of the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

theorem NumberField.isFundamentalDiscr_iff_exists_discr_numberField {D : ℤ} : IsFundamentalDiscr D ↔ ∃ (K : Type) (x : Field K) (x_1 : NumberField K), Algebra.IsQuadraticExtension ℚ K ∧ discr K = D

An integer D is a fundamental discriminant iff it is the discriminant of some number field.

theorem WallSunSun.exists_isWallSunSunPrime : ∃ (p : ℕ), IsWallSunSunPrime p

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. It is conjectured that there is at least one Wall–Sun–Sun prime.

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

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. It is conjectured that there are infinitely many Wall-Sun-Sun primes.

theorem WallSunSun.infinite_isWallSunSunPrime_of_disc_eq {D : ℤ} (hD : NumberField.IsFundamentalDiscr D) (hD₁ : D ≠ 1) : {p : ℕ | ∃ (a : ℤ) (b : ℤ), a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite

A Lucas–Wieferich prime associated with $(a,b)$ is an odd prime $p$, not dividing $a^2 - 4b$, such that $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)$. The discriminant of this number is the quantity $a^2 - 4b$. It is conjectured that there are infinitely many Lucas–Wieferich primes of any given non-one fundamental discriminant.

TODO: Source this conjecture