We proceed by contradiction. Suppose \(S(y) = \emptyset \). Then for every \(v \in V\) we have \(y_v = 0\): indeed, if \(y_v \neq 0\) then \(v \in S(y)\), contradicting \(S(y) = \emptyset \). Hence \(y(v)(i) = 0\) for all \(v\) and \(i\), giving \(y = 0\), a contradiction.

We compute:

The first inequality holds because for \(v \in S(y)\) we have \(y_v \neq 0\), so \(\operatorname {wt}(y_v) \geq 1\). The second holds by extending the sum to all of \(V\) (all terms are non-negative).

We split the sum \(\sum _{v \in V} \operatorname {wt}(y_v) = \sum _{v \in S(y)} \operatorname {wt}(y_v) + \sum _{v \notin S(y)} \operatorname {wt}(y_v)\). For \(v \notin S(y)\) we have \(y_v = 0\) so \(\operatorname {wt}(y_v) = 0\), hence the second sum vanishes. Then

since the Hamming weight of any \(\mathbb {F}_2^m\)-vector is at most \(m\).

Since \(m {\gt} 0\), we may divide both sides of \(\operatorname {totalWeight}(y) \leq m \cdot |S(y)|\) by \(m\) to obtain the result. More precisely, rewriting the inequality as \(\operatorname {totalWeight}(y) \leq |S(y)| \cdot m\) and dividing by \(m\) (which is positive) yields \(\operatorname {totalWeight}(y)/m \leq |S(y)|\) over \(\mathbb {R}\).

We show \(\ker (H^\top ) = \{ 0\} \). Suppose \(H^\top y = 0\), i.e., \(\langle y, H(e_j)\rangle = 0\) for all \(j\). We must show \(y = 0\). For any index \(i\), since \(H\) is surjective, there exists \(x \in \mathbb {F}_2^s\) with \(H(x) = e_i\) (the \(i\)-th standard basis vector). Writing \(x = \sum _j x_j e_j\) and using linearity of \(H\),

since each \(\langle y, H(e_j)\rangle = (H^\top y)(j) = 0\). But \(\langle y, e_i\rangle = y(i)\), so \(y(i) = 0\) for all \(i\), giving \(y = 0\). The converse (\(y = 0 \Rightarrow H^\top y = 0\)) is immediate.

We need to show that for every \(c \in C = \ker (H)\), \(\langle H^\top y, c\rangle = 0\). We have

Rewriting the double sum and exchanging order of summation,

Since \(c \in \ker (H)\), we have \(H(c) = 0\), so \(\langle y, H(c)\rangle = 0\).

Since \(H\) is surjective, by Lemma 415, \(H^\top \) is injective. Because \(y \neq 0\), we have \(H^\top y \neq 0\) (otherwise \(y = H^\top (0) = 0\) by injectivity). By Lemma 416, \(H^\top y \in C^\perp \). Therefore \(H^\top y\) is a nonzero codeword of \(C^\perp \), and so its Hamming weight is at least \(d_{L^\perp }\) (by definition of minimum distance as the infimum of weights of nonzero codewords).

This holds by definition (reflexivity).

We write \(\delta (y)(e) = \langle y_v, \partial _\Lambda ^H(\mathbf{1}_e)(v)\rangle + \sum _{u \neq v} \langle y_u, \partial _\Lambda ^H(\mathbf{1}_e)(u)\rangle \) by extracting the \(v\)-term from the full sum. It suffices to show the remaining sum is zero. For \(u \neq v\), we consider two cases. If \(u \in e\) (i.e., \(u\) is the other endpoint), then by hypothesis \(y_u = 0\), so \(\langle y_u, \partial _\Lambda ^H(\mathbf{1}_e)(u)\rangle = 0\). If \(u \notin e\), then the local view \(\mathcal{L}_\Lambda (u)(\mathbf{1}_e) = 0\), because the edge \(\{ u, (\Lambda _u)^{-1}(i)\} \) (for any label \(i\)) is not equal to \(e\) (since \(u \notin e\)); hence \(\partial _\Lambda ^H(\mathbf{1}_e)(u) = H(0) = 0\) by applying Lemma 250, so the dot product vanishes.

