WallSunSun.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 9 contain sorry, 0 declared as axioms

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

Imports (1)

FormalConjecturesUtil

lemma QuadraticAlgebra.discr_rat_of_modEq_one The discriminant of ℚ[√d] for d ≥ 2 squarefree congruent to 1 mod 4 is d sorry line 39 source
Source documentation
The discriminant of ℚ[√d] for d ≥ 2 squarefree congruent to 1 mod 4 is d.

depends on sorry what this means
Statement uses: Int, Fact, Squarefree, Ne, OfNat.ofNat, Int.ModEq, Eq, NumberField.discr, QuadraticAlgebra, Rat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma discr_rat_of_modEq_one (hd₄ : d ≡ 1 [ZMOD 4]) : discr (QuadraticAlgebra ℚ d 0) = d := by
…
```
lemma QuadraticAlgebra.discr_rat_of_not_modEq_one The discriminant of ℚ[√d] for d ≥ 2 squarefree not congruent to 1 mod 4 is 4 * d sorry line 44 source
Source documentation
The discriminant of ℚ[√d] for d ≥ 2 squarefree not congruent to 1 mod 4 is 4 * d.

depends on sorry what this means
Statement uses: Int, Fact, Squarefree, Ne, OfNat.ofNat, Not, Int.ModEq, Eq, NumberField.discr, QuadraticAlgebra, Rat, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma discr_rat_of_not_modEq_one (hd₄ : ¬ d ≡ 1 [ZMOD 4]) :
    discr (QuadraticAlgebra ℚ d 0) = 4 * d := by
…
```
lemma Algebra.exists_quadraticAlgebra_of_isQuadraticExtension A quadratic algebra L over a field K is isomorphic to the explicit quadratic algebra QuadraticAlgebra K a b for some a b : K sorry line 57 source
Source documentation
A quadratic algebra L over a field K is isomorphic to the explicit quadratic algebra QuadraticAlgebra K a b for some a b : K.

depends on sorry what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Exists, Nonempty, AlgEquiv, QuadraticAlgebra
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
41 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma exists_quadraticAlgebra_of_isQuadraticExtension [IsQuadraticExtension K L] :
    ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b) := by
…
```
lemma Algebra.isQuadraticExtension_iff_exists_quadraticAlgebra 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 sorry line 64 source
Source documentation
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.

depends on sorry what this means
Statement uses: Field, Algebra, Iff, Algebra.IsQuadraticExtension, Exists, Nonempty, AlgEquiv, QuadraticAlgebra
Proof uses: Iff.intro, Algebra.exists_quadraticAlgebra_of_isQuadraticExtension, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma isQuadraticExtension_iff_exists_quadraticAlgebra :
    IsQuadraticExtension K L ↔ ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b) where
…
```
lemma NumberField.exists_quadraticAlgebra_of_isQuadraticExtension A quadratic number field K is isomorphic to the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1 sorry line 78 source
Source documentation
A quadratic number field K is isomorphic to the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

depends on sorry what this means
Statement uses: Field, NumberField, Algebra.IsQuadraticExtension, Rat, Exists, Int, And, Ne, OfNat.ofNat, Squarefree, Nonempty, RingEquiv, QuadraticAlgebra
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
45 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma exists_quadraticAlgebra_of_isQuadraticExtension [IsQuadraticExtension ℚ K] :
    ∃ d ≠ (1 : ℤ), Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ d 0) := by
…
```
lemma NumberField.isQuadraticExtension_iff_exists_quadraticAlgebra 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 sorry line 85 source
Source documentation
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.

depends on sorry what this means
Statement uses: Field, NumberField, Iff, Algebra.IsQuadraticExtension, Rat, Exists, Int, And, Ne, OfNat.ofNat, Squarefree, Nonempty, RingEquiv, QuadraticAlgebra
Proof uses: Iff.intro, NumberField.exists_quadraticAlgebra_of_isQuadraticExtension, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma isQuadraticExtension_iff_exists_quadraticAlgebra :
    IsQuadraticExtension ℚ K ↔
      ∃ d ≠ (1 : ℤ), Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ d 0) where
…
```
lemma NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra 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 line 94 source
Source documentation
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.

