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.
-/
module

public import FormalConjecturesUtil

Infinitude of Wall–Sun–Sun primes

References:

Wikipedia

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

@[expose] public sectionopen 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 WallSunSunopen scoped NumberTheorySymbols

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! 🐙

@[category API, AMS 11]
private lemma exists_parameters {D : ℤ} {p : ℕ}
    (hmod : (4 : ℤ) ∣ D ∨ D ≡ 1 [ZMOD 4]) (hodd : Odd p) :
    ∃ a b : ℤ, a ^ 2 - 4 * b = D ∧ (p : ℤ) ^ 2 ∣ a := byD:ℤp:ℕhmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]hodd:Odd p⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑p ^ 2 ∣ a
  rcases hmod with hfour | honeinlD:ℤp:ℕhodd:Odd phfour:4 ∣ D⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑p ^ 2 ∣ ainrD:ℤp:ℕhodd:Odd phone:D ≡ 1 [ZMOD 4]⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑p ^ 2 ∣ a
  ·inlD:ℤp:ℕhodd:Odd phfour:4 ∣ D⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑p ^ 2 ∣ a rcases hfour with ⟨d, rfl⟩inlp:ℕhodd:Odd pd:ℤ⊢ ∃ a b, a ^ 2 - 4 * b = 4 * d ∧ ↑p ^ 2 ∣ a
    refine ⟨2 * (p : ℤ) ^ 2, (p : ℤ) ^ 4 - d, byp:ℕhodd:Odd pd:ℤ⊢ (2 * ↑p ^ 2) ^ 2 - 4 * (↑p ^ 4 - d) = 4 * d ringAll goals completed! 🐙, ?_⟩
    exact dvd_mul_left _ _All goals completed! 🐙
  ·inrD:ℤp:ℕhodd:Odd phone:D ≡ 1 [ZMOD 4]⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑p ^ 2 ∣ a rcases hodd with ⟨k, rfl⟩inrD:ℤhone:D ≡ 1 [ZMOD 4]k:ℕ⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑(2 * k + 1) ^ 2 ∣ a
    rcases hone.dvd with ⟨c, hc⟩inrD:ℤhone:D ≡ 1 [ZMOD 4]k:ℕc:ℤhc:1 - D = 4 * c⊢ ∃ a b, a ^ 2 - 4 * b = D ∧ ↑(2 * k + 1) ^ 2 ∣ a
    refine ⟨((2 * k + 1 : ℕ) : ℤ) ^ 2,
      4 * (k : ℤ) ^ 4 + 8 * (k : ℤ) ^ 3 + 6 * (k : ℤ) ^ 2 + 2 * (k : ℤ) + c,
      ?_, dvd_refl _⟩inrD:ℤhone:D ≡ 1 [ZMOD 4]k:ℕc:ℤhc:1 - D = 4 * c⊢ (↑(2 * k + 1) ^ 2) ^ 2 - 4 * (4 * ↑k ^ 4 + 8 * ↑k ^ 3 + 6 * ↑k ^ 2 + 2 * ↑k + c) = D
    push_castinrD:ℤhone:D ≡ 1 [ZMOD 4]k:ℕc:ℤhc:1 - D = 4 * c⊢ ((2 * ↑k + 1) ^ 2) ^ 2 - 4 * (4 * ↑k ^ 4 + 8 * ↑k ^ 3 + 6 * ↑k ^ 2 + 2 * ↑k + c) = D
    nlinarithAll goals completed! 🐙

An earlier formulation of infinite_isWallSunSunPrime_of_disc_eq, which chose the Lucas parameters $(a, b)$ separately for every prime $p$, was degenerate: it is provable.


