Proof of Lemma 2, p. 11 — for such a divisor p, M/gcd(p, M) + p ≤ 2M/3

Proved

JRPHard.Periodic.small_divisor_value

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

gcdinteger-factorizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ and $p$ be natural numbers with $p \mid M$ , $3 \le p$ and $3p \le M$ . Then the objective of problem (4) at $p$ satisfies

\frac{M}{\gcd(p,M)} + p \le \frac{2M}{3}.

Together with the existence of such a divisor for odd composite $M$ , this shows that the optimal value of problem (4) is at most $2M/3$ , strictly below $M$ .

Preamble

import Mathlib
import Definitions.Def_JRPHard_Periodic_Setting

Formal statement

namespace JRPHard.Periodic

theorem small_divisor_value (M p : ℕ) (hpM : p ∣ M) (hp3 : 3 ≤ p) (hple : 3 * p ≤ M) :
    obj4 M p ≤ 2 * (M : ℝ) / 3 := by sorry

end JRPHard.Periodic

Source

Schulz and Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, p. 11, §2.2, proof of Lemma 2, "Optimal replenishment cycle for item 1", last sentence of p. 11

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