depends on sorry what this means
Statement uses: Int, Iff, NumberField.IsFundamentalDiscr, Exists, Fact, Ne, OfNat.ofNat, Squarefree, Eq, NumberField.discr, QuadraticAlgebra, Rat
Proof uses: Iff.intro, And, Dvd.dvd, Not, Int.ModEq, HDiv.hDiv, HMul.hMul, Fact.mk, False, False.elim, Eq.mp, Eq.trans, True, congrArg, not_true_eq_false, Eq.symm, mul_div_cancel_left₀, of_eq_true, Nat, not_false_eq_true and 13 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma isFundamentalDiscr_iff_exists_discr_quadraticAlgebra {D : ℤ} :
    IsFundamentalDiscr D ↔ ∃ (d : ℤ) (_ : Fact <| d ≠ 1) (_ : Fact <| Squarefree d),
      discr (QuadraticAlgebra ℚ d 0) = D where
…
```
Mentions: NumberField.IsFundamentalDiscr
lemma NumberField.isFundamentalDiscr_iff_exists_discr_numberField An integer D is a fundamental discriminant iff it is the discriminant of some number field line 111 source
Source documentation
An integer D is a fundamental discriminant iff it is the discriminant of some number field.

depends on sorry what this means
Statement uses: Int, Iff, NumberField.IsFundamentalDiscr, Exists, Field, NumberField, And, Algebra.IsQuadraticExtension, Rat, Eq, NumberField.discr
Proof uses: Eq.mpr, Fact, Ne, OfNat.ofNat, Squarefree, QuadraticAlgebra, id, congrArg, propext, NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra, Iff.intro, Exists.intro, inferInstance, And.intro, rfl, Nonempty, RingEquiv, NumberField.exists_quadraticAlgebra_of_isQuadraticExtension, Fact.mk, NumberField.discr_eq_discr_of_ringEquiv and 1 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma isFundamentalDiscr_iff_exists_discr_numberField {D : ℤ} :
    IsFundamentalDiscr D ↔
      ∃ (K : Type) (_ : Field K) (_ : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D := by
…
```
Mentions: NumberField.IsFundamentalDiscr
theorem WallSunSun.exists_isWallSunSunPrime 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 sorry line 135 source
Source documentation
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.

depends on sorry what this means
Statement uses: Exists, Nat, IsWallSunSunPrime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_isWallSunSunPrime : ∃ p, IsWallSunSunPrime p := by
…
```
Mentions: IsWallSunSunPrime
theorem WallSunSun.infinite_isWallSunSunPrime 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 sorry line 143 source
Source documentation
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.

depends on sorry what this means
Statement uses: Set.Infinite, Nat, Set.ofPred, IsWallSunSunPrime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem infinite_isWallSunSunPrime : {p : ℕ | IsWallSunSunPrime p}.Infinite := by
…
```
Mentions: IsWallSunSunPrime
lemma WallSunSun.exists_parameters line 147 source
theorem WallSunSun.infinite_isWallSunSunPrime_of_disc_eq_varying_parameters 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 line 165 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, NumberField.IsFundamentalDiscr, Set.Infinite, Nat, Set.ofPred, Exists, And, Eq, HSub.hSub, HPow.hPow, OfNat.ofNat, HMul.hMul, IsLucasWieferichPrime
Proof uses: Ne, False, False.elim, Eq.mp, Eq.trans, Or, Dvd.dvd, Not, Int.ModEq, HDiv.hDiv, Squarefree, congr, congrArg, True, congrFun', EuclideanDomain.zero_div, and_false, not_false_eq_true, or_self, Eq.symm and 27 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: IsLucasWieferichPrime
theorem WallSunSun.infinite_isWallSunSunPrime_of_disc_eq Let $K$ be a real quadratic field of discriminant $D$ and let $\varepsilon$ be a fundamental unit of $K$ sorry line 214 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Field, NumberField, Algebra.IsQuadraticExtension, Rat, NumberField.IsTotallyReal, Int, Eq, NumberField.discr, Set.Infinite, Nat, Set.ofPred, And, Nat.Prime, Odd, Not, Dvd.dvd, Units, NumberField.RingOfIntegers, HPow.hPow, OfNat.ofNat and 5 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
92 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```