MerLean-example

15 Def 5: Deformed Check

This chapter formalizes the deformed check construction. Given a stabilizer check \(s_j\) from the original code, the deformed check \(\tilde{s}_j\) is obtained by multiplying \(s_j\) with additional \(Z\)-operators along an edge-path \(\gamma \) in the graph \(G\). The original stabilizer checks are partitioned into two sets: Set \(\mathcal{C}\) (checks with \(\mathcal{S}_Z \cap V_G = \emptyset \), requiring no deformation) and Set \(\mathcal{S}\) (checks with nontrivial \(Z\)-type support on \(V_G\), genuinely deformed by the gauging procedure).

Definition 422 Stabilizer Check
#

A stabilizer check from the original code is a DeformablePauliOperator on the graph \(G\). It carries the additional semantic meaning that it represents a generator of the original code’s stabilizer group. The key inherited property is that \(|\mathcal{S}_Z \cap V_G|\) is even (the check commutes with \(L\)).

Definition 423 \(Z\)-Support on Graph
#

The \(Z\)-type support of a stabilizer check \(s\) restricted to the graph vertices \(V_G\) is defined as

\[ \mathcal{S}_Z \cap V_G := s.\mathrm{zSupportOnV}. \]

This corresponds to \(\mathcal{S}_Z \cap V_G\) in the paper notation.

Definition 424 \(X\)-Support on Graph
#

The \(X\)-type support of a stabilizer check \(s\) restricted to the graph vertices is defined as \(s.\mathrm{xSupportOnV}\).

Definition 425 In Set \(\mathcal{C}\)
#

A stabilizer check \(s\) is in Set \(\mathcal{C}\) if it has no \(Z\)-support on graph vertices:

\[ \mathrm{InSetC}(G, s) \iff s.\mathrm{zSupportOnV} = \emptyset . \]

For these checks, no deformation is needed.

Definition 426 In Set \(\mathcal{S}\)
#

A stabilizer check \(s\) is in Set \(\mathcal{S}\) if it has nontrivial \(Z\)-support on graph vertices:

\[ \mathrm{InSetS}(G, s) \iff s.\mathrm{zSupportOnV} \neq \emptyset . \]

These checks are genuinely deformed by the gauging procedure.

Theorem 427 Partition is Complete

Every stabilizer check \(s\) is either in Set \(\mathcal{C}\) or in Set \(\mathcal{S}\):

\[ \mathrm{InSetC}(G, s) \lor \mathrm{InSetS}(G, s). \]
Proof

We consider two cases on whether \(s.\mathrm{zSupportOnV} = \emptyset \). If \(s.\mathrm{zSupportOnV} = \emptyset \), then \(s\) is in Set \(\mathcal{C}\) by definition. If \(s.\mathrm{zSupportOnV} \neq \emptyset \), then \(s\) is in Set \(\mathcal{S}\) by definition.

Theorem 428 Partition is Disjoint

No stabilizer check is in both Set \(\mathcal{C}\) and Set \(\mathcal{S}\):

\[ \neg (\mathrm{InSetC}(G, s) \land \mathrm{InSetS}(G, s)). \]
Proof

Assume both \(h_{\mathcal{C}} : s.\mathrm{zSupportOnV} = \emptyset \) and \(h_{\mathcal{S}} : s.\mathrm{zSupportOnV} \neq \emptyset \) hold. Then \(h_{\mathcal{S}}\) contradicts \(h_{\mathcal{C}}\) directly.

Lemma 429 InSetS iff Exists Vertex with \(Z\)-Support

A stabilizer check \(s\) is in Set \(\mathcal{S}\) if and only if there exists a vertex \(v \in V\) such that \(v \in s.\mathrm{zSupportOnV}\):

\[ \mathrm{InSetS}(G, s) \iff \exists v \in V,\; v \in s.\mathrm{zSupportOnV}. \]
Proof

