Proof of Lemma 3, p. 14 — a period q with gcd(q, M) ≠ q has objective at least 2√(2LU) > L + U

Proved

JRPHard.RangeDiv.nondivisor_lower_bound

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

am-gmgcdp2o-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 $\gcd(q, M) \ne q$ (that is, $q$ does not divide $M$ ). Then the objective of problem (5) at $q$ satisfies

\frac{LU}{\gcd(q,M)} + q \ \ge\ 2\sqrt{2LU} \qquad\text{and}\qquad \frac{LU}{\gcd(q,M)} + q \ >\ L + U.

So a period that does not divide $M$ never reaches the level $L + U$ ; this is where RangeDivisor's condition $L + U < 2\sqrt{2LU}$ is used.

Preamble

import Mathlib
import Definitions.Def_JRPHard_RangeDiv_Setting

Formal statement

namespace JRPHard.RangeDiv

theorem nondivisor_lower_bound (M L U : ℕ) (hI : IsRangeDivisorInstance M L U) (q : ℕ)
    (hq : 0 < q) (hne : Nat.gcd q M ≠ q) :
    2 * Real.sqrt (2 * (L : ℝ) * U) ≤ obj5 M L U q ∧ (L : ℝ) + U < obj5 M L U 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, display "min_{q>0} 2K₀/q + q ≥ 2√(2K₀) = 2√(2LU) > L + U"

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