Prove2Me

Eq. (2): C∗≥w(π)C^* \ge w(\pi) — every 1-tree bound is below the optimum tour weight

Proved
HeldKarp.Ascent.eq_2

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

lagrangian-relaxationlower-boundp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1traveling-salesman

Let n≥3n \ge 3, let (cij)(c_{ij}) be arbitrary symmetric real edge weights on KnK_n, and let w(π)=min⁡k[ck+π⋅vk]w(\pi) = \min_k [c_k + \pi\cdot v_k] be the 1-tree bound. Then for every real nn-vector π\pi and every tour HH of KnK_n,

w(π)≤c(H).w(\pi) \le c(H).

Equivalently, with C∗C^* the weight of a minimum tour,

C∗≥w(π)for every π∈Rn.C^* \ge w(\pi) \quad \text{for every } \pi \in \mathbb R^n.

This is the family of lower bounds on which the whole method rests: the best such bound is max⁡πw(π)\max_\pi w(\pi), and in particular ww is bounded above, so its maximum exists.

Formalization Note C∗C^* is not named; the statement quantifies over every tour instead, which is equivalent. No metric assumption is made on the weights. The hypothesis n≥3n \ge 3 is implicit in the paper (for n≤2n \le 2 there are no tours and no 1-trees).

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

/-- **Eq. (2)** (with Eq. (1)) — Held & Karp, *The traveling-salesman problem and minimum spanning
trees: Part II*, Math. Programming 1 (1971), §1, p. 8 (PDF p. 3): "C* ≥ w(π)", where C* is the
weight of a minimum tour with respect to the weights `c_ij` and
`w(π) = min_k [c_k + π · v_k]` is the minimum over 1-trees.

For `n ≥ 3`, arbitrary real edge weights `c`, every real `n`-vector `π` and every tour `H`,
`w(π) ≤ weight c H`. Since this holds for every tour, it is `C* ≥ w(π)`.

Formalization Note: `C*` is not named; quantifying over every tour is equivalent (for `n ≥ 3`
tours exist, finitely many). `3 ≤ n` is implicit in the paper: for `n ≤ 2` there is neither a
tour nor a 1-tree. Weights are arbitrary reals; no metric assumption. -/
theorem eq_2 {n : ℕ} [NeZero n] (hn : 3 ≤ n) (c : Sym2 (Fin n) → ℝ) (π : Fin n → ℝ)
    (H : SimpleGraph (Fin n)) (hH : IsTour H) :
    oneTreeBound c π ≤ weight c H := 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, §1, p. 8 (PDF p. 3), Eq. (1) and Eq. (2)
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