slug: zhang-tian-2025-steiner-diameter-radius-trees
bibkey: zhangtian2025steinerradius
doi: 10.48550/arXiv.2511.22492
triage: theorem
motivation_gids:
  - D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.result

Zhang–Tian Conjecture 5.1: Steiner diameter and anchored radius of trees

Problem

Qingnan Zhang and Yingzhi Tian, On the Steiner k-diameter and Steiner (k, k′)-radius of trees, arXiv:2511.22492v1, p. 14, Conjecture 5.1, states:

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 $d_T(S)$ is the minimum edge count among connected subgraphs containing $S$; ${\epsilon }_k(v;T)$ maximizes $d_T(S)$ over $k$-sets containing $v$; $S{d}_k(T)$ maximizes these vertex eccentricities. For an anchor set $B$, ${\epsilon }_{k,r}(B;T)$ maximizes $d_T(S)$ over $k$-sets containing $B$, and $S{r}_{k,r}(T)$ minimizes this quantity over $r$-sets $B$.

Statement echo

Motivation

The settling declaration is D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.result. It proves the conjecture for all finite trees and all source parameters. The public theorem pointwise_bound gives the stronger estimate

$$(k-r)d_T(A)+r{d}_T(B)\le k{\epsilon }_{k,r}(B;T)$$

for every $k$-set $A$ and $r$-set $B$, provided $1\le r<k\le n$.

Gap

This is a tier-1 externally named conjecture, preregistered in issue #20671. That issue records the source and literal Lean conventions, a proof route, and a bounded literature screen. The reported arXiv, MathDB 371714, title/identifier/author/topic and formal-conjectures searches found no settlement in their searched scope. The listed later Tian papers contain no Steiner material. Full texts by X. Li (Axioms 2025), Reiswig (DAM 2024), Li–Zeng–Pan–Li (DAM 2024), and Zeng–Li (DAM 2026) remain unread in that screen. Literature completeness is ASSUMED-UNVERIFIED.

Route

steinerDist_cut identifies the defining distance with the number of edges whose deletion separates two terminals. The private connected hull supplies the minimum connected subgraph. Its cut characterization constructs the component containing a chosen terminal after an edge is deleted.

For $H=H(A)$, $J=H(B)$ and $s=k-r$, every edge of $J$ survives in every $H(B\cup X)$ for an $s$-subset $X$ of $A$. For an edge of $H\setminus J$, a terminal across that cut forces survival when it is selected. The fraction of $s$-subsets containing any fixed terminal is $s/k$. Double counting gives

$${\epsilon }_{k,r}(B;T)\ge |E(J)|+\frac{k-r}{k}(|E(H)|-|E(H)\cap E(J)|)\ge \frac{k-r}{k}{d}_T(A)+\frac{r}{k}{d}_T(B).$$

This display explains the estimate proved by pointwise_bound; the proof uses natural-valued binomial counts before rational division. The private steinerDist_lower proves $|B|-1\le d_T(B)$. The private diameter_attained and radius_attained supply extremizers; conjecture_nat and result give the conjectured inequality.

Falsifier

The formal target has every source hypothesis and the full rational conclusion. A source-level counterexample would be a finite tree with $1\le r<k\le n$, $k\ge 3$, and $(k-r)S{d}_k(T)+r(r-1)>kS{r}_{k,r}(T)$. The public result rules out such a counterexample in the stated model. The extension to arbitrary connected graphs is open here.

Evidence

The mathematical module is D5/S3/Combinatorics/Graph/Eccentric/ZhangTianSteinerTreeRadius.lean, with its corresponding Blueprint Scribe and emitted Markdown. It imports only pinned Mathlib. The module’s admission basis is open-problem-resolution (#20671; Proved); its utility is none. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

Independent computation

Published checker and output. Command: python3 docs/reports/zhang-tian-2025-steiner-diameter-radius-trees/check.py from that experiments-repository revision; exit 0. Script SHA-256: c9f56ed496fd34dd7317501871c6fc798c5726c8d97d1c55d3690abbe54b711f. The computation reproduces the six equality examples listed below and tests all 985 nonisomorphic trees with $3\le n\le 12$, all $3\le k\le n$ and $1\le r<k$: 55,778 parameter instances, zero failures of Conjecture 5.1 or Theorem 3.4, and 16,847,366 pointwise checks with zero failures. These are finite computations, separate from the universal kernel proof.

Escape audit

The escape audit is unfinished for steinerDist_cut, pointwise_bound and result; see issue #20778. The attempted dependent-family readouts lack compiled rejected-realization, variation, sensitivity, observational-dependence and source-binding evidence. No successful Reg mirror is retained and no registration is asserted declared_validated.

Declaration judgement

Triage

What the settlement shows

ASSUMED-UNVERIFIED

Literature completeness and publication priority are not established. The unread full texts named in Gap remain outside the literature screen. The experiments establish only their finite tested scope. Four-slot escape-registration evidence is incomplete as disclosed in issue #20778; it is distinct from the kernel-checked mathematical result.