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 NumberField


namespace QuadraticAlgebra

variable {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 declaration uses 'sorry'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 declaration uses 'sorry'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 QuadraticAlgebra


namespace Algebra

variable {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 declaration uses 'sorry'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 declaration uses 'sorry'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 Algebra


namespace NumberField

variable {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 declaration uses 'sorry'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 declaration uses 'sorry'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! 🐙

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.

def IsFundamentalDiscr (D : ℤ) : Prop :=
  4 ∣ D ∧ ¬ D / 4 ≡ 1 [ZMOD 4] ∧ Squarefree (D / 4) ∨ D ≠ 1 ∧ D ≡ 1 [ZMOD 4] ∧ Squarefree 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.

@[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 ≠ 1 rintro rflhD:Squarefree 1hD₄:¬1 ≡ 1 [ZMOD 4]⊢ False; simp at hD₄All goals completed! 🐙⟩
      have : Fact <| Squarefree d := ⟨hD⟩inld:ℤhD:Squarefree dhD₄:¬d ≡ 1 [ZMOD 4]this✝:Fact (d ≠ 1) := 
  {
    out := fun a =>
      Eq.ndrec (motive := fun d => Squarefree d → ¬d ≡ 1 [ZMOD 4] → False)
        (fun hD hD₄ => False.elim (Eq.mp (Eq.trans (congrArg Not (Int.ModEq.refl._simp_1 1)) not_true_eq_false) hD₄))
        (Eq.symm a) hD hD₄ }this:Fact (Squarefree d) := { out := hD }⊢ ∃ 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) := { out := hD₁ }⊢ ∃ 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) := { out := hD₁ }this:Fact (Squarefree D) := { out := hD }⊢ ∃ 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_quadraticAlgebra]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) := { out := hd₁ }⊢ ∃ 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) := { out := hd₁ }this:Fact (Squarefree d) := { out := hd }⊢ ∃ 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 NumberField


namespace 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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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