We rewrite \(\mathrm{InSetS}\) as \(s.\mathrm{zSupportOnV} \neq \emptyset \), which by the equivalence between nonemptiness and existence of an element gives the result.

For a stabilizer check \(s\) in Set \(\mathcal{C}\), the empty path \(\gamma = \emptyset \) is a valid deforming path, i.e., \(\mathrm{IsValidDeformingPath}(G, s.\mathrm{zSupportOnV}, \emptyset )\).

Proof

We unfold \(\mathrm{IsValidDeformingPath}\) and \(\mathrm{edgePathBoundary}\). First, we establish that \(\mathrm{edgePathVector}(G, \emptyset ) = 0\) by extensionality: for each edge \(e\), the membership in \(\emptyset \) is false, so the vector is zero. Then applying \(\mathrm{boundaryMap\_ zero}\), we get that \(\mathrm{boundaryMap}(G, 0) = 0\). Since \(s\) is in Set \(\mathcal{C}\), we have \(s.\mathrm{zSupportOnV} = \emptyset \), so \(\mathrm{zSupportVector}(G, s.\mathrm{zSupportOnV})\) is identically zero at every vertex (since no vertex is in \(\emptyset \)). By extensionality, the boundary equals the \(Z\)-support vector, both being zero.

Theorem 431 Deformed Equals Original for Set \(\mathcal{C}\)

For a stabilizer check \(s\) in Set \(\mathcal{C}\) with empty edge path, the deformed check equals the original:

\[ \mathrm{DeformedOperator}(G, s, \emptyset ) = s. \]
Proof

By simplification using the definition of \(\mathrm{DeformedOperator}\): the \(Z\)-support on edges becomes \(s.\mathrm{zSupportOnE} \mathbin {\triangle } \emptyset \). Since \(\emptyset \) is the identity for symmetric difference (rewriting \(\emptyset \) as \(\bot \) and applying \(\mathrm{symmDiff\_ bot}\)), this equals \(s.\mathrm{zSupportOnE}\), so the deformed operator is equal to \(s\).

Definition 432 Deformed Check
#

The deformed check of a stabilizer check \(s\) along an edge-path \(\gamma \) is defined as

\[ \tilde{s} := \mathrm{DeformedOperator}(G, s, \gamma ) = s \cdot \prod _{e \in \gamma } Z_e, \]

which is an alias for the DeformedOperator construction applied to a stabilizer check.

Theorem 433 Deformed Check Preserves \(X\)-Support on Vertices

For any stabilizer check \(s\) and edge-path \(\gamma \):

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{xSupportOnV} = s.\mathrm{xSupportOnV}. \]
Proof

This holds by definitional equality (reflexivity).

Theorem 434 Deformed Check Preserves \(Z\)-Support on Vertices

For any stabilizer check \(s\) and edge-path \(\gamma \):

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnV} = s.\mathrm{zSupportOnV}. \]
Proof

This holds by definitional equality (reflexivity).

Theorem 435 Deformed Check Preserves \(X\)-Support on Edges

For any stabilizer check \(s\) and edge-path \(\gamma \):

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{xSupportOnE} = s.\mathrm{xSupportOnE}. \]
Proof

This holds by definitional equality (reflexivity).

Theorem 436 Deformed Check \(Z\)-Support on Edges

The deformed check’s \(Z\)-support on edges is the symmetric difference of the original support and the path:

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnE} = s.\mathrm{zSupportOnE} \mathbin {\triangle } \gamma . \]
Proof

This holds by definitional equality (reflexivity), since \(\mathrm{DeformedCheck}\) is defined as \(\mathrm{DeformedOperator}\) which modifies \(\mathrm{zSupportOnE}\) by symmetric difference.

Theorem 437 Deformed Check Preserves Phase

For any stabilizer check \(s\) and edge-path \(\gamma \):

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{phase} = s.\mathrm{phase}. \]
Proof

This holds by definitional equality (reflexivity).

