§2, pp. 199–200 — the recurrence $S(m,D) = \min_k (d_{mk} + S_k(D))$

Proved

DreyfusWagner.Steiner.steinerLength_recurrence

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 $d_{mk} = D(m,k)$ be the shortest-path length from $m$ to $k$ , and let $\operatorname{St}(X)$ be the Steiner length of a node set $X$ . Let $D \subseteq N$ have at least two nodes and let $m \in N$ be any node. For $k \in N$ put

S_k(D) = \min\big\{\operatorname{St}(\{k\} \cup E) + \operatorname{St}(\{k\} \cup (D - E)) : \emptyset \ne E \subsetneq D\big\},

the best way of joining the two parts of a splitting of $D$ into nonempty disjoint sets $E$ , $F = D - E$ at the node $k$ . Then

\operatorname{St}(\{m\} \cup D) = \min_{k \in N}\big(d_{mk} + S_k(D)\big).

This is the dynamic-programming recurrence of Dreyfus and Wagner: the Steiner length for a terminal set of size $j+1$ is obtained from shortest-path lengths and Steiner lengths of terminal sets of size at most $j$ . The node $m$ may belong to $D$ .

Preamble

import Mathlib
import Definitions.Def_DreyfusWagner_Steiner_SteinerProblem

Formal statement

namespace DreyfusWagner.Steiner

/-- Dreyfus–Wagner 1971, §2, pp. 199–200: for a set `D` of at least two nodes and any node `m`,
the Steiner length of `{m} ∪ D` is `min_k (d_mk + S_k(D))`, where
`S_k(D)` is the minimum, over all splittings of `D` into two nonempty disjoint parts `E` and
`F = D − E`, of the Steiner lengths of `{k} ∪ E` and `{k} ∪ F` added together. -/
theorem steinerLength_recurrence {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (ℓ : Sym2 V → ℝ)
    (hpos : ∀ e ∈ G.edgeSet, 0 < ℓ e) (hconn : G.Connected)
    (D : Finset V) (hD : 2 ≤ D.card) (m : V) :
    steinerLength G ℓ (insert m D) =
      Finset.univ.inf fun k => pathDist G ℓ m k +
        (D.powerset.filter fun E => E.Nonempty ∧ E ≠ D).inf fun E =>
          steinerLength G ℓ (insert k E) + steinerLength G ℓ (insert k (D \ E)) := by sorry

end DreyfusWagner.Steiner

Source

Dreyfus, Wagner, The Steiner Problem in Graphs, Networks 1 (1971), pp. 199–200, §2, last paragraph of p. 199 continued on p. 200 (definition of S_k(D), d_mk and S(m,D))

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$ . Here $\mathrm{St}(X) \in \mathbb{R} \cup \{\infty\}$ is the minimum total length $\sum_{e \in S} \ell(e)$ over arc sets $S \subseteq A$ that join every two nodes of $X$ using only arcs of $S$ . $D_{G,\ell}(m,k)$ is the minimum total length of a path in $G$ from $m$ to $k$ that repeats no node. The statement says that for every node set $D$ with $|D| \ge 2$ and every node $m$ (which may or may not belong to $D$ ):

\mathrm{St}(\{m\} \cup D) = \min_{k \in V}\Big( D_{G,\ell}(m,k) + \min_{\substack{E \subseteq D \\ E \neq \emptyset,\ E \neq D}} \big( \mathrm{St}(\{k\} \cup E) + \mathrm{St}(\{k\} \cup (D \setminus E)) \big) \Big).

The inner minimum ranges over all nonempty proper subsets $E$ of $D$ , so each unordered split appears twice, once as $E$ and once as $D \setminus E$ . The outer minimum ranges over all nodes $k$ of $V$ , including $m$ and the nodes of $D$ .

Degenerate cases. Because $|D| \ge 2$ , the inner index set is nonempty. Because $G$ is connected, all quantities involved are finite. The case $m \in D$ is included, and there the left side is $\mathrm{St}(D)$ .

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

§2, pp. 199–200 — the recurrence S(m,D)=min⁡k(dmk+Sk(D))S(m,D) = \min_k (d_{mk} + S_k(D))S(m,D)=mink​(dmk​+Sk​(D))

§2, pp. 199–200 — the recurrence $S(m,D) = \min_k (d_{mk} + S_k(D))$