Let \(\langle h_{\neq }, h_{\lor }\rangle \) be the hypothesis. We have \(q \neq p\) by symmetry of \(\neq \). We case-split on \(h_{\lor }\):

• Rung case: We have \(b_1 \neq b_2\) and \(i = j\). By symmetry, \(b_2 \neq b_1\) and \(j = i\).

• Rail case: We have \(b_1 = b_2\) and (\(i + 1 = j\) or \(j + 1 = i\)). By symmetry, \(b_2 = b_1\) and the disjunction is swapped.

Suppose \(\operatorname {ladderAdj}(p, p)\). Then \(p \neq p\), which is a contradiction.

By simplification using the cardinality of product types, \(|\mathrm{Bool}| = 2\) and \(|\mathrm{Fin}\, n| = n\).

Unfolding the definitions, the pair satisfies \(p \neq q\) (since \(\mathrm{false} \neq \mathrm{true}\)) and the rung condition: different boundaries, same position.

Unfolding the definitions, the pair satisfies the rail condition: same boundary, consecutive positions. The distinctness \(p \neq q\) follows because \(i \neq j\) (since \(i + 1 = j\) implies \(i {\lt} j\)), which is verified by integer arithmetic.

We show preconnectedness: for any two vertices \(u\) and \(v\), there is a path from \(u\) to \(v\). It suffices to show that every vertex \(w = (b, k)\) is reachable from \((\mathrm{false}, 0)\). We proceed by induction on \(k\):

• Base case (\(k = 0\)): \((\mathrm{false}, 0)\) is reachable from itself by reflexivity.

• Inductive step: By the induction hypothesis, \((\mathrm{false}, m)\) is reachable. Since \(m + 1 {\lt} n\), the rail edge from \((\mathrm{false}, m)\) to \((\mathrm{false}, m+1)\) extends the path.

This shows \((\mathrm{false}, k)\) is reachable. For \(b = \mathrm{true}\), we use the rung edge from \((\mathrm{false}, k)\) to \((\mathrm{true}, k)\). Nonemptiness holds since \((\mathrm{false}, 0)\) exists when \(n \geq 1\).

For any vertex \(v\), the neighbor set is contained in the set \(\{ (\neg v_1, v_2),\, (v_1, \min (v_2+1, n-1)),\, (v_1, v_2-1)\} \), which has at most \(3\) elements. Any neighbor \(w\) is either a rung partner (different boundary, same position) or a rail neighbor (same boundary, position differing by \(1\)), and each falls into one of these three candidates. Hence the degree is at most \(3\).

By the handshaking lemma, \(2|E| = \sum _v \deg (v)\). Since each vertex has degree \(\leq 3\) and there are \(2n\) vertices, we have \(\sum _v \deg (v) \leq 2n \cdot 3 = 6n\). Therefore \(|E| \leq 3n\).

This follows directly from the general pairwise commutation theorem \(\operatorname {allChecks\_ commute}\).

By extensionality, for each qubit \(q\), the \(Z\)-component of \(\operatorname {gaussLawOp}(G, v)\) is zero by simplification of the definition.

This is the symmetric form of the Gauss law product identity \(\prod _v A_v = L\).

The three components follow directly from:

1. \(\operatorname {edgeZOperatorMeasured\_ xVec}\) (the edge \(Z\) operator has no \(X\) support),

2. \(\operatorname {edgeZ\_ measured\_ commute}\) (edge \(Z\) operators pairwise commute),

3. \(\operatorname {edgeZOperatorMeasured\_ mul\_ self}\) (each edge \(Z\) operator is self-inverse).

By extensionality, for each qubit \(q\), the \(Z\)-component of \(\operatorname {logicalOp}(G)\) is zero by simplification of the definition.

By extensionality on both the \(X\) and \(Z\) vector components, each component squared is zero in \(\mathbb {F}_2\), giving the identity.

By simplification using cardinalities of product types: \(|\mathrm{Bool}| \cdot |\mathrm{Fin}\, n| = 2n = n + n\).

The four components follow directly from the previously established results: connectedness of the ladder graph, vertex count \(2n\), degree bound \(\leq 3\), and edge count bound \(\leq 3n\).

By simplification using cardinalities of product and \(\mathrm{Fin}\) types.

The pair satisfies the horizontal adjacency condition: same row, adjacent columns. Distinctness follows because \(j \neq j'\) (since \(j + 1 = j'\) implies \(j {\lt} j'\)), verified by integer arithmetic.

The pair satisfies the vertical adjacency condition: same column, adjacent rows. Distinctness follows because \(i \neq i'\) (since \(i + 1 = i'\)), verified by integer arithmetic.

