The "good C₄" certificate #
An induced 4-cycle a–b–c–d–a (with a ≁ c, b ≁ d) whose four vertices have small total degree
is a sparse weighted cut: each cycle vertex has exactly two neighbours inside {a,b,c,d}, so the
cut value is ∑ deg − 8, and the weighted-cut inequality n · (∑deg − 8) ≤ 2·4·(n−4) certifies
algConn G ≤ 2. This complements the "good triangle" certificate and, since C₄ is 2K₂-free,
applies in the no-2K₂ regime where the induced-2K₂ method fails.
theorem
ACMax.algConn_le_two_of_good_C4
{V : Type u_1}
[Fintype V]
[Nonempty V]
(G : SimpleGraph V)
(a b c d : V)
(hcard : {a, b, c, d}.card = 4)
(hn : 5 ≤ Fintype.card V)
(hab : G.Adj a b)
(hbc : G.Adj b c)
(hcd : G.Adj c d)
(hda : G.Adj d a)
(hac : ¬G.Adj a c)
(hbd : ¬G.Adj b d)
(hcut : Fintype.card V * (G.degree a + G.degree b + G.degree c + G.degree d - 8) ≤ 2 * (4 * (Fintype.card V - 4)))
:
An induced C₄ on {a,b,c,d} with n · (∑deg − 8) ≤ 2·4·(n−4) certifies algConn G ≤ 2.