Documentation

LeanPool.ACMax.Cuts.LowDegreeVertex

A single low-degree vertex already forces algConn ≤ 2 #

If G has a vertex u of degree ≤ 2 and there is at least one vertex outside {u} ∪ N(u), then algConn G ≤ 2.

Certificate: with C := N(u) (|C| = deg u ≤ 2) and T := V ∖ ({u} ∪ C), take x := |T|·e_u − 𝟙_T. Then ∑ x = 0, ∑ x² = |T|² + |T|, and the only edges that contribute to the Laplacian form are the deg u edges u–C (each |T|²) and the T–C edges (each 1); there are no u–T edges. Since every vertex of T meets at most |C| ≤ 2 vertices of C, the T–C edge count is ≤ 2|T|, so xᵀ L x = deg u · |T|² + e(T,C) ≤ 2|T|² + 2|T| = 2 ∑ x².

This closes every n ≤ 7 instance of the conjecture: m = 2(n-2) < 3n/2 for n ≤ 7 forces a vertex of degree ≤ 2. The open core is exactly the graphs with minimum degree ≥ 3 (possible only for n ≥ 8).

theorem ACMax.algConn_le_two_of_low_degree_vertex {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (u : V) (hdeg : G.degree u ≤ 2) (hT : (Finset.univ \ insert u (G.neighborFinset u)).Nonempty) :

If G has a vertex of degree ≤ 2 with a vertex outside its closed neighborhood, then algConn G ≤ 2.

theorem ACMax.algConn_le_two_of_degree_le_two {n : ℕ} [Nonempty (Fin n)] (hn : 4 ≤ n) (G : SimpleGraph (Fin n)) (u : Fin n) (hdeg : G.degree u ≤ 2) :

On Fin n with n ≥ 4, the complement of the closed neighborhood of a vertex of degree at most 2 is automatically nonempty.