Extremal graphs of girth five

DefinitionGirth-five extremal number#✓fully proved

For a natural number \(n\), \(\mathrm{ex}(n; \{C_3, C_4\})\) is the largest number of edges of a simple graph on \(n\) vertices whose girth is at least \(5\), that is, which contains no triangle and no four-cycle (OEIS A006856). An acyclic graph has infinite girth, so the empty graph always qualifies.

noncomputable def girthFiveExtremalNumber (n : ℕ) : ℕ :=
  (univ.filter fun G : SimpleGraph (Fin n) => 5 ≤ G.egirth).sup (fun G => #G.edgeFinset)

Used by 2

Used byGirth-five extremal number on fifty vertices · Girth-five extremal numbers up to twenty vertices

TheoremGirth-five extremal numbers up to twenty vertices#●ready to prove

For \(n = 1, 2, \dots, 20\) the girth-five extremal numbers \(\mathrm{ex}(n; \{C_3, C_4\})\), the largest numbers of edges of a simple graph on \(n\) vertices that contains no triangle and no four-cycle, are, in order, \(0, 1, 2, 3, 5, 6, 8, 10, 12, 15, 16, 18, 21, 23, 26, 28, 31, 34, 38, 41\).

public theorem_wanted girthFiveExtremalNumber_one_to_twenty :
    (List.range 20).map (fun i => girthFiveExtremalNumber (i + 1)) =
      [0, 1, 2, 3, 5, 6, 8, 10, 12, 15, 16, 18, 21, 23, 26, 28, 31, 34, 38, 41]

Sources

• D. K. Garnick, Y. H. H. Kwong, and F. Lazebnik, Extremal graphs without three-cycles or four-cycles, J. Graph Theory 17 (1993), 633–645 (n ≤ 24); OEIS A006856; listed in leansolving/SqueezeBench SqueezeBench/Problems/ExGirthFive/README.md.

Uses 1

Statement usesGirth-five extremal number

TheoremGirth-five extremal number on fifty vertices#●ready to prove

The girth-five extremal number \(\mathrm{ex}(50; \{C_3, C_4\})\), the largest number of edges of a simple graph on \(50\) vertices that contains no triangle and no four-cycle, equals \(175\).

For graphs on \(n\) vertices of girth at least \(5\), the Hoffman–Singleton graph attains the Moore-type bound \(\frac{n}{2} \sqrt{n - 1}\) on the number of edges, with \(n = 50\).

public theorem_wanted girthFiveExtremalNumber_fifty : girthFiveExtremalNumber 50 = 175

Sources

• A. J. Hoffman and R. R. Singleton, On Moore graphs with diameters 2 and 3, IBM J. Res. Develop. 4 (1960), 497–504; OEIS A006856; listed in SqueezeBench SqueezeBench/Problems/ExGirthFive/README.md.

Uses 1

Statement usesGirth-five extremal number

1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.