Primitive divisors

DefinitionPrimitive divisor of an integer sequence#✓fully proved

Let \((a_s)_{s \ge 0}\) be a sequence of integers and let \(m\) and \(u\) be natural numbers. Then \(u\) is a primitive divisor of \(a_m\) when \(m \ge 1\), \(u \ge 2\), \(u\) divides \(a_m\), and \(u\) divides no \(a_s\) with \(1 \le s < m\).

def IsPrimitiveDivisor (a : ℕ → ℤ) (m u : ℕ) : Prop :=
  1 ≤ m ∧ 2 ≤ u ∧ (u : ℤ) ∣ a m ∧ ∀ s : ℕ, 1 ≤ s → s < m → ¬ (u : ℤ) ∣ a s
Used by 6
Used by\(7\) is a large Zsigmondy prime for \((2, 1, 3)\) · Primitive prime divisor of an integer sequence · A primitive divisor appears at the least positive index · A primitive divisor occurs at only one index · A primitive prime divisor occurs at only one index · Zsigmondy's theorem

DefinitionPrimitive prime divisor of an integer sequence#✓fully proved

Let \((a_s)_{s \ge 0}\) be a sequence of integers and let \(m\) and \(u\) be natural numbers. Then \(u\) is a primitive prime divisor of \(a_m\) when \(u\) is prime and \(u\) is a primitive divisor of \(a_m\).

def IsPrimitivePrimeDivisor (a : ℕ → ℤ) (m u : ℕ) : Prop :=
  Nat.Prime u ∧ IsPrimitiveDivisor a m u
Uses 1 · Used by 14
Statement usesPrimitive divisor of an integer sequence
Used byPrimitive prime factors of \(a^n + 1\) · Primitive prime divisors of \(a^n - 1\) are \(1\) modulo \(n\) · Carmichael's congruence for primitive prime divisors of Fibonacci numbers · Carmichael's primitive divisor theorem · Bilu–Hanrot–Voutier theorem for Lucas sequences · Zsigmondy primes divide the homogenized cyclotomic value · A Zsigmondy prime \(q\) that is not large satisfies \(n = q - 1\) · Large Zsigmondy prime · \(7\) is a large Zsigmondy prime for \((2, 1, 3)\) · Prime divisors of homogenized cyclotomic values · A primitive prime divisor occurs at only one index · Zsigmondy's theorem · Infinitely many Riesel repunits from primitive divisors of \(2^{2^j} - 1\) · Infinitely many Sierpiński repunits from primitive divisors of \(2^{2^j} - 1\)

TheoremA primitive divisor appears at the least positive index#✓fully proved

Let \((a_s)_{s \ge 0}\) be a sequence of integers and let the natural number \(u\) be a primitive divisor of \(a_m\). If \(n \ge 1\) and \(u\) divides \(a_n\), then \(m \le n\).

theorem IsPrimitiveDivisor.le_of_dvd {a : ℕ → ℤ} {m u n : ℕ}
    (hm : IsPrimitiveDivisor a m u) (hn : 1 ≤ n) (hdvd : (u : ℤ) ∣ a n) :
    m ≤ n
Uses 1 · Used by 1
Statement usesPrimitive divisor of an integer sequence
Used byA primitive divisor occurs at only one index

TheoremA primitive divisor occurs at only one index#✓fully proved

Let \((a_s)_{s \ge 0}\) be a sequence of integers. If a natural number \(u\) is a primitive divisor of both \(a_m\) and \(a_n\), then \(m = n\).

theorem IsPrimitiveDivisor.unique {a : ℕ → ℤ} {m n u : ℕ}
    (hm : IsPrimitiveDivisor a m u) (hn : IsPrimitiveDivisor a n u) :
    m = n
Uses 2 · Used by 1
Statement usesPrimitive divisor of an integer sequence
Proof usesA primitive divisor appears at the least positive index
Used byA primitive prime divisor occurs at only one index

TheoremA primitive prime divisor occurs at only one index#✓fully proved

Let \((a_s)_{s \ge 0}\) be a sequence of integers. If a natural number \(u\) is a primitive prime divisor of both \(a_m\) and \(a_n\), then \(m = n\).

theorem IsPrimitivePrimeDivisor.unique {a : ℕ → ℤ} {m n u : ℕ}
    (hm : IsPrimitivePrimeDivisor a m u) (hn : IsPrimitivePrimeDivisor a n u) :
    m = n
