Since \(A\) is defined as a filtered subset of \(S\) (i.e., \(A = S.\operatorname {filter}(\cdots )\)), the inclusion \(A \subseteq S\) follows immediately from the fact that any filtered subset of a finset is contained in that finset.

Assume there exist \(v \in S\) and a proof \(h_{vb}\) that \(s - b \leq |(\delta S)_v|\). Decomposing the hypothesis, we obtain the vertex \(v\), its membership \(v \in S\), and the bound \(h_{vb}\). Then \(v \in A\) follows directly from the membership criterion \(A = S.\operatorname {filter}(s - b \leq |(\delta S)_\cdot |)\), and hence \(A\) is nonempty.

We first show that \(\delta S = \bigcup _{v \in S} (\delta S)_v\). For the forward direction: given \(e \in \delta S\), by the characterization of the edge boundary (using mem_edgeBoundary), \(e = \{ a, b\} \) with \(a \in S\) and \(b \notin S\); thus \(e \in (\delta S)_a\) and \(a \in S\), so \(e\) lies in the big union. For the reverse direction: if \(e \in (\delta S)_v\) for some \(v \in S\), then \(e \in \delta S\) by the filter condition.

Next, we show the family \(\{ (\delta S)_v\} _{v \in S}\) is pairwise disjoint. Suppose \(e \in (\delta S)_v \cap (\delta S)_w\) with \(v \neq w\). Then \(e \in \delta S\), and by mem_edgeBoundary, \(e = \{ a,b\} \) with \(a \in S\), \(b \notin S\). Both \(v \in e\) and \(w \in e\) hold. By the membership condition for \(\operatorname {Sym2}\), each of \(v, w\) equals either \(a\) or \(b\). Since \(b \notin S\) but \(v, w \in S\), both \(v = a\) and \(w = a\), contradicting \(v \neq w\).

Having established the disjoint partition, the cardinality identity follows from the finset big-union cardinality formula for pairwise disjoint families.

We compute:

The first inequality holds because \((\delta S)_v \subseteq G.\operatorname {incidenceFinset}(v)\): any edge \(e \in (\delta S)_v\) lies in the edge boundary \(\delta S \subseteq E(G)\) (by edgeBoundary_subset_edgeFinset) and satisfies \(v \in e\), hence \(e \in G.\operatorname {incidenceFinset}(v)\). The equality of the incidence finset cardinality with \(\deg _G(v)\) follows from the standard identity, and \(\deg _G(v) = s\) by \(s\)-regularity.

We have \(|S| {\gt} 0\) (given) and \(|V| {\gt} 0\) (since \(|V| \geq 2\)). Since \(|S| \leq \alpha |V|\) and \(\alpha {\lt} 1\), we deduce \(|S| {\lt} |V|\), so \(S\) is a proper nonempty subset.

We split into two cases based on the sign of \(s - \lambda _2\).

Case 1: \(s - \lambda _2 \geq 0\). Apply the spectral Laplacian bound (spectralLaplacianBound):

Since \(|S|/|V| \leq \alpha \) (as \(|S| \leq \alpha |V|\)), we have \(1 - \alpha \leq 1 - |S|/|V|\). Multiplying both sides of the latter by the nonneg quantity \((s-\lambda _2)|S| \geq 0\) preserves the inequality, yielding

Case 2: \(s - \lambda _2 {\lt} 0\). Then \((1-\alpha )(s-\lambda _2) {\lt} 0\) (since \(1-\alpha {\gt} 0\)), so \((1-\alpha )(s-\lambda _2)|S| {\lt} 0 \leq |\delta S|\) by linear arithmetic.

Let \(B := S \setminus A\). Since \(A \subseteq S\), we have the disjoint decomposition \(S = A \sqcup B\).

By the partition sum identity (Lemma 360):

For the sum over \(A\): since each \(|(\delta S)_v| \leq s\) by \(s\)-regularity (Lemma 361), the bounded sum inequality gives \(\sum _{v \in A} |(\delta S)_v| \leq s|A|\).

For the sum over \(B\): for any \(v \in B = S \setminus A\), we have \(v \notin A\), meaning \(|(\delta S)_v| {\lt} s - b\) (i.e., the defining condition for \(A\) fails). Hence \(|(\delta S)_v| \leq s - b\) (strict inequality implies \(\leq \)), and again by the bounded sum inequality, \(\sum _{v \in B} |(\delta S)_v| \leq (s-b)|B|\).

Finally, \(|B| = |S \setminus A| = |S| - |A|\) (since \(A \subseteq S\)), obtained by the cardinality identity for set differences. Combining all estimates gives \(|\delta S| \leq s|A| + (s-b)(|S| - |A|)\).

Step 0: Trivial case. If \(|S| = 0\), then both sides are zero and the inequality holds trivially by simplification. Henceforth assume \(|S| {\gt} 0\).

Step 1: Lower bound on \(|\delta S|\). By Lemma 362 (relative Cheeger with \(\leq \)):

Step 2: Upper bound on \(|\delta S|\). By Lemma 363:

Step 3: Combine. From Steps 1 and 2 by linear arithmetic:

Expanding the right side: \(s|A| + (s-b)|S| - (s-b)|A| = b|A| + (s-b)|S|\). Hence:

Step 4: Simplify the coefficient. We compute by ring arithmetic:

Thus:

Step 5: Divide by \(b\). Since \(b {\gt} 0\), dividing both sides by \(b\) gives:

which is the desired conclusion. This final step is performed by rewriting with \(\operatorname {div_mul_eq_mul_div}\), applying \(\operatorname {div_le_iff}\) with \(b {\gt} 0\), and concluding by linear arithmetic.