Remark 10: Flexibility of Graph G

Statement

The gauging measurement procedure (Definition 5) allows arbitrary choice of the connected graph G with vertex set equal to the support of L. The properties of the deformed code depend strongly on this choice.

Additional flexibility:

1. Dummy vertices: G can have additional vertices beyond the support of L, achieved by gauging L' = L · ∏_{dummy} X_v.
2. Graph properties: The choice of G determines |E| (edge qubit count), deformed check weights (path lengths), and distance (expansion).

Main Results

• extendedLogicalOp : L' on V ⊕ D, the extended logical with dummy vertices
• extendedLogicalOp_eq_mul : L' = L · ∏_{d ∈ D} X_d (factorization)
• extendedLogicalOp_self_inverse : L' is self-inverse
• measurement_sign_with_dummies : σ(L') = σ(L) when dummies give +1
• deformed_code_edge_overhead : the deformed code has |V| + |E| qubits, so different graphs give different overhead via |E|
• deformed_code_check_overhead : the deformed code has |V| + |C| + |J| checks
• edge_expansion_lower_bounds_boundary : expansion of G controls distance

Dummy vertices

The graph G can have additional "dummy" vertices beyond the support of L. We formalize this by considering a type V ⊕ D that extends V with dummy vertices, and defining L' = L · ∏{d ∈ D} X_d = ∏{q ∈ V ⊕ D} X_q.

The key insight: since dummy qubits are in |+⟩ (eigenstate of X with eigenvalue +1), measuring X on a dummy vertex always gives +1 (outcome 0 in ZMod 2). Therefore the measurement sign of L' equals that of L.

def FlexibilityOfGraphG.originalLogicalOp {V : Type u_1} : PauliOp V

The original logical operator L on V: L = ∏_{v ∈ V} X_v.

Equations

• FlexibilityOfGraphG.originalLogicalOp = { xVec := fun (x : V) => 1, zVec := 0 }

def FlexibilityOfGraphG.extendedLogicalOp {V : Type u_1} {D : Type u_2} : PauliOp (V ⊕ D)

The extended logical operator L' on the extended vertex type V ⊕ D. L' = ∏{q ∈ V ⊕ D} X_q = L · ∏{d ∈ D} X_d.

Equations

• FlexibilityOfGraphG.extendedLogicalOp = { xVec := fun (x : V ⊕ D) => 1, zVec := 0 }

def FlexibilityOfGraphG.dummyXProduct {V : Type u_1} {D : Type u_2} : PauliOp (V ⊕ D)

The dummy X product: ∏_{d ∈ D} X_d acting on V ⊕ D.

Equations

• FlexibilityOfGraphG.dummyXProduct = { xVec := fun (q : V ⊕ D) => match q with | Sum.inl val => 0 | Sum.inr val => 1, zVec := 0 }

def FlexibilityOfGraphG.liftedLogicalOp {V : Type u_1} {D : Type u_2} : PauliOp (V ⊕ D)

L lifted to V ⊕ D: acts as X on all V-qubits and I on D-qubits.

Equations

• FlexibilityOfGraphG.liftedLogicalOp = { xVec := fun (q : V ⊕ D) => match q with | Sum.inl val => 1 | Sum.inr val => 0, zVec := 0 }

theorem FlexibilityOfGraphG.extendedLogicalOp_eq_mul {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : extendedLogicalOp = liftedLogicalOp * dummyXProduct

Key factorization: L' = L_lift · ∏_{d ∈ D} X_d on V ⊕ D. The extended logical is the product of the lifted original logical and the dummy X product.

theorem FlexibilityOfGraphG.extendedLogicalOp_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : extendedLogicalOp * extendedLogicalOp = 1

L' is self-inverse: L' · L' = 1.

theorem FlexibilityOfGraphG.extendedLogicalOp_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : extendedLogicalOp.zVec = 0

L' is pure X-type: it has no Z-support.

theorem FlexibilityOfGraphG.extendedLogicalOp_supportX_eq_univ {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : extendedLogicalOp.supportX = Finset.univ

The X-support of L' is all of V ⊕ D.

theorem FlexibilityOfGraphG.extendedLogicalOp_eq_prodX_univ {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : extendedLogicalOp = PauliOp.prodX Finset.univ

L' equals prodX(univ) on V ⊕ D.

@[simp]

theorem FlexibilityOfGraphG.extendedLogicalOp_xVec_original {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (v : V) : extendedLogicalOp.xVec (Sum.inl v) = 1

L' restricted to original vertices matches L: xVec on Sum.inl v is 1.

@[simp]

theorem FlexibilityOfGraphG.extendedLogicalOp_xVec_dummy {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (d : D) : extendedLogicalOp.xVec (Sum.inr d) = 1

L' on dummy vertices: xVec on Sum.inr d is 1.

@[simp]

theorem FlexibilityOfGraphG.extendedLogicalOp_zVec_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (q : V ⊕ D) : extendedLogicalOp.zVec q = 0

L' has no Z-action on any qubit.

@[simp]

theorem FlexibilityOfGraphG.liftedLogicalOp_xVec_original {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (v : V) : liftedLogicalOp.xVec (Sum.inl v) = 1

The lifted logical matches the original on V-qubits.

@[simp]

theorem FlexibilityOfGraphG.liftedLogicalOp_xVec_dummy {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (d : D) : liftedLogicalOp.xVec (Sum.inr d) = 0

The lifted logical is identity on D-qubits.

@[simp]

theorem FlexibilityOfGraphG.dummyXProduct_xVec_original {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (v : V) : dummyXProduct.xVec (Sum.inl v) = 0

The dummy X product is identity on V-qubits.

@[simp]

theorem FlexibilityOfGraphG.dummyXProduct_xVec_dummy {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (d : D) : dummyXProduct.xVec (Sum.inr d) = 1

The dummy X product acts as X on D-qubits.

theorem FlexibilityOfGraphG.measurement_sign_with_dummies {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (originalOutcomes : V → ZMod 2) (dummyOutcomes : D → ZMod 2) (h_dummy_plus : ∀ (d : D), dummyOutcomes d = 0) : ∑ q : V ⊕ D, Sum.elim originalOutcomes dummyOutcomes q = ∑ v : V, originalOutcomes v

Measurement sign with dummies: the measurement sign of L' equals that of L when dummy vertices give +1 outcomes (outcome 0 in ZMod 2). This is the formal content of "dummy vertices don't affect the logical measurement."

theorem FlexibilityOfGraphG.extendedLogicalOp_weight {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : extendedLogicalOp.weight = Fintype.card V + Fintype.card D

The weight of L' equals |V| + |D|.

theorem FlexibilityOfGraphG.extendedLogicalOp_no_dummies {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] [IsEmpty D] : extendedLogicalOp.weight = Fintype.card V

When D is empty, L' restricted to V has the same weight as L.

theorem FlexibilityOfGraphG.dummyXProduct_zVec_zero {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (q : V ⊕ D) : dummyXProduct.zVec q = 0

The Z-support of the dummy X product is empty on all qubits. This means dummyXProduct commutes with everything on the Z side, and adding dummy X operators never changes Z-support parity.

theorem FlexibilityOfGraphG.liftedLogicalOp_zVec_zero {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] (q : V ⊕ D) : liftedLogicalOp.zVec q = 0

The lifted logical has empty Z-support (pure X-type).

theorem FlexibilityOfGraphG.dummyXProduct_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : dummyXProduct * dummyXProduct = 1

The dummy X product is self-inverse.

theorem FlexibilityOfGraphG.liftedLogicalOp_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : liftedLogicalOp * liftedLogicalOp = 1

The lifted logical is self-inverse.

theorem FlexibilityOfGraphG.liftedLogicalOp_comm_dummyXProduct {V : Type u_1} [Fintype V] [DecidableEq V] {D : Type u_2} [Fintype D] [DecidableEq D] : liftedLogicalOp * dummyXProduct = dummyXProduct * liftedLogicalOp

The lifted logical and dummy X product commute (both pure X-type).

Graph properties affect deformed code overhead

The choice of graph G determines the parameters of the deformed code:

• Number of edge qubits = |E(G)| (from deformedStabilizerCode_numQubits)
• Number of Gauss checks = |V| (one per vertex)
• Number of flux checks = |C| (one per cycle) These facts connect existing definitions to the remark's claims.

theorem FlexibilityOfGraphG.deformed_code_edge_overhead {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 : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).numQubits = Fintype.card V + Fintype.card ↑G.edgeSet

The deformed code's qubit count is |V| + |E|, so the edge qubit overhead (the additional qubits beyond the original |V|) is exactly |E(G)|. Different graphs G give different overhead via their edge count.

theorem FlexibilityOfGraphG.deformed_code_check_overhead {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 : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).numChecks = Fintype.card V + Fintype.card C + Fintype.card J

The deformed code's check count is |V| + |C| + |J|: |V| Gauss checks, |C| flux checks, and |J| deformed original checks. The overhead in checks beyond the original |J| is |V| + |C|.

theorem FlexibilityOfGraphG.different_graphs_different_qubit_count {V : Type u_1} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V) [DecidableRel G₁.Adj] [Fintype ↑G₁.edgeSet] [DecidableRel G₂.Adj] [Fintype ↑G₂.edgeSet] (h_ne : Fintype.card ↑G₁.edgeSet ≠ Fintype.card ↑G₂.edgeSet) : Fintype.card V + Fintype.card ↑G₁.edgeSet ≠ Fintype.card V + Fintype.card ↑G₂.edgeSet

Two graphs with different edge counts produce deformed codes with different qubit counts. The qubit overhead difference equals the edge count difference.

Expansion and code distance

The Cheeger constant of G affects the distance of the deformed code. By Rem_4, for any valid subset S ⊆ V with |S| ≤ |V|/2: h(G) · |S| ≤ |∂S| This means an expander graph ensures that small vertex subsets have large edge boundaries, which prevents low-weight logical operators in the deformed code from surviving the deformation.

theorem FlexibilityOfGraphG.edge_expansion_lower_bounds_boundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c : ℝ) (hexp : QEC1.SimpleGraph.IsExpander G c) (S : Finset V) (hne : S.Nonempty) (hsize : 2 * S.card ≤ Fintype.card V) : c * ↑S.card ≤ ↑(QEC1.SimpleGraph.edgeBoundary G S).card

For an expander graph, every valid subset has proportionally large boundary. This is the mechanism by which expansion of G controls the distance of the deformed code: logical operators supported on small subsets necessarily have large edge boundary.

theorem FlexibilityOfGraphG.connected_has_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (hconn : G.Connected) (hcard : 2 ≤ Fintype.card V) : 0 < Fintype.card ↑G.edgeSet

For a connected graph on ≥ 2 vertices, the edge set is nonempty (at least one edge exists). This means gauging always introduces at least one auxiliary qubit.

Deformed check weight depends on edge-path length

The weight of the deformed check s̃_j on the extended system V ⊕ E depends on:

• The original check s_j (its X- and Z-support on V)
• The edge-path γ_j (determines the Z-support on E)

The Z-support of s̃_j on edges is exactly the support of γ_j, so the deformed check weight includes a contribution from the number of edges in γ_j. Shorter paths in G lead to lower-weight deformed checks.

theorem FlexibilityOfGraphG.deformedCheck_zSupport_on_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (DeformedCode.deformedCheck G s γ).zVec (Sum.inr e) = γ e

The edge Z-support of a deformed check equals the support of the edge-path γ. More edges in γ means more Z-support on edge qubits, hence higher weight. This connects the graph structure (path lengths) to check weights.

theorem FlexibilityOfGraphG.deformedCheck_xSupport_on_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (DeformedCode.deformedCheck G s γ).xVec (Sum.inr e) = 0

The edge X-support of a deformed check is empty: deformed checks have no X-action on edge qubits.

theorem FlexibilityOfGraphG.deformedCheck_edge_action_count {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) : {e : ↑G.edgeSet | (DeformedCode.deformedCheck G s γ).zVec (Sum.inr e) ≠ 0}.card = {e : ↑G.edgeSet | γ e ≠ 0}.card

The number of edge qubits where the deformed check acts non-trivially (via Z) equals the number of edges in γ with γ(e) ≠ 0. This is the "edge contribution" to the deformed check weight.

theorem FlexibilityOfGraphG.deformedCheck_zero_path_edge_count {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) : {e : ↑G.edgeSet | (DeformedCode.deformedCheck G s 0).zVec (Sum.inr e) ≠ 0}.card = 0

A zero edge-path adds no edge weight: the deformed check acts only on vertices.