FormalConjectures.Wikipedia.WallSunSun

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil

Infinitude of Wall–Sun–Sun primes

Reference: Wikipedia

open Algebra (IsQuadraticExtension)open NumberFieldnamespace QuadraticAlgebravariable {d : ℤ} [Fact <| Squarefree d] [Fact <| d ≠ 1]

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

@[category textbook, AMS 11, simp]
lemma discr_rat_of_modEq_one (hd₄ : d ≡ 1 [ZMOD 4]) : discr (QuadraticAlgebra ℚ d 0) = d := byd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)hd₄:d ≡ 1 [ZMOD 4]⊢ discr (QuadraticAlgebra ℚ (↑d) 0) = d
  sorryAll goals completed! 🐙

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

@[category textbook, AMS 11, simp]
lemma discr_rat_of_not_modEq_one (hd₄ : ¬ d ≡ 1 [ZMOD 4]) :
    discr (QuadraticAlgebra ℚ d 0) = 4 * d := byd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)hd₄:¬d ≡ 1 [ZMOD 4]⊢ discr (QuadraticAlgebra ℚ (↑d) 0) = 4 * d
  sorryAll goals completed! 🐙

end QuadraticAlgebranamespace Algebravariable {K L : Type*} [Field K] [Field L] [Algebra K L]variable (K L) in

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

@[category textbook, AMS 11]
lemma exists_quadraticAlgebra_of_isQuadraticExtension [IsQuadraticExtension K L] :
    ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b) := byK:Type u_1L:Type u_2inst✝³:Field Kinst✝²:Field Linst✝¹:Algebra K Linst✝:IsQuadraticExtension K L⊢ ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b)
  sorryAll goals completed! 🐙

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.

@[category textbook, AMS 11]
lemma isQuadraticExtension_iff_exists_quadraticAlgebra :
    IsQuadraticExtension K L ↔ ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b) where
  mp _ := exists_quadraticAlgebra_of_isQuadraticExtension ..
  mpr := byK:Type u_1L:Type u_2inst✝²:Field Kinst✝¹:Field Linst✝:Algebra K L⊢ (∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b)) → IsQuadraticExtension K L rintro ⟨a, b, ⟨e⟩⟩K:Type u_1L:Type u_2inst✝²:Field Kinst✝¹:Field Linst✝:Algebra K La:Kb:Ke:L ≃ₐ[K] QuadraticAlgebra K a b⊢ IsQuadraticExtension K L; sorryAll goals completed! 🐙

end Algebranamespace NumberFieldvariable {K : Type*} [Field K] [NumberField K]variable (K) in

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

@[category textbook, AMS 11]
lemma exists_quadraticAlgebra_of_isQuadraticExtension [IsQuadraticExtension ℚ K] :
    ∃ d ≠ (1 : ℤ), Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ d 0) := byK:Type u_1inst✝²:Field Kinst✝¹:NumberField Kinst✝:IsQuadraticExtension ℚ K⊢ ∃ d, d ≠ 1 ∧ Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ (↑d) 0)
  sorryAll goals completed! 🐙

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.

@[category textbook, AMS 11]
lemma isQuadraticExtension_iff_exists_quadraticAlgebra :
    IsQuadraticExtension ℚ K ↔
      ∃ d ≠ (1 : ℤ), Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ d 0) where
  mp _ := exists_quadraticAlgebra_of_isQuadraticExtension _
  mpr := byK:Type u_1inst✝¹:Field Kinst✝:NumberField K⊢ (∃ d, d ≠ 1 ∧ Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ (↑d) 0)) → IsQuadraticExtension ℚ K rintro ⟨d, hd₁, hd, ⟨e⟩⟩K:Type u_1inst✝¹:Field Kinst✝:NumberField Kd:ℤhd₁:d ≠ 1hd:Squarefree de:K ≃+* QuadraticAlgebra ℚ (↑d) 0⊢ IsQuadraticExtension ℚ K; sorryAll goals completed! 🐙

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.


