§2, p. 200 and §4, p. 203 — every table entry $S[D,I]$ of Algorithm A is the Steiner length of $\{I\} \cup D$

Proved

DreyfusWagner.Steiner.tableA_eq_steinerLength

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

algorithmsdynamic-programmingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1steiner-tree

Let $G = (N, A)$ be a finite connected undirected graph whose arcs have positive lengths, with $N$ linearly ordered. Let $S[D, I]$ be the table of Algorithm A built from the shortest-path lengths $D(i,j)$ of $G$ . Then for every nonempty node set $D$ and every node $I$ ,

S[D, I] = \operatorname{St}(\{I\} \cup D),

the length of the Steiner path $S(I, D)$ for the nodes $\{I\} \cup D$ .

This is the invariant that the table of Algorithm A maintains: each entry is the optimal value of the subproblem it stands for. With it, the value returned by the algorithm is the recurrence of §2 evaluated at $m = q$ and $D = C$ .

Formalization Note The statement is made for every nonempty $D$ , not only for the proper subsets of $C = Y - \{q\}$ that the algorithm stores; the table is defined for all node sets by the same recursion.

Preamble

import Mathlib
import Definitions.Def_DreyfusWagner_Steiner_SteinerProblem
import Definitions.Def_DreyfusWagner_Steiner_AlgorithmA

Formal statement

namespace DreyfusWagner.Steiner

/-- Dreyfus–Wagner 1971, §2, p. 200 and §4, p. 203: every entry `S[D, I]` of the table of
Algorithm A, built from the shortest-path lengths `D(i,j)`, is the length `S(I, D)` of the
Steiner path for the nodes `{I} ∪ D`. -/
theorem tableA_eq_steinerLength {V : Type*} [Fintype V] [LinearOrder V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (ℓ : Sym2 V → ℝ)
    (hpos : ∀ e ∈ G.edgeSet, 0 < ℓ e) (hconn : G.Connected)
    (D : Finset V) (hD : D.Nonempty) (I : V) :
    tableA (pathDist G ℓ) D I = steinerLength G ℓ (insert I D) := by sorry

end DreyfusWagner.Steiner

Source

Dreyfus, Wagner, The Steiner Problem in Graphs, Networks 1 (1971), p. 200, §2 ('Let S(m,D) denote the Steiner path for nodes {m ∪ D}'), and p. 203, §4, Algorithm A, lines (1)–(14); worked values p. 201

Read-back

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

Let $V$ be a finite, linearly ordered node type, $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$ . Take $d = D_{G,\ell}$ , the shortest node-repeat-free path length in $G$ . Let $S_d[D,I]$ be the table defined recursively on $|D|$ :

$S_d[\{t\}, I] = d(t,I)$ ;
$S_d[\emptyset, I] = \infty$ ;
for $|D| \ge 2$ :

S_d[D,I] = \min_{J \in V}\Big( d(I,J) + \min_{E} \big( S_d[E,J] + S_d[D \setminus E, J] \big) \Big),

where $E$ ranges over the subsets of $D$ that contain the least element of $D$ and differ from $D$ .

The statement says that for every nonempty node set $D$ and every node $I$ :

S_d[D,I] = \mathrm{St}(\{I\} \cup D).

Here $\mathrm{St}(X)$ is the minimum total length $\sum_{e \in S} \ell(e)$ over $S \subseteq A$ joining every two nodes of $X$ using only arcs of $S$ .

Degenerate cases. For $D = \{t\}$ the claim reads $D_{G,\ell}(t, I) = \mathrm{St}(\{I, t\})$ . For $I = t$ both sides are $0$ . The node $I$ may belong to $D$ . The empty $D$ is excluded by hypothesis; for it the table value $\infty$ is not claimed to equal anything.

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, p. 200 and §4, p. 203 — every table entry S[D,I]S[D,I]S[D,I] of Algorithm A is the Steiner length of {I}∪D\{I\} \cup D{I}∪D

§2, p. 200 and §4, p. 203 — every table entry $S[D,I]$ of Algorithm A is the Steiner length of $\{I\} \cup D$