This is verified by computation in \(\mathbb {Z}/2\mathbb {Z}\).

By extensionality, it suffices to show \(\delta (\mathbf{1})(e) = 0\) for an arbitrary edge \(e\). Using the formula \(\delta (\mathbf{1})(e) = \sum _{v \in \operatorname {edgeVertices}(e)} \mathbf{1}(v)\) and the definition of \(\mathbf{1}\), we expand the sum. Since the endpoints of \(e\) are distinct (by edge_endpoints_ne), we have \(\operatorname {edgeVertices}(e) = \{ v_1, v_2\} \) with \(v_1 \neq v_2\). Rewriting the membership set as a pair and applying the pair-sum formula, we obtain \(\delta (\mathbf{1})(e) = 1 + 1 = 0\) in \(\mathbb {F}_2\), verified by computation.

We note that \(\mathbf{0} = 0\) by definition. Rewriting with this, the result follows directly from \(\delta \) being a linear map: \(\delta (0) = 0\) by map_zero.

This is the conjunction of zero_in_ker_coboundary and allOnes_in_ker_coboundary.

Assume \(f = 0 \lor f = \mathbf{1}\). We decompose by cases:

• If \(f = 0\): the result follows from zero_in_ker_coboundary.

• If \(f = \mathbf{1}\): the result follows from allOnes_in_ker_coboundary.

Suppose for contradiction that \(\mathbf{1} = 0\). Evaluating at an arbitrary vertex \(v_0 \in V\) (which exists since \(V\) is nonempty), we obtain \(1 = 0\) in \(\mathbb {F}_2\) by simplification using the definition of \(\mathbf{1}\), which is a contradiction.

Take \(f = \mathbf{1}\). Then \(f \neq 0\) by allOnesV_ne_zero, and \(\delta (f) = 0\) by allOnes_in_ker_coboundary.

We rewrite using the formula \(\delta (f)(e) = \sum _{v \in \operatorname {edgeVertices}(e)} f(v)\). Since the endpoints are distinct (\(v_1 \neq v_2\) by edge_endpoints_ne), and \(\operatorname {edgeVertices}(e) = \{ v_1, v_2\} \) by definition, we apply the pair-sum formula to obtain \(\delta (f)(e) = f(v_1) + f(v_2)\).

We prove both directions. \((\Rightarrow )\): Assume \(a + b = 0\). Adding \(b\) to both sides gives \(a + b + b = b\). Since \(b + b = 0\) in \(\mathbb {F}_2\) (verified by case analysis on \(b\)), we have \(a + 0 = b\) by associativity, hence \(a = b\). \((\Leftarrow )\): Assume \(a = b\). Rewriting, we need \(b + b = 0\), which holds by case analysis on \(b \in \{ 0, 1\} \) in \(\mathbb {F}_2\).

Rewriting using the edge formula \(\delta (f)(e) = f(v_1) + f(v_2)\), the result follows from the characterization \(a + b = 0 \iff a = b\) in \(\mathbb {F}_2\).

Rewriting using the edge formula, \(\delta (\mathbf{1})(e) = \mathbf{1}(v_1) + \mathbf{1}(v_2) = 1 + 1\). By the definition of \(\mathbf{1}\) and computation in \(\mathbb {F}_2\), this equals \(0\).

By extensionality, let \(v\) be an arbitrary vertex. We simplify using the boundary formula. We establish that the sum \(\sum _{e \in \operatorname {incidentEdges}(v)} \mathbf{1}_S(e)\) equals the cardinality \(|S \cap \operatorname {incidentEdges}(v)|\) cast to \(\mathbb {F}_2\): this follows by rewriting the sum via the filter-sum identity \(\sum _{e \in A} [e \in S] = |A \cap S|\) and using the constant sum formula with natural number cast. The filter sets \(\{ e \in \operatorname {incidentEdges}(v) \mid e \in S\} \) and \(\{ e \in S \mid e \text{ incident to } v\} \) are equal by extensionality and logical equivalence. Since \(S\) is a valid cycle, this cardinality is even. The even natural number casts to \(0\) in \(\mathbb {F}_2\).

