26 Thm 5: Alon–Boppana Bound
Let \(G\) be a connected simple graph on a finite vertex type \(V\) with \(\operatorname {diam}(G) \geq 2\). Then \(|V| \geq 2\).
By contradiction, assume \(|V| \leq 1\). Then \(V\) is a subsingleton, so every simple graph on \(V\) has extended diameter \(\operatorname {ediam}(G) = 0\) (by SimpleGraph.ediam_eq_zero_of_subsingleton). But then \(\operatorname {diam}(G) = 0\), contradicting \(\operatorname {diam}(G) \geq 2\).
Let \(G\) be a connected simple graph on a finite vertex type \(V\) that is \(s\)-regular for some \(s \geq 3\). Then \(|V| \geq 2\).
By contradiction, assume \(|V| \leq 1\). Then \(V\) is a subsingleton. Since \(G\) is connected, \(V\) is nonempty; obtain a vertex \(v\). Since \(V\) is a subsingleton, the only element is \(v\), so the neighborhood of \(v\) in the simple graph is empty: for any neighbor \(w\) of \(v\), adjacency implies \(v \neq w\), yet \(v = w\) in a subsingleton, a contradiction. Hence \(\deg (v) = 0\). But by \(s\)-regularity, \(\deg (v) = s \geq 3\), a contradiction. We conclude by integer arithmetic.
red[UNPROVEN AXIOM]
Let \(G\) be a finite, connected \(s\)-regular simple graph on a finite vertex type \(V\) with \(s \geq 3\) and diameter \(D = \operatorname {diam}(G) \geq 2\). Let \(\lambda _2\) denote the second-largest eigenvalue of the adjacency matrix of \(G\). Then
Note: This is stated as an axiom because the full proof (using Nilli’s edge-based Laplacian approach, constructing test vectors supported on BFS layers and bounding the Rayleigh quotient) was not completed in the formalization.
There exist a finite vertex type \(V\), a simple graph \(G\) on \(V\), and \(s \geq 3\) such that \(G\) is connected, \(s\)-regular, and \(\operatorname {diam}(G) \geq 2\). In particular, the hypotheses of alonBoppanaBound are satisfiable.
We exhibit the complete bipartite graph \(K_{3,3}\) on vertex set \(\operatorname {Fin}(6)\), with parts \(\{ 0,1,2\} \) and \(\{ 3,4,5\} \), where \(i\) and \(j\) are adjacent iff \(i {\lt} 3 \leq j\) or \(j {\lt} 3 \leq i\).
Connected: For any two vertices \(u, v\), we find a path by cases. If both \(u, v \in \{ 0,1,2\} \), use the path \(u \to 3 \to v\). If both \(u, v \in \{ 3,4,5\} \), use the path \(u \to 0 \to v\). If \(u \in \{ 0,1,2\} \) and \(v \in \{ 3,4,5\} \) (or vice versa), then \(u\) and \(v\) are directly adjacent.
3-regular: For each vertex \(v \in \operatorname {Fin}(6)\), \(\deg (v) = 3\) is verified by computation (native_decide).
Diameter \(\geq 2\): Let \(v_0 = 0\), \(v_1 = 1\), \(v_3 = 3\). The walk \(v_0 \to v_3 \to v_1\) has length 2, so \(\operatorname {dist}(v_0, v_1) \leq 2\). Since \(v_0 \neq v_1\) (by computation) and \(v_0, v_1\) are not adjacent (both in \(\{ 0,1,2\} \), by computation), we have \(\operatorname {dist}(v_0, v_1) \neq 0\) and \(\neq 1\), hence \(\operatorname {dist}(v_0, v_1) = 2\) by integer arithmetic. Since \(K_{3,3}\) is connected its extended diameter is finite, and \(\operatorname {diam}(K_{3,3}) \geq \operatorname {dist}(v_0, v_1) = 2\).
Let \(G\) be a finite, connected \(s\)-regular simple graph on vertex type \(V\) with \(s \geq 3\). Let \(D = \operatorname {diam}(G)\). Then
We use the real-valued bound \(|V| \cdot (s-2) / s \leq (s-1)^D\) (rewriting via Real.rpow_natCast). It suffices to prove the natural number inequality \(|V| \cdot (s-2) \leq s \cdot (s-1)^D\) and then cast to \(\mathbb {R}\).
Geometric sum: We establish by induction on \(D\) that
The base case \(D = 0\) is trivial. For the inductive step, expanding \(\sum _{k=0}^{D} (s-1)^k = \sum _{k=0}^{D-1}(s-1)^k + (s-1)^D\) and using the induction hypothesis, with careful handling of natural number subtraction (using zify and ring after establishing nonnegativity conditions), we verify the telescoping identity.
BFS layer decomposition: Fix a vertex \(v_0\). Define layers \(L_k = \{ w : \operatorname {dist}(v_0, w) = k\} \) for \(k \in \{ 0, \ldots , D\} \). Since \(G\) is connected, every vertex lies within distance \(D\) of \(v_0\), so
The disjointness of distinct layers follows because vertices have unique distances. We have \(|L_0| = 1\) (only \(v_0\), since \(\operatorname {dist}(v_0, v_0) = 0\) and \(\operatorname {dist}(v_0, w) = 0\) implies \(w = v_0\) for a connected graph).
Layer size bound: We claim \(|L_k| \leq s \cdot (s-1)^{k-1}\) for all \(1 \leq k \leq D\), proved by induction on \(k\):
\(k = 1\): The vertices at distance 1 are exactly the neighbors of \(v_0\), so \(|L_1| \leq \deg (v_0) = s\).
\(k \geq 2\) (inductive step): We show \(|L_{k+1}| \leq (s-1) \cdot |L_k|\). For each \(w \in L_{k+1}\), let \(u\) be the penultimate vertex on a shortest walk from \(v_0\) to \(w\); then \(u \in L_k\) and \(G.\text{Adj}(u, w)\). Hence \(L_{k+1} \subseteq \bigcup _{u \in L_k} (\mathcal{N}(u) \cap L_{k+1})\).
For each \(u \in L_k\), we bound \(|\mathcal{N}(u) \cap L_{k+1}| \leq s - 1\). Indeed, \(u\) has degree \(s\). Since \(k \geq 1\), there exists a predecessor vertex \(\operatorname {pred}(u)\) at distance \(k-1\) from \(v_0\) adjacent to \(u\) (the penultimate vertex of a shortest walk to \(u\)). This predecessor is not in \(L_{k+1}\), so it lies in \(\mathcal{N}(u) \setminus (\mathcal{N}(u) \cap L_{k+1})\), giving \(|\mathcal{N}(u) \cap L_{k+1}| {\lt} |\mathcal{N}(u)| = s\), i.e., \(|\mathcal{N}(u) \cap L_{k+1}| \leq s - 1\).
By \(\texttt{Finset.card\_ biUnion\_ le}\) and summing over \(L_k\):
\[ |L_{k+1}| \leq \sum _{u \in L_k} |\mathcal{N}(u) \cap L_{k+1}| \leq |L_k| \cdot (s-1). \]Combined with the inductive hypothesis \(|L_k| \leq s \cdot (s-1)^{k-1}\), we get \(|L_{k+1}| \leq s \cdot (s-1)^k\).
Combining: By the Finset sum reindexing (Finset.sum_range_succ’),
Using the geometric sum identity and natural number arithmetic:
where the last step follows since \((s-2) \leq s \cdot 1 \leq s \cdot (s-1)^D\), verified by nlinarith after zify.
Let \(G\) be a finite, connected \(s\)-regular simple graph on vertex type \(V\) with \(s \geq 3\). Then
We have \(1 {\lt} s - 1\) since \(s \geq 3\). We consider two cases.
Case 1: \(|V| \cdot (s-2) / s \leq 0\). Then \(\log _{s-1}(|V| \cdot (s-2)/s) \leq 0\) (since the argument is \(\leq 1\) after noting it is \(\geq 0\) by nonnegativity of \(|V|\), \(s-2\), and \(s\)). The right-hand side \(\operatorname {diam}(G)\) is a natural number, hence \(\geq 0\). The inequality follows.
Case 2: \(|V| \cdot (s-2)/s {\gt} 0\). By Real.logb_le_iff_le_rpow (valid since \(s-1 {\gt} 1\) and the argument is positive), the inequality \(\log _{s-1}(|V|\cdot (s-2)/s) \leq D\) is equivalent to \(|V|\cdot (s-2)/s \leq (s-1)^D\). This follows directly from the Moore bound (moore_bound).
There exist a finite vertex type \(V\), a simple graph \(G\) on \(V\), and \(s \geq 3\) such that \(G\) is connected and \(s\)-regular. In particular, the hypotheses of diam_lower_bound are satisfiable.
We use \(V = \operatorname {Fin}(4)\) and \(G = \top \) (the complete graph on 4 vertices). The complete graph on \(\operatorname {Fin}(4)\) is connected by SimpleGraph.connected_top and is 3-regular (each vertex has degree \(4 - 1 = 3\)), verified via SimpleGraph.IsRegularOfDegree.top and simplification with \(|\operatorname {Fin}(4)| = 4\).
red[UNPROVEN AXIOM]
Let \(s \geq 3\), let \(n : \mathbb {N} \to \mathbb {N}\), and let \(G_i\) be a connected \(s\)-regular simple graph on \(\operatorname {Fin}(n(i))\) for each \(i\), with \(|\operatorname {Fin}(n(i))| \geq 2\) for all \(i\). If \(n(i) \to \infty \), then
where \(\lambda _2(G_i)\) denotes the second-largest eigenvalue of the adjacency matrix of \(G_i\).
Note: This follows conceptually from alonBoppanaBound and diam_lower_bound: since \(n(i) \to \infty \), the Moore bound gives \(\operatorname {diam}(G_i) \to \infty \), so for large \(i\) the correction term \((2\sqrt{s-1} - 1)/\lfloor D_i/2 \rfloor \to 0\) and the bound approaches \(2\sqrt{s-1}\). It is stated as an axiom because connecting SimpleGraph.diam growth with Filter.liminf through logarithmic estimates requires infrastructure not directly available for SimpleGraph in Mathlib.
Let \(G\) be an \(s\)-regular simple graph on a finite vertex type \(W\). For each \(i \in \operatorname {Fin}(|W|)\),
where \(\lambda _i(G)\) denotes the \(i\)-th adjacency eigenvalue of \(G\).
Step 1. We show the eigenvalue \(\lambda _i = (\texttt{adjMatrix\_ isHermitian}\ G).\texttt{eigenvalues}_0\ i\) lies in the \(\mathbb {R}\)-spectrum of the adjacency matrix \(A = G.\texttt{adjMatrix}\ \mathbb {R}\), using IsHermitian.eigenvalues_mem_spectrum_real.
Step 2. Since the spectrum of \(A\) as a matrix equals the spectrum of the corresponding linear endomorphism \(\texttt{toLin}'(A)\) (via Matrix.spectrum_toLin’), we obtain a module eigenvalue via Module.End.HasEigenvalue.
Step 3. We apply the Gershgorin circle theorem (eigenvalue_mem_ball): every eigenvalue lies in a closed disk centered at some diagonal entry \(A_{kk}\) with radius \(\sum _{j \neq k} |A_{kj}|\) for some row index \(k\).
Step 4. The diagonal entry satisfies \(A_{kk} = 0\) since \(G\) has no self-loops (SimpleGraph.adjMatrix_apply with G.loopless).
Step 5. We compute the Gershgorin radius of row \(k\): since \(|A_{kj}| = 1\) if \(G.\text{Adj}(k, j)\) and \(0\) otherwise, and since \(G\) has no self-loops,
This uses the identification of the filtered set with the neighbor finset and the regularity hypothesis hreg k.
Step 6. From the Gershgorin bound with center \(0\) and radius \(s\), we obtain \(|\lambda _i| \leq s\) via Metric.mem_closedBall and Real.norm_eq_abs.
There exist a finite vertex type \(W\), a simple graph \(G\) on \(W\), and \(s \geq 0\) such that \(G\) is \(s\)-regular. In particular, the hypotheses of adjEigenvalue_abs_le are satisfiable.
We use \(W = \operatorname {Fin}(4)\), \(G = \top \) (the complete graph), and \(s = 3\), witnessing \(G.\text{IsRegularOfDegree}(3)\) via SimpleGraph.IsRegularOfDegree.top.
Let \(G\) be an \(s\)-regular simple graph on a finite vertex type \(W\) with \(|W| \geq 2\). Then
where \(\lambda _2(G)\) denotes the second-largest eigenvalue of the adjacency matrix of \(G\).
Apply adjEigenvalue_abs_le at index \(i = \langle 1, \cdot \rangle \in \operatorname {Fin}(|W|)\) (valid since \(|W| \geq 2\)) to obtain \(|\lambda _2(G)| \leq s\). By the absolute value bound (abs_le), this gives both \(\lambda _2(G) \leq s\) and \(-s \leq \lambda _2(G)\); we use the latter.
Let \(s \geq 3\), let \(n : \mathbb {N} \to \mathbb {N}\), and let \(G_i\) be a connected \(s\)-regular simple graph on \(\operatorname {Fin}(n(i))\) for each \(i\), with \(|\operatorname {Fin}(n(i))| \geq 2\) and \(n(i) \to \infty \). Suppose that there exists \(\varepsilon {\gt} 0\) such that
Then \(\varepsilon \leq s - 2\sqrt{s-1}\). In particular, any uniform spectral gap for an expander family cannot exceed \(s - 2\sqrt{s-1}\), so the Ramanujan bound \(\lambda _2 \leq 2\sqrt{s-1}\) is best possible.
Step 1. By the asymptotic Alon–Boppana bound (alonBoppana_liminf), since \(n(i) \to \infty \) and each \(G_i\) is connected and \(s\)-regular with \(|V_i| \geq 2\):
Step 2. The uniform bound \(\lambda _2(G_i) \leq s - \varepsilon \) holds for all \(i\). By Filter.Frequently.of_forall, this event occurs frequently (in fact, always), so:
using Filter.liminf_le_of_frequently_le. The required lower boundedness of \((\lambda _2(G_i))_i\) is provided by \(\lambda _2(G_i) \geq -s\) (secondLargestEigenvalue_ge_neg), establishing Filter.IsBoundedUnder via Filter.Eventually.of_forall.
Step 3. Combining Steps 1 and 2:
hence \(\varepsilon \leq s - 2\sqrt{s-1}\) by linear arithmetic (linarith).