Numbers $1+Qm$ with indices in a window of width $D$ are pairwise coprime when $D!\mid Q$

Proved

IntMul.HvdH.coprime_window

by xuanji · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

integer-multiplicationnumber-theory

Let $D,Q,m,m'$ be natural numbers with $D!\mid Q$ , $m\ne m'$ and $|m-m'|\le D$ . Then

\gcd(1+Qm,\;1+Qm')=1 .

Indeed a common prime factor $p$ would divide $Q(m'-m)$ but not $Q$ , hence $p\mid m'-m$ , so $p\le D$ and $p\mid D!\mid Q$ , a contradiction. This elementary fact replaces the use of primes in short intervals (Lemma 5.1) in the parameter selection of Harvey–van der Hoeven.

Preamble

import Mathlib

Formal statement

namespace IntMul.HvdH
theorem coprime_window (D Q m m' : ℕ) (hQ : D.factorial ∣ Q) (hne : m ≠ m')
    (hw : m ≤ m' + D) (hw' : m' ≤ m + D) : Nat.Coprime (1 + Q * m) (1 + Q * m') := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Section 5.1 (Lemma 5.1 and condition (5.11)); elementary replacement

View graph

Numbers 1+Qm1+Qm1+Qm with indices in a window of width DDD are pairwise coprime when D!∣QD!\mid QD!∣Q

Numbers $1+Qm$ with indices in a window of width $D$ are pairwise coprime when $D!\mid Q$