By linear map extensionality, let \(\mathbf{c} \in \mathbb {F}_2^C\) be arbitrary, and let \(w \in V\) be an arbitrary vertex. We show \((\partial \circ \partial _2)(\mathbf{c})(w) = 0\). Expanding, we rewrite using the boundary formula at vertex \(w\) and the boundary-2 map formula. After simplification, we exchange the order of summation (sum over edges first, then cycles, becomes sum over cycles first). For each cycle \(c\), we compute the inner sum \(\sum _{e \in \operatorname {incidentEdges}(w)} \mathbf{c}(c) \cdot \partial _2(\mathbf{e}_c)(e)\). Factoring out \(\mathbf{c}(c)\), this equals \(\mathbf{c}(c) \cdot |\{ e \in \operatorname {cycles}(c) \mid e \text{ incident to } w\} |\), where we use the filter-sum identity and the indicator function for cycle membership. Since each cycle is valid, the cardinality \(|\{ e \in \operatorname {cycles}(c) \mid e \text{ incident to } w\} |\) is even. An even natural number casts to \(0\) in \(\mathbb {F}_2\), so each term becomes \(\mathbf{c}(c) \cdot 0 = 0\). The sum of zeros is zero.

From the chain complex property \(\partial \circ \partial _2 = 0\), we evaluate at \(\mathbf{c}\): \((\partial \circ \partial _2)(\mathbf{c}) = 0\). Simplifying the composition gives \(\partial (\partial _2(\mathbf{c})) = 0\).

This is immediate from the definition of valid cycle edge set applied to vertex \(v\).

By linear map extensionality, let \(\mathbf{v} \in \mathbb {F}_2^V\) be an arbitrary vertex-vector, and let \(c\) be an arbitrary cycle index. We show \((\delta _2 \circ \delta )(\mathbf{v})(c) = 0\). Expanding using the coboundary-2 formula, we need \(\sum _{e \in \operatorname {cycles}(c)} \delta (\mathbf{v})(e) = 0\).

Using the edge formula, each \(\delta (\mathbf{v})(e) = \mathbf{v}(v_1^e) + \mathbf{v}(v_2^e)\) where \(v_1^e, v_2^e\) are the endpoints of \(e\). We distribute the sum:

We rewrite each sum using fiberwise summation: grouping edges by their first (resp. second) endpoint \(v\), we obtain

Combining these sums, we factor out \(\mathbf{v}(v)\) for each vertex \(v\). The key observation is that for each \(v\), the sets \(\{ e \mid v_1^e = v\} \) and \(\{ e \mid v_2^e = v\} \) are disjoint (since \(v_1^e \neq v_2^e\) by edge_endpoints_ne), and their union equals \(\{ e \in \operatorname {cycles}(c) \mid e \text{ incident to } v\} \). Thus the sum of cardinalities equals the total incident count.

Since cycles are valid, each vertex has even incident count in the cycle. The sum of the two cardinalities cast to \(\mathbb {F}_2\) is therefore \(0\), giving \((|A_v| + |B_v|) \cdot \mathbf{v}(v) = 0 \cdot \mathbf{v}(v) = 0\) for each \(v\). The total sum is zero.

From the cochain complex property \(\delta _2 \circ \delta = 0\), we evaluate at \(\mathbf{v}\): \((\delta _2 \circ \delta )(\mathbf{v}) = 0\). Simplifying the composition gives \(\delta _2(\delta (\mathbf{v})) = 0\).

Unfolding the definition of \(\operatorname {deg}_2\), this is exactly the formula for \(\partial (f)(v)\) given by boundaryMap_apply_vertex.

