Remark 8: Freedom in Deformed Checks

Statement

The deformed code is uniquely determined (as a codespace), but there is freedom in choosing the generating set:

• The A_v checks are fixed.
• The B_p checks can use any generating set of cycles for G.
• The s̃_j checks have freedom in choosing the paths γ_j.

Different choices of γ give equivalent codes: if γ and γ' both satisfy ∂γ = ∂γ' = S_Z(s)|_V, then s̃(γ') = s̃(γ) · B_c for some product of flux operators B_c. In particular, the difference γ + γ' lies in ker(∂) (the cycle space).

Main Results

• deformedCheck_diff_is_pure_Z_edge : s̃(γ') = s̃(γ) · (pure Z on edges from γ + γ')
• diff_path_in_ker_boundary : γ + γ' ∈ ker(∂) when both satisfy the boundary condition
• deformedCheck_diff_eq_fluxProduct : the difference operator has the form of a product of Z on edges
• different_paths_same_code : two DeformedCodeData produce codes with the same stabilizer group

Path Difference Lies in Cycle Space

theorem FreedomInDeformedChecks.diff_path_in_ker_boundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ γ' : ↑G.edgeSet → ZMod 2) (hbc : DeformedOperator.BoundaryCondition G s γ) (hbc' : DeformedOperator.BoundaryCondition G s γ') : (GraphMaps.boundaryMap G) (γ + γ') = 0

If two edge-paths both satisfy the boundary condition for the same check, their difference lies in ker(∂).

theorem FreedomInDeformedChecks.diff_path_mem_ker_boundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ γ' : ↑G.edgeSet → ZMod 2) (hbc : DeformedOperator.BoundaryCondition G s γ) (hbc' : DeformedOperator.BoundaryCondition G s γ') : γ + γ' ∈ (GraphMaps.boundaryMap G).ker

The path difference is in the kernel of the boundary map (LinearMap.ker version).

Deformed Checks Differ by a Pure-Z Edge Operator

def FreedomInDeformedChecks.pureZEdgeOp {V : Type u_1} (G : SimpleGraph V) (δ : ↑G.edgeSet → ZMod 2) : PauliOp (GaussFlux.ExtQubit G)

The pure-Z edge operator for an edge vector δ: acts as identity on vertices, Z on edges according to δ. This is exactly deformedOpExt G 1 δ.

Equations

• FreedomInDeformedChecks.pureZEdgeOp G δ = DeformedOperator.deformedOpExt G 1 δ

@[simp]

theorem FreedomInDeformedChecks.pureZEdgeOp_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) (v : V) : (pureZEdgeOp G δ).xVec (Sum.inl v) = 0

@[simp]

theorem FreedomInDeformedChecks.pureZEdgeOp_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (pureZEdgeOp G δ).xVec (Sum.inr e) = 0

@[simp]

theorem FreedomInDeformedChecks.pureZEdgeOp_zVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) (v : V) : (pureZEdgeOp G δ).zVec (Sum.inl v) = 0

@[simp]

theorem FreedomInDeformedChecks.pureZEdgeOp_zVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (pureZEdgeOp G δ).zVec (Sum.inr e) = δ e

theorem FreedomInDeformedChecks.pureZEdgeOp_pure_Z {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) : (pureZEdgeOp G δ).xVec = 0

A pure-Z edge operator is pure Z-type: no X-support.

theorem FreedomInDeformedChecks.pureZEdgeOp_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) : pureZEdgeOp G δ * pureZEdgeOp G δ = 1

A pure-Z edge operator is self-inverse.

theorem FreedomInDeformedChecks.deformedCheck_diff_is_pure_Z_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ γ' : ↑G.edgeSet → ZMod 2) : DeformedCode.deformedCheck G s γ' = DeformedCode.deformedCheck G s γ * pureZEdgeOp G (γ + γ')

The deformed check with path γ' equals the deformed check with path γ multiplied by the pure-Z edge operator for the path difference γ + γ'.

theorem FreedomInDeformedChecks.deformedCheck_diff_is_pure_Z_edge' {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ γ' : ↑G.edgeSet → ZMod 2) : DeformedCode.deformedCheck G s γ' = DeformedCode.deformedCheck G s γ * pureZEdgeOp G (γ' + γ)

Equivalently: s̃(γ') = s̃(γ) · B where B = pureZEdgeOp(γ' + γ).

The Difference Operator Commutes with All Checks

theorem FreedomInDeformedChecks.pureZEdgeOp_comm_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) (hδ : (GraphMaps.boundaryMap G) δ = 0) (v : V) : (pureZEdgeOp G δ).PauliCommute (GaussFlux.gaussLawOp G v)

The pure-Z edge operator for a cycle (boundary-zero edge vector) commutes with all Gauss's law operators.

