Weighted (unbalanced) cut certificate #
Generalizes algConn_le_two_of_balanced_cut to an arbitrary bipartition A ⊔ Aᶜ.
With p = |A|, q = |Aᶜ|, the vector x = q·𝟙_A − p·𝟙_{Aᶜ} is orthogonal to 𝟙,
has squared norm p·q·n, and Laplacian quadratic form n²·cut, so
xᵀ L x = n²·cut ≤ 2·p·q·n = 2‖x‖² whenever n·cut ≤ 2·p·q. This handles odd n
and unbalanced near-regular graphs where a balanced cut is unavailable.
theorem
ACMax.algConn_le_two_of_weighted_cut
{V : Type u_1}
[Fintype V]
[Nonempty V]
(G : SimpleGraph V)
(A : Finset V)
(hA : A.Nonempty)
(hAc : Aᶜ.Nonempty)
(hcut : Fintype.card V * ∑ a ∈ A, (G.neighborFinset a \ A).card ≤ 2 * (A.card * Aᶜ.card))
:
A bipartition A ⊔ Aᶜ with |V|·cut ≤ 2·|A|·|Aᶜ| certifies algConn G ≤ 2
(cut = ∑_{a ∈ A} |N(a) \ A|). Both parts must be nonempty.