Proof of Lemma 3, p. 15 — a period with objective at most L + U divides M and lies in [L, U]

Proved

JRPHard.RangeDiv.cheap_divisor_in_range

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

divisorsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1range-divisor

Let $M \ge U \ge L > 0$ be integers with $L + U < 2\sqrt{2LU}$ , and let $q$ be a positive integer with

\frac{LU}{\gcd(q,M)} + q \ \le\ L + U.

Then $q$ divides $M$ , and $L \le q \le U$ .

This is the "no-instance" direction of the reduction: if problem (5) reaches the level $L + U$ , the period achieving it is a divisor of $M$ in the range $[L, U]$ .

Preamble

import Mathlib
import Definitions.Def_JRPHard_RangeDiv_Setting

Formal statement

namespace JRPHard.RangeDiv

theorem cheap_divisor_in_range (M L U : ℕ) (hI : IsRangeDivisorInstance M L U) (q : ℕ)
    (hq : 0 < q) (hle : obj5 M L U q ≤ (L : ℝ) + U) :
    q ∣ M ∧ L ≤ q ∧ q ≤ U := 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. 15, §3.1, proof of Lemma 3, "On the other hand, if JRP_{M,U,L} ≤ L + U, then the optimizer must be a divisor of M"

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