Optimal Decomposition Theorem — a Steiner tree splits at a node $p$ into Steiner trees for $\{p,q\}$ , $\{p\} \cup D$ , $\{p\} \cup (Y - D - \{q\})$

Proved

DreyfusWagner.Steiner.optimal_decomposition

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

dynamic-programminggraph-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1steiner-tree

Let $G = (N, A)$ be a finite connected undirected graph whose arcs have positive lengths. Let $Y \subseteq N$ contain at least three nodes, let $S$ be a Steiner tree connecting $Y$ , and let $q \in Y$ . Then there exist a node $p \in N$ and a set $D \subseteq Y$ such that

$D$ is a nonempty proper subset of $Y - \{q\}$ ;
$S = S_1 \cup S_2 \cup S_3$ with $S_1, S_2, S_3$ pairwise disjoint;
$S_1$ is a Steiner path connecting $\{p, q\}$ , $S_2$ is a Steiner path connecting $\{p\} \cup D$ , and $S_3$ is a Steiner path connecting $\{p\} \cup (Y - D - \{q\})$ .

The node $p$ need not belong to $Y$ , may equal $q$ (then $S_1 = \emptyset$ ), and $S_3$ may be empty. In particular

|S| = D(p, q) + \operatorname{St}(\{p\} \cup D) + \operatorname{St}(\{p\} \cup (Y - D - \{q\})).

This is the structural fact behind the Dreyfus–Wagner dynamic program: an optimal tree for $Y$ is assembled from a shortest path and two optimal trees for strictly smaller terminal sets meeting at a junction node.

Formalization Note " $S$ consists of 3 disjoint subsets" is stated as $S = S_1 \cup S_2 \cup S_3$ with the three sets pairwise disjoint; no $S_i$ is required to be nonempty and $p$ is not required to lie outside $Y$ , as in the paper's Figures 5 and 6. The hypothesis $\|Y\| \ge 3$ is the paper's own (Appendix A, p. 205).

Preamble

import Mathlib
import Definitions.Def_DreyfusWagner_Steiner_SteinerProblem

Formal statement

namespace DreyfusWagner.Steiner

/-- Dreyfus–Wagner 1971, Appendix A, Optimal Decomposition Theorem, p. 206 (also §1, p. 197). -/
theorem optimal_decomposition {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (ℓ : Sym2 V → ℝ)
    (hpos : ∀ e ∈ G.edgeSet, 0 < ℓ e) (hconn : G.Connected)
    (Y : Finset V) (S : Finset (Sym2 V)) (hS : IsSteinerTree G ℓ Y S)
    (q : V) (hq : q ∈ Y) (hY : 3 ≤ Y.card) :
    ∃ (p : V) (D : Finset V) (S₁ S₂ S₃ : Finset (Sym2 V)),
      D ⊆ Y.erase q ∧ D ≠ Y.erase q ∧ D.Nonempty ∧
      S = S₁ ∪ S₂ ∪ S₃ ∧ Disjoint S₁ S₂ ∧ Disjoint S₁ S₃ ∧ Disjoint S₂ S₃ ∧
      IsSteinerTree G ℓ {p, q} S₁ ∧
      IsSteinerTree G ℓ (insert p D) S₂ ∧
      IsSteinerTree G ℓ (insert p (Y.erase q \ D)) S₃ := by sorry

end DreyfusWagner.Steiner

Source

Dreyfus, Wagner, The Steiner Problem in Graphs, Networks 1 (1971), p. 206, Appendix A, Optimal Decomposition Theorem (also stated in §1, p. 197)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $V$ be a finite node type with decidable equality, $G$ a connected simple graph on $V$ with edge set $A$ , and $\ell$ a length function with $\ell(e) > 0$ for every $e \in A$ . Let $Y$ be a finite node set with $|Y| \ge 3$ and $S$ a Steiner tree for $Y$ . That is, $S \subseteq A$ , $S$ joins every two nodes of $Y$ using its own arcs, and $S$ has minimum total length among all such subsets of $A$ . Let $q \in Y$ . The statement asserts that there exist:

a node $p$ ;
a node set $D$ with

\emptyset \neq D \subsetneq Y \setminus \{q\};

arc sets $S_1, S_2, S_3$ $S_{1}, S_{2}, S_{3}$ that are pairwise disjoint, with $S = S_1 \cup S_2 \cup S_3$ $S = S_{1} \cup S_{2} \cup S_{3}$ , such that
- $S_1$ is a Steiner tree for $\{p, q\}$ ;
- $S_2$ is a Steiner tree for $\{p\} \cup D$ ;
- $S_3$ is a Steiner tree for $\{p\} \cup \big((Y \setminus \{q\}) \setminus D\big)$ .

All three Steiner trees are taken in the same $(G,\ell)$ . Nothing constrains $p$ : it may equal $q$ , lie in $D$ or its complement, or be any other node. None of $S_1, S_2, S_3$ is required to be nonempty.

Degenerate cases. The conditions on $D$ force both $D$ and $(Y \setminus \{q\}) \setminus D$ to be nonempty. This is possible because $|Y \setminus \{q\}| \ge 2$ . If $p = q$ , then $S_1$ , being a Steiner tree for the singleton $\{q\}$ under positive lengths, must be $\emptyset$ .

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

Optimal Decomposition Theorem — a Steiner tree splits at a node ppp into Steiner trees for {p,q}\{p,q\}{p,q}, {p}∪D\{p\} \cup D{p}∪D, {p}∪(Y−D−{q})\{p\} \cup (Y - D - \{q\}){p}∪(Y−D−{q})

Optimal Decomposition Theorem — a Steiner tree splits at a node $p$ into Steiner trees for $\{p,q\}$ , $\{p\} \cup D$ , $\{p\} \cup (Y - D - \{q\})$