fix(Wikipedia/WallSunSun): restrict D to fundamental discriminants

FormalConjectures/Wikipedia/WallSunSun.lean

@@ -40,15 +40,26 @@ $p$-th Lucas number. It is conjectured that there are infinitely many Wall-Sun-S
 theorem infinite_isWallSunSunPrime : {p : ℕ | IsWallSunSunPrime p}.Infinite := by
   sorry
 
+/-- 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 IsFundamentalDiscriminant (D : ℤ) : Prop :=
+  4 ∣ D ∧ (D / 4 ≡ 2 [ZMOD 4] ∨ D / 4 ≡ 3 [ZMOD 4]) ∧ Squarefree (D / 4) ∨
+    D ≡ 1 [ZMOD 4] ∧ Squarefree D
+
 /--
-A Lucas–Wieferich prime associated with $(a,b)$ is an odd prime $p$, not dividing $a^2 - b$, such
+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 discriminant.
+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₀ : 0 < D)
-    (hD : D ≡ 0 [MOD 4] ∨ D ≡ 1 [MOD 4]) :
-    {p : ℕ | ∃ a b : ℕ, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite := by
+theorem infinite_isWallSunSunPrime_of_disc_eq {D : ℤ} (hD : IsFundamentalDiscriminant D)
+    (hD₁ : D ≠ 1) :
+    {p : ℕ | ∃ a b, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite := by
   sorry

FormalConjecturesForMathlib/NumberTheory/WallSunSunPrimes.lean

@@ -70,7 +70,7 @@ See first paragraph of
 https://en.wikipedia.org/wiki/Wall%E2%80%93Sun%E2%80%93Sun_prime#Wall%E2%80%93Sun%E2%80%93Sun_primes_with_discriminant_D
 for the condition that $p$ is odd and coprime to the discriminant
 -/
-structure IsLucasWieferichPrime (a b p : ℕ) : Prop where
+structure IsLucasWieferichPrime (a b : ℤ) (p : ℕ) : Prop where
   prime : p.Prime
   odd : Odd p
   not_dvd : ¬(p : ℤ) ∣ a ^ 2 - 4 * b