We unfold the definition of \(\partial \gamma \) using the boundary map applied at vertex \(v\). We establish that \(\mathrm{incidentEdges}(v) \cap \gamma = \gamma .\mathrm{filter}(\text{isIncident to } v)\) by extensionality, using the definition of incident edges and basic set membership. On the left-hand side, we rewrite using the edge-path vector definition. We then split the sum over \(\mathrm{incidentEdges}(v)\) into edges in \(\gamma \) and edges not in \(\gamma \). For edges \(e\) in the filter with \(e \in \gamma \), the indicator \(\mathbf{1}_{e \in \gamma }\) equals \(1\), so the first sum equals \(\sum _{e \in \mathrm{incidentEdges}(v) \cap \gamma } 1\). For edges \(e\) not in \(\gamma \), the indicator is \(0\), so the second sum equals \(0\). Adding, we get \(\sum _{e \in \mathrm{incidentEdges}(v) \cap \gamma } 1 + 0\). Finally, we rewrite the filter set as \(\gamma .\mathrm{filter}(\text{isIncident to } v)\) by extensionality.

We rewrite using the edge path boundary formula. The sum \(\sum _{e \in \gamma \cap \mathrm{inc}(v)} 1\) equals \(|\gamma \cap \mathrm{inc}(v)|\) cast into \(\mathbb {Z}_2\). For the forward direction, we extract the \(\mathbb {Z}_2\)-value using ZMod.val, yielding \(|\gamma \cap \mathrm{inc}(v)| \bmod 2 = 1\). For the reverse direction, given \(|\gamma \cap \mathrm{inc}(v)| \bmod 2 = 1\), we use the fact that the natural number cast to \(\mathbb {Z}_2\) equals the cast of its residue modulo 2, rewrite with the hypothesis, and conclude by reflexivity.

We rewrite using the edge path boundary formula. The sum \(\sum _{e \in \gamma \cap \mathrm{inc}(v)} 1\) equals \(|\gamma \cap \mathrm{inc}(v)|\) cast into \(\mathbb {Z}_2\). For the forward direction, we extract the \(\mathbb {Z}_2\)-value using ZMod.val, obtaining \(|\gamma \cap \mathrm{inc}(v)| \bmod 2 = 0\). For the reverse direction, given \(|\gamma \cap \mathrm{inc}(v)| \bmod 2 = 0\), we use the fact that the natural number cast to \(\mathbb {Z}_2\) equals the cast of its residue modulo 2, rewrite with the hypothesis, and conclude by reflexivity.

We unfold the definition of IsValidDeformingPath. For the forward direction, given the function equality \(\partial \gamma = \mathbf{s}_S\), we apply it at an arbitrary vertex \(v\) using congrFun. For the reverse direction, given pointwise equality \(\forall v, (\partial \gamma )(v) = \mathbf{s}_S(v)\), we conclude function equality by extensionality.

We rewrite the valid path condition using the pointwise characterization. Then \((\partial \gamma )(v) = \mathbf{s}_S(v)\), and since \(v \in S\), we have \(\mathbf{s}_S(v) = 1\).

We rewrite the valid path condition using the pointwise characterization. Then \((\partial \gamma )(v) = \mathbf{s}_S(v)\), and since \(v \notin S\), we have \(\mathbf{s}_S(v) = 0\).

We unfold \(\partial \gamma \) and compute:

where the exchange of summation order uses the equivalence that \(e\) is incident to \(v\) if and only if \(v\) is an endpoint of \(e\). For each edge \(e\) with endpoints \(v_1, v_2\) (which are distinct by the graph axiom \(v_1 \neq v_2\)), we have \(\mathrm{endpoints}(e) = \{ v_1, v_2\} \). Thus

The total sum becomes \(\sum _{e \in E} (\boldsymbol {\gamma }(e) + \boldsymbol {\gamma }(e)) = 0\), since \(a + a = 0\) in \(\mathbb {Z}_2\) for all \(a\).

Let \(\gamma \) be a valid deforming path for \(S\). By the boundary sum theorem, \(\sum _{v \in V} (\partial \gamma )(v) = 0\) in \(\mathbb {Z}_2\). Since \(\gamma \) is a valid path, \((\partial \gamma )(v) = \mathbf{s}_S(v)\) for all \(v\) (by the pointwise characterization). We compute

where the first equality splits the sum into vertices in \(S\) (contributing \(1\)) and vertices not in \(S\) (contributing \(0\)). The filter of \(\mathrm{univ}\) by membership in \(S\) equals \(S\) itself, and the sum of zeros vanishes. Substituting into the boundary sum equation gives \(|S| = 0\) in \(\mathbb {Z}_2\). Extracting the \(\mathbb {Z}_2\)-value yields \(|S| \bmod 2 = 0\).

Suppose for contradiction that there exists a valid deforming path \(\gamma \) for \(S\). Decomposing the existential, let \(\gamma \) be such a path with \(h_\gamma \) witnessing validity. By the even \(Z\)-support theorem, \(|S| \bmod 2 = 0\). But we assumed \(|S| \bmod 2 = 1\), which is a contradiction by integer arithmetic.

