Suppose for contradiction that \(\operatorname {parityCheck}(x) = 0\). Then \(x \in \ker (\operatorname {parityCheck})\), which by ClassicalCode.code_eq_ker means \(x\) belongs to the classical code. Since \(x \neq 0\), the definition of minimum distance gives \(d_L \leq \operatorname {wt}(x)\). But \(\operatorname {wt}(x) \leq d_L - 1 {\lt} d_L\), a contradiction. Hence \(\operatorname {parityCheck}(x) \neq 0\).

Let \(e \in \operatorname {supportEdges}(G, c)\) and \(w \in e\). Unfolding definitions, \(e\) is the image of some edge \(e'\) in the support of \(c\) (i.e. \(c(e') \neq 0\)) with \(e = e'.val\). Since \(w \in e = e'.val\), we have \(w \in \operatorname {incidentToSupport}(G, c)\) by definition, as witnessed by the edge \(e'\) with \(c(e') \neq 0\) and \(w \in e'\).

Suppose \(e \in \partial _E(S)\) where \(S = \operatorname {incidentToSupport}(G, c)\). By membership in the edge boundary, there exist \(a, b\) with \(e = \{ a, b\} \), \(a \in S\), and \(b \notin S\). But since \(e \in \operatorname {supportEdges}(G, c)\) and \(b \in e\), by Lemma 392 we have \(b \in S\), a contradiction.

Both the set of boundary edges at \(v\) and the set of within-\(S\) edges at \(v\) are subsets of the incidence finset \(\operatorname {incidenceFinset}(v)\), which has cardinality \(\deg (v) = s\). Moreover, these two sets are disjoint: if \(e\) is in the edge boundary, then \(e\) has one endpoint outside \(S\), so it cannot have all endpoints in \(S\). By disjointness and the union bound:

Let \(v \in V\). The Hamming weight \(\operatorname {wt}(\operatorname {localView}_\Lambda (v, c))\) equals \(|\{ i \in \operatorname {Fin}(s) \mid \operatorname {localView}_\Lambda (v, c)(i) \neq 0\} |\). Define a map \(\operatorname {mapEdge} : \operatorname {Fin}(s) \to \operatorname {Sym2}(V)\) by \(i \mapsto \{ v, (\Lambda (v))^{-1}(i)\} \).

We show this map sends the support indices into the within-\(S\) edges: if \(\operatorname {localView}_\Lambda (v, c)(i) \neq 0\), then \(c(\{ v, (\Lambda (v))^{-1}(i)\} ) \neq 0\), so both endpoints lie in \(S\) by hypothesis.

We then show \(\operatorname {mapEdge}\) is injective on the support indices: if \(\{ v, w_1\} = \{ v, w_2\} \) as elements of \(\operatorname {Sym2}(V)\) with \(v \neq w_1\), then \(w_1 = w_2\), hence the preimages under \(\Lambda (v)\) coincide.

By injectivity and inclusion, \(|\text{support indices}| = |\operatorname {image}| \leq |\text{within-}S\text{ edges at }v|\).

Combine Lemma 395 (bounding the local view weight by within-\(S\) edge count) and Lemma 394 (bounding the sum of within-\(S\) and boundary counts by \(s\)). The result follows by integer arithmetic.

Unfolding definitions, \(\operatorname {supportEdges}(G, c)\) is the image of the support of \(c\) under the injective map \(\operatorname {Subtype.val}\). The cardinality of the image under an injective map equals the cardinality of the domain, which is \(\operatorname {edgeHammingWeight}(G, c)\).

By extensionality: a vertex \(v\) belongs to \(\operatorname {incidentToSupport}(G, c)\) if and only if there exists an edge \(e\) in the support of \(c\) with \(v \in e\), which holds if and only if there exists \(e \in \operatorname {supportEdges}(G, c)\) with \(v \in e\), i.e. \(v \in \operatorname {incidentVertices}(\operatorname {supportEdges}(G, c))\). Both directions follow by unfolding definitions and matching witnesses.

Apply the standard handshaking identity \(\sum _{v \in V} \deg (v) = 2|E|\). Since \(G\) is \(s\)-regular, \(\deg (v) = s\) for all \(v\), so \(\sum _{v \in V} s = s \cdot |V| = 2|E|\).

Let \(E = \operatorname {supportEdges}(G, c)\). By Lemma 398, \(|\operatorname {incidentToSupport}| = |\operatorname {incidentVertices}(E)|\). Since each edge \(e \in E\) contributes at most 2 vertices (as \(|\{ v \mid v \in e\} | \leq 2\) for any \(e \in \operatorname {Sym2}(V)\)), we have:

where the last equality uses Lemma 397.

By Lemma 400, \(|S| \leq 2\, \operatorname {edgeHammingWeight}(G, x) \leq 2\alpha |G.\operatorname {edgeFinset}|\). By the handshaking lemma (Lemma 399), \(2|G.\operatorname {edgeFinset}| = s|V|\). Therefore:

Since \(v \in \operatorname {incidentToSupport}(G, c)\), there exists an edge \(e\) in the support of \(c\) (i.e. \(c(e) \neq 0\)) with \(v \in e\). Write \(e = \{ v, w\} \) for some neighbor \(w\) of \(v\). Let \(i = \Lambda (v)(w, \cdot )\) be the label assigned to \(w\). Then by definition of \(\operatorname {localView}\), \(\operatorname {localView}_\Lambda (v, c)(i) = c(e) \neq 0\). Hence \(\operatorname {localView}_\Lambda (v, c) \neq 0\).

It suffices to show \(A \subseteq \{ v \in V \mid \operatorname {parityCheck}(\operatorname {localView}_\Lambda (v, c)) \neq 0\} \). Let \(v \in A\).

By Lemma 358, \(v \in S\). By the definition of high-expansion vertices, \(|(\partial _E S)_v| \geq s - (d_L - 1)\).

Since every edge \(e\) with \(c(e) \neq 0\) has both endpoints in \(S\) (by definition of \(S = \operatorname {incidentToSupport}\)), Lemma 396 gives \(\operatorname {wt}(\operatorname {localView}_\Lambda (v, c)) + |(\partial _E S)_v| \leq s\).

Therefore \(\operatorname {wt}(\operatorname {localView}_\Lambda (v, c)) \leq s - |(\partial _E S)_v| \leq d_L - 1\).

Since \(v \in S = \operatorname {incidentToSupport}(G, c)\), Lemma 402 gives \(\operatorname {localView}_\Lambda (v, c) \neq 0\).

Applying Lemma 390 with \(x = \operatorname {localView}_\Lambda (v, c)\), \(\operatorname {wt}(x) \leq d_L - 1\), and \(x \neq 0\), we conclude \(\operatorname {parityCheck}(x) \neq 0\).

Unfolding \(\beta ' = \operatorname {betaParam}\), we have

The denominator satisfies \(s(s - \lambda _2)\alpha {\gt} 0\) since \(s \geq 1\), \(s - \lambda _2 {\gt} 0\), and \(\alpha {\gt} 0\).

For the numerator \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\alpha } - \lambda _2 {\gt} 0\), we consider two cases:

