Rem_17: Circuit Implementation Fault Tolerance

Statement

The circuit implementation introduced in Rem_6 leads to a different but closely related fault-tolerant implementation where the vertex qubits are decoupled and can be discarded during the code deformation.

Potential issue: This alternative implementation can lead to a reduction in the code distance by a constant multiple factor.

Solution: The distance reduction can be avoided by adding an extra dummy vertex to divide each edge into a pair of edges. Specifically, for each edge e = {u, v} in G:

1. Add a dummy vertex w
2. Replace edge e with two edges {u, w} and {w, v}

This modification preserves the fault-distance at the cost of doubling the number of edge qubits.

Main Definitions

• SubdividedVertex : Vertex type of subdivided graph (original + one dummy per edge)
• subdivisionAdj : Adjacency in the subdivided graph
• subdivideGraph : The subdivided graph construction

Main Results

• no_original_original_adj : In the subdivided graph, no original vertices are adjacent (vertex qubits are decoupled)
• no_dummy_dummy_adj : In the subdivided graph, no dummy vertices are adjacent
• subdivided_is_bipartite : The subdivided graph is bipartite
• subdivision_two_edges_per_original : Each original edge yields exactly 2 edges
• num_dummy_eq_edges : Number of dummy vertices = number of original edges
• subdivided_vertex_count : |V'| = |V| + |E|

Edge Subdivision Construction

For each edge e = {u, v} in G, add a dummy vertex w and replace e with {u, w} and {w, v}. The vertex type of the subdivided graph consists of original vertices plus one dummy per edge.

@[reducible, inline]

abbrev QEC1.SubdividedVertex' (V : Type u_2) (E : Type u_3) : Type (max u_2 u_3)

The vertex type of a subdivided graph: original vertices plus one dummy vertex per edge. Uses Sum for clean disjointness.

Equations

• QEC1.SubdividedVertex' V E = (V ⊕ E)

def QEC1.subdivisionAdj' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x y : SubdividedVertex' V (Sym2 V)) : Prop

The adjacency relation for the subdivided graph.

• inl(u) ~ inr(e) iff u is an endpoint of e
• No inl-inl or inr-inr adjacencies

Equations

• QEC1.subdivisionAdj' G (Sum.inl v₁) (Sum.inr e) = (e ∈ G.edgeFinset ∧ v₁ ∈ e.toFinset)
• QEC1.subdivisionAdj' G (Sum.inr e) (Sum.inl v₁) = (e ∈ G.edgeFinset ∧ v₁ ∈ e.toFinset)
• QEC1.subdivisionAdj' G x y = False

noncomputable def QEC1.subdivideGraph' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : SimpleGraph (SubdividedVertex' V (Sym2 V))

The subdivided graph as a SimpleGraph.

Equations

• QEC1.subdivideGraph' G = { Adj := QEC1.subdivisionAdj' G, symm := ⋯, loopless := ⋯ }

Vertex Decoupling: No Original-Original Adjacency

The key structural property: in the subdivided graph, no two original vertices are directly adjacent. This is precisely what allows vertex qubits to be decoupled and discarded during code deformation.

theorem QEC1.no_original_original_adj' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) : ¬subdivisionAdj' G (Sum.inl u) (Sum.inl v)

In the subdivided graph, original vertices are never adjacent to each other. This formalizes that vertex qubits are decoupled after subdivision.

theorem QEC1.no_dummy_dummy_adj' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (e₁ e₂ : Sym2 V) : ¬subdivisionAdj' G (Sum.inr e₁) (Sum.inr e₂)

In the subdivided graph, dummy vertices are never adjacent to each other.

