Powerful numbers in arithmetic progressions

TheoremArithmetic progressions of 2-full numbers of every length#✓fully proved

For every natural number \(k\) there are positive integers \(a\) and \(d\) such that \(a + id\) is \(2\)-full (powerful) for every natural number \(i < k\).

theorem arbitrarily_long_arithmetic_progressions_of_powerful_numbers_general (k : ℕ) :
    ∃ a d : ℕ, 0 < a ∧ 0 < d ∧
      ∀ i : ℕ, i < k → Nat.IsKFull 2 (a + i * d)

Uses 1 · Used by 1

Statement uses\(k\)-full numbers

Used byArbitrarily long arithmetic progressions of powerful numbers

TheoremArbitrarily long arithmetic progressions of powerful numbers#✓fully proved

For every integer \(k \ge 3\) there are positive integers \(a\) and \(d\) such that each of the \(k\) numbers \(a + id\) with \(0 \le i < k\) is powerful: every prime that divides \(a + id\) has its square dividing \(a + id\).

theorem arbitrarily_long_arithmetic_progressions_of_powerful_numbers
    (k : ℕ) (hk : 3 ≤ k) :
    ∃ a d : ℕ, 0 < a ∧ 0 < d ∧
      ∀ i : ℕ, i < k →
        ∀ p : ℕ, p.Prime → p ∣ a + i * d → p ^ 2 ∣ a + i * d

Sources

• Tsz Ho Chan, "Arithmetic Progressions Among Powerful Numbers", Journal of Integer Sequences 26 (2023), Article 23.1.1, Theorem thm-longAP, source lines 97–99, https://cs.uwaterloo.ca/journals/JIS/VOL26/Chan/chan33.tex. The paper notes the result is not new (see remark 2 in [H] there) and includes a proof for completeness. Powerful (squarefull) means every prime divisor appears with exponent at least two; nonconstant is 0 < d. It follows from arbitrarily_long_arithmetic_progressions_of_powerful_numbers_general, which states powerfulness as Nat.IsKFull 2; the hypothesis hk is unused and keeps the source's shape.

Uses 2

Proof usesArithmetic progressions of 2-full numbers of every length · \(k\)-full numbers

DefinitionFour-term progressions of pairwise coprime powerful numbers#✓fully proved

For natural numbers \(a\) and \(d\), the numbers \(a\), \(a + d\), \(a + 2d\), \(a + 3d\) form a four-term arithmetic progression of pairwise coprime powerful numbers when \(d > 0\), each of the four numbers is powerful (that is, \(2\)-full: nonzero and divisible by \(p^2\) for every prime \(p\) dividing it), and any two of the four numbers are coprime.

def IsCoprimePowerfulAP4 (a d : ℕ) : Prop :=
  0 < d ∧
  Nat.IsKFull 2 a ∧ Nat.IsKFull 2 (a + d) ∧ Nat.IsKFull 2 (a + 2 * d) ∧
  Nat.IsKFull 2 (a + 3 * d) ∧
  a.Coprime (a + d) ∧ a.Coprime (a + 2 * d) ∧ a.Coprime (a + 3 * d) ∧
  (a + d).Coprime (a + 2 * d) ∧ (a + d).Coprime (a + 3 * d) ∧
  (a + 2 * d).Coprime (a + 3 * d)

Uses 1 · Used by 1

Statement uses\(k\)-full numbers

Used byStatement of Erdős Problem 937

DefinitionStatement of Erdős Problem 937#✓fully proved

There are infinitely many pairs of natural numbers \((a, d)\) with \(d > 0\) such that the four numbers \(a\), \(a + d\), \(a + 2d\), \(a + 3d\) are powerful (each is nonzero and divisible by \(p^2\) for every prime \(p\) dividing it) and pairwise coprime; that is, infinitely many four-term arithmetic progressions of pairwise coprime powerful numbers.

def conjecture : Prop :=
  {p : ℕ × ℕ | IsCoprimePowerfulAP4 p.1 p.2}.Infinite

Uses 1 · Used by 1

Statement usesFour-term progressions of pairwise coprime powerful numbers

Used byErdős Problem 937 holds (Bajpai–Bennett–Chan)

TheoremErdős Problem 937 holds (Bajpai–Bennett–Chan)#●ready to prove

There are infinitely many pairs of natural numbers \((a, d)\) with \(d > 0\) such that the four numbers \(a\), \(a + d\), \(a + 2d\), \(a + 3d\) are powerful (each is nonzero and divisible by \(p^2\) for every prime \(p\) dividing it) and pairwise coprime. That is, there are infinitely many four-term arithmetic progressions of pairwise coprime powerful numbers.

public theorem_wanted conjecture_holds : conjecture

Sources

• Prajeet Bajpai, Michael A. Bennett, and Tsz Ho Chan, Arithmetic progressions in squarefull numbers, International Journal of Number Theory 20 (2024), 19–45, https://mathscinet.ams.org/mathscinet-getitem?mr=4688726. Resolved true: Resolved true by Bajpai–Bennett–Chan; a proof is available in an external Lean development.

Uses 1

Statement usesStatement of Erdős Problem 937

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.