• If \(\lambda _2 \geq 0\): since \(4s(s-\lambda _2)\alpha {\gt} 0\), we have \(\lambda _2^2 + 4s(s-\lambda _2)\alpha {\gt} \lambda _2^2\), so \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\alpha } {\gt} \sqrt{\lambda _2^2} = \lambda _2\) (using \(\lambda _2 \geq 0\)). Thus the numerator is positive.

• If \(\lambda _2 {\lt} 0\): then \(\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\alpha } \geq 0 {\gt} \lambda _2\), so the numerator is positive.

In both cases \(\beta ' {\gt} 0\).

Trivial case. If \(\beta '(s, \lambda _2, \alpha ) \cdot \beta ''(s, \lambda _2, \alpha , d_L) \leq 0\), then the right-hand side is at most \(0 \leq \operatorname {differentialWeight}(\ldots )\), and the bound holds.

Main case: \(\beta ' \cdot \beta '' {\gt} 0\).

By Lemma 404, \(\beta ' {\gt} 0\) holds whenever \(s \geq 1\), \(\lambda _2 {\lt} s\), \(\alpha {\gt} 0\). Since \(\beta ' \cdot \beta '' {\gt} 0\) and \(\beta ' {\gt} 0\), we also have \(\beta '' {\gt} 0\).

From \(\beta '' {\gt} 0\), we deduce \(d_L \geq 2\) as follows: if \(d_L = 1\), then \(\beta '' = ({-\lambda _2 - \alpha s(s-\lambda _2)})/0 = 0\) in Lean’s division, contradicting \(\beta '' {\gt} 0\).

From \(\beta '' {\gt} 0\), we also deduce \(\alpha s {\lt} 1\): since \(d_L \geq 2\), the denominator \(d_L - 1 {\gt} 0\), so the numerator \((d_L - 1 - \lambda _2) - \alpha s(s - \lambda _2) {\gt} 0\). If \(\alpha s \geq 1\), then \(\alpha s(s - \lambda _2) \geq s - \lambda _2 \geq d_L - \lambda _2 {\gt} d_L - 1 - \lambda _2\) (using \(d_L \leq s\)), contradicting positivity of the numerator. Hence \(\alpha s {\lt} 1\).

Edge case: \(x = 0\). If \(\operatorname {edgeHammingWeight}(G, x) = 0\), the right-hand side is \(0\) and the bound holds trivially.

Main inequality chain. Assume \(\operatorname {edgeHammingWeight}(G, x) {\gt} 0\). Set \(S = \operatorname {incidentToSupport}(G, x)\), \(E = \operatorname {supportEdges}(G, x)\), \(A = \operatorname {highExpansionVertices}(G, S, s, d_L - 1)\).

Step 1: \(|A| \leq \operatorname {differentialWeight}(\ldots )\). By Lemma 403.

Step 2: \(\beta ' \cdot \operatorname {edgeHammingWeight}(G, x) \leq |S|\). Since \(E \subseteq G.\operatorname {edgeFinset}\) (by Lemma 378) and \(|E| = \operatorname {edgeHammingWeight}(G, x)\) (by Lemma 397) with \(|E| \leq \alpha |G.\operatorname {edgeFinset}|\), we may apply the edge-to-vertex expansion theorem (Theorem 355):

Since \(S = \operatorname {incidentVertices}(E)\) (Lemma 398) and \(\beta ' = \operatorname {betaParam}\), this yields \(|S| \geq \beta ' \cdot \operatorname {edgeHammingWeight}(G, x)\).

Step 3: \(\beta '' \cdot |S| \leq |A|\). Since \(|S| \leq \alpha s |V|\) (Lemma 401) and \(\alpha s {\lt} 1\), \(d_L - 1 \in (0, s]\), we apply the relative vertex-to-edge expansion theorem (Theorem 364) with parameters \(\alpha ' = \alpha s\) and \(b = d_L - 1\):

which is exactly \(\beta '' \cdot |S| \leq |A|\).

Combining. The chain

follows from Steps 2, 3, and 1 respectively (using \(\beta '' {\gt} 0\) in Step 2, and applying linear arithmetic to combine the bounds).