We prove both directions. \((\Rightarrow )\): Assume \(\partial (f) = 0\) and let \(v\) be arbitrary. From \(\partial (f) = 0\), evaluating at \(v\) gives \(\partial (f)(v) = 0\). Rewriting using the equality \(\partial (f)(v) = \operatorname {deg}_2(f, v)\) yields the result. \((\Leftarrow )\): Assume \(\operatorname {deg}_2(f, v) = 0\) for all \(v\). By extensionality, for arbitrary \(v\), rewriting \(\partial (f)(v) = \operatorname {deg}_2(f, v) = 0\) gives \(\partial (f) = 0\).

This is identical to boundary_zero_iff_all_degrees_zero.

From the adjacency \(v \sim w\), we obtain an edge \(e\) connecting them. Since \(\delta (f) = 0\), evaluating at \(e\) gives \(\delta (f)(e) = 0\). By the characterization coboundaryMap_zero_at_edge_iff, this means \(f(v_1^e) = f(v_2^e)\) where \(v_1^e, v_2^e\) are the endpoints of \(e\).

We consider two cases for the adjacency witness: either \((v_1^e, v_2^e) = (v, w)\) or \((v_1^e, v_2^e) = (w, v)\). In the first case, \(f(v) = f(w)\) directly. In the second case, \(f(w) = f(v)\) and we take the symmetric equality.

Let \(v, w \in V\). By connectedness, \(w\) is reachable from \(v\) by the reflexive-transitive closure of the adjacency relation. We proceed by induction on the reachability proof.

Base case (reflexivity): \(v = w\), so \(f(v) = f(w)\) by reflexivity.

Inductive step: Suppose \(v\) reaches some vertex \(u\) (with \(f(v) = f(u)\) by the inductive hypothesis) and \(u \sim w\). By ker_coboundary_constant_on_adjacent, \(f(u) = f(w)\). By transitivity, \(f(v) = f(w)\).

By case analysis on \(x \in \mathbb {F}_2\) (which has exactly two elements), followed by simplification.

We consider whether \(V\) is nonempty.

Case 1: \(V\) is nonempty. Choose some \(v_0 \in V\). By ker_coboundary_constant_of_connected, \(f\) is constant: \(f(v) = f(v_0)\) for all \(v\). By the \(\mathbb {F}_2\) dichotomy, \(f(v_0) = 0\) or \(f(v_0) = 1\).

• If \(f(v_0) = 0\): then \(f(v) = 0\) for all \(v\), so \(f = 0\) by extensionality and simplification.

• If \(f(v_0) = 1\): then \(f(v) = 1\) for all \(v\), so \(f = \mathbf{1}\) by extensionality and simplification using the definition of \(\mathbf{1}\).

Case 2: \(V\) is empty. Then \(f = 0\) vacuously, since for any \(v\), the hypothesis that \(V\) is empty yields a contradiction.

This follows directly from ker_coboundary_classification.

We prove both directions. \((\Rightarrow )\): This is ker_coboundary_classification. \((\Leftarrow )\): We decompose the disjunction. If \(f = 0\), then \(\delta (0) = 0\) by zero_in_ker_coboundary. If \(f = \mathbf{1}\), then \(\delta (\mathbf{1}) = 0\) by allOnes_in_ker_coboundary.

We prove both directions. \((\Rightarrow )\): Suppose \(\partial _2(g) = f\) for some \(g\). Rewriting, \(\partial (f) = \partial (\partial _2(g)) = 0\) by im_boundary2_subset_ker_boundary. \((\Leftarrow )\): This is exactly the cycle generation property applied to \(f\).

We prove both directions. \((\Rightarrow )\): Suppose \(\delta (g) = f\) for some \(g\). Rewriting, \(\delta _2(f) = \delta _2(\delta (g)) = 0\) by im_coboundary_subset_ker_coboundary2. \((\Leftarrow )\): This is exactly the cut generation property applied to \(f\).

This follows directly from ker_coboundary_iff.