Perfect powers in products of arithmetic progressions

StructureSolutions of the Erdős equation for products of arithmetic progressions#✓fully proved

For a natural number \(k\), a solution consists of a natural number \(l\) and integers \(n\), \(d\), \(y\) such that \(\gcd(n, d) = 1\) and

\[\prod_{i=0}^{k-1} (n + i d) = y^l,\]

that is, \(n (n + d) (n + 2d) \cdots (n + (k - 1)d) = y^l\).

structure Solution (k : ℕ) where
  /-- The exponent `l` in the solution. -/
  l : ℕ
  /-- The value of `n` in the solution. -/
  n : ℤ
  /-- The value of `d` in the solution. -/
  d : ℤ
  /-- The value of `y` in the solution. -/
  y : ℤ
  gcd : gcd n d = 1
  eq : ∏ i ∈ Finset.range k, (n + i * d) = y ^ l

Used by 1

Used byBennett–Siksek theorem on perfect powers in arithmetic progressions

DefinitionThe threshold constant \(k_0\) in the Bennett–Siksek theorem#●ready to state

A natural number \(k_0\), to be supplied: the absolute constant from which Theorem 2 holds, that is, for every natural number \(k \ge k_0\), every solution in integers \(n\), \(d\), \(y\) and a prime natural number \(l\) of \(\prod_{i=0}^{k-1} (n + i d) = y^l\) with \(\gcd(n, d) = 1\) has \(y = 0\) or \(d = 0\) or \(l \le \exp(10^k)\).

The source requires \(k_0\) to be effectively computable; the formal statement does not enforce this.

public def_wanted k₀ : ℕ

Sources

• M. Bennett and S. Siksek, A conjecture of Erdős, supersingular primes and short character sums, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_erdos_supersingular_primes of the lean-eval benchmark.

Used by 1

Used byBennett–Siksek theorem on perfect powers in arithmetic progressions

TheoremBennett–Siksek theorem on perfect powers in arithmetic progressions#●statement formalized

Let \(k_0\) be the threshold constant of this module. For every natural number \(k \ge k_0\), every natural number \(l\) that is prime, and all integers \(n\), \(d\), \(y\) with \(\gcd(n, d) = 1\) and

\[\prod_{i=0}^{k-1} (n + i d) = y^l,\]

we have \(y = 0\) or \(d = 0\) or \(l \le \exp(10^k)\).

The source asserts that \(k_0\) is an effectively computable absolute constant; the formal statement leaves \(k_0\) to be supplied and does not enforce computability.

public theorem_wanted theorem_2 (k : ℕ) (s : Solution k) (hs : s.l.Prime) :
    k ≥ ❰k₀❱ → s.y = 0 ∨ s.d = 0 ∨ s.l ≤ exp (10 ^ k)

Sources

• M. Bennett and S. Siksek, A conjecture of Erdős, supersingular primes and short character sums, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_erdos_supersingular_primes of the lean-eval benchmark.

Uses 2

Statement usesSolutions of the Erdős equation for products of arithmetic progressions · The threshold constant \(k_0\) in the Bennett–Siksek theorem

1 fully proved1 statement formalized1 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.