Documentation

QEC1.Definitions.Def_4_DeformedOperator

Def_4: Deformed Operator #

Statement #

Let $P$ be a Pauli operator that commutes with the logical operator $L = \prod_{v \in V_G} X_v$. Write $P = i^{\sigma} \prod_{v \in \mathcal{S}_X} X_v \prod_{v \in \mathcal{S}_Z} Z_v$ where $\mathcal{S}_X$ is the $X$-type support and $\mathcal{S}_Z$ is the $Z$-type support of $P$. Since $P$ commutes with $L$, we have $|\mathcal{S}_Z| \equiv 0 \pmod{2}$.

The deformed operator $\tilde{P}$ is defined as: $$\tilde{P} = P \prod_{e \in \gamma} Z_e$$ where $\gamma$ is an edge-path in $G$ satisfying $\partial \gamma = \mathcal{S}_Z \cap V_G$ (i.e., the boundary of the edge-set $\gamma$ equals the $Z$-type support of $P$ restricted to the vertices of $G$). Such a path $\gamma$ exists because $|\mathcal{S}_Z \cap V_G|$ is even.

Convention: We typically choose $\gamma$ to be a minimum-weight path (shortest collection of edges) satisfying the boundary condition.

Note: If $P$ does not commute with $L$, then $|\mathcal{S}_Z \cap V_G|$ is odd, no valid path $\gamma$ exists, and $P$ has no well-defined deformed version.

Main Definitions #

Key Properties #

Corollaries #

Z-Type Support Restricted to Graph Vertices #

In the gauging context, we have:

The Z-type support of P restricted to vertices V_G determines the boundary condition.

def GraphWithCycles.zSupportOnVertices {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) (zSupport : Finset V) :

A Pauli operator's Z-type support restricted to the graph vertices. This is S_Z ∩ V_G in the paper notation. We represent it as a binary vector over V.