Uses 3
Statement usesPrimitive prime divisor of an integer sequence
Proof usesPrimitive divisor of an integer sequence · A primitive divisor occurs at only one index

DefinitionPrimitive divisor relative to a discriminant#✓fully proved

Let \(u_0, u_1, u_2, \dots\) be a sequence of integers and let \(D\) be an integer (for a Lucas pair \((\alpha, \beta)\), the discriminant \(D = (\alpha - \beta)^2\)). A natural number \(p\) is a primitive divisor of \(u_n\) when \(n \ge 1\), \(p\) is prime, \(p\) divides \(u_n\), and \(p\) does not divide \(D \, u_1 u_2 \cdots u_{n-1}\) (for \(n = 1\) the product is empty, and the condition is that \(p\) does not divide \(D\)).

def IsPrimitiveDivisor (u : ℕ → ℤ) (discriminant : ℤ) (n p : ℕ) : Prop :=
  0 < n ∧ p.Prime ∧ (p : ℤ) ∣ u n ∧
    ¬(p : ℤ) ∣ discriminant * ∏ k ∈ Finset.Ico 1 n, u k
Used by 1
Used byPrimitive divisors of Fibonacci numbers

TheoremPrimitive divisors of Fibonacci numbers#✓fully proved

Write \(F_j\) for the \(j\)-th Fibonacci number. For every natural number \(n \ge 7\) with \(n \ne 12\), \(F_n\) has a primitive divisor with respect to the discriminant \(5\): there is a prime \(p\) that divides \(F_n\) but does not divide \(5 F_1 F_2 \cdots F_{n-1}\).

This is the Fibonacci case of Carmichael's theorem on Lucas sequences, with \(\alpha = (1 + \sqrt{5})/2\) and \(\beta = (1 - \sqrt{5})/2\), so that \((\alpha - \beta)^2 = 5\).

theorem exists_isPrimitiveDivisor_fib {n : Nat} (hn : 7 ≤ n) (hne : n ≠ 12) :
    ∃ p, LucasSequence.IsPrimitiveDivisor (fun k => (Nat.fib k : Int)) (5 : Int) n p
Sources
  • Haojie Hong, On big primitive divisors of Fibonacci numbers, arXiv:2312.04354v1, bigPFn.tex lines 153–158 (https://arxiv.org/abs/2312.04354); R. D. Carmichael, On the numerical factors of the arithmetic forms αⁿ±βⁿ, Ann. of Math. (2) 15 (1913), 30–70.
Uses 2
Statement usesPrimitive divisor relative to a discriminant
Proof usesLifting the exponent for Fibonacci numbers

TheoremSomer's primitive divisor theorem#●ready to prove

Let \(P\) and \(Q\) be integers with \(Q \ne 0\), and let \((u_n)_{n \ge 0}\) be the integer sequence with \(u_0 = 0\), \(u_1 = 1\) and \(u_{n+2} = Pu_{n+1} - Qu_n\) (the Lucas sequence of the first kind). Suppose the sequence is nondegenerate: whenever complex numbers \(\alpha\) and \(\beta\) satisfy \(\alpha + \beta = P\), \(\alpha\beta = Q\) and \(\beta \ne 0\), no power \((\alpha / \beta)^k\) with \(k \ge 1\) equals \(1\). Then for all sufficiently large \(n\) the term \(u_n\) has a primitive prime divisor: a prime \(p\) that divides \(u_n\) but divides no \(u_m\) with \(0 < m < n\).

Nondegeneracy also excludes the double-root case \(\alpha = \beta\).

theorem_wanted somer_eventually_has_primitive_prime_divisor
    (P Q : ℤ) (u : ℕ → ℤ)
    (hu0 : u 0 = 0)
    (hu1 : u 1 = 1)
    (huRec : ∀ n : ℕ, u (n + 2) = P * u (n + 1) - Q * u n)
    (hQ : Q ≠ 0)
    (hNondeg : ∀ α β : ℂ, α + β = (P : ℂ) → α * β = (Q : ℂ) → β ≠ 0 →
      ∀ k : ℕ, 0 < k → (α / β) ^ k ≠ 1) :
    ∀ᶠ n : ℕ in Filter.atTop,
      ∃ p : ℕ, Nat.Prime p ∧ (p : ℤ) ∣ u n ∧
        ∀ m : ℕ, 0 < m → m < n → ¬ (p : ℤ) ∣ u m
Sources
7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.