Written on the Wall II - Conjecture 31

The WOWII page records this as Chung's theorem: proved in F. R. K. Chung, The average distance and the independence number, J. Graph Theory 12 (1988), 229-235. We state it here as a theorem; the formal proof is left as sorry pending a Lean port of Chung's argument.

Here $\mathrm{path}(G)$ is the floor of the average distance over ordered pairs of distinct vertices (definition path in FormalConjecturesForMathlib), and $\mathrm{rad}(G)$ is the graph radius.

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

theorem WrittenOnTheWallII.GraphConjecture31.conjecture31 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : 2 * ↑G.radius.toNat - 1 ≤ ↑G.path

WOWII Conjecture 31 (Chung 1988):

For every simple connected graph $G$, $\mathrm{path}(G) \ge 2 \cdot \mathrm{rad}(G) - 1$, where $\mathrm{path}(G)$ is the floor of the average distance and $\mathrm{rad}(G)$ is the graph radius.