Exact Moore closure for every order at least 48 #
This assembly replaces the split between the finite exact-Moore range and the polynomial large-order range by one exact non-backtracking certificate.
theorem
ACMax.starved_dead_ge_48_exact
{n : ℕ}
[Nonempty (Fin n)]
(G : SimpleGraph (Fin n))
(hn48 : 48 ≤ n)
(hm : G.edgeFinset.card = 2 * (n - 2))
(h3 : ∀ (v : Fin n), 3 ≤ G.degree v)
(hnf : ¬algConn G ≤ 2)
(hs0 : ∀ (v w : Fin n), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w)
:
A degree-3-separated obstruction cannot have order at least 48.
theorem
ACMax.upperBound_ge_48_exact
{n : ℕ}
[Nonempty (Fin n)]
(hn48 : 48 ≤ n)
(G : SimpleGraph (Fin n))
(hm : G.edgeFinset.card = 2 * (n - 2))
:
Every graph of order at least 48 with exactly 2(n-2) edges has
algebraic connectivity at most 2.