Theorem 438 Set \(\mathcal{S}\) Checks Have Even \(Z\)-Support

For any stabilizer check \(s\) in Set \(\mathcal{S}\):

\[ |s.\mathrm{zSupportOnV}| \bmod 2 = 0. \]
Proof

This follows directly from the inherited property \(s.\mathrm{zSupport\_ even}\) of deformable Pauli operators.

Theorem 439 Set \(\mathcal{S}\) Checks Have \(Z\)-Support \(\geq 2\)

For any stabilizer check \(s\) in Set \(\mathcal{S}\):

\[ |s.\mathrm{zSupportOnV}| \geq 2. \]
Proof

Since \(s\) is in Set \(\mathcal{S}\), we have \(s.\mathrm{zSupportOnV} \neq \emptyset \). The even cardinality property gives \(|s.\mathrm{zSupportOnV}| \bmod 2 = 0\). Since the set is nonempty, \(|s.\mathrm{zSupportOnV}| {\gt} 0\). By integer arithmetic (omega), an even positive integer is at least \(2\).

Theorem 440 Deformed Check Well-Defined (Even \(Z\)-Support)

For any stabilizer check \(s\):

\[ |s.\mathrm{zSupportOnV}| \bmod 2 = 0. \]
Proof

This follows directly from the inherited property \(s.\mathrm{zSupport\_ even}\).

Theorem 441 Deformed Check Preserves Deformability

The deformed check preserves the even \(Z\)-support property:

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupport\_ even} = s.\mathrm{zSupport\_ even}. \]
Proof

This holds by definitional equality (reflexivity), since the deformed check preserves \(\mathrm{zSupportOnV}\).

Theorem 442 Deformed Check Commutes with Gauss Law

Given a stabilizer check \(s\) with \(s.\mathrm{zSupportOnE} = \emptyset \) and a valid deforming path \(\gamma \) (i.e., \(\partial \gamma = \mathcal{S}_Z \cap V_G\)), the deformed check commutes with the Gauss law operator \(A_v\) for every vertex \(v\):

\[ \mathrm{deformed\_ gaussLaw\_ symplectic\_ simple}(G, s.\mathrm{zSupportOnV}, \gamma , v) \bmod 2 = 0. \]
Proof

This follows directly from the general theorem \(\mathrm{deformed\_ commutes\_ with\_ gaussLaw}\) applied with the check’s \(Z\)-support on vertices and the valid deforming path \(\gamma \).

Theorem 443 Deformed Check Commutes with All Gauss Law Operators

Given a stabilizer check \(s\) with \(s.\mathrm{zSupportOnE} = \emptyset \) and a valid deforming path \(\gamma \), the deformed check commutes with all Gauss law operators:

\[ \forall v \in V,\quad \mathrm{deformed\_ gaussLaw\_ symplectic\_ simple}(G, s.\mathrm{zSupportOnV}, \gamma , v) \bmod 2 = 0. \]
Proof

This follows directly from the general theorem \(\mathrm{deformed\_ commutes\_ with\_ all\_ gaussLaw}\) applied to the stabilizer check \(s\), path \(\gamma \), and the hypotheses.

Theorem 444 Deformed Check Equals Original for Set \(\mathcal{C}\)

For a stabilizer check \(s\) in Set \(\mathcal{C}\), the deformed check with empty path equals the original:

\[ \mathrm{DeformedCheck}(G, s, \emptyset ) = s. \]
Proof

This follows directly from the previously established result \(\mathrm{deformed\_ eq\_ original\_ for\_ setC}\).

Theorem 445 Set \(\mathcal{C}\) Commutes with Gauss Law

For a stabilizer check \(s\) in Set \(\mathcal{C}\) with \(s.\mathrm{zSupportOnE} = \emptyset \), and for any vertex \(v\):