@[category test, AMS 11]
theorem infinite_isWallSunSunPrime_of_disc_eq_varying_parameters {D : ℤ}
    (hD : IsFundamentalDiscr D) :
    {p : ℕ | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite := byD:ℤhD:IsFundamentalDiscr D⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
  have hDzero : D ≠ 0 := by
    intro hD:ℤhD:IsFundamentalDiscr Dh:D = 0⊢ FalseD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
    subst DhD:IsFundamentalDiscr 0⊢ FalseD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
    simp [IsFundamentalDiscr] at hDD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.InfiniteD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
  have hmod : (4 : ℤ) ∣ D ∨ D ≡ 1 [ZMOD 4] := by
    rcases hD with h | hinlD:ℤhDzero:D ≠ 0h:4 ∣ D ∧ ¬D / 4 ≡ 1 [ZMOD 4] ∧ Squarefree (D / 4)⊢ 4 ∣ D ∨ D ≡ 1 [ZMOD 4]inrD:ℤhDzero:D ≠ 0h:D ≠ 1 ∧ D ≡ 1 [ZMOD 4] ∧ Squarefree D⊢ 4 ∣ D ∨ D ≡ 1 [ZMOD 4]D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
    ·inlD:ℤhDzero:D ≠ 0h:4 ∣ D ∧ ¬D / 4 ≡ 1 [ZMOD 4] ∧ Squarefree (D / 4)⊢ 4 ∣ D ∨ D ≡ 1 [ZMOD 4]D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite exact Or.inl h.1All goals completed! 🐙D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
    ·inrD:ℤhDzero:D ≠ 0h:D ≠ 1 ∧ D ≡ 1 [ZMOD 4] ∧ Squarefree D⊢ 4 ∣ D ∨ D ≡ 1 [ZMOD 4]D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite exact Or.inr h.2.1D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.InfiniteD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
  let B := max D.natAbs 2D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
  have hinf : ({p : ℕ | p.Prime} \ Set.Iic B).Infinite :=
    Nat.infinite_setOfPred_prime.sdiff (Set.finite_Iic B)D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinite⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite
  apply hinf.monoD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinite⊢ {p | Nat.Prime p} \ Set.Iic B ⊆ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  intro p hpBD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhpB:p ∈ {p | Nat.Prime p} \ Set.Iic B⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  rcases hpB with ⟨hp, hpB⟩D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:p ∈ {p | Nat.Prime p}hpB:p ∉ Set.Iic B⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  simp only [Set.mem_ofPred_eq] at hpD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:p ∉ Set.Iic B⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  simp only [Set.mem_Iic, not_le] at hpBD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < p⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  have hpD : D.natAbs < p := lt_of_le_of_lt (le_max_left _ _) hpBD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < p⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  have hp2 : 2 < p := lt_of_le_of_lt (le_max_right _ _) hpBD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < p⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  have hodd : Odd p := hp.odd_of_ne_two (byD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < p⊢ p ≠ 2D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd p⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p} omegaAll goals completed! 🐙D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd p⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p})D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd p⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  have hpd : ¬ (p : ℤ) ∣ D := byD:ℤhD:IsFundamentalDiscr D⊢ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.InfiniteD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ D⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
    intro hD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd ph:↑p ∣ D⊢ FalseD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ D⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
    have := Int.natAbs_le_of_dvd_ne_zero h hDzeroD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd ph:↑p ∣ Dthis:(↑p).natAbs ≤ D.natAbs⊢ FalseD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ D⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
    simp only [Int.natAbs_natCast] at thisD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd ph:↑p ∣ Dthis:p ≤ D.natAbs⊢ FalseD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ D⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
    omegaD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ D⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}D:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ D⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  obtain ⟨a, b, hab, ha⟩ := exists_parameters hmod hoddD:ℤhD:IsFundamentalDiscr DhDzero:D ≠ 0hmod:4 ∣ D ∨ D ≡ 1 [ZMOD 4]B:ℕ := max D.natAbs 2hinf:({p | Nat.Prime p} \ Set.Iic B).Infinitep:ℕhp:Nat.Prime phpB:B < phpD:D.natAbs < php2:2 < phodd:Odd phpd:¬↑p ∣ Da:ℤb:ℤhab:a ^ 2 - 4 * b = Dha:↑p ^ 2 ∣ a⊢ p ∈ {p | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}
  exact ⟨a, b, hab, IsLucasWieferichPrime.of_sq_dvd hp hodd (hab ▸ hpd) ha⟩All goals completed! 🐙

Let $K$ be a real quadratic field of discriminant $D$ and let $\varepsilon$ be a fundamental unit of $K$. Following [EJ10, Remark 2.2.8], an odd prime $p \nmid D$ is a Wall–Sun–Sun prime for $K$ if, in $\mathcal{O}_K$, $\varepsilon^{p-1} \equiv 1 \pmod{p^2}$ when $\left(\tfrac{D}{p}\right) = 1$, and $\varepsilon^{2p+2} \equiv 1 \pmod{p^2}$ when $\left(\tfrac{D}{p}\right) = -1$. Both exponents are even, so the condition does not depend on the choice of $\varepsilon$, and it is equivalent to asking the same congruence for every unit of $K$. For $K = \mathbb{Q}(\sqrt{5})$ and $\varepsilon = \frac{1 + \sqrt{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 $\mathbb{Q}(\sqrt{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 $2p + 2$ for every odd prime $p \nmid D$.

@[category research open, AMS 11]
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 := byK:Type u_1inst✝³:Field Kinst✝²:NumberField Kinst✝¹:IsQuadraticExtension ℚ Kinst✝:IsTotallyReal KD:ℤhD:discr K = D⊢ {p |
    Nat.Prime p ∧
      Odd p ∧ ¬↑p ∣ D ∧ ∀ (ε : (𝓞 K)ˣ), ↑p ^ 2 ∣ (↑ε ^ if J(D | p) = 1 then p - 1 else 2 * p + 2) - 1}.Infinite
  sorryAll goals completed! 🐙

end WallSunSun