FormalConjecturesForMathlib/NumberTheory/WallSunSunPrimes.lean

GitHub source file

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

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

7 declarations, 0 contain sorry, 0 declared as axioms

Wall-Sun-Sun primes

References:

Imports (1)
Imported by 1 file
  1. def LucasSequence.U The Lucas sequence of the first kind $U_0(P, Q) = 0$, $U_1(P, Q)=1$, $U_{n+2}(P, Q)=PU_{n+1}(P, Q)-QU_n(P, Q)$ line 38 source

    Source documentation

    The Lucas sequence of the first kind $U_0(P, Q) = 0$, $U_1(P, Q)=1$, $U_{n+2}(P, Q)=PU_{n+1}(P, Q)-QU_n(P, Q)$

    no axioms what this means

    Statement uses: Int, Nat

    2 instances, coercions and auxiliary constants left out.

    def LucasSequence.U (P Q : ℤ) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => P * LucasSequence.U P Q (n + 1) - Q * LucasSequence.U P Q n

/--
**The Lucas sequence of the second kind**
$V_0(P, Q) = 0$, $V_1(P, Q)=P$, $V_{n+2}(P, Q)=PV_{n+1}(P, Q)-QV_n(P, Q)$
-/
  2. def LucasSequence.V The Lucas sequence of the second kind $V_0(P, Q) = 0$, $V_1(P, Q)=P$, $V_{n+2}(P, Q)=PV_{n+1}(P, Q)-QV_n(P, Q)$ line 47 source

    Source documentation

    The Lucas sequence of the second kind $V_0(P, Q) = 0$, $V_1(P, Q)=P$, $V_{n+2}(P, Q)=PV_{n+1}(P, Q)-QV_n(P, Q)$

    no axioms what this means

    Statement uses: Int, Nat

    2 instances, coercions and auxiliary constants left out.

    def LucasSequence.V (P Q : ℤ) : ℕ → ℤ
  | 0 => 2
  | 1 => P
  | n + 2 => P * LucasSequence.V P Q (n + 1) - Q * LucasSequence.V P Q n

/--
**The Lucas numbers**
$L_0 = 2$, $L_1=1$, $L_{n+2} = L_{n+1}+L_n$
-/
  3. def lucasNumber The Lucas numbers $L_0 = 2$, $L_1=1$, $L_{n+2} = L_{n+1}+L_n$ line 56 source

    Source documentation

    The Lucas numbers $L_0 = 2$, $L_1=1$, $L_{n+2} = L_{n+1}+L_n$

    no axioms what this means

    Statement uses: Nat, Int

    Proof uses: LucasSequence.V, OfNat.ofNat, Neg.neg

    2 instances, coercions and auxiliary constants left out.

    def lucasNumber : ℕ → ℤ := LucasSequence.V 1 (-1)

    Mentions: LucasSequence.V

  4. structure IsWallSunSunPrime Wall–Sun–Sun prime 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 line 63 source

    Source documentation

    Wall–Sun–Sun prime 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.

    standard axioms: propext what this means

    Statement uses: Nat

    structure IsWallSunSunPrime (p : ℕ) : Prop where
…
  5. structure IsLucasWieferichPrime Documented declaration: IsLucasWieferichPrime line 77 source

    Source documentation

    Lucas–Wieferich prime 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)$.

    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

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Int, Nat

    structure IsLucasWieferichPrime (a b : ℤ) (p : ℕ) : Prop where
…
  6. theorem LucasSequence.dvd_U_two_mul The parameter $P$ divides every even-indexed term of the Lucas sequence $U(P, Q)$ line 84 source

    Source documentation

    The parameter $P$ divides every even-indexed term of the Lucas sequence $U(P, Q)$.

    standard axioms: Quot.sound, propext what this means

    Statement uses: Int, Nat, Dvd.dvd, LucasSequence.U, HMul.hMul, OfNat.ofNat

    Proof uses: Nat.recAux, of_eq_true, Eq.mpr, HAdd.hAdd, id, Eq, congrArg, Nat.succ, Nat.mul_succ, dvd_sub, dvd_mul_right, dvd_mul_of_dvd_right

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

    theorem LucasSequence.dvd_U_two_mul (P Q : ℤ) (k : ℕ) : P ∣ LucasSequence.U P Q (2 * k) := by
…

    Mentions: LucasSequence.U

  7. theorem IsLucasWieferichPrime.of_sq_dvd Documented declaration: of_sq_dvd line 95 source

    Source documentation

    If $p^2 \mid a$, then every odd prime $p$ not dividing $a^2 - 4b$ is a Lucas–Wieferich prime associated with $(a, b)$: the index $p - \left(\tfrac{a^2-4b}{p}\right)$ is even, and $a$ divides every even-indexed term of $U(a, b)$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Int, Nat, Nat.Prime, Odd, Not, Dvd.dvd, HSub.hSub, HPow.hPow, OfNat.ofNat, HMul.hMul, IsLucasWieferichPrime

    Proof uses: IsLucasWieferichPrime.mk, Eq.mpr, Int.ModEq, LucasSequence.U, Int.toNat, jacobiSym, id, Eq, congrArg, propext, Int.modEq_zero_iff_dvd, Int.gcd, Int.natAbs, Iff.mpr, Int.natCast_dvd, Nat.gcd, Int.gcd_eq_natAbs, Int.natAbs_natCast, Nat.gcd_comm, Nat.Coprime and 8 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

    Open to load the checked before-and-after goal states.

    theorem IsLucasWieferichPrime.of_sq_dvd {a b : ℤ} {p : ℕ} (hp : p.Prime) (hodd : Odd p)
    (hpd : ¬(p : ℤ) ∣ a ^ 2 - 4 * b) (ha : (p : ℤ) ^ 2 ∣ a) : IsLucasWieferichPrime a b p := by
…

    Mentions: IsLucasWieferichPrime