Universal test-vector interface #
algConn_le_two_of_testvector: any nonzero vector x orthogonal to the all-ones
vector whose Laplacian quadratic form is at most 2 ‖x‖² certifies algConn G ≤ 2.
This is the direct corollary of the Courant–Fischer bridge algConn_mul_sq_le that
every concrete upper-bound certificate in the Cuts/ chapter factors through: the
balanced, weighted and signed cuts, the induced-2K₂ bound and the good-C₄/K_{2,3}
certificates all build an explicit x ⊥ 𝟙 and discharge the Rayleigh inequality here.
theorem
ACMax.algConn_le_two_of_testvector
{V : Type u_1}
[Fintype V]
[Nonempty V]
(G : SimpleGraph V)
(x : V → ℝ)
(hx0 : ∑ i : V, x i = 0)
(hxne : ∃ (i : V), x i ≠ 0)
(hQ : x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x ≤ 2 * ∑ i : V, x i ^ 2)
:
Universal certificate: a nonzero x ⊥ 𝟙 with xᵀ L x ≤ 2‖x‖² forces
algConn G ≤ 2.