Proof of Theorem 1, p. 124 — Problems 5 and 6 are equivalent

Proved

MurtyKabadi.Reduction.problems5_6_equiv

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1quadratic-programmingsubset-sum

Let $d_0; d_1, \dots, d_n$ be positive integers and let $\delta$ be an integer with

\delta > 4\Big(d_0 \sum_{j=1}^n d_j\Big)^2 n^3.

With $f_1$ and the polytope $P = \{(y,s) : y, s \ge 0,\ \sum_j (y_j + s_j) = n\}$ as defined for the reduction, the subset sum instance is solvable if and only if there is $(y, s) \in P$ with

f_1(y, s) \le 0.

This is the first link of the chain from subset sum (Problem 5) to Problem 4: $f_1$ is a sum of nonnegative terms on $P$ that vanishes exactly at the $0$ – $1$ solutions $y$ with $s = e - y$ .

Formalization Note Only $\delta \ge 0$ is used for this step; the hypotheses are those of the whole reduction.

Preamble

import Mathlib
import Definitions.Def_MurtyKabadi_Reduction_SubsetSum
import Definitions.Def_MurtyKabadi_Reduction_Construction

Formal statement

namespace MurtyKabadi.Reduction

theorem problems5_6_equiv {n : ℕ} (d : Fin n → ℕ) (d0 δ : ℕ)
    (hd : ∀ j, 0 < d j) (hd0 : 0 < d0)
    (hδ : 4 * (d0 * ∑ j, d j) ^ 2 * n ^ 3 < δ) :
    SubsetSumSolvable d d0 ↔ ∃ p ∈ P n, f1 d d0 δ p.1 p.2 ≤ 0 := by sorry

end MurtyKabadi.Reduction

Source

Murty and Kabadi, Some NP-complete problems in quadratic and nonlinear programming, Math. Programming 39 (1987), p. 124, proof of Theorem 1, first paragraph (Problems 5 and 6 are equivalent)

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph