Documentation

QEC1.Definitions.Def_5_DeformedCheck

Def_5: Deformed Check #

Statement #

Let $s_j$ be a stabilizer check from the original code, written as $s_j = i^{\sigma} \prod_{v \in \mathcal{S}_X} X_v \prod_{v \in \mathcal{S}_Z} Z_v$. The deformed check $\tilde{s}_j$ is the deformed version of $s_j$: $$\tilde{s}_j = s_j \prod_{e \in \gamma} Z_e$$ where $\gamma$ is an edge-path in $G$ satisfying $\partial \gamma = \mathcal{S}_Z \cap V_G$.

The original stabilizer checks are partitioned into two sets:

The deformed checks $\tilde{s}_j$ are well-defined because all original stabilizers commute with $L$, so $|\mathcal{S}_Z \cap V_G|$ is always even and a valid path $\gamma$ always exists.

Main Definitions #

Key Properties #

Corollaries #

Stabilizer Checks from the Original Code #

A stabilizer check s_j is a Pauli operator from the original code that:

  1. Is a product of X and Z operators (possibly with a global phase)
  2. Commutes with all other stabilizers
  3. Commutes with the logical operator L = ∏_{v ∈ V} X_v

We represent a stabilizer check using the same structure as DeformablePauliOperator, but with the semantic meaning that it comes from the original code's stabilizer group.

@[reducible, inline]
abbrev GraphWithCycles.StabilizerCheck {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) :
Type (max u_1 u_2)

A stabilizer check from the original code. This is essentially a DeformablePauliOperator with the additional semantic meaning that it represents a generator of the original code's stabilizer group.

The key property inherited from DeformablePauliOperator is that |zSupportOnV| is even (the check commutes with L).