@[category textbook, AMS 11]
lemma isFundamentalDiscr_iff_exists_discr_quadraticAlgebra {D : ℤ} :
    IsFundamentalDiscr D ↔ ∃ (d : ℤ) (_ : Fact <| d ≠ 1) (_ : Fact <| Squarefree d),
      discr (QuadraticAlgebra ℚ d 0) = D where
  mp := byD:ℤ⊢ IsFundamentalDiscr D → ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D
    rintro (⟨⟨d, rfl⟩, hD₄, hD⟩ | ⟨hD₁, hD₄, hD⟩)inld:ℤhD₄:¬4 * d / 4 ≡ 1 [ZMOD 4]hD:Squarefree (4 * d / 4)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * dinrD:ℤhD₁:D ≠ 1hD₄:D ≡ 1 [ZMOD 4]hD:Squarefree D⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D
    ·inld:ℤhD₄:¬4 * d / 4 ≡ 1 [ZMOD 4]hD:Squarefree (4 * d / 4)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, mul_div_cancel_left₀] at hD hD₄inld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d
      have : Fact <| d ≠ 1 := ⟨byd:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]⊢ d ≠ 1inld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]this:Fact (d ≠ 1)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d rintro rflhD:Squarefree 1hD₄:¬1 ≡ 1 [ZMOD 4]⊢ Falseinld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]this:Fact (d ≠ 1)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d; simp at hD₄All goals completed! 🐙inld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]this:Fact (d ≠ 1)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d⟩inld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]this:Fact (d ≠ 1)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d
      have : Fact <| Squarefree d := ⟨hD⟩inld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]this✝:Fact (d ≠ 1)this:Fact (Squarefree d)⊢ ∃ d_1, ∃ (x : Fact (d_1 ≠ 1)) (x_1 : Fact (Squarefree d_1)), discr (QuadraticAlgebra ℚ (↑d_1) 0) = 4 * d
      exact ⟨d, inferInstance, inferInstance, QuadraticAlgebra.discr_rat_of_not_modEq_one hD₄⟩All goals completed! 🐙
    ·inrD:ℤhD₁:D ≠ 1hD₄:D ≡ 1 [ZMOD 4]hD:Squarefree D⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D have : Fact <| D ≠ 1 := ⟨hD₁⟩inrD:ℤhD₁:D ≠ 1hD₄:D ≡ 1 [ZMOD 4]hD:Squarefree Dthis:Fact (D ≠ 1)⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D
      have : Fact <| Squarefree D := ⟨hD⟩inrD:ℤhD₁:D ≠ 1hD₄:D ≡ 1 [ZMOD 4]hD:Squarefree Dthis✝:Fact (D ≠ 1)this:Fact (Squarefree D)⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D
      exact ⟨D, inferInstance, inferInstance, QuadraticAlgebra.discr_rat_of_modEq_one hD₄⟩All goals completed! 🐙
  mpr := byD:ℤ⊢ (∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D) → IsFundamentalDiscr D
    rintro ⟨d, _, _, rfl⟩d:ℤw✝¹:Fact (d ≠ 1)w✝:Fact (Squarefree d)⊢ IsFundamentalDiscr (discr (QuadraticAlgebra ℚ (↑d) 0)); by_cases hd₄ : d ≡ 1 [ZMOD 4]posd:ℤw✝¹:Fact (d ≠ 1)w✝:Fact (Squarefree d)hd₄:d ≡ 1 [ZMOD 4]⊢ IsFundamentalDiscr (discr (QuadraticAlgebra ℚ (↑d) 0))negd:ℤw✝¹:Fact (d ≠ 1)w✝:Fact (Squarefree d)hd₄:¬d ≡ 1 [ZMOD 4]⊢ IsFundamentalDiscr (discr (QuadraticAlgebra ℚ (↑d) 0)) <;>posd:ℤw✝¹:Fact (d ≠ 1)w✝:Fact (Squarefree d)hd₄:d ≡ 1 [ZMOD 4]⊢ IsFundamentalDiscr (discr (QuadraticAlgebra ℚ (↑d) 0))negd:ℤw✝¹:Fact (d ≠ 1)w✝:Fact (Squarefree d)hd₄:¬d ≡ 1 [ZMOD 4]⊢ IsFundamentalDiscr (discr (QuadraticAlgebra ℚ (↑d) 0)) simp [*, IsFundamentalDiscr, Fact.out]All goals completed! 🐙

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