Equations
Instances For
    def GraphWithCycles.zSupportVector {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) (zSupport : Finset V) :

    The binary vector representation of Z-support restricted to V

    Equations
    Instances For
      @[simp]
      theorem GraphWithCycles.zSupportVector_apply {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 : Finset V) (v : V) :
      G.zSupportVector S v = if v S then 1 else 0
      @[simp]
      theorem GraphWithCycles.zSupportVector_mem {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 : Finset V) (v : V) (h : v S) :
      @[simp]
      theorem GraphWithCycles.zSupportVector_not_mem {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 : Finset V) (v : V) (h : vS) :

      Edge Paths as Binary Vectors #

      An edge-path γ in the graph is represented as a subset of edges (or equivalently, a binary vector over E). The boundary map ∂ gives the vertices that are endpoints of an odd number of edges in γ.

      @[reducible, inline]
      abbrev GraphWithCycles.EdgePath (E : Type u_4) :
      Type u_4

      An edge-path in the graph, represented as a subset of edges

      Equations
      Instances For
        def GraphWithCycles.edgePathVector {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-path as a binary vector over edges

        Equations
        Instances For
          @[simp]
          theorem GraphWithCycles.edgePathVector_apply {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) (e : E) :
          G.edgePathVector γ e = if e γ then 1 else 0
          @[simp]
          theorem GraphWithCycles.edgePathVector_mem {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) (e : E) (h : e γ) :
          G.edgePathVector γ e = 1
          @[simp]
          theorem GraphWithCycles.edgePathVector_not_mem {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) (e : E) (h : eγ) :
          G.edgePathVector γ e = 0
          def GraphWithCycles.edgePathBoundary {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 boundary of an edge-path: ∂γ = sum of boundaries of individual edges

          Equations
          Instances For
            theorem GraphWithCycles.edgePathBoundary_apply {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) (v : V) :
            G.edgePathBoundary γ v = _eγ with G.isIncident _e v, 1

            Alternative characterization: the boundary at vertex v counts (mod 2) edges in γ incident to v

            theorem GraphWithCycles.edgePathBoundary_eq_one_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) (γ : EdgePath E) (v : V) :
            G.edgePathBoundary γ v = 1 {eγ | G.isIncident e v}.card % 2 = 1

            The boundary is 1 at v iff an odd number of edges in γ are incident to v

            theorem GraphWithCycles.edgePathBoundary_eq_zero_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) (γ : EdgePath E) (v : V) :
            G.edgePathBoundary γ v = 0 {eγ | G.isIncident e v}.card % 2 = 0

            The boundary is 0 at v iff an even number of edges in γ are incident to v

            Valid Deforming Paths #

            A valid deforming path γ for Z-support S_Z is one satisfying the boundary condition: ∂γ = S_Z (as binary vectors over V).

            For such a path to exist, |S_Z| must be even (since ∂ is the boundary map and boundaries in Z₂-homology have even cardinality).

            def GraphWithCycles.IsValidDeformingPath {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) (zSupport : Finset V) (γ : EdgePath E) :

            A valid deforming path γ for Z-support S is one where ∂γ = S (as binary vectors)

            Equations
            Instances For
              theorem GraphWithCycles.isValidDeformingPath_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 : Finset V) (γ : EdgePath E) :
              G.IsValidDeformingPath S γ ∀ (v : V), G.edgePathBoundary γ v = G.zSupportVector S v

              Characterization: γ is valid iff ∂γ = S at each vertex

              theorem GraphWithCycles.validPath_boundary_on_support {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 : Finset V) (γ : EdgePath E) (h : G.IsValidDeformingPath S γ) (v : V) (hv : v S) :

              At vertices in S, the boundary is 1

              theorem GraphWithCycles.validPath_boundary_off_support {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 : Finset V) (γ : EdgePath E) (h : G.IsValidDeformingPath S γ) (v : V) (hv : vS) :

              At vertices not in S, the boundary is 0

              Even Cardinality Condition #

              The boundary map ∂ : Z₂^E → Z₂^V has the property that the sum of ∂γ over all vertices is 0 (since each edge contributes to exactly 2 vertices, and 1+1=0 in Z₂).

              This means: if ∂γ = S (as vectors), then |S| must be even for a solution to exist.

              theorem GraphWithCycles.boundary_sum_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) (γ : EdgePath E) :
              v : V, G.edgePathBoundary γ v = 0

              The sum of boundary values over all vertices is always 0. This is because each edge is incident to exactly 2 vertices.

              theorem GraphWithCycles.zSupport_even_of_valid_path_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 : Finset V) (γ : EdgePath E) (h : G.IsValidDeformingPath S γ) :
              S.card % 2 = 0

              If a valid deforming path exists for S, then |S| is even

              theorem GraphWithCycles.no_valid_path_if_odd {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 : Finset V) (h : S.card % 2 = 1) :
              ¬∃ (γ : EdgePath E), G.IsValidDeformingPath S γ

              The contrapositive: if |S| is odd, no valid deforming path exists

              Deformable Pauli Operators #

              A Pauli operator P is deformable if it commutes with the logical operator L = ∏_v X_v. This ensures that |S_Z ∩ V_G| is even, so a valid deforming path exists.

              structure GraphWithCycles.DeformablePauliOperator {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 Pauli operator (represented by its supports) that is deformable. The key condition is that it commutes with L = ∏_{v ∈ V} X_v, which means the Z-support restricted to V has even cardinality.

              • xSupportOnV : Finset V

                The X-type support on vertices: {v | P acts as X or Y on v}

              • zSupportOnV : Finset V

                The Z-type support on vertices: {v | P acts as Z or Y on v}

              • xSupportOnE : Finset E

                The X-type support on edges (typically empty for original code checks)

              • zSupportOnE : Finset E

                The Z-type support on edges (typically empty for original code checks)

              • phase : ZMod 4

                The global phase (represented as ZMod 4: 0=+1, 1=+i, 2=-1, 3=-i)

              • zSupport_even : self.zSupportOnV.card % 2 = 0

                The key deformability condition: |S_Z ∩ V| is even

              Instances For
                theorem GraphWithCycles.deformable_iff_commutes_with_L {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) (_xS zS : Finset V) (_xE _zE : Finset E) (_ph : ZMod 4) :
                zS.card % 2 = 0 zS.card % 2 = 0

                The deformability condition as stated: P commutes with L = ∏_v X_v. This is equivalent to having even Z-support on V.

                Construction of the Deformed Operator #

                Given a deformable operator P and a valid deforming path γ, the deformed operator P̃ is:

                In the binary vector representation:

                The deformed operator P̃ = P · ∏_{e ∈ γ} Z_e. Given P and a valid deforming path γ, construct P̃.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The deformed operator's Z-support on edges (alternative formulation using XOR)

                  theorem GraphWithCycles.symmDiff_vector {E : Type u_2} [DecidableEq E] [Fintype E] (S T : Finset E) (e : E) :
                  (if e symmDiff S T then 1 else 0) = (if e S then 1 else 0) + if e T then 1 else 0

                  Binary vector representation of symmetric difference

                  theorem GraphWithCycles.deformedOperator_zSupport_eq_sum {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) (P : G.DeformablePauliOperator) (γ : EdgePath E) (e : E) :

                  The deformed operator's edge Z-support as binary vector is P's + γ's

                  The Deformed Operator Commutes with Gauss Law Operators #

                  The key property: if γ is a valid deforming path (∂γ = S_Z^V), then P̃ commutes with all Gauss law operators A_v.

                  Recall: A_v = X_v ∏_{e∋v} X_e The symplectic form ω(P̃, A_v) counts:

                  For commutation: ω(P̃, A_v) ≡ 0 (mod 2)

                  If ∂γ = S_Z^V, then:

                  So ω(P̃, A_v) = |S_Z^V ∩ {v}| + |γ ∩ edges(v)| ≡ 0 (mod 2) in both cases.

                  def GraphWithCycles.deformed_gaussLaw_symplectic {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) (P : G.DeformablePauliOperator) (γ : EdgePath E) (v : V) :

                  The symplectic form between the deformed operator and a Gauss law operator. This counts anticommuting pairs: positions where P̃ has Z-type and A_v has X-type.

                  Equations
                  Instances For
                    def GraphWithCycles.deformed_gaussLaw_symplectic_simple {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) (zSupportOnV : Finset V) (γ : EdgePath E) (v : V) :

                    Assuming P has no Z-support on edges originally, simplification

                    Equations
                    Instances For
                      theorem GraphWithCycles.deformed_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) (zSupportOnV : Finset V) (γ : EdgePath E) (h_valid : G.IsValidDeformingPath zSupportOnV γ) (v : V) :
                      G.deformed_gaussLaw_symplectic_simple zSupportOnV γ v % 2 = 0

                      The key theorem: if γ is a valid deforming path, P̃ commutes with all A_v. Proof outline:

                      • If v ∈ S_Z^V: contributes 1 from vertex, and (∂γ)_v = 1 means odd edges, so total even
                      • If v ∉ S_Z^V: contributes 0 from vertex, and (∂γ)_v = 0 means even edges, so total even
                      theorem GraphWithCycles.deformed_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) (P : G.DeformablePauliOperator) (γ : EdgePath E) (_h_no_edge_Z : P.zSupportOnE = ) (h_valid : G.IsValidDeformingPath P.zSupportOnV γ) (v : V) :

                      Corollary: the full deformed operator (assuming P originally had no Z-support on edges) commutes with all Gauss law operators

                      Non-Commuting Operators Cannot Be Deformed #

                      If P does not commute with L (i.e., |S_Z ∩ V| is odd), then no valid deforming path exists, and P has no well-defined deformed version.

                      theorem GraphWithCycles.no_deformed_if_odd_zSupport {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) (zSupportOnV : Finset V) (h_odd : zSupportOnV.card % 2 = 1) :
                      ¬∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ

                      If |S_Z^V| is odd, P doesn't commute with L and cannot be deformed

                      theorem GraphWithCycles.valid_path_implies_commutes {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) (zSupportOnV : Finset V) (γ : EdgePath E) (h : G.IsValidDeformingPath zSupportOnV γ) :
                      zSupportOnV.card % 2 = 0

                      Alternative statement: if ∃ valid path, then P commutes with L (even Z-support)

                      Properties of the Deformed Operator #

                      The X-support on vertices is unchanged after deformation

                      The Z-support on vertices is unchanged after deformation

                      The X-support on edges is unchanged after deformation

                      theorem GraphWithCycles.deformed_phase_eq {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) (P : G.DeformablePauliOperator) (γ : EdgePath E) :

                      The phase is unchanged after deformation

                      theorem GraphWithCycles.deformed_zSupport_even_eq {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) (P : G.DeformablePauliOperator) (γ : EdgePath E) :
                      =

                      The deformability condition is preserved

                      Minimum Weight Path Convention #

                      The paper mentions choosing γ to be a minimum-weight path. This is a convention for making the choice canonical and minimizing the overhead of the deformation.

                      def GraphWithCycles.edgePathWeight {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 weight of an edge-path is its cardinality

                      Equations
                      Instances For
                        def GraphWithCycles.IsMinWeightValidPath {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) (zSupportOnV : Finset V) (γ : EdgePath E) :

                        A minimum-weight valid deforming path

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem GraphWithCycles.min_weight_path_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) (zSupportOnV : Finset V) (h : ∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ) :
                          ∃ (γ : EdgePath E), G.IsMinWeightValidPath zSupportOnV γ

                          If any valid path exists, a minimum-weight one exists (by finiteness of E)

                          Summary of Deformed Operator #

                          The deformed operator construction captures:

                          1. Input: A Pauli operator P with Z-support S_Z on vertices
                          2. Condition: P must commute with L = ∏_v X_v, equivalently |S_Z| even
                          3. Construction: Choose edge-path γ with ∂γ = S_Z, form P̃ = P · ∏_{e∈γ} Z_e
                          4. Result: P̃ has the same vertex supports as P, with additional Z on edges in γ
                          5. Key Property: P̃ commutes with all Gauss law operators A_v
                          6. Non-existence: If P doesn't commute with L (|S_Z| odd), no deformed version exists
                          7. Convention: Choose γ to be minimum-weight among valid paths

                          Summary #

                          The deformed operator formalization captures:

                          1. Deformability Condition: A Pauli operator P is deformable iff it commutes with L = ∏_v X_v, equivalently iff |S_Z ∩ V_G| is even (Z-support restricted to graph vertices).

                          2. Valid Deforming Path: An edge-path γ satisfying ∂γ = S_Z ∩ V_G (the boundary equals the Z-support on vertices). Such paths exist iff |S_Z ∩ V_G| is even.

                          3. Deformed Operator P̃: Given P and valid path γ, form P̃ = P · ∏_{e∈γ} Z_e.

                            • Same X-support on V and E as P
                            • Same Z-support on V as P
                            • Z-support on E = P's Z-support on E ⊕ γ (symmetric difference)
                            • Same phase as P
                          4. Key Property: P̃ commutes with all Gauss law operators A_v. This is because at each vertex v, the contribution from Z-support on V and edges in γ incident to v always sums to 0 (mod 2) by the boundary condition.

                          5. Non-Commuting Case: If P doesn't commute with L (|S_Z| odd), no valid deforming path exists, and P has no well-defined deformed version.

                          6. Minimum Weight Convention: Typically choose γ to minimize |γ| among valid paths.

                          This construction is fundamental to the gauging measurement: it shows how original code operators transform during the gauging procedure while maintaining compatibility with the new Gauss law constraints.