The degree-three core at orders eight and nine #
At these two orders the global excess ledger leaves at least eight degree-three
vertices and at most one other vertex. Hence every degree-three vertex has at
least two neighbors inside the degree-three core. A triangle in the core is a
good-triangle certificate; if the core is triangle-free, the standard
small-degree lemma supplies an induced 2K₂.
theorem
ACMax.small_degree_three_core_fires
{n : ℕ}
[Nonempty (Fin n)]
(hn8 : 8 ≤ n)
(hn9 : n ≤ 9)
(G : SimpleGraph (Fin n))
(hm : G.edgeFinset.card = 2 * (n - 2))
(h3 : ∀ (v : Fin n), 3 ≤ G.degree v)
:
Every minimum-degree-three graph in the ACMAX family on eight or nine vertices has algebraic connectivity at most two.