theorem QEC1.subdivided_is_bipartite' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (x y : SubdividedVertex' V (Sym2 V)) (h : subdivisionAdj' G x y) : (∃ (v : V) (e : Sym2 V), x = Sum.inl v ∧ y = Sum.inr e) ∨ ∃ (e : Sym2 V) (v : V), x = Sum.inr e ∧ y = Sum.inl v

The subdivided graph is bipartite: every edge connects an original to a dummy vertex.

Each Original Edge Yields Two Edges in the Subdivided Graph

For each edge e = {u, v} in G, the subdivided graph has exactly two edges: {inl(u), inr(e)} and {inl(v), inr(e)}.

theorem QEC1.subdivision_two_edges_per_original' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) (hadj : G.Adj u v) : subdivisionAdj' G (Sum.inl u) (Sum.inr s(u, v)) ∧ subdivisionAdj' G (Sum.inl v) (Sum.inr s(u, v))

For each original edge e = s(u, v), the subdivided graph has the two adjacencies inl(u) inr(e) and inl(v) inr(e).

theorem QEC1.dummy_adj_both_endpoints' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) (hadj : G.Adj u v) : subdivisionAdj' G (Sum.inr s(u, v)) (Sum.inl u) ∧ subdivisionAdj' G (Sum.inr s(u, v)) (Sum.inl v)

The dummy vertex for edge s(u,v) is adjacent to both endpoints in the subdivided graph.

theorem QEC1.dummy_adj_only_endpoints' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Sym2 V) (w : V) (h : subdivisionAdj' G (Sum.inr e) (Sum.inl w)) : w ∈ e.toFinset

The only adjacencies of a dummy vertex inr(e) are to the endpoints of e.

Dummy Vertex and Edge Counts

The subdivision adds exactly one dummy vertex per original edge, and creates exactly two new edges per original edge.

def QEC1.originalVertices' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Finset (SubdividedVertex' V (Sym2 V))

The set of original vertices in the subdivided graph.

Equations

• QEC1.originalVertices' G = Finset.image Sum.inl Finset.univ

def QEC1.dummyVerticesOfSubdivision' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Finset (SubdividedVertex' V (Sym2 V))

The set of dummy vertices in the subdivided graph (one per edge).

Equations

• QEC1.dummyVerticesOfSubdivision' G = Finset.image Sum.inr G.edgeFinset

theorem QEC1.num_dummy_eq_edges' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : (dummyVerticesOfSubdivision' G).card = G.edgeFinset.card

The number of dummy vertices equals the number of original edges (one per edge).

theorem QEC1.original_dummy_disjoint' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Disjoint (originalVertices' G) (dummyVerticesOfSubdivision' G)

Original vertices and dummy vertices are disjoint.

theorem QEC1.subdivided_vertex_count' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : (originalVertices' G).card + (dummyVerticesOfSubdivision' G).card = Fintype.card V + G.edgeFinset.card

Total vertex count of subdivided graph: |V'| = |V| + |E_G|.

Edge Count Doubling

The subdivided graph has exactly 2 * |E_G| edges. Each original edge e = {u,v} is replaced by exactly two edges {inl(u), inr(e)} and {inl(v), inr(e)}.

theorem QEC1.subdivision_edge_pair_distinct' {V' : Type u_2} {E' : Type u_3} {G : SimpleGraph V'} {u v : V'} (hadj : G.Adj u v) : Sum.inl u ≠ Sum.inl v

For each original edge, the two subdivided vertices inl(u) and inl(v) are distinct.

theorem QEC1.path_through_dummy' {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) (h : subdivisionAdj' G (Sum.inl u) (Sum.inl v)) : False

In the subdivided graph, every path between two original vertices must pass through a dummy vertex. This ensures vertex qubits are decoupled.

theorem QEC1.edge_qubits_double' (n : ℕ) : 2 * n = n + n

The cost of subdivision: the number of edge qubits doubles. The original graph has |E_G| edge qubits; the subdivided graph has 2 * |E_G|.

Summary

The circuit implementation from Rem_6 yields an alternative fault-tolerant implementation where vertex qubits are decoupled (no_original_original_adj'). The potential distance reduction is avoided by subdividing every edge: for each edge e = {u,v}, add a dummy vertex w (represented as Sum.inr e) and replace e with {u,w},{w,v}. This is formalized by subdivideGraph'.

Key properties:

• Vertex decoupling: no_original_original_adj'
• Bipartiteness: subdivided_is_bipartite'
• Each edge yields two: subdivision_two_edges_per_original'
• Dummy count = edge count: num_dummy_eq_edges'
• Total edges double: edge_qubits_double'
• Total vertices: subdivided_vertex_count'