5 Rem 5: Cheeger Constant Definition
For a graph \(G = (V, E)\), the Cheeger constant (also called isoperimetric number or edge expansion) is defined as \(h(G) = \min _{S \subseteq V,\, 0 {\lt} |S| \leq |V|/2} \frac{|\partial S|}{|S|}\), where \(\partial S\) is the edge boundary of \(S\), i.e., the set of edges with exactly one endpoint in \(S\). A graph is called an expander if \(h(G) \geq c\) for some constant \(c {\gt} 0\). In this work, we require \(h(G) \geq 1\) to ensure that the deformed code preserves the distance of the original code.
Given a vertex set \(S \subseteq V\) and an edge \(e = \{ u, v\} \in \mathrm{Sym}_2(V)\), we say that \(e\) crosses the boundary of \(S\) if exactly one of its endpoints lies in \(S\), i.e., \((u \in S \land v \notin S) \lor (u \notin S \land v \in S)\).
The edge boundary \(\partial S\) of a vertex set \(S\) in a simple graph \(G = (V, E)\) is the set of edges with exactly one endpoint in \(S\):
Formally, \(\partial S\) is computed by filtering the edge set of \(G\) to those edges that cross the boundary of \(S\).
For a simple graph \(G = (V, E)\), a vertex set \(S \subseteq V\), and vertices \(u, v \in V\),
By simplification using the definitions of edgeBoundary, mem_filter, mem_edgeFinset, mem_edgeSet, edgeCrossesBoundary, Sym2.lift_mk, and decide_eq_true_eq, the membership condition unfolds directly to the stated equivalence.
The Cheeger constant of a simple graph \(G = (V, E)\) is defined as
where \(\partial S\) is the edge boundary of \(S\). The infimum is taken over all nonempty subsets \(S\) of \(V\) satisfying \(2|S| \leq |V|\).
A simple graph \(G\) is an expander if there exists a constant \(c {\gt} 0\) such that \(h(G) \geq c\):
A simple graph \(G\) is a strong expander if its Cheeger constant is at least \(1\):
This is the condition required in this work to preserve the distance of the original code.
For any simple graph \(G = (V, E)\), the edge boundary of the empty set is empty:
We unfold the definitions of edgeBoundary and edgeCrossesBoundary. By extensionality, it suffices to show that no edge \(e\) belongs to \(\partial \emptyset \). We simplify using mem_filter and notMem_empty. Let \(e\) be an arbitrary edge; we assume \(e\) is in the edge set of \(G\). We proceed by induction on the symmetric pair structure of \(e\): for \(e = \{ u, v\} \), since neither \(u\) nor \(v\) belongs to \(\emptyset \), both disjuncts \((u \in \emptyset \land v \notin \emptyset )\) and \((u \notin \emptyset \land v \in \emptyset )\) are false. Therefore \(\texttt{edgeCrossesBoundary}(\emptyset , e) = \texttt{false}\), and \(e \notin \partial \emptyset \).
For any simple graph \(G = (V, E)\), the edge boundary of the full vertex set is empty:
We unfold the definitions of edgeBoundary and edgeCrossesBoundary. By extensionality, it suffices to show that no edge \(e\) belongs to \(\partial V\). We simplify using mem_filter and notMem_empty. Let \(e\) be an arbitrary edge; we assume \(e\) is in the edge set of \(G\). We proceed by case analysis on the symmetric pair structure: for \(e = \{ u, v\} \), since both \(u \in V\) and \(v \in V\) (as \(V\) is the full vertex set), the condition \(v \notin V\) is false and the condition \(u \notin V\) is false. Therefore both disjuncts \((u \in V \land v \notin V)\) and \((u \notin V \land v \in V)\) are false, so \(\texttt{edgeCrossesBoundary}(V, e) = \texttt{false}\), and \(e \notin \partial V\).
The edge boundary is symmetric under complementation: for any vertex set \(S \subseteq V\),
By extensionality, let \(e\) be an arbitrary edge. We unfold the definitions of edgeBoundary, mem_filter, edgeCrossesBoundary, and mem_compl. We proceed by case analysis on the symmetric pair structure: for \(e = \{ u, v\} \), we simplify using Sym2.lift_mk, mem_compl, and decide_eq_true_eq. We prove both directions.
Forward direction: Assume \(\langle h_e, h_b \rangle \) where \(h_e\) states \(e\) is an edge of \(G\) and \(h_b\) states \((u \in S \land v \notin S) \lor (u \notin S \land v \in S)\). We consider the two cases of \(h_b\):
If \(u \in S\) and \(v \notin S\), then \(\neg (u \notin S)\) holds (by double negation of \(u \in S\)) and \(v \notin S\) holds, giving the right disjunct for the complement condition.
If \(u \notin S\) and \(v \in S\), then \(u \notin S\) holds and \(\neg (v \notin S)\) holds (by double negation of \(v \in S\)), giving the left disjunct for the complement condition.
Backward direction: Assume \(\langle h_e, h_b \rangle \) where \(h_b\) states \((u \notin S \land \neg (v \notin S)) \lor (\neg (u \notin S) \land v \notin S)\). We consider the two cases:
If \(u \notin S\) and \(\neg (v \notin S)\), then \(u \notin S\) holds and \(v \in S\) follows by eliminating the double negation, giving the right disjunct.
If \(\neg (u \notin S)\) and \(v \notin S\), then \(u \in S\) follows by eliminating the double negation and \(v \notin S\) holds, giving the left disjunct.
A strong expander is an expander. That is, if \(h(G) \geq 1\), then \(G\) is an expander (with witness \(c = 1\)).
Given the hypothesis \(h : h(G) \geq 1\), we exhibit the witness \(c = 1\). We need \(c {\gt} 0\) and \(h(G) \geq c\). The first condition \(1 {\gt} 0\) holds by one_pos, and the second condition \(h(G) \geq 1\) is exactly the hypothesis \(h\).
For any simple graph \(G\), the Cheeger constant is nonnegative: \(h(G) \geq 0\).
We show that \(0\) is a lower bound for the infimum defining \(h(G)\). We apply Real.iInf_nonneg three times, once for each parameter of the iterated infimum: first for the subset \(S\), then for the nonemptiness condition, and finally for the cardinality condition \(2|S| \leq |V|\). It remains to show that each term \(\frac{|\partial S|}{|S|}\) is nonnegative. This follows by applying div_nonneg, since both \(|\partial S|\) and \(|S|\) are natural numbers cast to \(\mathbb {R}\), and natural number casts are nonneg by Nat.cast_nonneg.