Written on the Wall II - Conjecture 33

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

theorem WrittenOnTheWallII.GraphConjecture33.conjecture33 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : False ↔ ∀ (G : SimpleGraph α) [inst : DecidableRel G.Adj], G.Connected → have M := {v : α | G.degree v = G.maxDegree}; ⌈2 * G.distavg M⌉ ≤ ↑G.path

WOWII Conjecture 33

For a simple connected graph G, path(G) ≥ ⌈2 · dist_avg(M, V)⌉, where path(G) is the floor of the average distance of G, M is the set of maximum-degree vertices, and dist_avg(M, V) is the average distance from all vertices to M.