Let \(h_{\mathrm{comm}} := h_{L,\mathrm{comm}}(i)\) be the commutation condition \(\langle L, C.\operatorname {check}(i) \rangle _{\mathrm{symp}} = 0\). Unfolding the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\), and using that \(L.\operatorname {zVec} = 0\) and \((C.\operatorname {check}(i)).\operatorname {xVec} = 0\) (since \(i\) is \(Z\)-type), the symplectic inner product simplifies to \(\sum _q L.\operatorname {xVec}(q) \cdot (C.\operatorname {check}(i)).\operatorname {zVec}(q) = 0\). We rewrite the cardinality condition using \(\operatorname {natCast\_ eq\_ zero\_ iff\_ even}\), express the cardinality as a sum of ones over the filter, and push the cast. We then show the sums agree by extensionality: for each \(q\), we case-split on whether \(L.\operatorname {xVec}(q) = 0\) and whether \((C.\operatorname {check}(i)).\operatorname {zVec}(q) = 0\). Over \(\mathbb {Z}_2\), each nonzero element equals \(1\), so both sides of the summand agree in all cases.

Unfolding \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\), we apply the helper lemma that computes the symplectic inner product of \(\operatorname {prodX}(S)\) with a \(Z\)-type check as a filtered sum. The result then follows by rewriting the even-cardinality condition via \(\operatorname {natCast\_ eq\_ zero\_ iff\_ even}\), expressing the cardinality as a sum of ones over the filter, and pushing the cast. The two sides are definitionally equal.

Let \(i\) be any check index. By the CSS property, check \(i\) is either pure \(X\)-type or pure \(Z\)-type. In the first case, \(\operatorname {prodX}(S)\) commutes with it by the pure-\(X\)/pure-\(X\) commutation lemma (since \(\operatorname {prodX}(S)\) has zero \(Z\)-vector). In the second case, the check is \(Z\)-type, and commutation follows from the even overlap hypothesis via \(\operatorname {prodX\_ commutes\_ zCheck\_ iff\_ even}\).

We apply \(\operatorname {prodX\_ centralizer\_ of\_ even\_ overlap}\), using the CSS hypothesis. For each \(Z\)-type check \(j\), the kernel condition \(f \in \ker (\delta )\) gives \(\delta (f)(j) = 0\), which by definition means \(\sum _q [\text{incident}(q,j)] \cdot f(q) = 0\). We rewrite the even-cardinality goal using \(\operatorname {natCast\_ eq\_ zero\_ iff\_ even}\) and express the cardinality as a sum. The two sums are then shown to agree by a summand-by-summand case analysis: for each \(q\), we consider whether \(f(q) = 0\), whether the restricted incidence holds, and whether \(q \in V_L\). Over \(\mathbb {Z}_2\), nonzero values equal \(1\), so the terms match in all cases. If \(q \notin V_L\), the support hypothesis forces \(f(q) = 0\).

We rewrite both maps as matrix multiplication linear maps: \(\partial = M \cdot \) and \(\delta = M^T \cdot \), where \(M\) is the \(\mathbb {Z}_2\) incidence matrix. Applying the rank-nullity theorem \(\operatorname {finrank}(\operatorname {range}(A)) + \operatorname {finrank}(\ker (A)) = \operatorname {finrank}(\text{domain})\) to both \(M\) and \(M^T\), and using \(\operatorname {rank}(M) = \operatorname {rank}(M^T)\) (by \(\operatorname {Matrix.rank\_ transpose}\)), the result follows by linear arithmetic (omega).

From the \(\mathbb {Z}_2\) rank-nullity formula and the hypothesis \(|E_0| \le |V_0|\), we obtain \(\dim (\ker (\delta )) \ge 2\). We then apply the submodule existence lemma: in a \(\mathbb {Z}_2\)-submodule of \(\operatorname {finrank} \ge 2\), given any element \(w\), there exists \(v \neq 0\) with \(v \neq w\).

Let \(g_1, g_2\) be functions on \(V_L\) with \(\operatorname {liftVL}(g_1) = \operatorname {liftVL}(g_2)\). By extensionality, for any \(\langle q, h_q \rangle \in V_L\), evaluating the equality at \(q\) and using the definition of \(\operatorname {liftVL}\) (which applies \(g\) at \(q\) when \(q \in V_L\)) gives \(g_1(\langle q, h_q \rangle ) = g_2(\langle q, h_q \rangle )\).

We show the coboundary applied to \(\operatorname {liftVL}(g)\) is zero componentwise. For each check index \(j\), we consider two cases. If \(j \in E_L\) (the relevant \(Z\)-checks), we convert between the sum over all qubits \(Q\) (with restricted incidence) and the sum over the subtype \(V_L\) (with core incidence). The key step normalizes the subtype summand, converts the subtype sum to a finset sum via \(\operatorname {sum\_ coe\_ sort}\), then to a full type sum via \(\operatorname {sum\_ ite\_ mem}\), and finally shows summand-by-summand agreement with the restricted incidence formulation. For each qubit \(q\), we case-split on membership in \(V_L\) and on whether the \(Z\)-vector is nonzero, showing agreement in all cases. If \(j \notin E_L\), no vertex is incident to \(j\) (by the definition of relevant checks), so every summand is zero.