This holds by reflexivity of the biconditional.

This holds by reflexivity (it is the definition of the deformed operator’s edge \(Z\)-support).

We consider four cases based on membership of \(e\) in \(S\) and \(T\):

1. \(e \in S\) and \(e \in T\): Then \(e \notin S \triangle T\) (since symmetric difference excludes elements in both), so the left side is \(0\). The right side is \(1 + 1 = 0\) in \(\mathbb {Z}_2\) (by the self-addition lemma \(a + a = 0\)).

2. \(e \in S\) and \(e \notin T\): Then \(e \in S \triangle T\), so both sides equal \(1 + 0 = 1\).

3. \(e \notin S\) and \(e \in T\): Then \(e \in S \triangle T\), so both sides equal \(0 + 1 = 1\).

4. \(e \notin S\) and \(e \notin T\): Then \(e \notin S \triangle T\), so both sides equal \(0 + 0 = 0\).

In each case the equality holds by simplification.

We rewrite the deformed operator’s edge \(Z\)-support as the symmetric difference \(S_Z^E(P) \triangle \gamma \) using the previous lemma, then apply the symmetric difference vector identity.

We unfold the simplified symplectic form and use the pointwise characterization of the valid path condition. Let \(v\) be an arbitrary vertex. We have \((\partial \gamma )(v) = \mathbf{s}_{S_Z^V}(v)\).

Case 1: \(v \in S_Z^V\). Then \(\mathbf{1}_{v \in S_Z^V} = 1\). By the valid path condition, \(\mathbf{s}_{S_Z^V}(v) = 1\), so \((\partial \gamma )(v) = 1\). By the boundary-one characterization, \(|\{ e \in \gamma \mid e \text{ incident to } v\} | \equiv 1 \pmod{2}\). We establish that \(\gamma \cap \mathrm{inc}(v) = \gamma .\mathrm{filter}(\text{isIncident to } v)\) by extensionality using the definition of incident edges. Therefore \(\omega = 1 + |\gamma \cap \mathrm{inc}(v)|\) where \(|\gamma \cap \mathrm{inc}(v)|\) is odd, so \(\omega \) is even. This follows by integer arithmetic (omega).

Case 2: \(v \notin S_Z^V\). Then \(\mathbf{1}_{v \in S_Z^V} = 0\). By the valid path condition, \(\mathbf{s}_{S_Z^V}(v) = 0\), so \((\partial \gamma )(v) = 0\). By the boundary-zero characterization, \(|\{ e \in \gamma \mid e \text{ incident to } v\} | \equiv 0 \pmod{2}\). Again \(\gamma \cap \mathrm{inc}(v) = \gamma .\mathrm{filter}(\text{isIncident to } v)\). Therefore \(\omega = 0 + |\gamma \cap \mathrm{inc}(v)|\) where \(|\gamma \cap \mathrm{inc}(v)|\) is even, so \(\omega \equiv 0 \pmod{2}\).

Let \(v\) be an arbitrary vertex. The result follows directly from the previous theorem applied to \(S_Z^V(P)\), \(\gamma \), the valid path hypothesis, and \(v\).

This follows directly from the theorem no_valid_path_if_odd.

This follows directly from the theorem zSupport_even_of_valid_path_exists.

This holds by reflexivity (definitional equality).

This holds by reflexivity (definitional equality).

This holds by reflexivity (definitional equality).

This holds by reflexivity (definitional equality).

This holds by reflexivity, since \(S_Z^V(\tilde{P}) = S_Z^V(P)\) and the proof of evenness is the same.

We argue by finiteness. Let \(\mathcal{V} = \{ \gamma \mid \text{IsValidDeformingPath}(G, S_Z^V, \gamma )\} \) be the set of valid paths. By hypothesis, \(\mathcal{V}\) is nonempty. Since \(\mathcal{V}\) is a subset of the powerset of \(E\) (which is a finite type), \(\mathcal{V}\) is finite. We convert \(\mathcal{V}\) to a finite set \(S\), which is nonempty.

Consider the image \(\mathrm{cards} = \{ |\gamma | \mid \gamma \in S\} \), which is nonempty since \(S\) is nonempty. Let \(m = \min (\mathrm{cards})\) be the minimum cardinality. Since \(m \in \mathrm{cards}\), there exists \(\gamma _{\min } \in S\) with \(|\gamma _{\min }| = m\).

We claim \(\gamma _{\min }\) is a minimum-weight valid path. First, \(\gamma _{\min } \in S\) means it is a valid deforming path. Second, for any other valid path \(\gamma '\), we have \(\gamma ' \in S\), so \(|\gamma '| \in \mathrm{cards}\), and therefore \(m \leq |\gamma '|\). Since \(|\gamma _{\min }| = m\), we conclude \(|\gamma _{\min }| \leq |\gamma '|\), establishing the minimum weight property.