Artin's conjecture on primitive roots

Artin's conjecture predicts, given an integer $a$, densities of primes $p$ for which $a$ is a primitive root modulo $p$. Under certain conditions (when $a$ is not a power and its squarefree part is $1\pmod{4}$) the density is given by Artin's constant $$\prod_{p\ \text{prime}} \left(1 - \frac{1}{p(p - 1)}\right).$$ For more general values of $a$, this constant must be corrected by certain factors.

• When $a = b^m$, $m$ is a maximal odd power, the squarefree part of $b$ satisfies $b_0 \not\equiv 1\pmod{4}$. Then Artin's constant should be multiplied by $$\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}.$$
• When $a = b^m$, $m$ is a maximal power, the squarefree part of $b$ satisfies $b_0\equiv 1\pmod{4}$. Then Artin's constant should be multiplied by the factor in the above bullet, as well as an additional entanglement factor from the primes dividing $\gcd(b_0, m)$ and primes dividing $b_0$: $$1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{1 + p - p^2}.$$
• When $a = -1$ or $a$ is a square, then the density is $0$.

Note that Artin's conjecture has been proved subject to the Generalized Riemann Hypothesis [Ho67].

References:

• Wikipedia
• OEIS
• LMS14 Lenstra, H.W. et al. "Character sums for primitive root densities" arXiv:1112.4816 [math.NT] (2014).
• [Ho67] Hooley, C. "On Artin's conjecture." Journal für die reine und angewandte Mathematik 225 (1967): 209-220.

@[reducible, inline]

abbrev ArtinPrimitiveRootsConjecture.S (a : ℤ) : Set ℕ

Let $S(a)$ be the set of primes such that $a$ is a primitive root modulo $p$.

Equations

• ArtinPrimitiveRootsConjecture.S a = {p : ℕ | Nat.Prime p ∧ orderOf ↑a = p - 1}

noncomputable def ArtinPrimitiveRootsConjecture.ArtinConstant : ℝ

Artin's Constant is defined to be the product $$\prod_{p\ \text{prime}}, \left(1 - \frac{1}{p(p - 1)}\right)$$.

Equations

• ArtinPrimitiveRootsConjecture.ArtinConstant = ∏' (p : Nat.Primes), (1 - 1 / (↑↑p * (↑↑p - 1)))

noncomputable def ArtinPrimitiveRootsConjecture.powCorrectionFactor (m : ℕ) : ℝ

Artin's conjecture on $S(a)$ when $a = b^m$ is a power, where $m$ is odd and maximal, requires a correction factor to multiply ArtinConstant and is given by $$\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}.$$

Equations

• ArtinPrimitiveRootsConjecture.powCorrectionFactor m = ∏ p ∈ m.primeFactors, ↑p * (↑p - 2) / (↑p ^ 2 - ↑p - 1)

noncomputable def ArtinPrimitiveRootsConjecture.entanglementFactor (b m : ℕ) : ℝ

Artin's conjecture on $S(a)$ when $a = b^m$ is a power, and the squarefree part of $b_0\equiv 1\pmod{4}$, requires a further correct factor to ArtinConstant * powCorrectionFactor m, which modifies primes which divide $\gcd(b_0, m)$ and primes which do not divide $m$ separately as $$ 1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{1 + p - p^2}.$$

Equations

• One or more equations did not get rendered due to their size.

theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1) : ∃ x > 0, (S a).HasDensity x {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, first half. Let $a$ be an integer that is not a square number and not $−1$. Then the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ has a positive asymptotic density inside the set of primes. In particular, $S(a)$ is infinite.

theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1) (h : ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → ∀ (s : ℂ), DirichletCharacter.LFunction χ s = 0 → s ∉ Int.cast '' GRH.trivialZeros χ → s.re = 1 / 2) : ∃ x > 0, (S a).HasDensity x {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, first half, conditional on GRH.

theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.ii (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2) (ha' : ∀ (n : ℤ) (m : ℕ), m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0) (ha_0' : ¬a_0 ≡ 1 [ZMOD 4]) : (S a).HasDensity ArtinConstant {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half. Write $a = a_0 b^2$ where $a_0$ is squarefree. Under the conditions that $a$ is not a perfect power and $a_0\not\equiv 1\pmod{4}$ (sequence A085397 in the OEIS), the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is independent of $a$ and equals Artin's constant.

theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.ii (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2) (ha' : ∀ (n : ℤ) (m : ℕ), m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0) (ha_0' : ¬a_0 ≡ 1 [ZMOD 4]) (h : ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → ∀ (s : ℂ), DirichletCharacter.LFunction χ s = 0 → s ∉ Int.cast '' GRH.trivialZeros χ → s.re = 1 / 2) : (S a).HasDensity ArtinConstant {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half, conditional on GRH.

theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_square_or_minus_one (a : ℤ) (ha : IsSquare a ∨ a = -1) : (S a).HasDensity 0 {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half, different residue version If $a$ is a square number or $a = −1$, then the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is $0$.

theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_prime_power_squarefree_not_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ (u v : ℕ), 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : Odd m) (hb' : ¬b.squarefreePart ≡ 1 [MOD 4]) : (S ↑a).HasDensity (ArtinConstant * powCorrectionFactor m) {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half, power version If $a = b^m$ is a perfect odd power of a number $b$ whose squarefree part $b_0\not\equiv 1 \pmod{4}$, then the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is given by $$C\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}$$, where $C$ is Artin's constant.

theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_prime_power_squarefree_not_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ (u v : ℕ), 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : Odd m) (hb' : ¬b.squarefreePart ≡ 1 [MOD 4]) (h : ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → ∀ (s : ℂ), DirichletCharacter.LFunction χ s = 0 → s ∉ Int.cast '' GRH.trivialZeros χ → s.re = 1 / 2) : (S ↑a).HasDensity (ArtinConstant * powCorrectionFactor m) {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half, power version, conditional on GRH

theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_prime_power_squarefree_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ (u v : ℕ), 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : m.primeFactorsList.Nodup) (hm₃ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4]) : (S ↑a).HasDensity (ArtinConstant * powCorrectionFactor m * entanglementFactor b m) {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half, power version If $a = b^m$ is a perfect power of a number $b$ whose squarefree part $b_0\equiv 1 \pmod{4}$, then the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is given by $$C \left(\prod_{p \mid m} \frac{p(p-2)}{(p ^ 2 - p - 1)}\right) \left(1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{(1 + p - p ^ 2)}\right)$$, where $C$ is Artin's constant.

theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_prime_power_squarefree_modeq_one (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ (u v : ℕ), 1 < u → b ≠ v ^ u) (hm₁ : 1 < m) (hm₂ : m.primeFactorsList.Nodup) (hm₃ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4]) (h : ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → ∀ (s : ℂ), DirichletCharacter.LFunction χ s = 0 → s ∉ Int.cast '' GRH.trivialZeros χ → s.re = 1 / 2) : (S ↑a).HasDensity (ArtinConstant * powCorrectionFactor m * entanglementFactor b m) {p : ℕ | Nat.Prime p}

Artin's Conjecture on Primitive Roots, second half, power version, conditional on GRH.