Prove2Me

Proof of Lemma 3, p. 15 — a divisor q of M in [L, U] has objective at most L + U

Proved
JRPHard.RangeDiv.divisor_in_range_cheap

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

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

Let M≥U≥L>0M \ge U \ge L > 0 be integers with L+U<22LUL + U < 2\sqrt{2LU}. If qq divides MM and L≤q≤UL \le q \le U, then

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

This is the "yes-instance" direction of the reduction: a divisor in the range yields a cheap period for item 1.

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

theorem divisor_in_range_cheap (M L U : ℕ) (hI : IsRangeDivisorInstance M L U) (q : ℕ)
    (hdvd : q ∣ M) (hL : L ≤ q) (hU : q ≤ U) :
    obj5 M L U q ≤ (L : ℝ) + 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, "Now, suppose there exists q in [L, U] dividing 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