Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Steiner diameter and anchored radius of trees

Abstract

Terminal-cut averaging proves Zhang–Tian Conjecture 5.1 for every finite tree.

Definition 1.1 (Steiner distance).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.steinerDist (✓ std3).

Citation. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Page 2: “The Steiner distance d_G(S) among the vertices of S (or simply the distance of S) is defined as the minimum size among all connected subgraphs whose vertex sets contain S.” The size of a graph is its number of edges. The natural infimum ranges over actual connected subgraphs, recording both vertices and edges. The displayed set coercion views the finite terminal set as a set of vertices.

Definition 1.2 (Steiner vertex eccentricity).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.steinerEcc (✓ std3).

Citation. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Page 2: “The Steiner k-eccentricity ε_k(v; G) of a vertex v in G is defined by max{d_G(S) : v ∈ S ⊆ V(G), |S| = k}, where k ≥ 2.” Finite subsets of the vertex type express S ⊆ V(G); their cardinality is the number of terminals.

Definition 1.3 (Steiner diameter).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.steinerDiam (✓ std3).

Citation. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Page 2: “The Steiner k-radius of G is Sr_k(G) = min{ε_k(v) : v ∈ V(G)}, and the Steiner k-diameter of G is Sd_k(G) = max{ε_k(v) : v ∈ V(G)}.” steinerDiam is the natural supremum of the vertex eccentricities; the radius mentioned in this source sentence is not a separate definition here.

Definition 1.4 (Anchored Steiner eccentricity).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.steinerSetEcc (✓ std3).

Citation. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Page 2: “The Steiner (k, k′)-eccentricity ε_{k,k′}(S′; G) of a k′-subset S′ in G is defined as the maximum Steiner distance over k-subsets of V(G) that include S′, that is, ε_{k,k′}(S′; G) = max{d_G(S) : S′ ⊆ S ⊆ V(G), |S| = k}, where k ≥ 2 and k ≥ k′ ≥ 1.” The anchor cardinality is supplied by the theorem hypotheses, while steinerSetEcc takes the anchor set itself.

Definition 1.5 (Anchored Steiner radius).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.steinerRadius (✓ std3).

Citation. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Page 2: “The Steiner (k, k′)-radius of G is Sr_{k,k′}(G) = min{ε_{k,k′}(S′; G) : S′ ⊆ V(G), |S′| = k′}, where k′ ≥ 1.” steinerRadius takes the natural infimum over every anchor set of the specified cardinality.

Definition 1.6 (Zhang–Tian Conjecture 5.1).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.claim (✓ std3).

Citation. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Conjecture 5.1, page 14: “Let n, k, k′ be integers with n ≥ k ≥ 3 and k > k′ ≥ 1 and let T be a tree with order n. Then Sd_k(T) ≤ k/(k − k′) Sr_{k,k′}(T) − k′(k′ − 1)/(k − k′).” Here n is Fintype.card V and r denotes k′. Natural-valued distances, k and r are cast into ℚ before the displayed divisions and subtractions. Finiteness and decidable equality appear as anonymous instance arguments; IsTree means connected and acyclic.

Definition 1.7 (Terminal separation after edge deletion).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.Separates (✓ std3).

Source. Repository-derived.

Acknowledgement. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Separates T S e means that deleting e disconnects two terminals of S. No choice of an orientation or a component is part of this predicate.

Definition 1.8 (Separating edges).

Formalization. D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.cutEdges (✓ std3).

Source. Repository-derived.

Acknowledgement. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

cutEdges filters the graph’s finite edge set by terminal separation. Each undirected edge is counted once as an element of Sym2 V.

Theorem 1.9 (Distance counts separating edges).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.steinerDist_cut (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

For a finite tree and a nonempty terminal set, the defining minimum equals the number of separating edges. The intersection of all connected terminal-containing subgraphs is connected because the tree has a unique path between any two vertices. An edge in that intersection separates terminals: otherwise the deletion component containing a chosen terminal contains all terminals and excludes the edge.

Theorem 1.10 (A bound for every pair of terminal sets).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.pointwise_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

For every k-set A and r-set B in a finite tree, with 1 ≤ r < k and enough vertices, (k−r) steinerDist T A + r steinerDist T B ≤ k steinerSetEcc T k B. Every edge of the B-hull persists when B is enlarged. For each edge of the A-hull outside it, select an A-terminal separated from a B-terminal. That edge persists whenever the selected terminal belongs to a sampled (k−r)-subset of A. Double counting these samples yields the inequality. The sets may overlap, and A need not maximize the distance.

Theorem 1.11 (The conjecture holds for all finite trees).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.result (✓ std3). ∎

Resolves. Problems/zhang-tian-2025-steiner-diameter-radius-trees (proved) by D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.result.

Source. Repository-derived.

Acknowledgement. Qingnan Zhang; Yingzhi Tian (2025). On the Steiner k-diameter and Steiner (k, k′)-radius of trees. DOI: 10.48550/arXiv.2511.22492. URL: https://arxiv.org/abs/2511.22492v1.

Commentary.

Choose terminal sets attaining the Steiner diameter and the anchored radius. The pointwise inequality retains the entire anchor hull, whose edge count is at least r−1. This supplies the additive r(r−1) correction. Division by the positive rational k−r gives the displayed inequality.

References