Proof of Lemma 2, p. 11 — an odd composite M has a divisor p with 3 ≤ p ≤ M/3

Proved

JRPHard.Periodic.exists_small_divisor

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

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

Let $M$ be an odd composite number (odd, greater than $1$ , and not prime). Then $M$ has a divisor $p$ with

3 \le p \le \frac{M}{3}.

Such a $p$ is a non-trivial divisor of $M$ ; it supplies a feasible point of problem (4) whose value is well below $M$ .

Formalization Note The paper prints " $3 \le p < M/3$ ", which is false for $M = 9$ , whose only non-trivial divisor is $3 = M/3$ . The statement here uses $p \le M/3$ , written as $3p \le M$ ; this suffices for the next step of the proof. Non-triviality ( $1 < p < M$ ) follows from $3 \le p$ and $3p \le M$ .

Preamble

import Mathlib
import Definitions.Def_JRPHard_Periodic_Setting

Formal statement

namespace JRPHard.Periodic

theorem exists_small_divisor (M : ℕ) (hodd : Odd M) (h1 : 1 < M) (hcomp : ¬ M.Prime) :
    ∃ p : ℕ, p ∣ M ∧ 3 ≤ p ∧ 3 * p ≤ M := 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", second sentence (printed "< M/3", corrected to "≤ M/3")

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