Theorem 1 — the branch of a Steiner tree through $C \subseteq B(x)$ is a Steiner tree for $Y_C(x) \cup \{x\}$

Proved

DreyfusWagner.Steiner.theorem1_branch_isSteinerTree

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

graph-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$ , and let $S$ be a Steiner tree connecting $Y$ . Let $x$ be a node touching an arc of $S$ , let $B(x)$ be the set of arcs of $S$ touching $x$ , and let $C \subseteq B(x)$ . Let $Y_C(x)$ be the set of nodes of $Y$ reachable from $x$ along paths in $S$ whose first arc lies in $C$ , and put $Y_C = Y_C(x) \cup \{x\}$ . Then

\text{the arcs of } S \text{ involved in connecting the nodes of } Y_C \text{ form a Steiner tree connecting } Y_C.

In words: cutting a Steiner tree at any of its nodes and keeping the branches through a chosen set of arcs at that node gives an optimal Steiner tree for the terminals on those branches together with the cut node. Dreyfus and Wagner use this to view Steiner trees as collections of optimal subtrees joined at their roots, which is the first half of the proof of the Optimal Decomposition Theorem.

Formalization Note "The arcs of $S$ involved in connecting the nodes of $Y_C$ " is read as the set of arcs of $S$ lying on some path in $S$ from $x$ to a node of $Y_C(x)$ (see the definition of the branch). The paper writes $C \subset B(x)$ for a not necessarily proper subset; the statement uses $C \subseteq B(x)$ , so $C = \emptyset$ (branch empty, $Y_C = \{x\}$ ) and $C = B(x)$ are included.

Preamble

import Mathlib
import Definitions.Def_DreyfusWagner_Steiner_SteinerProblem
import Definitions.Def_DreyfusWagner_Steiner_Branch

Formal statement

namespace DreyfusWagner.Steiner

/-- Dreyfus–Wagner 1971, Appendix A, Theorem 1, p. 206: for a Steiner tree `S` connecting `Y`, a
node `x` touching an arc of `S` and a set `C ⊆ B(x)` of arcs of `S` at `x`, the arcs of `S`
involved in connecting `Y_C = Y_C(x) ∪ {x}` form a Steiner tree connecting `Y_C`. -/
theorem theorem1_branch_isSteinerTree {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)
    (x : V) (hx : ∃ e ∈ S, x ∈ e) (C : Finset (Sym2 V)) (hC : C ⊆ touchingArcs S x) :
    IsSteinerTree G ℓ (insert x (reachVia Y S x C)) (branchArcs Y S x C) := by sorry

end DreyfusWagner.Steiner

Source

Dreyfus, Wagner, The Steiner Problem in Graphs, Networks 1 (1971), p. 206, Appendix A, Theorem 1 (definitions on p. 205)

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$ . The hypotheses are:

$Y$ is a finite node set and $S$ is a Steiner tree for $Y$ . That is, $S \subseteq A$ , $S$ joins every two nodes of $Y$ in the graph $H_S$ formed by its arcs, and $S$ has minimum total length $\sum_{e \in S} \ell(e)$ among all subsets of $A$ with that property.
$x$ is a node that lies on at least one arc of $S$ . It need not belong to $Y$ .
$C$ is a set of arcs with $C \subseteq B_S(x) = \{e \in S : x \in e\}$ .

Define two sets:

$Y_C(x)$ is the set of $y \in Y$ reachable from $x$ by a path in $H_S$ that repeats no node, has at least one arc, and has its first arc in $C$ .
$\mathrm{Br}$ is the set of arcs of $S$ that lie on some node-repeat-free path in $H_S$ from $x$ to some $y \in Y_C(x)$ . That path need not begin with an arc of $C$ .

The conclusion is that $\mathrm{Br}$ is a Steiner tree for the node set $\{x\} \cup Y_C(x)$ in $(G,\ell)$ . That is:

$\mathrm{Br} \subseteq A$ ;
$\mathrm{Br}$ connects $\{x\} \cup Y_C(x)$ ;
$\mathrm{Br}$ has total length $\le$ that of every subset of $A$ connecting $\{x\} \cup Y_C(x)$ .

Degenerate cases. If $C = \emptyset$ , then $Y_C(x) = \emptyset$ and $\mathrm{Br} = \emptyset$ . The claim then says that $\emptyset$ is a Steiner tree for $\{x\}$ , which, since lengths on $A$ are positive, holds exactly as the minimum-length set. If $Y$ is empty or a singleton, positive lengths force $S = \emptyset$ . The hypothesis that $x$ touches an arc of $S$ is then unsatisfiable, and the statement is vacuous.

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

Theorem 1 — the branch of a Steiner tree through C⊆B(x)C \subseteq B(x)C⊆B(x) is a Steiner tree for YC(x)∪{x}Y_C(x) \cup \{x\}YC​(x)∪{x}

Theorem 1 — the branch of a Steiner tree through $C \subseteq B(x)$ is a Steiner tree for $Y_C(x) \cup \{x\}$