@[category textbook, AMS 11]
lemma isFundamentalDiscr_iff_exists_discr_numberField {D : ℤ} :
    IsFundamentalDiscr D ↔
      ∃ (K : Type) (_ : Field K) (_ : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D := byD:ℤ⊢ IsFundamentalDiscr D ↔ ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D
  rw [isFundamentalDiscr_iff_exists_discr_quadraticAlgebraD:ℤ⊢ (∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D) ↔
  ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = DD:ℤ⊢ (∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D) ↔
  ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D]D:ℤ⊢ (∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D) ↔
  ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D
  constructormpD:ℤ⊢ (∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D) →
  ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = DmprD:ℤ⊢ (∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D) →
  ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D
  ·mpD:ℤ⊢ (∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D) →
  ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D rintro ⟨d, _, _, rfl⟩mpd:ℤw✝¹:Fact (d ≠ 1)w✝:Fact (Squarefree d)⊢ ∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = discr (QuadraticAlgebra ℚ (↑d) 0)
    exact ⟨_, inferInstance, inferInstance, inferInstance, rfl⟩All goals completed! 🐙
  ·mprD:ℤ⊢ (∃ K x, ∃ (x_1 : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D) →
  ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = D rintro ⟨K, _, _, _, rfl⟩mprK:Typew✝¹:Field Kw✝:NumberField Kleft✝:IsQuadraticExtension ℚ K⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = discr K
    obtain ⟨d, hd₁, hd, ⟨e⟩⟩ := exists_quadraticAlgebra_of_isQuadraticExtension KmprK:Typew✝¹:Field Kw✝:NumberField Kleft✝:IsQuadraticExtension ℚ Kd:ℤhd₁:d ≠ 1hd:Squarefree de:K ≃+* QuadraticAlgebra ℚ (↑d) 0⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = discr K
    have : Fact <| d ≠ 1 := ⟨hd₁⟩mprK:Typew✝¹:Field Kw✝:NumberField Kleft✝:IsQuadraticExtension ℚ Kd:ℤhd₁:d ≠ 1hd:Squarefree de:K ≃+* QuadraticAlgebra ℚ (↑d) 0this:Fact (d ≠ 1)⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = discr K
    have : Fact <| Squarefree d := ⟨hd⟩mprK:Typew✝¹:Field Kw✝:NumberField Kleft✝:IsQuadraticExtension ℚ Kd:ℤhd₁:d ≠ 1hd:Squarefree de:K ≃+* QuadraticAlgebra ℚ (↑d) 0this✝:Fact (d ≠ 1)this:Fact (Squarefree d)⊢ ∃ d, ∃ (x : Fact (d ≠ 1)) (x_1 : Fact (Squarefree d)), discr (QuadraticAlgebra ℚ (↑d) 0) = discr K
    exact ⟨d, inferInstance, inferInstance, discr_eq_discr_of_ringEquiv _ e.symm⟩All goals completed! 🐙

end NumberFieldnamespace WallSunSun

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.

@[category research open, AMS 11]
theorem exists_isWallSunSunPrime : ∃ p, IsWallSunSunPrime p := by⊢ ∃ p, IsWallSunSunPrime p
  sorryAll goals completed! 🐙

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.

@[category research open, AMS 11]
theorem infinite_isWallSunSunPrime : {p : ℕ | IsWallSunSunPrime p}.Infinite := by⊢ {p | IsWallSunSunPrime p}.Infinite
  sorryAll goals completed! 🐙

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

@[category research open, AMS 11]
theorem infinite_isWallSunSunPrime_of_disc_eq {D : ℤ} (hD : IsFundamentalDiscr D)
    (hD₁ : D ≠ 1) :
    {p : ℕ | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite := byD:ℤhD:IsFundamentalDiscr DhD₁:D ≠ 1⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
  sorryAll goals completed! 🐙

end WallSunSun