Proof of Lemma 1, p. 9 — with q₂ = M the instance reduces to problem (2): JRP(q₁, M) = EOQ_{K₂,H₂}(M) + JRP^red(q₁)

Proved

JRPHard.Aperiodic.reduction_to_2

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

eoqjoint-replenishmentp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ be an odd composite number and let $\mathrm{JRP}$ be the aperiodic objective of the instance of Lemma 1. For every positive integer $q_1$ ,

\mathrm{JRP}(q_1, M) = \mathrm{EOQ}_{K_2,H_2}(M) + \mathrm{JRP}^{\mathrm{red}}(q_1), \qquad \mathrm{JRP}^{\mathrm{red}}(q_1) = M(M-1)\left(\frac{1}{q_1} - \frac{1}{\mathrm{lcm}(q_1,M)}\right) + 4q_1 .

Once item 2 is fixed at $q_2 = M$ , minimizing the two-item objective is therefore the same as minimizing the one-variable objective of problem (2) over $q_1 \in \mathbb Z^+$ .

Preamble

import Mathlib
import Definitions.Def_JRPHard_Aperiodic_Setting

Formal statement

namespace JRPHard.Aperiodic

theorem reduction_to_2 (M : ℕ) (hodd : Odd M) (h1 : 1 < M) (hcomp : ¬ M.Prime)
    (q : ℕ) (hq : 0 < q) :
    lemma1Cost M q M = eoq2 M M + jrpRed M q := by sorry

end JRPHard.Aperiodic

Source

Schulz and Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, p. 9, proof of Lemma 1, "Optimal replenishment cycle for item 1", first sentence; problem (2), p. 8

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