Written on the Wall II - Conjecture 33

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

theorem WrittenOnTheWallII.GraphConjecture33.conjecture33 : False ↔ ∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [inst_3 : 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.