We show preconnectedness. It suffices to show every vertex \((r, c)\) is reachable from \((0, 0)\). First, we reach \((0, c)\) from \((0, 0)\) by induction on \(c\), using horizontal edges at each step. Then we reach \((r, c)\) from \((0, c)\) by induction on \(r\), using vertical edges at each step. Composing these two paths gives reachability of any vertex from \((0, 0)\). For any two vertices \(u, v\), we have paths from \((0,0)\) to each, giving a path between them by transitivity and symmetry. Nonemptiness holds since \((0, 0)\) exists when \(n \geq 1\).

For any vertex \(v = (r, c)\), the neighbor set is contained in the set of at most four candidates: \((r, \min (c+1, D+1))\), \((r, c-1)\), \((\min (r+1, n-1), c)\), and \((r-1, c)\). This set has at most \(4\) elements. Any neighbor \(w\) must be horizontally or vertically adjacent, and in either case falls into one of these four candidates. Hence the degree is at most \(4\).

This follows by ring arithmetic.

This follows by ring arithmetic.

By the handshaking lemma, \(2|E| = \sum _v \deg (v)\). Since each vertex has degree \(\leq 4\) and there are \(n(D+2)\) vertices, we have \(\sum _v \deg (v) \leq n(D+2) \cdot 4\). Therefore \(|E| \leq 2 \cdot n \cdot (D+2)\).

We match on \(p\) and \(q\). If both are in the same copy, symmetry follows from \(G\)’s symmetry. If they are in different copies, we have \(v = w\) and \(v \in \operatorname {bridges}\); swapping gives \(w = v\) and \(w \in \operatorname {bridges}\) (after substitution).

Matching on \(p\): if \(p = \operatorname {inl}(v)\) or \(p = \operatorname {inr}(v)\), then \(\operatorname {bridgeAdj}(p, p)\) would require \(G.\operatorname {Adj}(v, v)\), which contradicts the loopless property of \(G\).

This holds directly by the definition of bridge adjacency for same-copy vertices.

This holds directly by the definition of bridge adjacency for same-copy vertices.

Unfolding the definition of bridge adjacency for cross-copy vertices, the condition \(v = v \land v \in \operatorname {bridges}\) holds by reflexivity and the hypothesis.

By simplification using the cardinality of sum types and ring arithmetic.

Let \(b \in \operatorname {bridges}\). It suffices to show every vertex \(w \in V \oplus V\) is reachable from \(\operatorname {inl}(b)\).

• If \(w = \operatorname {inl}(v)\): Since \(G\) is connected, \(b\) and \(v\) are connected in \(G\). The copy 1 embedding maps this path to a path in the bridge graph from \(\operatorname {inl}(b)\) to \(\operatorname {inl}(v)\).

• If \(w = \operatorname {inr}(v)\): First cross the bridge from \(\operatorname {inl}(b)\) to \(\operatorname {inr}(b)\) (using \(b \in \operatorname {bridges}\)). Then, since \(G\) is connected, \(b\) and \(v\) are connected in \(G\). The copy 2 embedding maps this to a path from \(\operatorname {inr}(b)\) to \(\operatorname {inr}(v)\).

Nonemptiness holds since \(\operatorname {inl}(b)\) exists.

From the reachability hypothesis, we obtain a walk \(p\) in \(G\) from \(v\) to \(w\) with \(|p| = \operatorname {dist}_G(v, w)\). Mapping \(p\) via the copy 1 embedding gives a walk in the bridge graph of the same length. Since the distance is at most the length of any walk, we conclude \(\operatorname {dist}_{\operatorname {BridgeGraph}}(\operatorname {inl}(v), \operatorname {inl}(w)) \leq |p| = \operatorname {dist}_G(v, w)\).

We compute:

where the first inequality is the bridge graph distance bound (since \(u\) and \(v\) are reachable in the connected graph \(G\)), and the second follows from the short paths property.

This follows directly from the low-weight cycle basis property of \(G\).

The three components follow from the bridge graph connectivity theorem, the short paths transfer theorem, and the low-weight cycles inheritance, respectively.

The four components follow from bridge graph connectivity, the vertex count identity \(|V \oplus V| = 2|V|\), the short paths transfer theorem, and the low-weight cycles inheritance, respectively.

The three components follow from the grid graph connectivity theorem, the vertex count formula, and the overhead decomposition identity.

We prove each part separately:

1. For the ladder graph with \(n \geq 1\): connectivity, vertex count \(2n\), degree bound \(\leq 3\), and edge bound \(\leq 3n\) follow from the established results.

2. For the grid graph with \(n \geq 1\): connectivity follows from the grid connectivity theorem, and the decomposition \(n(D+2) = 2n + nD\) follows from the overhead decomposition.

3. For the bridge graph: connectivity follows from the bridge graph connectivity theorem (using \(G\) connected and bridges nonempty), and the vertex count \(|V \oplus V| = 2|V|\) follows from the cardinality identity.