Prove2Me

Lemma 1: (πˉ−π)⋅vk(π)≥w(πˉ)−w(π)≥0(\bar\pi - \pi)\cdot v_{k(\pi)} \ge w(\bar\pi) - w(\pi) \ge 0

Proved
HeldKarp.Ascent.lemma_1

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

lagrangian-relaxationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1subgradienttraveling-salesman

Let n≥3n \ge 3, let (cij)(c_{ij}) be symmetric real edge weights on KnK_n, and let ww be the 1-tree bound. Let π,πˉ∈Rn\pi, \bar\pi \in \mathbb R^n satisfy w(πˉ)≥w(π)w(\bar\pi) \ge w(\pi), and let k(π)k(\pi) be any minimum-weight 1-tree at the point π\pi, with degree-excess vector vk(π)v_{k(\pi)}. Then

(πˉ−π)⋅vk(π)  ≥  w(πˉ)−w(π)  ≥  0.(\bar\pi - \pi)\cdot v_{k(\pi)} \;\ge\; w(\bar\pi) - w(\pi) \;\ge\; 0.

Geometrically, the hyperplane through π\pi with normal vk(π)v_{k(\pi)} bounds a closed half-space containing every point πˉ\bar\pi at least as good as π\pi, in particular every maximizer of ww: vk(π)v_{k(\pi)} is a supergradient of the concave function ww at π\pi. This justifies stepping from π\pi along vk(π)v_{k(\pi)}.

Formalization Note The inner product is Euclidean, written as a coordinate sum. The minimum-weight 1-tree may be any of the tied minimizers.

Preamble
import Mathlib
import Definitions.Def_HeldKarp_Ascent_IsOneTree
import Definitions.Def_HeldKarp_Ascent_oneTreeBound
Formal statement
namespace HeldKarp.Ascent

/-- **Lemma 1** — Held & Karp, *The traveling-salesman problem and minimum spanning trees: Part II*,
Math. Programming 1 (1971), §2, p. 9 (PDF p. 4): "Let π̄ and π be such that w(π̄) ≥ w(π). Then
(π̄ − π) · v_{k(π)} ≥ w(π̄) − w(π) ≥ 0."

Here `G` plays the role of the 1-tree `k(π)`: any minimum-weight 1-tree at the point `π`.

Formalization Note: `·` is the Euclidean inner product, written as a sum over coordinates. The
choice of minimum-weight 1-tree is arbitrary among ties (every choice is covered). `3 ≤ n` is
implicit in the paper (1-trees exist only for `n ≥ 3`). -/
theorem lemma_1 {n : ℕ} [NeZero n] (hn : 3 ≤ n) (c : Sym2 (Fin n) → ℝ) (πbar π : Fin n → ℝ)
    (G : SimpleGraph (Fin n)) (hG : IsMinOneTree c π G)
    (hw : oneTreeBound c π ≤ oneTreeBound c πbar) :
    oneTreeBound c πbar - oneTreeBound c π ≤ ∑ i, (πbar i - π i) * degExcess G i ∧
      0 ≤ oneTreeBound c πbar - oneTreeBound c π := by sorry

end HeldKarp.Ascent
Source
Held & Karp, The traveling-salesman problem and minimum spanning trees: Part II, Math. Programming 1 (1971), DOI 10.1007/BF01584070, §2, p. 9 (PDF p. 4), Lemma 1
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

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

View graph