Define the complementary set \(P_{\bar{S}}(v) = \{ j \in \operatorname {Fin} s \mid (\Lambda _v)^{-1}(j) \notin S\} \). Since \(P_S(v)\) and \(P_{\bar{S}}(v)\) partition \(\operatorname {Fin} s\), we have \(|P_S(v)| + |P_{\bar{S}}(v)| = s\). Thus it suffices to show \(|(\partial _e S)_v| \leq |P_{\bar{S}}(v)|\), i.e., there is an injection from boundary edges at \(v\) into \(P_{\bar{S}}(v)\).

If \(s = 0\), then there are no edges and the boundary at \(v\) is empty, so the inequality is trivial by Lemma 361.

For \(s {\gt} 0\), we define a map \(f : \partial _e S \to \operatorname {Fin} s\) by sending a boundary edge \(e\) (with \(v \in e\)) to \((\Lambda _v)(\text{other endpoint of } e)\). We show:

\(f\) maps into \(P_{\bar{S}}(v)\): For a boundary edge \(e \in \partial _e S\), there exist \(a \in S\) and \(b \notin S\) with \(e = \{ a, b\} \). Since \(v \in S\), we have \(v = a\) and the other endpoint is \(b \notin S\), so \(f(e)\) corresponds to a neighbor outside \(S\).

\(f\) is injective: If \(f(e_1) = f(e_2)\), then both edges have the same other endpoint \(w\) at \(v\) (by injectivity of \(\Lambda _v\)), and both edges equal \(\{ v, w\} \), so \(e_1 = e_2\).

Thus \(|(\partial _e S)_v| \leq |P_{\bar{S}}(v)|\), giving \(|P_S(v)| + |(\partial _e S)_v| \leq |P_S(v)| + |P_{\bar{S}}(v)| = s\).

Base case. If \(y = 0\), then \(\operatorname {totalWeight}(y) = 0\) and \(\operatorname {wt}(\delta (y)) = 0\), so \(\beta \cdot 0 \leq 0\) holds trivially.

Setup for \(y \neq 0\). Let \(S = S(y)\) be the vertex support of \(y\). Since \(y \neq 0\), the support \(S\) is nonempty, so \(|S| {\gt} 0\). Since \(y \neq 0\) and \(y\) takes values in \(\mathbb {F}_2^m\), we must have \(m {\gt} 0\) (otherwise \(y\) would be \(0\) by vacuity).