Equations
Instances For
    def GraphWithCycles.zSupportOnGraph {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

    The Z-type support of a stabilizer check restricted to the graph vertices V_G. This is S_Z ∩ V_G in the paper notation.

    Equations
    Instances For
      def GraphWithCycles.xSupportOnGraph {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

      The X-type support of a stabilizer check restricted to the graph vertices.

      Equations
      Instances For

        Partition of Stabilizer Checks into Sets C and S #

        The original stabilizer checks are partitioned based on their Z-type support on V_G:

        def GraphWithCycles.InSetC {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

        Predicate: a stabilizer check is in Set C (no Z-support on graph vertices)

        Equations
        Instances For
          def GraphWithCycles.InSetS {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

          Predicate: a stabilizer check is in Set S (nontrivial Z-support on graph vertices)

          Equations
          Instances For
            instance GraphWithCycles.decInSetC {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :
            Equations
            theorem GraphWithCycles.partition_complete {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :
            G.InSetC s G.InSetS s

            The partition is complete: every check is either in Set C or Set S

            theorem GraphWithCycles.partition_disjoint {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :
            ¬(G.InSetC s G.InSetS s)

            The partition is disjoint: no check is in both Set C and Set S

            @[simp]
            theorem GraphWithCycles.inSetC_iff {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

            Characterization: in Set C iff Z-support on V is empty

            @[simp]
            theorem GraphWithCycles.inSetS_iff {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

            Characterization: in Set S iff Z-support on V is nonempty

            theorem GraphWithCycles.inSetS_iff_exists {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :
            G.InSetS s ∃ (v : V), v s.zSupportOnV

            Alternative: in Set S iff exists a vertex with Z-support

            Properties of Set C Checks #

            For checks in Set C, the deformation is trivial: γ = ∅ works because ∂∅ = 0 = S_Z ∩ V_G (both are empty).

            The empty path is a valid deforming path for Set C checks

            theorem GraphWithCycles.deformed_eq_original_for_setC {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (_h : G.InSetC s) :

            For Set C checks with empty edge path, the deformed check equals the original

            @[simp]

            The deformed check for Set C has the same edge support as the original

            Properties of Set S Checks #

            For checks in Set S, a nontrivial edge path γ is needed. The existence of such a path is guaranteed by the even cardinality of S_Z ∩ V_G.

            theorem GraphWithCycles.setS_zSupport_even {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (_h : G.InSetS s) :

            Set S checks have even Z-support cardinality (inherited from deformability)

            theorem GraphWithCycles.setS_zSupport_card_ge_two {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (h : G.InSetS s) :

            Set S checks have at least 2 vertices in Z-support (even and nonempty implies ≥2)

            The Deformed Check Definition #

            The deformed check s̃_j is defined as s_j · ∏_{e ∈ γ} Z_e where γ is a valid deforming path.

            This reuses the DeformedOperator construction from Def_4.

            @[reducible, inline]
            abbrev GraphWithCycles.DeformedCheck {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) :

            The deformed check: s̃ = s · ∏_{e ∈ γ} Z_e This is just an alias for DeformedOperator applied to a StabilizerCheck.

            Equations
            Instances For
              @[simp]

              The deformed check preserves X-support on vertices

              @[simp]

              The deformed check preserves Z-support on vertices

              @[simp]

              The deformed check preserves X-support on edges

              The deformed check's Z-support on edges is modified by the path γ

              @[simp]
              theorem GraphWithCycles.deformedCheck_phase {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) :

              The deformed check preserves the phase

              Well-Definedness of Deformed Checks #

              The deformed checks are well-defined because:

              1. All original stabilizers commute with L, so |S_Z ∩ V_G| is always even
              2. A valid path γ always exists when the cardinality is even (graph connectivity)

              We state the well-definedness as the existence of a valid deforming path.

              Deformed checks are well-defined in the sense that |S_Z ∩ V_G| is even

              theorem GraphWithCycles.deformedCheck_preserves_deformability {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) :
              =

              Given a valid deforming path, the deformed check is well-defined (preserves even Z-support)

              Deformed Checks Commute with Gauss Law Operators #

              The key property: if γ is a valid deforming path, then s̃ commutes with all A_v.

              This follows from the boundary condition ∂γ = S_Z ∩ V_G and the calculation that at each vertex v, the number of anticommuting pairs (from Z on vertices + Z on edges) is even.

              theorem GraphWithCycles.deformedCheck_commutes_with_gaussLaw {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) (_h_no_edge_Z : s.zSupportOnE = ) (h_valid : G.IsValidDeformingPath s.zSupportOnV γ) (v : V) :

              The deformed check commutes with all Gauss law operators A_v

              theorem GraphWithCycles.deformedCheck_commutes_with_all_gaussLaw {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) (h_no_edge_Z : s.zSupportOnE = ) (h_valid : G.IsValidDeformingPath s.zSupportOnV γ) (v : V) :

              The deformed check commutes with all Gauss law operators (universal statement)

              Set C: No Deformation Needed #

              For checks in Set C (S_Z ∩ V_G = ∅), the deformed check equals the original check when using the empty path.

              theorem GraphWithCycles.deformedCheck_eq_original_for_SetC {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (h : G.InSetC s) :

              For Set C checks, the deformed check equals the original

              theorem GraphWithCycles.setC_commutes_with_gaussLaw {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (h : G.InSetC s) (h_no_edge_Z : s.zSupportOnE = ) (v : V) :

              Set C checks trivially commute with Gauss law operators (since they equal the original)

              Set S: Genuine Deformation #

              For checks in Set S (S_Z ∩ V_G ≠ ∅), a nontrivial path γ is required. The deformed check differs from the original by having additional Z operators on edges.

              theorem GraphWithCycles.deformedCheck_genuinely_changed_for_SetS {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) (h_nonempty : Finset.Nonempty γ) (h_orig_empty : s.zSupportOnE = ) :

              For Set S checks with a non-empty valid path, the edge support is genuinely changed

              For Set S checks, using the empty path doesn't give a valid deforming path

              Preservation Properties #

              Deformed checks preserve various algebraic properties.

              theorem GraphWithCycles.deformedCheck_deformable {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) :

              Deformed checks of deformable operators are still deformable

              Deformed checks preserve the Z-support on V exactly

              Deformed checks preserve the X-support on V exactly

              Multiple Deformations #

              Applying deformation twice with the same path returns to the original (since symmetric difference is its own inverse).

              theorem GraphWithCycles.deformedCheck_twice {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) :
              G.DeformedCheck (G.DeformedCheck s γ) γ = s

              Deforming twice with the same path returns to the original

              theorem GraphWithCycles.deformedCheck_involutive {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (γ : EdgePath E) :

              Deformation is involutive

              Composition of Deformations #

              Deforming with two paths is equivalent to deforming with their symmetric difference.

              theorem GraphWithCycles.deformedCheck_compose {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ₁ γ₂ : EdgePath E) :
              G.DeformedCheck (G.DeformedCheck s γ₁) γ₂ = G.DeformedCheck s (symmDiff γ₁ γ₂)

              Composition of deformations: s̃_{γ₁ ∘ γ₂} = s̃_{γ₁ Δ γ₂}

              Classification by Z-Support Cardinality #

              We can further classify Set S checks by the cardinality of their Z-support.

              def GraphWithCycles.zSupportCard {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) :

              The Z-support cardinality of a stabilizer check

              Equations
              Instances For
                theorem GraphWithCycles.setS_zSupportCard_ge_two' {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (h : G.InSetS s) :

                Set S checks have Z-support cardinality at least 2

                theorem GraphWithCycles.setC_zSupportCard_eq_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (h : G.InSetC s) :

                Set C checks have Z-support cardinality exactly 0

                Existence of Valid Paths (Axiom) #

                The existence of valid deforming paths depends on the graph structure. For a connected graph, paths between pairs of vertices always exist, and the boundary condition can be satisfied when the cardinality is even.

                We state this as an axiom that should hold for well-chosen graphs satisfying the desiderata (short paths, sufficient expansion, low-weight cycles).

                class GraphWithCycles.HasValidPaths {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) :

                Assumption: For a connected graph with appropriate structure, valid deforming paths exist. This is the graph-theoretic content of "well-defined deformed checks".

                In a connected graph, for any even-cardinality subset S of vertices, there exists an edge-set γ such that ∂γ = S. This follows from:

                • For 2 vertices: take any path between them
                • For 4 vertices: pair them up and take paths for each pair
                • Inductively: pair up and connect

                We state this as a hypothesis that should be verified for the specific graph G.

                Instances
                  theorem GraphWithCycles.deformedCheck_exists {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) [G.HasValidPaths] (s : G.StabilizerCheck) :

                  Given the HasValidPaths assumption, deformed checks are always well-defined

                  The Deformed Check as Operator Product #

                  We can characterize the deformed check in terms of operator multiplication.

                  def GraphWithCycles.edgeZOperatorSupport {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) (γ : EdgePath E) :

                  The edge Z-support can be viewed as a product of Z operators

                  Equations
                  Instances For

                    The deformed check's edge Z-support is the symmetric difference of the original support and the path

                    Summary Theorems #

                    theorem GraphWithCycles.deformedCheck_main {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (s : G.StabilizerCheck) (γ : EdgePath E) (h_no_edge_Z : s.zSupportOnE = ) (h_valid : G.IsValidDeformingPath s.zSupportOnV γ) :

                    Main theorem: Deformed checks are well-defined and commute with Gauss law operators.

                    Given:

                    • A stabilizer check s from the original code (commutes with L)
                    • A valid deforming path γ with ∂γ = S_Z ∩ V_G
                    • The original check has no Z-support on edges

                    Then:

                    • The deformed check s̃ = s · ∏_{e∈γ} Z_e is well-defined
                    • s̃ commutes with all Gauss law operators A_v

                    The partition theorem: every stabilizer check falls into exactly one of Set C or Set S, and its deformation behavior is determined by which set it belongs to.

                    Summary #

                    The deformed check formalization captures:

                    1. Definition: For a stabilizer check s_j with Z-support S_Z, the deformed check is: s̃_j = s_j · ∏_{e ∈ γ} Z_e where γ is an edge-path satisfying ∂γ = S_Z ∩ V_G.

                    2. Partition into Sets C and S:

                      • Set C: Checks with S_Z ∩ V_G = ∅ (no Z-support on graph vertices) For these: s̃_j = s_j (use empty path γ = ∅)
                      • Set S: Checks with S_Z ∩ V_G ≠ ∅ (nontrivial Z-support on graph vertices) For these: s̃_j ≠ s_j (require nontrivial path)
                    3. Well-Definedness: Deformed checks are well-defined because:

                      • All stabilizers commute with L, so |S_Z ∩ V_G| is even
                      • For even-cardinality vertex sets, valid paths exist in connected graphs
                    4. Key Property: Deformed checks commute with all Gauss law operators A_v. This follows from the boundary condition: at each vertex, the symplectic form (counting anticommuting pairs) is even.

                    5. Preservation: Deformation preserves:

                      • X-support on vertices
                      • Z-support on vertices
                      • X-support on edges
                      • Phase
                      • Deformability (even Z-support cardinality)
                    6. Algebraic Structure:

                      • Deformation is involutive: deforming twice returns to original
                      • Composition of deformations uses symmetric difference of paths

                    This is the specialization of the general DeformedOperator construction (Def_4) to the case of stabilizer checks from the original code.