Prove2Me

Proof of Lemma 2, p. 12 — if gcd(q, M) = 1 or gcd(q, M) = M, then M/gcd(q, M) + q ≥ M

Proved
JRPHard.Periodic.trivial_gcd_value

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

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

Let MM be a natural number and qq a positive integer with gcd⁡(q,M)=1\gcd(q,M) = 1 or gcd⁡(q,M)=M\gcd(q,M) = M. Then the objective of problem (4) at qq satisfies

Mgcd⁡(q,M)+q≥M.\frac{M}{\gcd(q,M)} + q \ge M.

A period q1q_1 that shares no non-trivial factor with MM (or is a multiple of MM) therefore costs at least MM in problem (4), more than the value 2M/32M/3 attained at a non-trivial divisor; so every optimal q1q_1 has 1<gcd⁡(q1,M)<M1 < \gcd(q_1,M) < M.

Formalization Note The paper states this for the odd composite MM of Lemma 2; it holds for every natural number MM, which is how it is stated.

Preamble
import Mathlib
import Definitions.Def_JRPHard_Periodic_Setting
Formal statement
namespace JRPHard.Periodic

theorem trivial_gcd_value (M q : ℕ) (hq : 0 < q)
    (hg : Nat.gcd q M = 1 ∨ Nat.gcd q M = M) :
    (M : ℝ) ≤ obj4 M q := 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. 12, §2.2, proof of Lemma 2, first sentence of p. 12
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