Prove2Me

Lemma 2: a step 0<t<2(w(πˉ)−w(π))/∥vk(π)∥20 < t < 2(w(\bar\pi)-w(\pi))/\|v_{k(\pi)}\|^2 moves strictly closer to πˉ\bar\pi

Proved
HeldKarp.Ascent.lemma_2

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

p2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1step-sizesubgradienttraveling-salesman

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

0<t<2 (w(πˉ)−w(π))∥vk(π)∥2,0 < t < \frac{2\,(w(\bar\pi) - w(\pi))}{\|v_{k(\pi)}\|^2},

then

∥πˉ−(π+t vk(π))∥<∥πˉ−π∥.\|\bar\pi - (\pi + t\,v_{k(\pi)})\| < \|\bar\pi - \pi\|.

So a step of the iteration (3) with a suitably small positive step size moves strictly closer to every point with a larger value of ww, in particular to every maximizer of ww. This is the rationale for the choice of step sizes in the ascent method.

Formalization Note Both sides are compared through squared Euclidean norms, written as sums of squares (equivalent, since the square root is strictly increasing). If vk(π)=0v_{k(\pi)} = 0 the right-hand bound is 00 in Lean (division by zero), so the hypothesis cannot hold; in the paper vk(π)=0v_{k(\pi)} = 0 only at a maximizer of ww, where it cannot hold either.

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

/-- **Lemma 2** — Held & Karp, *The traveling-salesman problem and minimum spanning trees: Part II*,
Math. Programming 1 (1971), §2, p. 9 (PDF p. 4): "If 0 < t < 2(w(π̄) − w(π)) / ‖v_{k(π)}‖² then
‖π̄ − (π + t v_{k(π)})‖ < ‖π̄ − π‖", where "‖ ‖ denotes Euclidean norm" (footnote, p. 9).

Here `G` is any minimum-weight 1-tree at the point `π` (the paper's `k(π)`).

Formalization Note: both sides are compared through squared Euclidean norms, written as sums of
squares (the square root is strictly monotone, so this is equivalent). Mathlib's `‖·‖` on
`Fin n → ℝ` is the sup norm and is not used. If `‖v_{k(π)}‖² = 0`, Lean's division gives
`2(w(π̄) − w(π)) / 0 = 0` and the hypothesis `0 < t < 0` is unsatisfiable; in the paper
`v_{k(π)} = 0` only when `π` maximizes `w`, where the hypothesis cannot hold either. `3 ≤ n`
is implicit in the paper. -/
theorem lemma_2 {n : ℕ} [NeZero n] (hn : 3 ≤ n) (c : Sym2 (Fin n) → ℝ) (πbar π : Fin n → ℝ)
    (G : SimpleGraph (Fin n)) (hG : IsMinOneTree c π G) (t : ℝ) (ht : 0 < t)
    (ht' : t < 2 * (oneTreeBound c πbar - oneTreeBound c π) / ∑ i, (degExcess G i) ^ 2) :
    ∑ i, (πbar i - (π i + t * degExcess G i)) ^ 2 < ∑ i, (πbar i - π i) ^ 2 := 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 2 and its footnote (Euclidean norm)
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