Variational (Courant–Fischer) upper bound for algebraic connectivity

algConn_mul_sq_le: for any test vector x orthogonal to the all-ones vector (∑ i, x i = 0), the second-smallest Laplacian eigenvalue is bounded by the Rayleigh quotient of x, in division-free form algConn G * ‖x‖² ≤ xᵀ L x.

This is the reusable bridge both clauses of the ACMAX conjecture rely on.

theorem ACMax.algConn_mul_sq_le {V : Type u_1} [Fintype V] [Nonempty V] (G : SimpleGraph V) (x : V → ℝ) (hx0 : ∑ i : V, x i = 0) : algConn G * ∑ i : V, x i ^ 2 ≤ x ⬝ᵥ (SimpleGraph.lapMatrix ℝ G).mulVec x