A disconnected graph has algebraic connectivity at most 2

If the vertex set splits as A ⊔ Aᶜ (both nonempty) with no edges between the parts, then the cut is empty, so the weighted-cut certificate gives algConn G ≤ 2 (indeed algConn G = 0). This handles disconnected graphs uniformly for every n.

theorem ACMax.algConn_le_two_of_separated {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (A : Finset V) (hA : A.Nonempty) (hAc : Aᶜ.Nonempty) (hsep : ∀ a ∈ A, ∀ b ∉ A, ¬G.Adj a b) : algConn G ≤ 2

If G has a nonempty proper vertex set A with no edges to its complement, then algConn G ≤ 2.

theorem ACMax.algConn_le_two_of_not_connected {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (hG : ¬G.Connected) : algConn G ≤ 2

A disconnected graph (on a nonempty vertex type) has algConn G ≤ 2 — uniformly, for every n. The connected component of any vertex is a nonempty proper set with no edges leaving it, so algConn_le_two_of_separated applies.