Unfolding the definition of \(\operatorname {fluxComm}\), we rewrite using the characterization of zero in \(\mathbb {Z}/2\mathbb {Z}\) via evenness, and then apply the equivalence between evenness and divisibility by \(2\).

This follows by simplification using the definition of \(\mathrm{isOneCocycle}\) and the pointwise equivalence from Theorem 786.

We rewrite the coboundary map at edge \(e\) using \(\delta (f)(e) = \sum _{v \in \{ v_1, v_2\} } f(v)\) where \(v_1, v_2\) are the endpoints of \(e\) (which are distinct by the edge endpoints property). Let \(v_1 = (\mathrm{edgeEndpoints}\; e).1\) and \(v_2 = (\mathrm{edgeEndpoints}\; e).2\). We compute the sum \(\mathbf{1}_S(v_1) + \mathbf{1}_S(v_2)\) over \(\mathbb {Z}/2\mathbb {Z}\) by case splitting on membership of \(v_1\) and \(v_2\) in \(S\):

• \(v_1 \in S\), \(v_2 \in S\): not in cut, sum \(= 1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\).

• \(v_1 \in S\), \(v_2 \notin S\): in cut, sum \(= 1 + 0 = 1\).

• \(v_1 \notin S\), \(v_2 \in S\): in cut, sum \(= 0 + 1 = 1\).

• \(v_1 \notin S\), \(v_2 \notin S\): not in cut, sum \(= 0 + 0 = 0\).

In each case the result matches the indicator of the vertex cut, as required.

Let \(f : E \to \mathbb {Z}/2\mathbb {Z}\) be the characteristic function of \(S_X^E\). We first show \(f \in \ker (\delta _2)\): by extensionality at each cycle \(c\), the value \(\delta _2(f)(c) = \sum _{e \in c} f(e)\) equals \(|S_X^E \cap c| \pmod{2}\). We compute this sum by splitting \(c\) into edges in \(S_X^E\) (contributing \(|S_X^E \cap c|\) copies of \(1\)) and edges not in \(S_X^E\) (contributing \(0\)), obtaining \(\sum = |S_X^E \cap c|\) in \(\mathbb {Z}/2\mathbb {Z}\). The cocycle condition and Theorem 786 give \(|S_X^E \cap c| \equiv 0 \pmod{2}\), hence \(\delta _2(f)(c) = 0\).

By the exactness condition (cuts generate), \(f \in \operatorname {im}(\delta )\), so there exists \(g : V \to \mathbb {Z}/2\mathbb {Z}\) with \(\delta (g) = f\). We set \(S = \{ v \in V \mid g(v) = 1\} \). For each edge \(e\), we have \(\delta (g)(e) = f(e) = \mathbf{1}_{S_X^E}(e)\).

It remains to show \(\delta (g)(e) = \mathbf{1}_{\partial S}(e)\). Writing the coboundary as \(\delta (g)(e) = g(v_1) + g(v_2)\) for the endpoints \(v_1, v_2\) of \(e\), we case-split on whether \(g(v_1) = 1\) and \(g(v_2) = 1\) (using the fact that in \(\mathbb {Z}/2\mathbb {Z}\), every element is \(0\) or \(1\)). In each of the four cases, we verify that the sum matches the indicator of the vertex cut \(\partial S\), completing the proof.

By definition, \(\bar{L}.S_X^E = L.S_X^E \, \triangle \, \partial S\). Since \(L.S_X^E = \partial S\) by hypothesis, this equals \(\partial S \, \triangle \, \partial S = \emptyset \).

We convert the nontriviality condition: \(\bar{L}|_V\) has nonempty support, so the corresponding \(\mathrm{OriginalCodeOperator}\) is nontrivial. We then apply the code distance property \(\mathrm{code.logical\_ weight\_ bound}\) to the cleaned-to-original operator, using the hypotheses that it is a logical and nontrivial. The weight equality \(\mathrm{cleanedToOriginalOp\_ weight}\) converts the result to the vertex weight of the cleaned operator.

Since \(S\) is nonempty, \(|S| {\gt} 0\). We compute:

where the inequality follows from \(h_G \le |\partial S|/|S|\) and \(|S| {\gt} 0\).

If \(2|S| \le |V|\), take \(S' = S\). Otherwise, take \(S' = V \setminus S\). The vertex cut of the complement equals the vertex cut of \(S\) (an edge crosses the boundary of \(S\) if and only if it crosses the boundary of \(V \setminus S\)), and \(|V \setminus S| = |V| - |S|\) satisfies \(2|V \setminus S| \le |V|\) by integer arithmetic.