\[ \mathrm{deformed\_ gaussLaw\_ symplectic\_ simple}(G, s.\mathrm{zSupportOnV}, \emptyset , v) \bmod 2 = 0. \]
Proof

We first establish that the empty path is a valid deforming path for Set \(\mathcal{C}\) checks by applying \(\mathrm{empty\_ path\_ valid\_ for\_ setC}\). Then we apply \(\mathrm{deformedCheck\_ commutes\_ with\_ gaussLaw}\) with the empty path and the validity hypothesis.

Theorem 446 Deformed Check Genuinely Changed for Set \(\mathcal{S}\)

For a stabilizer check \(s\) in Set \(\mathcal{S}\) with a non-empty valid path \(\gamma \) and \(s.\mathrm{zSupportOnE} = \emptyset \), the deformed check’s edge support differs from the original:

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnE} \neq s.\mathrm{zSupportOnE}. \]
Proof

By the formula for the deformed check’s \(Z\)-support on edges, \((\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnE} = s.\mathrm{zSupportOnE} \mathbin {\triangle } \gamma \). Since \(s.\mathrm{zSupportOnE} = \emptyset \), we have \(\emptyset \mathbin {\triangle } \gamma = \gamma \) (by simplification). Since \(\gamma \) is nonempty, this is nonempty and thus not equal to \(\emptyset = s.\mathrm{zSupportOnE}\).

For a stabilizer check \(s\) in Set \(\mathcal{S}\), the empty path is not a valid deforming path:

\[ \neg \, \mathrm{IsValidDeformingPath}(G, s.\mathrm{zSupportOnV}, \emptyset ). \]
Proof

Suppose for contradiction that \(\emptyset \) is a valid deforming path. We first compute \(\mathrm{edgePathBoundary}(G, \emptyset )\): since \(\mathrm{edgePathVector}(G, \emptyset ) = 0\) (by extensionality, every component is zero), applying \(\mathrm{boundaryMap\_ zero}\) gives boundary \(= 0\). The validity condition then requires the \(Z\)-support vector to be zero. By extensionality at each vertex \(v\): if \(v \in s.\mathrm{zSupportOnV}\), the \(Z\)-support vector at \(v\) is \(1\), which must equal \(0\) — a contradiction. If \(v \notin s.\mathrm{zSupportOnV}\), membership in \(\emptyset \) gives a contradiction trivially. Therefore \(s.\mathrm{zSupportOnV} = \emptyset \), contradicting the hypothesis that \(s\) is in Set \(\mathcal{S}\) (i.e., \(s.\mathrm{zSupportOnV} \neq \emptyset \)).

Theorem 448 Deformed Check is Deformable

Deformed checks of deformable operators remain deformable:

\[ |(\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnV}| \bmod 2 = 0. \]
Proof

This follows directly from \(s.\mathrm{zSupport\_ even}\), since the deformed check preserves \(\mathrm{zSupportOnV}\).

Theorem 449 Deformed Check Preserves \(Z\)-Support on \(V\)

For any stabilizer check \(s\) and edge-path \(\gamma \):

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnV} = s.\mathrm{zSupportOnV}. \]
Proof

This holds by definitional equality (reflexivity).

Theorem 450 Deformed Check Preserves \(X\)-Support on \(V\)

For any stabilizer check \(s\) and edge-path \(\gamma \):

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{xSupportOnV} = s.\mathrm{xSupportOnV}. \]
Proof

This holds by definitional equality (reflexivity).

Theorem 451 Deforming Twice Returns to Original

Applying the deformation twice with the same path \(\gamma \) returns the original check:

\[ \mathrm{DeformedCheck}(G, \mathrm{DeformedCheck}(G, s, \gamma ), \gamma ) = s. \]
Proof