We restrict \(\gamma \) and the all-ones vector to the core (subtype) boundary map. Letting \(\gamma _{\mathrm{core}}(i) = \gamma (i_1)\) for \(i \in E_L\) and \(\mathbf{1}_{\mathrm{core}}(i) = 1\), we verify both lie in \(\ker (\operatorname {hyperBoundaryMap}(\operatorname {coreIncident}))\) by converting between the full \(C.I\) sums and subtype sums, matching summands by case analysis on membership and incidence. Since \(\gamma _{\mathrm{core}} \neq 0\) (from \(\gamma \neq 0\) and the support condition) and \(\gamma _{\mathrm{core}} \neq \mathbf{1}_{\mathrm{core}}\) (from \(\gamma \) not being all-ones), over \(\mathbb {Z}_2\) these two nonzero distinct kernel elements force \(\dim (\ker (\partial _{\mathrm{core}})) \ge 2\): if \(\dim \le 1\), by \(\operatorname {finrank\_ le\_ one}\) every element is a scalar multiple of a generator, but over \(\mathbb {Z}_2\) the only nonzero scalar is \(1\), forcing \(\gamma _{\mathrm{core}} = \mathbf{1}_{\mathrm{core}}\), a contradiction. The all-ones function on \(V_L\) lies in \(\ker (\delta _{\mathrm{core}})\) by row evenness. With \(|E_L| \le |V_L|\) and \(\dim (\ker (\partial _{\mathrm{core}})) \ge 2\), \(\operatorname {coboundary\_ third\_ element}\) yields \(g \in \ker (\delta _{\mathrm{core}})\) with \(g \neq 0\) and \(g \neq \mathbf{1}\). We lift \(g\) to \(Q\) via \(\operatorname {liftVL}\): the lift is in \(\ker (\delta )\) by \(\operatorname {liftVL\_ ker\_ coboundary}\), is supported on \(V_L\), is nonzero by injectivity of the lift, and since \(g \neq \mathbf{1}\), there exists \(q \in V_L\) with \(g(q) \neq 1\), hence \(g(q) = 0\) over \(\mathbb {Z}_2\).

Assume \(\gamma \neq 0\). We show \(\gamma \) is all-ones on \(E_L\). Suppose for contradiction that there exists \(i_0 \in E_L\) with \(\gamma (i_0) \neq 1\), so \(\gamma \) is neither zero nor all-ones.

By \(\operatorname {coboundary\_ from\_ boundary\_ step}\), there exists \(f \in \ker (\delta )\) supported on \(V_L\) with \(f \neq 0\) and some \(q \in V_L\) with \(f(q) = 0\). Let \(S = \{ q \mid f(q) \neq 0\} \) and \(T = \{ q \in V_L \mid f(q) = 0\} \).

Since \(f \in \ker (\delta )\), \(\operatorname {coboundary\_ ker\_ gives\_ centralizer\_ pair}\) gives \(\operatorname {prodX}(S) \in \operatorname {Centralizer}(C)\). The complement function \(g(q) = 1 + f(q)\) on \(V_L\) (extended by zero) also lies in \(\ker (\delta )\): its coboundary equals the sum of the all-ones coboundary (zero by row evenness) and \(f\)’s coboundary (zero by hypothesis). Applying \(\operatorname {coboundary\_ ker\_ gives\_ centralizer\_ pair}\) to \(g\) gives \(\operatorname {prodX}(T) \in \operatorname {Centralizer}(C)\).

Since \(S\) and \(T\) are disjoint with \(S \cup T = V_L = \operatorname {logicalSupport}(L)\), we have \(\operatorname {prodX}(S) \cdot \operatorname {prodX}(T) = \operatorname {prodX}(V_L) = L\) (as \(L\) is pure \(X\)-type). Both \(S\) and \(T\) are nonempty (\(S\) because \(f \neq 0\); \(T\) because some \(q \in V_L\) has \(f(q) = 0\)), so both factors have weight strictly less than \(\operatorname {wt}(L)\) and are not the identity. This contradicts the irreducibility of \(L\).

The first component follows by simplification using \(\operatorname {hyperGaussSubsetProduct\_ xVec\_ vertex}\). The second component is \(\operatorname {hyperGaussSubsetProduct\_ zVec}\) applied to the layered incidence.

Unfolding the definition, \(\operatorname {pathGraphAdj}(a, b)\) gives \(a + 1 = b \lor b + 1 = a\). Symmetry follows by swapping the disjuncts, which is verified by integer arithmetic (omega).

By simplification of the path graph adjacency definition, \(a + 1 = a\) is impossible.

The \(Z\)-vector vanishes by \(\operatorname {hyperGaussSubsetProduct\_ zVec}\). The \(X\)-vector restriction follows by simplification using \(\operatorname {hyperGaussSubsetProduct\_ xVec\_ vertex}\).

This follows directly from \(\operatorname {edgeBoundary\_ card\_ ge\_ of\_ cheeger}\) applied to the path graph.

After substituting \(c = \operatorname {Sum.elim}(c_1, c_2)\), the first two components follow by simplification using \(\operatorname {hyperGaussSubsetProduct\_ xVec\_ vertex}\), and the third is \(\operatorname {hyperGaussSubsetProduct\_ zVec}\) applied to the joint incidence.