theorem FreedomInDeformedChecks.pureZEdgeOp_comm_flux {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (δ : ↑G.edgeSet → ZMod 2) (p : C) : (pureZEdgeOp G δ).PauliCommute (GaussFlux.fluxOp G cycles p)

The pure-Z edge operator commutes with all flux operators (both are pure Z-type).

theorem FreedomInDeformedChecks.pureZEdgeOp_comm_deformed {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (δ : ↑G.edgeSet → ZMod 2) (data : DeformedCode.DeformedCodeData G checks) (j : J) : (pureZEdgeOp G δ).PauliCommute (DeformedCode.deformedOriginalChecks G checks data j)

The pure-Z edge operator commutes with deformed checks (both have no X-support on edges, and the pure-Z op has no Z-support on vertices).

Different Paths Yield the Same Stabilizer Group

theorem FreedomInDeformedChecks.deformedOriginalCheck_alternative_in_group {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data data' : DeformedCode.DeformedCodeData G checks) (j : J) : ∃ (B : PauliOp (GaussFlux.ExtQubit G)), DeformedCode.deformedOriginalChecks G checks data' j = DeformedCode.deformedOriginalChecks G checks data j * B ∧ B.xVec = 0 ∧ (GraphMaps.boundaryMap G) (data.edgePath j + data'.edgePath j) = 0

Helper: a deformed check with path γ' is in the stabilizer group generated by the deformed code using path γ, provided γ + γ' ∈ ker(∂) and the flux operators for the cycle are in the stabilizer group. More precisely, s̃_j(γ'_j) equals s̃_j(γ_j) times a pure-Z edge operator, and both factors are in the stabilizer group.

theorem FreedomInDeformedChecks.different_paths_same_code {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data data' : DeformedCode.DeformedCodeData G checks) (j : J) : DeformedCode.deformedOriginalChecks G checks data' j = DeformedCode.deformedOriginalChecks G checks data j * pureZEdgeOp G (data.edgePath j + data'.edgePath j)

Main theorem: Different choices of edge-paths produce the same deformed code (up to stabilizer equivalence). Specifically, if data and data' are two DeformedCodeData with potentially different edge-paths, then for each check index j, the deformed check from data' differs from that of data by a pure-Z edge operator whose edge support lies in ker(∂) (the cycle space). This means the two deformed checks are related by multiplication with an element that is a product of flux operators.

We prove the concrete algebraic fact: for each j, s̃_j(γ'_j) = s̃_j(γ_j) · pureZEdgeOp(γ_j + γ'_j) where ∂(γ_j + γ'_j) = 0.

theorem FreedomInDeformedChecks.different_paths_diff_in_cycle_space {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data data' : DeformedCode.DeformedCodeData G checks) (j : J) : data.edgePath j + data'.edgePath j ∈ (GraphMaps.boundaryMap G).ker

The path difference for any check lies in the cycle space (ker ∂).

Gauss's Law Checks Are Fixed

theorem FreedomInDeformedChecks.gaussLaw_checks_fixed {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data data' : DeformedCode.DeformedCodeData G checks) (v : V) : DeformedCode.deformedCodeChecks G cycles checks data (DeformedCode.CheckIndex.gaussLaw v) = DeformedCode.deformedCodeChecks G cycles checks data' (DeformedCode.CheckIndex.gaussLaw v)

The Gauss's law checks do not depend on the choice of DeformedCodeData.

theorem FreedomInDeformedChecks.flux_checks_fixed {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data data' : DeformedCode.DeformedCodeData G checks) (p : C) : DeformedCode.deformedCodeChecks G cycles checks data (DeformedCode.CheckIndex.flux p) = DeformedCode.deformedCodeChecks G cycles checks data' (DeformedCode.CheckIndex.flux p)

The flux checks do not depend on the choice of DeformedCodeData.

The Difference Operator Commutes with All Deformed Code Checks

theorem FreedomInDeformedChecks.pureZEdgeOp_comm_allChecks {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (δ : ↑G.edgeSet → ZMod 2) (hδ : (GraphMaps.boundaryMap G) δ = 0) (data : DeformedCode.DeformedCodeData G checks) (_hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (a : DeformedCode.CheckIndex V C J) : (pureZEdgeOp G δ).PauliCommute (DeformedCode.allChecks G cycles checks data a)

The pure-Z edge operator for a path difference commutes with every check in the deformed code, when the path difference is in ker(∂).

Corollaries

theorem FreedomInDeformedChecks.deformedChecks_different_paths_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ γ' : ↑G.edgeSet → ZMod 2) (_hbc : DeformedOperator.BoundaryCondition G s γ) (_hbc' : DeformedOperator.BoundaryCondition G s γ') : (DeformedCode.deformedCheck G s γ).PauliCommute (DeformedCode.deformedCheck G s γ')

Two deformed checks for the same original check always commute.

@[simp]

theorem FreedomInDeformedChecks.pureZEdgeOp_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (δ : ↑G.edgeSet → ZMod 2) : pureZEdgeOp G δ * pureZEdgeOp G δ = 1

The pure-Z edge operator for a path difference is self-inverse.

theorem FreedomInDeformedChecks.deformedCheck_recover {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ γ' : ↑G.edgeSet → ZMod 2) : DeformedCode.deformedCheck G s γ = DeformedCode.deformedCheck G s γ' * pureZEdgeOp G (γ' + γ)

Recovering one deformed check from another: s̃(γ) = s̃(γ') · pureZEdgeOp(γ' + γ).