Set \(\alpha ' = \alpha m\) and \(b = d_{L^\perp } - 1\). Then \(\alpha ' {\gt} 0\) (since \(\alpha {\gt} 0\) and \(m {\gt} 0\)), \(\alpha ' {\lt} 1\) (by hypothesis), and \(b {\gt} 0\) (since \(d_{L^\perp } \geq 2\)) and \(b \leq s\) (since \(d_{L^\perp } \leq s\)).

By Lemma 409, \(|S| \leq \operatorname {totalWeight}(y)\), and by the hypothesis \(\operatorname {totalWeight}(y) \leq \alpha \cdot |V| \cdot m = \alpha ' \cdot |V|\), we get \(|S| \leq \alpha ' \cdot |V|\).

Applying the relative vertex-to-edge expansion theorem. Let \(A = A_b(S)\) be the set of high-expansion vertices (those \(v \in S\) with \(|(\partial _e S)_v| \geq s - b\)). By Theorem 364 applied with parameters \(\alpha '\), \(b\), \(S\),

By Lemma 411, \(\operatorname {totalWeight}(y)/m \leq |S|\).

Reducing to \(|A| \leq \operatorname {wt}(\delta (y))\). We claim it suffices to show \(|A| \leq \operatorname {wt}(\delta (y))\). To derive the stated inequality from this:

• If \(\frac{b - \lambda _2 - \alpha '(s - \lambda _2)}{b} \geq 0\), then

  \[ \beta \cdot \operatorname {totalWeight}(y) = \frac{b - \lambda _2 - \alpha '(s - \lambda _2)}{mb} \cdot \operatorname {totalWeight}(y) = \frac{b - \lambda _2 - \alpha '(s - \lambda _2)}{b} \cdot \frac{\operatorname {totalWeight}(y)}{m} \leq \frac{b - \lambda _2 - \alpha '(s - \lambda _2)}{b} \cdot |S| \leq |A| \leq \operatorname {wt}(\delta (y)). \]

• If \(\frac{b - \lambda _2 - \alpha '(s - \lambda _2)}{b} {\lt} 0\), then \(\beta {\lt} 0\), so \(\beta \cdot \operatorname {totalWeight}(y) \leq 0 \leq \operatorname {wt}(\delta (y))\).

Proving \(|A| \leq \operatorname {wt}(\delta (y))\). We construct an injection \(g : A \to \{ e \in E(G) \mid \delta (y)(e) \neq 0\} \).

Note that \(G\) is connected with \(|V| \geq 2\) and \(s\)-regular with \(s \geq 1\), so \(G\) has at least one edge.

For each \(v \in A\), we show there exists an edge \(e\) incident to \(v\) in \(\partial _e S\) with \(\delta (y)(e) \neq 0\):

By Lemma 358, \(A \subseteq S\), so \(y_v \neq 0\) for all \(v \in A\).

Let \(v \in A\). By definition of \(A\), vertex \(v\) has \(|(\partial _e S)_v| \geq s - b\). Consider the transpose vector \(t_v = H^\top (y_v) \in \mathbb {F}_2^s\). By Lemma 417, \(\operatorname {wt}(t_v) \geq d_{L^\perp }\).

Let \(\operatorname {supp}(t_v) = \{ j \in \operatorname {Fin} s \mid t_v(j) \neq 0\} \) with \(|\operatorname {supp}(t_v)| \geq d_{L^\perp } = b + 1\). Define the set of label positions pointing into \(S\):

By Lemma 420, \(|P_S(v)| \leq s - |(\partial _e S)_v| \leq s - (s - b) = b\). Since \(|\operatorname {supp}(t_v)| \geq b + 1 {\gt} b \geq |P_S(v)|\), there exists \(j \in \operatorname {supp}(t_v) \setminus P_S(v)\).

For this \(j\), let \(w = (\Lambda _v)^{-1}(j)\) (the neighbor of \(v\) at label \(j\)) and let \(e = \{ v, w\} \in E(G)\). Since \(j \notin P_S(v)\), we have \(w \notin S\). Hence \(e\) is a boundary edge (\(v \in S\), \(w \notin S\)).

We show \(\delta (y)(e) \neq 0\): Since \(w \notin S = S(y)\), we have \(y_w = 0\). By Lemma 419, \(\delta (y)(e) = \langle y_v, \partial _\Lambda ^H(\mathbf{1}_e)(v)\rangle \). Applying Lemma 250 and computing the local view, the local view of \(v\) at edge \(e\) is the standard basis vector \(e_j\) (since \(\Lambda _v\) assigns label \(j\) to \(w\)). Thus

since \(j \in \operatorname {supp}(t_v)\).

Injectivity of the assignment. Choose for each \(v \in A\) a witness edge \(g(v)\) incident to \(v\) in \(\partial _e S\) with \(\delta (y)(g(v)) \neq 0\). We show the map \(v \mapsto g(v)\) is injective on \(A\). Suppose \(g(v_1) = g(v_2) = e\) for \(v_1, v_2 \in A\). The edge \(e \in \partial _e S\) has one endpoint \(a \in S\) and one endpoint \(b \notin S\). Both \(v_1, v_2 \in A \subseteq S\) are incident to \(e\), so both equal \(a\), giving \(v_1 = v_2\).

Conclusion. By Finset cardinality bounds, \(|A| \leq |\{ e \in E(G) \mid \delta (y)(e) \neq 0\} | = \operatorname {wt}(\delta (y))\).