Two-vertex-cut certificate (Fiedler's κ ≤ 2 bound)

If deleting two vertices a ≠ b disconnects the graph into two nonempty parts A and B (no A–B edges), then algConn G ≤ 2, unconditionally.

Test vector: x = |B|·𝟙_A − |A|·𝟙_B (zero on {a, b}). Then ∑ x = 0, x ≠ 0, and the key pointwise estimate is that every ordered adjacent pair contributes (x i − x j)² ≤ (x i)²·c j + c i·(x j)² where c is the indicator of the cut {a, b}: within A or within B the difference vanishes, A–B edges are excluded by the separation hypothesis, and an edge into the cut contributes exactly |B|² (from the A side) or |A|² (from the B side) — which is precisely (x·)² at the non-cut endpoint. Summing, the ordered quadratic form is at most 2 · (∑ c) · (∑ x²) = 4 ∑ x², hence xᵀ L x ≤ 2 ∑ x² and the universal test-vector certificate applies.

theorem ACMax.algConn_le_two_of_two_vertex_cut_general {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (a b : V) (hab : a ≠ b) (A B : Finset V) (hA : A.Nonempty) (hB : B.Nonempty) (hdisj : Disjoint A B) (haA : a ∉ A) (haB : a ∉ B) (hbA : b ∉ A) (hbB : b ∉ B) (hcover : ∀ (v : V), v ∈ A ∨ v ∈ B ∨ v = a ∨ v = b) (hsep : ∀ u ∈ A, ∀ v ∈ B, ¬G.Adj u v) : algConn G ≤ 2

Two-vertex-cut certificate, general vertex type. If {a, b} separates the nonempty sets A and B (which together with a, b cover all vertices, are disjoint, and have no edges between them), then algConn G ≤ 2.

theorem ACMax.algConn_le_two_of_two_vertex_cut {n : ℕ} [Nonempty (Fin n)] (G : SimpleGraph (Fin n)) (a b : Fin n) (hab : a ≠ b) (A B : Finset (Fin n)) (hA : A.Nonempty) (hB : B.Nonempty) (hdisj : Disjoint A B) (haA : a ∉ A ∪ B) (hbB : b ∉ A ∪ B) (hcover : ∀ (v : Fin n), v ∈ A ∨ v ∈ B ∨ v = a ∨ v = b) (hsep : ∀ u ∈ A, ∀ v ∈ B, ¬G.Adj u v) : algConn G ≤ 2

Two-vertex-cut certificate on Fin n (Fiedler's κ ≤ 2 bound): deleting the two vertices a ≠ b disconnects G into the nonempty parts A and B, hence algConn G ≤ 2, unconditionally.