This follows since \(\min (h_G, 1) \ge \min (0, 0) = 0\) using \(h_G \ge 0\) and \(1 \ge 0\).

This is immediate from \(\min (h_G, 1) \le 1\).

We case-split on whether \(h_G \ge 1\).

Case \(h_G \ge 1\): Then \(\min (h_G, 1) = 1\). We have

Therefore \(\mathrm{cleanedWeight} - \mathrm{cleaningSetSize} + \mathrm{boundarySize} \ge \mathrm{cleanedWeight} \ge d = 1 \cdot d\), as required.

Case \(h_G {\lt} 1\): Then \(\min (h_G, 1) = h_G\). We compute:

Step 3: By exactness (Theorem 789), the cocycle condition on \(L.S_X^E\) yields a vertex set \(S_0\) with \(\mathbf{1}_{S_X^E} = \mathbf{1}_{\partial S_0}\).

Step 7a: By Theorem 793, we choose \(S\) with \(\partial S = \partial S_0\) and \(2|S| \le |V|\).

We derive \(L.S_X^E = \partial S\) by showing membership equivalence: for each edge \(e\), the characteristic function equations force \(e \in S_X^E \Leftrightarrow e \in \partial S\) (using the fact that \(1 \ne 0\) and \(0 \ne 1\) in \(\mathbb {Z}/2\mathbb {Z}\)).

From the deformed logical operator structure, we obtain:

• \(\bar{L}|_V\) is nontrivial (Step 6 — the cleaned vertex nontriviality field).

• \(\bar{L}|_V\) is a logical of the original code (Step 5 — the cleaned is original logical field).

Steps 5–6: By Theorem 791, \(|\bar{L}|_V| \ge d\).

Case \(S = \emptyset \): When \(S\) is empty, the cleaned operator equals \(L\) on vertices (symmetric difference with \(\emptyset \) is identity), and vertex weight \(\le \) total weight, so \(|L'| \ge d\). Since \(\min (h_G, 1) \le 1\) and \(d {\gt} 0\), we get \(|L'| \ge d \ge \min (h_G, 1) \cdot d\).

Case \(S \ne \emptyset \): We obtain the Cheeger bound \(|\partial S| \ge h_G \cdot |S|\) from the hypothesis. The weight bound hypothesis gives \(|L'| \ge |\bar{L}|_V| - |S| + |\partial S|\) in natural numbers.

We then case-split on whether \(|S| \le |\bar{L}|_V|\):

• If \(|S| \le |\bar{L}|_V|\): we apply the core weight inequality (Theorem 796) with \(\mathrm{cleanedWeight} = |\bar{L}|_V|\), \(\mathrm{cleaningSetSize} = |S|\), \(\mathrm{boundarySize} = |\partial S|\). Converting the natural number inequality to real numbers (the subtraction does not truncate since \(|S| \le |\bar{L}|_V|\)), we obtain \(|L'| \ge \min (h_G, 1) \cdot d\).

• If \(|S| {\gt} |\bar{L}|_V|\): the natural subtraction \(|\bar{L}|_V| - |S|\) truncates to \(0\), so \(|L'| \ge |\partial S|\). Since \(|S| {\gt} |\bar{L}|_V| \ge d\), we have \(|S| {\gt} d\). If \(h_G \le 1\), then \(|L'| \ge |\partial S| \ge h_G \cdot |S| {\gt} h_G \cdot d = \min (h_G, 1) \cdot d\) (handling \(h_G = 0\) separately). If \(h_G {\gt} 1\), then \(|L'| \ge h_G \cdot |S| {\gt} h_G \cdot d \ge 1 \cdot d = d = \min (h_G, 1) \cdot d\).

Unfolding the definition of \(d^* = \inf \{ |L| \mid L \in \mathrm{logicals}\} \), the set of weights is nonempty (since logicals is nonempty). By the natural number infimum property, the infimum is attained by some \(L \in \mathrm{logicals}\). We then apply Theorem 797 to this \(L\) to conclude \(d^* = |L| \ge \min (h(G), 1) \cdot d\).

We apply Theorem 798 with \(h_G \ge 1\), noting that \(h_G \ge 0\) follows from \(h_G \ge 1 \ge 0\). The result gives \(d^* \ge \min (h_G, 1) \cdot d\). Since \(h_G \ge 1\), we have \(\min (h_G, 1) = 1\), so \(d^* \ge 1 \cdot d = d\). Converting from the real-number inequality back to natural numbers completes the proof.