Erdős Problem 742

References:

• erdosproblems.com/742
• [Pl75] Plesník, Ján, Critical graphs of given diameter. Acta Fac. Rerum Natur. Univ. Comenian. Math. 30 (1975), 71-93.
• [CaHa79] Caccetta, L. and Häggkvist, R., On diameter critical graphs. Discrete Math. 28 (1979), 223-229.
• [Fa87] Fan, Genghua, On diameter 2-critical graphs. Discrete Math. 67 (1987), 235-240.
• [Fü92] Füredi, Zoltán, The maximum number of edges in a minimal graph of diameter 2. J. Graph Theory 16 (1992), 81-98.

def Erdos742.IsDiameter2Critical {V : Type u_1} (G : SimpleGraph V) : Prop

A graph is diameter-2-critical if it has diameter $2$ and removing any edge increases the diameter beyond $2$.

Equations

• Erdos742.IsDiameter2Critical G = (G.diam = 2 ∧ ∀ e ∈ G.edgeSet, (G.deleteEdges {e}).diam ≠ 2)

theorem Erdos742.erdos_742 : sorry ↔ ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4

Murty-Simon Conjecture

Let $G$ be a graph on $n$ vertices with diameter $2$ such that deleting any edge increases the diameter. Is it true that $G$ has at most $\lfloor n^2 / 4 \rfloor$ edges? Equality is conjectured to hold for the complete balanced bipartite graph $K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}$.

The conjecture is resolved up to a finite check: Fan [Fa87] verified it for $n \leq 24$ and $n = 26$, and Füredi [Fü92] proved it for all sufficiently large $n$.

theorem Erdos742.complete_bipartite_edge_count (a b : ℕ) : (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b

The complete bipartite graph $K_{a, b}$ has exactly $a \cdot b$ edges. The bound $\lfloor n^2 / 4 \rfloor$ in the Murty-Simon conjecture is attained by the balanced case $K_{\lceil n/2 \rceil, \lfloor n/2 \rfloor}$.

theorem Erdos742.variants.plesnik_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : IsDiameter2Critical G) : ↑G.edgeFinset.card < 3 * ↑(Fintype.card V) * (↑(Fintype.card V) - 1) / 8

Plesník [Pl75] proved the bound $|E(G)| < 3n(n-1)/8$ for any diameter-$2$-critical graph on $n$ vertices.

theorem Erdos742.variants.fan_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hn : Fintype.card V ≤ 24 ∨ Fintype.card V = 26) (hG : IsDiameter2Critical G) : G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4

Fan [Fa87] verified the Murty-Simon conjecture for all $n \leq 24$ and for $n = 26$.

theorem Erdos742.variants.furedi_bound : ∃ (n₀ : ℕ), ∀ (V : Type u_2) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], n₀ ≤ Fintype.card V → IsDiameter2Critical G → G.edgeFinset.card ≤ Fintype.card V ^ 2 / 4

Füredi [Fü92] proved the Murty-Simon conjecture for all sufficiently large $n$, that is, there exists $n_0$ such that every diameter-$2$-critical graph on $n \geq n_0$ vertices has at most $\lfloor n^2 / 4 \rfloor$ edges.