Documentation

LeanPool.ACMax.Cuts.SignedCut

Signed (three-valued) certificate — the unifying general method #

Every n ≤ 8 upper-bound proof, and the n = 9 extremal graphs where the ±1 cut method provably fails, are all captured by a single {-1,0,1} test vector x = 𝟙_P − 𝟙_N with a third "neutral" set Z = (P ∪ N)ᶜ. Orthogonality to 𝟙 requires |P| = |N|; the squared norm is 2|P|; and the Laplacian quadratic form is xᵀ L x = 4·e(P,N) + e(P,Z) + e(N,Z) (cross edges between P and N cost 4, edges to the neutral set cost 1, edges inside a block cost 0). Hence the certificate 4·e(P,N) + e(P,Z) + e(N,Z) ≤ 4|P| gives algConn G ≤ 2.

This subsumes:

and, unlike any bipartition cut, it certifies the λ₂ = 2 Fiedler-eigenvector graphs at n = 9 (the eigenvectors are {-1,0,1}-valued, with the high-degree vertices in Z).

theorem ACMax.algConn_le_two_of_signed {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (P N : Finset V) (hd : Disjoint P N) (hc : P.card = N.card) (hpos : 0 < P.card) (hcond : 4 * ∑ p ∈ P, (G.neighborFinset p ∩ N).card + ∑ p ∈ P, (G.neighborFinset p \ (P ∪ N)).card + ∑ q ∈ N, (G.neighborFinset q \ (P ∪ N)).card ≤ 4 * P.card) :

Three-valued ({-1,0,1}) certificate: disjoint equal-size P, N with 4·e(P,N) + e(P, neutral) + e(N, neutral) ≤ 4|P| forces algConn G ≤ 2, where the neutral set is (P ∪ N)ᶜ.