By the definition of the boundary map, \(\partial (\mathbf{1}_c)(v) = \sum _{e \in E} [\! [v \in e]\! ] \cdot \mathbf{1}_c(e)\). We rewrite each summand: the term \([\! [v \in e]\! ] \cdot \mathbf{1}_c(e)\) equals \([\! [e \in c \land v \in e]\! ]\), by splitting on cases (if \(v \in e\), then the value is \(\mathbf{1}_c(e)\); otherwise \(0\), and if \(e \notin c\), both expressions are \(0\)). After this rewriting, we apply the identity \(\sum _{e} [\! [P(e)]\! ] = |\{ e : P(e)\} |\) (sum of boolean indicators equals the cardinality of the filtered set). This gives \(\partial (\mathbf{1}_c)(v) = |\{ e \in E : e \in c \land v \in e\} | \pmod{2}\). Since by hypothesis this cardinality is even, the natural number cast to \(\mathbb {Z}/2\mathbb {Z}\) is zero, as required.

We expand both maps using their definitions. By the definition of \(\partial _2\), for each edge \(e\), \((\partial _2(\mathbf{e}_c))(e) = \sum _{c'} [\! [e \in c']\! ] \cdot \mathbf{e}_c(c')\). We establish the key identity: for each edge \(e\), \(\sum _{c'} [\! [e \in c']\! ] \cdot \mathbf{e}_c(c') = \mathbf{1}_c(e)\). To see this, we rewrite the sum by cases: if \(c' = c\) the summand is \([\! [e \in c]\! ]\), and if \(c' \neq c\) the summand is \(0\) (since \(\mathbf{e}_c(c') = 0\)). Thus the sum telescopes via \(\sum _{c'} [\! [c' = c]\! ] \cdot [\! [e \in c']\! ] = [\! [e \in c]\! ]\) by evaluating at the unique term \(c' = c\).

Substituting this into the boundary map expression, for each edge \(e\) we replace the inner sum by \(\mathbf{1}_c(e)\) (splitting on whether \(v \in e\) to handle the outer indicator). The resulting expression is exactly \(\partial (\mathbf{1}_c)(v)\), which equals \(0\) by the theorem boundary_of_cycle_eq_zero.

By extensionality of linear maps, it suffices to show that for every \(\sigma : C \to \mathbb {Z}/2\mathbb {Z}\) and every \(v \in V\), \(\partial (\partial _2(\sigma ))(v) = 0\).

Expanding the definitions, the left-hand side is

We rewrite each summand: when \(v \in e\), the inner expression is \(\sum _c [\! [e \in c]\! ] \cdot \sigma (c)\); when \(v \notin e\), the summand is \(0\). Combining the conditions, each summand becomes \(\sum _c [\! [e \in c \land v \in e]\! ] \cdot \sigma (c)\).

Swapping the order of summation, we obtain \(\sum _{c \in C} \sum _{e \in E} [\! [e \in c \land v \in e]\! ] \cdot \sigma (c)\). For each fixed \(c\), we factor out \(\sigma (c)\) to get \(\sigma (c) \cdot \sum _{e \in E} [\! [e \in c \land v \in e]\! ]\). The inner sum \(\sum _{e} [\! [e \in c \land v \in e]\! ] = |\{ e \in E : e \in c \land v \in e\} |\) counts edges of \(c\) incident to \(v\), which is even by hypothesis. Therefore in \(\mathbb {Z}/2\mathbb {Z}\) this count is \(0\), and each term \(\sigma (c) \cdot 0 = 0\). Summing over all \(c\) gives \(0\).

By the characterization of range contained in kernel via composition, it suffices to show \(\partial \circ \partial _2 = 0\), which is exactly the chain complex property established in the previous theorem.

By extensionality, it suffices to show that for every \(f : V \to \mathbb {Z}/2\mathbb {Z}\) and every \(c \in C\), \(\delta _2(\delta (f))(c) = 0\). Expanding the definitions, the left-hand side equals \(\sum _{e \in E} [\! [e \in c]\! ] \cdot (\delta f)(e)\).

Let \(\mathbf{1}_c : E \to \mathbb {Z}/2\mathbb {Z}\) be the indicator function of cycle \(c\). We rewrite the sum as \(\sum _e (\delta f)(e) \cdot \mathbf{1}_c(e)\). By the transpose identity \(\sum _e (\delta f)(e) \cdot g(e) = \sum _v f(v) \cdot (\partial g)(v)\), this equals \(\sum _v f(v) \cdot (\partial \mathbf{1}_c)(v)\).

Since each vertex is incident to an even number of edges of each cycle, by the theorem boundary_of_cycle_eq_zero, \((\partial \mathbf{1}_c)(v) = 0\) for all \(v\). Therefore the right-hand side becomes \(\sum _v f(v) \cdot 0 = 0\).

It remains to verify that the original goal (which after simplification involves \(\operatorname {Sym2.lift}\) applied to edge terms) agrees with the coboundary map formulation. This is checked by a straightforward computation showing both expressions agree on each summand. Combining these equalities completes the proof.

By the characterization of range contained in kernel, it suffices to show \(\delta _2 \circ \delta = 0\), which is the coboundary chain complex property established above.

We must show \(\delta (\mathbf{1}) = 0\), i.e., for every edge \(e \in E\), \((\delta \mathbf{1})(e) = 0\). By the membership criterion for the kernel and extensionality, it suffices to check each edge. For an edge \(e = \{ a, b\} \), we use induction on \(\operatorname {Sym2}\) to reduce to the case \(e = s(a,b)\). Then \((\delta \mathbf{1})(e) = \mathbf{1}(a) + \mathbf{1}(b) = 1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), since in characteristic \(2\), any element added to itself is zero.

We verify \(\delta (f) = 0\) by extensionality over edges. For each edge \(e = \{ x, y\} \), using induction on \(\operatorname {Sym2}\), we have \((\delta f)(e) = f(x) + f(y) = a + a = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), since \(a + a = 0\) in characteristic \(2\).

Since \(f \in \ker (\delta )\), we have \(\delta (f) = 0\). Because \(a\) and \(b\) are adjacent, \(e = s(a,b) \in E\). Evaluating \(\delta (f)\) at \(e\) gives \((\delta f)(e) = f(a) + f(b) = 0\) in \(\mathbb {Z}/2\mathbb {Z}\). By the characterization of addition in \(\mathbb {Z}/2\mathbb {Z}\), \(f(a) + f(b) = 0\) implies \(f(a) = f(b)\).

We proceed by induction on the walk \(p\).

Base case (\(p\) is the nil walk, \(u = w\)): The equality \(f(u) = f(w)\) holds by reflexivity.

Inductive step (\(p\) is a cons walk \(u \to v \to \cdots \to w\) where \(u\) is adjacent to \(v\)): By the previous theorem, \(f(u) = f(v)\) since \(u\) and \(v\) are adjacent. By the induction hypothesis applied to the sub-walk from \(v\) to \(w\), \(f(v) = f(w)\). Combining by transitivity gives \(f(u) = f(w)\).

From the reachability hypothesis, we obtain a walk \(p\) from \(u\) to \(w\). The result follows directly from the theorem that \(f\) is constant along walks.

Since \(G\) is connected, the vertex set is nonempty; let \(v_0 \in V\). We claim \(a = f(v_0)\) works. By extensionality, for any \(w \in V\), since \(G\) is connected, \(v_0\) and \(w\) are reachable. By the theorem that \(f\) is constant on reachable vertices, \(f(v_0) = f(w)\). Taking the symmetric equality gives \(f(w) = f(v_0) = a\) for all \(w\).

We prove both directions.

\((\Rightarrow )\): Suppose \(f \in \ker (\delta )\). By the theorem that kernel elements of connected graphs are constant, there exists \(a \in \mathbb {Z}/2\mathbb {Z}\) such that \(f(v) = a\) for all \(v\). Since \(\mathbb {Z}/2\mathbb {Z} = \{ 0, 1\} \), we have \(a = 0\) or \(a = 1\) (verified by case analysis on the finite type). If \(a = 0\), then \(f = 0\) by extensionality. If \(a = 1\), then \(f = \mathbf{1}\) by extensionality and the definition of \(\mathbf{1}\).

\((\Leftarrow )\): If \(f = 0\), then \(f \in \ker (\delta )\) since the kernel is a submodule (containing \(0\)). If \(f = \mathbf{1}\), then \(f \in \ker (\delta )\) by the theorem that \(\mathbf{1} \in \ker (\delta )\).

Suppose for contradiction that \(\ker (\delta ) = \{ 0\} \) (i.e., the kernel is the bottom submodule). The all-ones vector \(\mathbf{1}\) lies in \(\ker (\delta )\) by the previously established theorem. By our assumption, \(\mathbf{1} = 0\) as functions \(V \to \mathbb {Z}/2\mathbb {Z}\). Since \(V\) is nonempty, let \(v \in V\). Evaluating at \(v\) gives \(\mathbf{1}(v) = 0(v)\), i.e., \(1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\). By the definition of \(\mathbf{1}\), this simplifies to a contradiction.

By the chain complex property \(\partial \circ \partial _2 = 0\), we have \((\partial \circ \partial _2)(\sigma ) = 0(\sigma ) = 0\), which is exactly \(\partial (\partial _2(\sigma )) = 0\). The proof rewrites the goal as the application of the composition and then applies the chain complex theorem.

By the coboundary chain complex property \(\delta _2 \circ \delta = 0\), we have \((\delta _2 \circ \delta )(f) = 0(f) = 0\), which is exactly \(\delta _2(\delta (f)) = 0\). The proof rewrites the goal as the application of the composition and then applies the coboundary chain complex theorem.