By simplification using the definitions of \(\mathrm{DeformedCheck}\) and \(\mathrm{DeformedOperator}\): the \(Z\)-support on edges becomes \((s.\mathrm{zSupportOnE} \mathbin {\triangle } \gamma ) \mathbin {\triangle } \gamma \). By the cancellation law for symmetric difference (\(A \mathbin {\triangle } B \mathbin {\triangle } B = A\), i.e., \(\mathrm{symmDiff\_ symmDiff\_ cancel\_ right}\)), this equals \(s.\mathrm{zSupportOnE}\), recovering \(s\).

Theorem 452 Deformation is Involutive

Deformation with a fixed path \(\gamma \) is an involutive function:

\[ \mathrm{Involutive}(\lambda s.\, \mathrm{DeformedCheck}(G, s, \gamma )). \]
Proof

Let \(s\) be an arbitrary stabilizer check. We must show \(\mathrm{DeformedCheck}(G, \mathrm{DeformedCheck}(G, s, \gamma ), \gamma ) = s\). This follows directly from \(\mathrm{deformedCheck\_ twice}\).

Theorem 453 Composition of Deformations

Composing two deformations with paths \(\gamma _1\) and \(\gamma _2\) is equivalent to a single deformation with their symmetric difference:

\[ \mathrm{DeformedCheck}(G, \mathrm{DeformedCheck}(G, s, \gamma _1), \gamma _2) = \mathrm{DeformedCheck}(G, s, \gamma _1 \mathbin {\triangle } \gamma _2). \]
Proof

By simplification using the definitions of \(\mathrm{DeformedCheck}\) and \(\mathrm{DeformedOperator}\): the \(Z\)-support on edges becomes \((s.\mathrm{zSupportOnE} \mathbin {\triangle } \gamma _1) \mathbin {\triangle } \gamma _2\). By associativity of symmetric difference (\(\mathrm{symmDiff\_ assoc}\)), this equals \(s.\mathrm{zSupportOnE} \mathbin {\triangle } (\gamma _1 \mathbin {\triangle } \gamma _2)\), which is \(\mathrm{DeformedCheck}(G, s, \gamma _1 \mathbin {\triangle } \gamma _2)\).

Definition 454 \(Z\)-Support Cardinality
#

The \(Z\)-support cardinality of a stabilizer check \(s\) is defined as

\[ \mathrm{zSupportCard}(G, s) := |s.\mathrm{zSupportOnV}|. \]
Theorem 455 Set \(\mathcal{S}\) Has \(Z\)-Support Cardinality \(\geq 2\)

For any stabilizer check \(s\) in Set \(\mathcal{S}\):

\[ \mathrm{zSupportCard}(G, s) \geq 2. \]
Proof

This follows directly from \(\mathrm{setS\_ zSupport\_ card\_ ge\_ two}\).

Theorem 456 Set \(\mathcal{C}\) Has \(Z\)-Support Cardinality \(0\)

For any stabilizer check \(s\) in Set \(\mathcal{C}\):

\[ \mathrm{zSupportCard}(G, s) = 0. \]
Proof

We simplify \(\mathrm{zSupportCard}\) and \(\mathrm{InSetC}\). Since \(s.\mathrm{zSupportOnV} = \emptyset \) (from the Set \(\mathcal{C}\) hypothesis), we have \(|s.\mathrm{zSupportOnV}| = 0\) by the fact that \(|\emptyset | = 0\).

Definition 457 Has Valid Paths
#

A graph \(G\) has valid paths if for any even-cardinality subset \(S \subseteq V\), there exists an edge-path \(\gamma \) such that \(\gamma \) is a valid deforming path for \(S\):

\[ \forall S \subseteq V,\quad |S| \bmod 2 = 0 \implies \exists \gamma ,\; \mathrm{IsValidDeformingPath}(G, S, \gamma ). \]

This follows from graph connectivity: for two vertices, take any path between them; for larger even-cardinality sets, pair up vertices and connect each pair.

Theorem 458 Deformed Check Exists

Given the \(\mathrm{HasValidPaths}\) assumption on \(G\), for any stabilizer check \(s\), there exists a valid deforming path:

