Prove2Me

Normalizing a k-Sum instance (corrected: n≥2n \ge 2)

Proved
SerialBatchTardy.ksum_normalize

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

batch-schedulingp2o-correctedp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1parameterized-complexityscheduling

Let n≥2n\ge2, c,k≥1c,k\ge1, N=nckN=n^{ck}, and let x1,…,xn∈{1,…,N}x_1,\dots,x_n\in\{1,\dots,N\} with target tt. Put xi′=xi+kNx_i'=x_i+kN and t′=t+k2Nt'=t+k^2N. Then

  1. some kk of the xix_i sum to tt iff some kk of the xi′x_i' sum to t′t';
  2. (k−1) xi′<t′(k-1)\,x_i'<t' for every ii;
  3. xi′∈{1,…,n3ck}x_i'\in\{1,\dots,n^{3ck}\} for every ii;
  4. if the xix_i are distinct, so are the xi′x_i'.

This puts every instance into the form assumed throughout the construction.

Differences from the source:

  • correction: no condition on n → n ≥ 2; reason: at n = 1 the printed bound x_i′ ≤ n^{3ck} fails: n = 1, x_1 = 1, c = k = 1 gives x_1′ = 2 > 1 = n^{3ck}
  • reading: k (the number of summands; k ≥ 1 implicit) → 1 ≤ k; reason: k-Sum asks for k integers; at k = 0 clause 2 fails for t = 0
  • generalization: "x_i ≤ n^{c′k} for c′ = 3c" and the normalized property → also positivity of the x_i′ and preservation of distinctness; reason: extra conclusions; the printed ones are among them
  • reading: c (a constant; c ≥ 1 implicit) → 1 ≤ c; reason: at c = 0 the range {1, …, n^{ck}} is {1}, which holds no set of n ≥ 2 integers; the Lean hypotheses do not ask for distinct entries, so c = 0 must be excluded explicitly
Preamble
import Definitions.Def_SerialBatchTardy_KSum
set_option autoImplicit false
Formal statement
namespace SerialBatchTardy

/-- **Normalizing a k-Sum instance.** Let `n ≥ 2`, `c, k ≥ 1`, `N = n^{ck}`, and let every entry of
`xs` lie in `{1, …, N}`. Adding `kN` to every entry and `k²N` to the target gives an equivalent
instance in which `k − 1` times every entry is below the target, every entry lies in
`{1, …, n^{3ck}}`, and distinct entries stay distinct. Hermelin, Mnich & Omlor, J. Scheduling 27
(2024), §4, pp.550–551 (PDF pp.6–7): "one can slightly modify the input by adding kn^{ck} to each
integer, and setting the target to t + k^2 n^{ck}. (Note that this way it holds that x_i ≤ n^{c′k}
for c′ = 3c …)". -/
theorem ksum_normalize (xs : List ℕ) (t c k : ℕ) (hc : 1 ≤ c) (hk : 1 ≤ k) (hn : 2 ≤ xs.length)
    (hxs : ∀ a ∈ xs, 1 ≤ a ∧ a ≤ xs.length ^ (c * k)) :
    (KSumSolvable xs t k ↔
        KSumSolvable (xs.map (· + k * xs.length ^ (c * k))) (t + k ^ 2 * xs.length ^ (c * k)) k) ∧
      (∀ a ∈ xs.map (· + k * xs.length ^ (c * k)), (k - 1) * a < t + k ^ 2 * xs.length ^ (c * k)) ∧
      (∀ a ∈ xs.map (· + k * xs.length ^ (c * k)), 1 ≤ a ∧ a ≤ xs.length ^ (3 * c * k)) ∧
      (xs.Nodup → (xs.map (· + k * xs.length ^ (c * k))).Nodup) := by sorry

end SerialBatchTardy
Source
Hermelin, Mnich & Omlor, Serial batching to minimize the weighted number of tardy jobs, J. Scheduling 27 (2024), §4, pp.550–551 (PDF pp.6–7), "one can slightly modify the input by adding kn^{ck} to each integer"
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph