Splitting off the Steiner vertices of an even multigraph

Disproved

MetricTSP.eliminate_steiner

by Shuze Chen · Aug 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatorial-optimizationconnectivitygraph-theory

Lovász splitting-off, metric form. Let $H$ be a multigraph (a symmetric multiplicity function with zero diagonal) on the cities with all degrees even, let $T$ be a set of terminals, and suppose every cut separating two terminals has at least $2N$ edges. Then all the non-terminal (Steiner) vertices can be split off: there is a multigraph $H'$ whose edges lie inside $T$ , with the same degrees on $T$ , still with every terminal-separating cut of size at least $2N$ , and, since splitting a path $u{-}v{-}w$ into the edge $u{-}w$ does not increase metric cost, with

\sum_{u,v} H'(u,v)\,c(u,v) \;\le\; \sum_{u,v} H(u,v)\,c(u,v).

The combinatorial core is Lovász's splitting-off lemma in its Eulerian form: at a vertex $v$ of even degree, some pair of edges at $v$ can be replaced by their shortcut while preserving all local edge-connectivities among the other vertices; the uniform-demand version needed here (preserve all terminal-separating cuts at level $2N$ ) follows from submodularity of the cut function by the standard analysis of dangerous sets. Iterating at one Steiner vertex reduces its degree to zero, and induction removes them all.

Combined with MetricTSP.even_set_matching on the resulting terminal-supported multigraph, this supplies the parity-correction matching (MetricTSP.parity_matching) of Wolsey's $\tfrac32$ analysis.

Preamble

import Mathlib
import Definitions.Def_MetricTSP_model

Formal statement

namespace MetricTSP

theorem eliminate_steiner (n : ℕ) (c : Fin n → Fin n → ℝ) (hc : IsMetricCost c)
    (T : Finset (Fin n)) (N : ℕ) (hN : 1 ≤ N)
    (H : Fin n → Fin n → ℕ) (hsym : ∀ u v, H u v = H v u) (hdiag : ∀ v, H v v = 0)
    (heven : ∀ v, Even (∑ u, H v u))
    (hcut : ∀ S : Finset (Fin n), (S ∩ T).Nonempty → (Sᶜ ∩ T).Nonempty →
      2 * N ≤ ∑ u ∈ S, ∑ v ∈ Sᶜ, H u v) :
    ∃ H' : Fin n → Fin n → ℕ, (∀ u v, H' u v = H' v u) ∧ (∀ v, H' v v = 0) ∧
      (∀ u v, H' u v ≠ 0 → u ∈ T ∧ v ∈ T) ∧
      (∀ v ∈ T, ∑ u, H' v u = ∑ u, H v u) ∧
      (∀ S : Finset (Fin n), (S ∩ T).Nonempty → (Sᶜ ∩ T).Nonempty →
        2 * N ≤ ∑ u ∈ S, ∑ v ∈ Sᶜ, H' u v) ∧
      ∑ u, ∑ v, (H' u v : ℝ) * c u v ≤ ∑ u, ∑ v, (H u v : ℝ) * c u v := by sorry

end MetricTSP

Source

L. Lovász, On some connectivity properties of Eulerian graphs, Acta Mathematica Academiae Scientiarum Hungaricae 28 (1976) 129-138, https://doi.org/10.1007/BF01902503 (the Eulerian splitting-off lemma); A. Frank, Connections in Combinatorial Optimization, Oxford University Press 2011, Chapter 8 (splitting-off techniques).

View graph