After measurement and Pauli corrections, every Gauss law operator \(A_v\) has eigenvalue \(+1\). That is, for all \(v \in V\):

The \(A_v\) operators form a valid stabilizer group: all mutually commute. For X-type operators, the symplectic form is always \(0\) (no Z-support). Precisely, for all \(v, w \in V\):

Each \(A_v\) is Hermitian with eigenvalues \(\pm 1\). In \(\mathbb {Z}/2\mathbb {Z}\): \(A_v^2 = I\) means \(2 \cdot \mathrm{support} = 0\). For all \(v, w \in V\):

Given a graph \(G\) and a gauging measurement \(m\), the following three properties hold:

1. After measurement and corrections, all \(A_v\) have eigenvalue \(+1\): \(\forall v \in V,\; \mathrm{correctedOutcomes}(G, m)(v) = 0\).

2. All \(A_v\) mutually commute: \(\forall v, w \in V,\; \omega (A_v, A_w) = 0\).

3. Each \(A_v\) is self-inverse: \(\forall v, w \in V,\; 2 \cdot \mathrm{gaussLawOperator\_ vertexSupport}(G, v, w) = 0\).

The initial eigenvalue of \(B_p\) is \(+1\): since \(Z|0\rangle = |0\rangle \), the eigenvalue is \(+1\) on the initial state \(|0\rangle ^{\otimes E}\). In \(\mathbb {Z}/2\mathbb {Z}\):

For a valid cycle \(p\) and any vertex \(v\), the number of cycle edges incident to \(v\) is even:

(If \(v \notin p\): \(0\) edges incident; if \(v \in p\): exactly \(2\) edges incident.)

For a valid cycle \(p\), \(B_p\) commutes with all \(A_v\). The symplectic form \(\omega (B_p, A_v)\) counts Z-X anticommutations, which equals the number of cycle edges incident to \(v\). This is always even:

Given that \(p\) is a valid cycle (each vertex has \(0\) or \(2\) incident edges from \(p\)), the following hold:

1. \(B_p\) has initial eigenvalue \(+1\) on \(|0\rangle ^{\otimes E}\).

2. \(B_p\) commutes with all measured operators \(A_v\).

Therefore \(B_p\) remains a stabilizer after the gauging measurement.

Let \(s\) be a stabilizer check with no Z-support on edges (\(s.\mathrm{zSupportOnE} = \emptyset \)), and let \(\gamma \) be a valid deforming path with \(\partial \gamma = \mathcal{S}_{Z}(s) \cap V_G\). Then the boundary condition ensures anticommutations cancel:

The deformed check \(\widetilde{s}_j\) has eigenvalue \(+1\) on the initial state \(|\psi \rangle |0\rangle ^{\otimes E}\):

Given:

• \(s_j\) is a stabilizer from the original code (no Z-support on edges),

• \(\gamma \) is a valid deforming path with \(\partial \gamma = \mathcal{S}_{Z,j} \cap V_G\),

• the original code state \(|\psi \rangle \) is a \(+1\) eigenstate of \(s_j\) (input assumption),

then:

1. \(\widetilde{s}_j\) commutes with all \(A_v\) (by the boundary condition).

2. \(\widetilde{s}_j\) has eigenvalue \(+1\) on \(|\psi \rangle |0\rangle ^{\otimes E}\).

Therefore \(\widetilde{s}_j\) is a stabilizer of the deformed code.

The product constraint \(\prod _v A_v = L\) holds:

1. Vertex support: all \(1\)s (i.e., \(\mathrm{gaussLaw\_ product\_ vertexSupport}(G) = v \mapsto 1\), which equals the support of \(L = \prod _v X_v\)).

2. Edge support: all \(0\)s (each edge appears twice, \(X_e^2 = I\)), i.e., \(\mathrm{gaussLaw\_ product\_ edgeSupport}(G) = 0\).

Due to the constraint \(\prod _v A_v = L\), the number of independent \(A_v\) is \(|V| - 1\). However, \(L\) itself now becomes a stabilizer (it is the product of all \(A_v\) outcomes). Given \(|V| \geq 1\):

1. \(\mathrm{gaussLaw\_ independent\_ count}(G) = |V| - 1\),

2. \(\mathrm{gaussLaw\_ product\_ vertexSupport}(G) = v \mapsto 1\).

For a connected graph satisfying \(|V| \leq |E|\) and \(|C| = |E| - |V| + 1\) (Euler’s formula):

Given an original \([[n, k]]\) code with \(n \geq k\) and \(k \geq 1\):

Given \(n \geq k\) and \(k \geq 1\):

The dimension drops from \(2^k\) to \(2^{k-1}\), exactly halving. For \(k \geq 1\):

One logical qubit (\(L\)) has been measured. For \(k \geq 1\):

Given a valid deformed code setup, the following all hold:

1. Part 1: All \(A_v\) become stabilizers via measurement:

   • \(\forall v \in V,\; \mathrm{correctedOutcomes}(G, m)(v) = 0\),

   • \(\forall v, w \in V,\; \omega (A_v, A_w) = 0\).

2. Part 2: All \(B_p\) are stabilizers:

   • \(\forall p \in C,\; \sum _{e \in \mathrm{cycles}(p)} \mathrm{initialEdgeStabilizerOutcome}(e) = 0\),

   • \(\forall p \in C,\; \forall v \in V,\; \omega (B_p, A_v) \bmod 2 = 0\).

3. Part 3: All \(\widetilde{s}_j\) are stabilizers:

   • \(\forall j,\; \forall v \in V,\; \omega _{\mathrm{simple}}(\widetilde{s}_j, A_v) \bmod 2 = 0\),

   • \(\forall j,\; \mathrm{original\_ eigenvalue} + \sum _{e \in \gamma _j} \mathrm{initialEdgeStabilizerOutcome}(e) = 0\).

4. Part 4: The dimension is \(2^{k-1}\):

   \[ \mathrm{total\_ qubits'} - \mathrm{total\_ stabilizers'} = k - 1. \]

The logical operator \(L\) becomes a stabilizer (measured via \(\prod _v A_v\)):

The number of new stabilizers from gauging is:

• \(|V| - 1\) independent \(A_v\) plus \(1\) for \(L\) gives \(|V|\) total from Gauss law,

• \(|E| - |V| + 1\) from flux operators (Euler’s formula).

Total new stabilizers: \(|V| + (|E| - |V| + 1) = |E| + 1\).

The deformed code is an \([[n + |E|, k - 1, d']]\) code. Specifically, given \(k \geq 1\):

1. New qubit count: \(\mathrm{total\_ qubits'} = n + |E|\).

2. New logical qubit count: \(k - 1\).

3. Dimension formula: \(2^{(\mathrm{total\_ qubits'} - \mathrm{total\_ stabilizers'})} = 2^{k-1}\).

The gauging procedure transforms \([[n, k, d]] \to [[n + |E|, k - 1, d']]\). That is, for \(k \geq 1\):

confirming that exactly one logical qubit has been measured.