The "good K_{2,3}" certificate #
An induced K_{2,3} (parts {a,b} and {c,d,e}, complete between, no edges inside parts) is a
weighted cut on 5 vertices with 6 internal edges: each of a,b has 3 neighbours inside, each of
c,d,e has 2, so the cut value is ∑deg − 12. The weighted-cut inequality
n · (∑deg − 12) ≤ 2·5·(n−5) certifies algConn G ≤ 2.
This is the dedicated cut for the n = 12 sparse-hub residual that good C₄ misses: a K_{2,3}
with two degree-4 vertices on the small side has C₄s of degree-sum 14 > 13 (not a good C₄),
yet the denser 5-vertex set still yields cut = 5.
theorem
ACMax.algConn_le_two_of_good_K23
{V : Type u_1}
[Fintype V]
[Nonempty V]
(G : SimpleGraph V)
(a b c d e : V)
(hcard : {a, b, c, d, e}.card = 5)
(hn : 6 ≤ Fintype.card V)
(hac : G.Adj a c)
(had : G.Adj a d)
(hae : G.Adj a e)
(hbc : G.Adj b c)
(hbd : G.Adj b d)
(hbe : G.Adj b e)
(hab : ¬G.Adj a b)
(hcd : ¬G.Adj c d)
(hce : ¬G.Adj c e)
(hde : ¬G.Adj d e)
(hcut :
Fintype.card V * (G.degree a + G.degree b + G.degree c + G.degree d + G.degree e - 12) ≤ 2 * (5 * (Fintype.card V - 5)))
:
An induced K_{2,3} with n · (∑deg − 12) ≤ 2·5·(n−5) certifies algConn G ≤ 2.