\[ \exists \gamma ,\; \mathrm{IsValidDeformingPath}(G, s.\mathrm{zSupportOnV}, \gamma ). \]
Proof

We apply \(\mathrm{HasValidPaths.valid\_ path\_ exists}\) to \(s.\mathrm{zSupportOnV}\) with the proof that \(|s.\mathrm{zSupportOnV}| \bmod 2 = 0\) (from \(s.\mathrm{zSupport\_ even}\)).

Definition 459 Edge \(Z\)-Operator Support
#

The edge \(Z\)-operator support of a path \(\gamma \) is simply the edge-set \(\gamma \) itself, representing the set of edges on which \(Z\)-operators are applied:

\[ \mathrm{edgeZOperatorSupport}(G, \gamma ) := \gamma . \]
Theorem 460 Deformed Check Edge Product

The deformed check’s edge \(Z\)-support is the symmetric difference of the original support and the path’s edge \(Z\)-operator support:

\[ (\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnE} = s.\mathrm{zSupportOnE} \mathbin {\triangle } \mathrm{edgeZOperatorSupport}(G, \gamma ). \]
Proof

This holds by definitional equality (reflexivity).

Theorem 461 Deformed Check Set \(\mathcal{C}\) Edge Support

For a stabilizer check \(s\) in Set \(\mathcal{C}\) with empty path, the deformed check has the same edge support as the original:

\[ (\mathrm{DeformedOperator}(G, s, \emptyset )).\mathrm{zSupportOnE} = s.\mathrm{zSupportOnE}. \]
Proof

By simplification using \(\mathrm{DeformedOperator}\): the \(Z\)-support on edges is \(s.\mathrm{zSupportOnE} \mathbin {\triangle } \emptyset \). Rewriting \(\emptyset \) as \(\bot \) and applying \(\mathrm{symmDiff\_ bot}\), this equals \(s.\mathrm{zSupportOnE}\).

Theorem 462 Main Theorem: Deformed Check Properties

Given a stabilizer check \(s\) with \(s.\mathrm{zSupportOnE} = \emptyset \) and a valid deforming path \(\gamma \) with \(\partial \gamma = \mathcal{S}_Z \cap V_G\), the following hold:

  1. The deformed check commutes with all Gauss law operators: for all \(v \in V\),

    \[ \mathrm{deformed\_ gaussLaw\_ symplectic\_ simple}(G, s.\mathrm{zSupportOnV}, \gamma , v) \bmod 2 = 0. \]
  2. The deformed check preserves deformability:

    \[ |(\mathrm{DeformedCheck}(G, s, \gamma )).\mathrm{zSupportOnV}| \bmod 2 = 0. \]
Proof

We prove each conjunct separately. The first conjunct follows from \(\mathrm{deformedCheck\_ commutes\_ with\_ all\_ gaussLaw}\) applied to \(s\), \(\gamma \), and the hypotheses. The second conjunct follows from \(\mathrm{deformedCheck\_ deformable}\).

Every stabilizer check falls into exactly one of two categories:

  • \(s\) is in Set \(\mathcal{C}\) and \(\mathrm{DeformedCheck}(G, s, \emptyset ) = s\), or

  • \(s\) is in Set \(\mathcal{S}\) and \(\neg \, \mathrm{IsValidDeformingPath}(G, s.\mathrm{zSupportOnV}, \emptyset )\).

Proof

We case-split using \(\mathrm{partition\_ complete}\). In the left case (Set \(\mathcal{C}\)), we combine the hypothesis \(h_{\mathcal{C}}\) with \(\mathrm{deformedCheck\_ eq\_ original\_ for\_ SetC}\) to show the deformed check equals the original. In the right case (Set \(\mathcal{S}\)), we combine the hypothesis \(h_{\mathcal{S}}\) with \(\mathrm{empty\_ path\_ invalid\_ for\_ setS}\) to show the empty path is not valid.