Documentation

FormalConjectures.WrittenOnTheWallII.GraphConjecture32

Written on the Wall II - Conjecture 32 #

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

theorem WrittenOnTheWallII.GraphConjecture32.conjecture32 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] :
False ∀ (G : SimpleGraph α) [inst : DecidableRel G.Adj], G.Connectedhave A := {v : α | G.degree v = G.minDegree}; have M := {v : α | G.degree v = G.maxDegree}; have eccavg := fun (S : Finset α) => (∑ vS, (G.eccentricity v).toNat) / S.card; G.distavg A + 1 / 2 * eccavg M G.path

WOWII Conjecture 32

For a simple connected graph $G$, $\operatorname{path}(G) \ge \operatorname{dist}\_{\operatorname{avg}}(A) + 0.5 \cdot \operatorname{ecc}\_{\operatorname{avg}}(M)$, where $\operatorname{path}(G)$ is the floor of the average distance of $G$, $A$ is the set of minimum-degree vertices, $M$ is the set of maximum-degree vertices, $\operatorname{dist}\_{\operatorname{avg}}(A)$ is the average distance from all vertices to $A$, and $\operatorname{ecc}\_{\operatorname{avg}}(M)$ is the average eccentricity of the vertices in $M$.

The conjecture is false, the authors present a counterexample: "The path on 5 vertices is a counterexample, path = 5, distavg(A) = 4 and the average of eccentricity of maximum degree vertices is 8/3."