Section 2, p. 76 — $0 = \lambda_0 < \lambda_1$ for a connected graph

Proved

AlonMilman.Diameter.lambda0_eq_zero_lt_lambda1

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1spectral-graph-theory

Let $G = (V, E)$ be a connected finite simple graph on $n \ge 2$ vertices with Laplacian $Q = \operatorname{diag}(d(v)) - A_G$ , and let $\lambda_0 \le \lambda_1 \le \cdots \le \lambda_{n-1}$ be the eigenvalues of $Q$ with multiplicity. Then

0 = \lambda_0 < \lambda_1 = \lambda_1(G).

The smallest eigenvalue of the Laplacian of a connected graph is $0$ (with the constant eigenvectors) and it is simple, so the algebraic connectivity is strictly positive. This is what makes the divisions by $\lambda_1$ in the diameter bound meaningful.

Formalization Note $\lambda_0$ is eigenvalues₀ at index $n-1$ (the list is decreasing) and $\lambda_1$ is the mission's lambda1, which is eigenvalues₀ at index $n-2$ .

Preamble

import Mathlib
import Definitions.Def_AlonMilman_Diameter_lambda1

Formal statement

namespace AlonMilman.Diameter

theorem lambda0_eq_zero_lt_lambda1 {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (hn : 2 ≤ Fintype.card V) :
    (G.isHermitian_lapMatrix ℝ).eigenvalues₀ ⟨Fintype.card V - 1, by omega⟩ = 0 ∧
      0 < lambda1 G := by sorry

end AlonMilman.Diameter

Source

Alon, Milman, λ1, Isoperimetric Inequalities for Graphs, and Superconcentrators, J. Combin. Theory Ser. B 38 (1985), p. 76, Section 2 (unnumbered: 'Let 0 = λ₀ < λ₁ = λ₁(G) ≤ λ₂ ≤ ··· ≤ λ_{n−1} be the eigenvalues of Q')

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Section 2, p. 76 — 0=λ0<λ10 = \lambda_0 < \lambda_10=λ0​<λ1​ for a connected graph

Section 2, p. 76 — $0 = \lambda_0 < \lambda_1$ for a connected graph