Prove2Me

Proof of Lemma 3, p. 14 — if gcd(q, M) ≠ q then gcd(q, M) ≤ q/2

Proved
JRPHard.RangeDiv.gcd_le_half

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisorsgcdp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let MM be a natural number and qq a positive integer. If gcd⁡(q,M)≠q\gcd(q, M) \ne q, then

gcd⁡(q,M)≤q2.\gcd(q, M) \le \frac{q}{2}.

The greatest common divisor is a divisor of qq; a divisor of qq other than qq itself is at most q/2q/2. This is what separates non-divisors of MM from divisors in problem (5).

Formalization Note The bound is stated without division, as 2gcd⁡(q,M)≤q2\gcd(q,M) \le q in the natural numbers.

Preamble
import Mathlib
import Definitions.Def_JRPHard_RangeDiv_Setting
Formal statement
namespace JRPHard.RangeDiv

theorem gcd_le_half (M q : ℕ) (hq : 0 < q) (hne : Nat.gcd q M ≠ q) :
    2 * Nat.gcd q M ≤ q := by sorry

end JRPHard.RangeDiv
Source
Schulz and Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, p. 14, §3.1, proof of Lemma 3, "Note that for any integer q satisfying gcd(q, M) ≠ q"
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 15, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph