By the linear equivalence \(\operatorname {piSubmoduleEquiv}\), the finrank of the pi submodule equals the finrank of \(\iota \to p\). Applying the formula \(\operatorname {finrank}(\iota \to p) = |\iota | \cdot \operatorname {finrank}(p)\) and simplifying with \(|\operatorname {Fin}\, n| = n\) yields the result.

Let \(f\) be in the range of \(\partial _\Lambda ^{\operatorname {parityCheck}}\). We must show \(f \in \operatorname {Submodule.pi}(\operatorname {Set.univ}, \lambda \, v \mapsto \operatorname {range}(\operatorname {parityCheck}))\), i.e., for every \(v \in V\), the value \(f(v)\) lies in \(\operatorname {range}(\operatorname {parityCheck})\). Since \(f\) is in the range, there exists \(c\) with \(\partial _\Lambda ^{\operatorname {parityCheck}}(c) = f\). For any vertex \(v\), we have \(f(v) = \operatorname {parityCheck}(\operatorname {localView}_\Lambda \, v\, c)\), so \(f(v)\) is the image of \(\operatorname {localView}_\Lambda \, v\, c\) under \(\operatorname {parityCheck}\), hence in its range.

We compute:

The first inequality follows from \(\operatorname {Submodule.finrank_mono}\) applied to the containment \(\operatorname {range_differential_le}\). The equality follows from \(\operatorname {finrank_pi_submodule}\).

By definition, \(\operatorname {tannerCode}\, \Lambda \, \operatorname {parityCheck} = \ker (\partial _\Lambda ^{\operatorname {parityCheck}})\).

Step 1 (Rank-nullity for \(\partial \)). By rank-nullity for the differential:

Step 2 (Rank-nullity for \(\operatorname {parityCheck}\)). We have \(\operatorname {finrank}(\operatorname {range}(\operatorname {parityCheck})) + k_L = s\), so \(\operatorname {finrank}(\operatorname {range}(\operatorname {parityCheck})) = s - k_L\). In particular \(k_L \leq s\).

Step 3 (Bounding the range). By \(\operatorname {finrank_range_differential_le}\) and Step 2:

Step 4 (Lower bound on dimension). Combining Steps 1 and 3 by integer arithmetic:

Step 5 (Handshaking). By the handshaking lemma \(\operatorname {twice_card_edgeFinset_eq}\), we have \(2|X_1| = s\cdot |V|\), so \(|V| = 2|X_1|/s\).

Step 6 (Real arithmetic). Rewriting Step 4 in \(\mathbb {R}\) and substituting the handshaking relation, we verify \(\dim (\operatorname {tannerCode}) - (2k_L/s - 1)\cdot |X_1| \geq 0\) via the identity

which holds since \((s-k_L)\cdot |V| = (s-k_L)\cdot 2|X_1|/s\). The inequality then follows by nonlinear arithmetic using \(s {\gt} 0\).

Rewriting using \(d_L = \operatorname {dist}(\operatorname {ClassicalCode.ofParityCheck}(\operatorname {parityCheck}))\). Since \(c \in \operatorname {tannerCode}\, \Lambda \, \operatorname {parityCheck}\), by \(\operatorname {mem_tannerCode_iff}\), the local view \(\operatorname {localView}_\Lambda \, v\, c\) lies in \(\ker (\operatorname {parityCheck})\), which equals the local code \(C_L\) by \(\operatorname {code_eq_ker}\). Since the local view is nonzero and is a codeword of \(C_L\), its Hamming weight witnesses that \(d_L = \operatorname {sInf}\{ \operatorname {wt}(x) \mid x \in C_L,\; x \neq 0\} \leq \operatorname {wt}(\operatorname {localView}_\Lambda \, v\, c)\).

By contraposition: suppose \(\operatorname {supp}(c) = \emptyset \). Then for every edge \(e\), \(e \notin \operatorname {supp}(c)\), which by definition of support and membership in the filter means \(c(e) = 0\). By function extensionality, \(c = 0\), contradicting the hypothesis \(c \neq 0\).

By \(\operatorname {support_nonempty_of_ne_zero}\), the set \(\operatorname {supp}(c)\) is nonempty, so its cardinality is positive.

For any \(e \in \operatorname {suppEdges}(c)\), by definition there exists a support element \(e' \in \operatorname {supp}(c)\) with \(e = e'.\operatorname {val}\). Since \(e'\) is an element of \(G.\operatorname {edgeSet}\), we have \(e'.\operatorname {val} \in G.\operatorname {edgeSet}\), so \(e \in G.\operatorname {edgeFinset}\).

By definition, \(\operatorname {suppEdges}(c)\) is the image of \(\operatorname {supp}(c)\) under the map \(e \mapsto e.\operatorname {val}\). Since subtype coercion \(\operatorname {val}\) is injective on \(G.\operatorname {edgeSet}\), this map is injective on \(\operatorname {supp}(c)\). Therefore \(|\operatorname {suppEdges}(c)| = |\operatorname {supp}(c)| = \operatorname {wt}(c)\).

Since \(v \in S(c)\), by definition of \(\operatorname {incidentToSupport}\), there exists an edge \(e\) with \(c(e) \neq 0\) and \(v \in e\). Suppose for contradiction that \(\operatorname {localView}_\Lambda \, v\, c = 0\). Then every component \((\operatorname {localView}_\Lambda \, v\, c)(i) = 0\) for all \(i \in \operatorname {Fin}(s)\).

Since \(e \in G.\operatorname {edgeSet}\) and \(v \in e\) (as an element of \(\operatorname {Sym2}(V)\)), let \(w = \operatorname {Sym2.Mem.other}(v \in e)\), so that \(s(v,w) = e\) by \(\operatorname {Sym2.other_spec}\). Then \(G.\operatorname {Adj}\, v\, w\), so \(w \in G.\operatorname {neighborSet}(v)\). Let \(i = \Lambda _v(w) \in \operatorname {Fin}(s)\).

Applying \(\operatorname {localView_apply}\), we get \((\operatorname {localView}_\Lambda \, v\, c)(i) = c(\langle s(v, (\Lambda _v)^{-1}(i)),\ldots \rangle )\). Since \((\Lambda _v)^{-1}(i) = (\Lambda _v)^{-1}(\Lambda _v(w)) = w\) by the invertibility of \(\Lambda _v\), this equals \(c(\langle s(v,w),\ldots \rangle ) = c(e) \neq 0\), contradicting the assumption that the local view is zero.

By \(\operatorname {localView_ne_zero_of_incident}\), since \(v \in S(c)\) we have \(\operatorname {localView}_\Lambda \, v\, c \neq 0\). By \(\operatorname {localView_weight_bound}\), \(d_L \leq \operatorname {wt}(\operatorname {localView}_\Lambda \, v\, c)\). Converting between the count of nonzero entries of the local view and the support degree at \(v\) closes the goal.

By induction on \(e\) using \(\operatorname {Sym2.ind}\), write \(e = s(a,b)\). The filter \(\{ v \in V \mid v \in s(a,b)\} \) is contained in \(\{ a,b\} \), so its cardinality is at most \(|\{ a,b\} |\). Using \(\operatorname {card_insert_le}\), \(|\{ a,b\} | \leq |\{ b\} | + 1 = 2\). Integer arithmetic closes the goal.

Define the counting set \(T = \{ (v, i) \in S(c) \times \operatorname {Fin}(s) \mid (\operatorname {localView}_\Lambda \, v\, c)(i) \neq 0\} \).

Lower bound on \(|T|\). For each \(v \in S(c)\), by \(\operatorname {localView_ne_zero_of_incident}\) we have \(\operatorname {localView}_\Lambda \, v\, c \neq 0\), and by \(\operatorname {localView_weight_bound}\), the number of nonzero entries of \(\operatorname {localView}_\Lambda \, v\, c\) is at least \(d_L\). By \(\operatorname {card_nsmul_le_sum}\):

Upper bound on \(|T|\). Define the edge map \(\varphi : (v, i) \mapsto \langle s(v, (\Lambda _v)^{-1}(i)),\ldots \rangle \in G.\operatorname {edgeSet}\). For each \((v,i) \in T\), the element \(\varphi (v,i)\) lies in \(\operatorname {supp}(c)\) by \(\operatorname {localView_apply}\).

Each support edge \(e \in \operatorname {supp}(c)\) has at most 2 preimages under \(\varphi \) in \(T\): for preimages \((v_1, i_1)\) and \((v_2, i_2)\) with \(v_1 = v_2\), equality \(\varphi (v_1, i_1) = \varphi (v_1, i_2)\) yields \(s(v_1, (\Lambda _{v_1})^{-1}(i_1)) = s(v_1, (\Lambda _{v_1})^{-1}(i_2))\). Applying \(\operatorname {Sym2.eq_iff}\) gives either \((\Lambda _{v_1})^{-1}(i_1).\operatorname {val} = (\Lambda _{v_1})^{-1}(i_2).\operatorname {val}\) (so \(i_1 = i_2\) by injectivity of \((\Lambda _{v_1})^{-1}\)), or \(v_1 = (\Lambda _{v_1})^{-1}(i_2).\operatorname {val}\) (impossible since \(G\) is loopless). So each fiber has size at most 1 per distinct first coordinate. The first coordinates project into \(\{ v \mid v \in e\} \), which has at most 2 elements by \(\operatorname {card_filter_mem_sym2_le_two}\).

Applying \(\operatorname {card_le_mul_card_image}\):

Combining the bounds gives \(|S(c)| \cdot d_L \leq |T| \leq 2\cdot \operatorname {wt}(c)\).

Unfolding the definition, \(\operatorname {wt}(x) = |\{ i \in \operatorname {Fin}(n) \mid x_i \neq 0\} |\), which is at most \(|\operatorname {Fin}(n)| = n\) by \(\operatorname {card_filter_le}\) and \(\operatorname {Fintype.card_fin}\).

Since the distance is positive, the set \(\{ \operatorname {wt}(x) \mid x \in C_L,\; x \neq 0\} \) is nonempty. We obtain \(x \in C_L\) with \(x \neq 0\) such that \(\operatorname {dist}(C_L) \leq \operatorname {wt}(x)\). By \(\operatorname {hammingWeight_le_card}\), \(\operatorname {wt}(x) \leq s\). Hence \(\operatorname {dist}(C_L) \leq s\).

Let \(c \in C(G, \Lambda , \operatorname {parityCheck})\) be nonzero. Set \(S = S(c)\), \(E = \operatorname {wt}(c)\), \(n = |V|\).

Positivity. Since \(d_L {\gt} \lambda _2 \geq 0\) and \(d_L \in \mathbb {N}\), we have \(d_L {\gt} 0\). Since \(d_L \leq s\) by \(\operatorname {distance_le_length’}\), we get \(s - \lambda _2 \geq d_L - \lambda _2 {\gt} 0\).

Key inequality (double counting). By \(\operatorname {incidentCount_le_twice_weight}\):

Nonemptiness of \(S\). Since \(c \neq 0\), there exists an edge \(e\) with \(c(e) \neq 0\); any endpoint of \(e\) belongs to \(S\), so \(S \neq \emptyset \).

Handshaking. By \(\operatorname {twice_card_edgeFinset_eq}\): \(2|X_1| = s \cdot n\).

Case 1: \(|S| \geq n\) (all vertices are incident). Then \(n \cdot d_L \leq |S| \cdot d_L \leq 2E\), so \(E \geq n d_L/2\). By handshaking, \(n d_L / 2 = (d_L/s) \cdot |X_1|\). Since \((d_L - \lambda _2)/(s-\lambda _2) \leq 1\), we have \((d_L/s) \geq (d_L - \lambda _2)d_L/((s-\lambda _2)s)\). Hence \(E \geq (d_L - \lambda _2)d_L/((s-\lambda _2)s) \cdot |X_1|\).

Case 2: \(|S| {\lt} n\). Set \(\gamma = |S|/n \in (0,1)\).

By \(\operatorname {alonChungContrapositive_direct}\) applied to the support edges \(\operatorname {suppEdges}(c) \subseteq G.\operatorname {edgeFinset}\) with expansion parameter \(\gamma \) (note \(|\operatorname {incidentVertices}(\operatorname {suppEdges}(c))| \leq |S| \leq \gamma n\)):

By \(\operatorname {card_supportEdges_eq}\), \(|\operatorname {suppEdges}(c)| = E\), so:

Combining the double counting bound \(\gamma n \cdot d_L \leq 2E\) with \(|X_1| = sn/2\):

Dividing by \(\gamma {\gt} 0\):

hence \(d_L - \lambda _2 \leq \gamma (s - \lambda _2)\), and since \(s - \lambda _2 {\gt} 0\):

Finally:

where the last equality uses handshaking. Real arithmetic closes the goal.