40 Rem 17: Circuit Implementation Fault Tolerance
This chapter formalizes the edge subdivision construction used to preserve fault-distance in the circuit implementation. The circuit implementation from Rem 6 leads to an alternative fault-tolerant scheme where vertex qubits are decoupled. A potential code distance reduction is avoided by subdividing each edge \(e = \{ u, v\} \) in \(G\): a dummy vertex \(w\) is added, replacing \(e\) with \(\{ u, w\} \) and \(\{ w, v\} \). This doubles the number of edge qubits but preserves the fault-distance.
Given a vertex type \(V\) and an edge type \(E\), the subdivided vertex type is the disjoint sum \(V \oplus E\), written \(\texttt{SubdividedVertex'}(V, E) := V \sqcup E\). Original vertices are embedded via \(\mathrm{inl}\) and dummy vertices (one per edge) via \(\mathrm{inr}\).
Let \(G\) be a simple graph on \(V\) with decidable adjacency. The subdivision adjacency on \(\texttt{SubdividedVertex'}(V, \mathrm{Sym2}(V))\) is defined by:
That is, a vertex \(\mathrm{inl}(v)\) is adjacent to \(\mathrm{inr}(e)\) if and only if \(v\) is an endpoint of the edge \(e\). There are no \(\mathrm{inl}\)–\(\mathrm{inl}\) or \(\mathrm{inr}\)–\(\mathrm{inr}\) adjacencies.
Let \(G\) be a simple graph on \(V\). The subdivided graph \(\mathrm{subdivideGraph}'(G)\) is the simple graph on \(\texttt{SubdividedVertex'}(V, \mathrm{Sym2}(V))\) with adjacency given by \(\mathrm{subdivisionAdj}'(G)\). The symmetry and irreflexivity axioms are verified as follows:
Symmetry: We case-split on \(x\) and \(y\). If \(x = \mathrm{inl}(v_1)\) and \(y = \mathrm{inr}(e)\), then the adjacency hypothesis directly gives the reverse. The cases \(\mathrm{inl}\)–\(\mathrm{inl}\) and \(\mathrm{inr}\)–\(\mathrm{inr}\) are contradictory by definition.
Irreflexivity: For any \(x\), we case-split; in both cases (\(\mathrm{inl}\) or \(\mathrm{inr}\)), the adjacency relation simplifies to \(\mathrm{False}\).
In the subdivided graph, no two original vertices are adjacent: for all \(u, v \in V\),
This formalizes that vertex qubits are decoupled after subdivision.
By simplification using the definition of \(\mathrm{subdivisionAdj}'\), the case \((\mathrm{inl}(u), \mathrm{inl}(v))\) reduces to \(\mathrm{False}\), so the negation holds trivially.
In the subdivided graph, no two dummy vertices are adjacent: for all edges \(e_1, e_2 \in \mathrm{Sym2}(V)\),
By simplification using the definition of \(\mathrm{subdivisionAdj}'\), the case \((\mathrm{inr}(e_1), \mathrm{inr}(e_2))\) reduces to \(\mathrm{False}\), so the negation holds trivially.
The subdivided graph is bipartite: every edge connects an original vertex to a dummy vertex. Formally, for all \(x, y \in \texttt{SubdividedVertex'}(V, \mathrm{Sym2}(V))\) with \(\mathrm{subdivisionAdj}'(G)(x,y)\), either
or
We case-split on \(x\) and \(y\).
Case \(x = \mathrm{inl}(v_1)\): We further case-split on \(y\).
If \(y = \mathrm{inl}(\_ )\), the adjacency hypothesis contradicts the definition (which reduces to \(\mathrm{False}\)).
If \(y = \mathrm{inr}(e)\), we take the first disjunct with witnesses \(v_1\) and \(e\), using reflexivity.
Case \(x = \mathrm{inr}(e)\): We further case-split on \(y\).
If \(y = \mathrm{inl}(v_1)\), we take the second disjunct with witnesses \(e\) and \(v_1\), using reflexivity.
If \(y = \mathrm{inr}(\_ )\), the adjacency hypothesis contradicts the definition.
For each original edge \(e = \{ u, v\} \) in \(G\) (i.e., \(G.\mathrm{Adj}(u, v)\)), the subdivided graph contains both adjacencies:
We prove each conjunct separately. For the first, we simplify \(\mathrm{subdivisionAdj}'\) to obtain the conditions \(\{ u, v\} \in E(G)\) (which holds since \(G.\mathrm{Adj}(u,v)\)) and \(u \in \{ u, v\} \) (which holds by membership in the symmetric pair). The second conjunct is proved identically, using \(v \in \{ u, v\} \).
The dummy vertex for edge \(\{ u, v\} \) is adjacent to both endpoints in the subdivided graph: if \(G.\mathrm{Adj}(u, v)\), then
We prove both conjuncts simultaneously. For each, we simplify \(\mathrm{subdivisionAdj}'\) and verify that \(\{ u,v\} \in E(G)\) (from \(G.\mathrm{Adj}(u,v)\)) and the relevant endpoint belongs to the symmetric pair \(\{ u,v\} \).
The only adjacencies of a dummy vertex \(\mathrm{inr}(e)\) are to the endpoints of \(e\): if \(\mathrm{subdivisionAdj}'(G)(\mathrm{inr}(e), \mathrm{inl}(w))\), then \(w \in e\).
Simplifying the hypothesis using the definition of \(\mathrm{subdivisionAdj}'\), we obtain a conjunction whose second component is \(w \in e.\mathrm{toFinset}\). This follows directly from the second component of the hypothesis.
The set of original vertices in the subdivided graph is \(\mathrm{originalVertices}'(G) := \{ \mathrm{inl}(v) \mid v \in V\} \subseteq \texttt{SubdividedVertex'}(V, \mathrm{Sym2}(V))\), defined as the image of \(\mathrm{Finset.univ}\) under \(\mathrm{inl}\).
The set of dummy vertices in the subdivided graph is \(\mathrm{dummyVerticesOfSubdivision}'(G) := \{ \mathrm{inr}(e) \mid e \in E(G)\} \subseteq \texttt{SubdividedVertex'}(V, \mathrm{Sym2}(V))\), defined as the image of \(G.\mathrm{edgeFinset}\) under \(\mathrm{inr}\).
The number of dummy vertices equals the number of original edges:
This follows directly from \(\mathrm{Finset.card\_ image\_ of\_ injective}\) applied to the injectivity of \(\mathrm{Sum.inr}\).
The sets of original and dummy vertices are disjoint:
We rewrite disjointness as a pairwise inequality condition. Let \(a \in \mathrm{originalVertices}'(G)\) and \(b \in \mathrm{dummyVerticesOfSubdivision}'(G)\). By the image membership conditions, we obtain \(a = \mathrm{inl}(v)\) and \(b = \mathrm{inr}(e)\) for some \(v \in V\) and \(e \in E(G)\). Then \(a \neq b\) follows from \(\mathrm{Sum.inl\_ ne\_ inr}\).
The total vertex count of the subdivided graph satisfies:
Rewriting the dummy count using \(\mathrm{num\_ dummy\_ eq\_ edges}'\), it suffices to show \(|\mathrm{originalVertices}'(G)| = |V|\). By congruence, this reduces to showing the cardinality of the image of \(\mathrm{Finset.univ}\) under \(\mathrm{inl}\) equals \(\mathrm{Fintype.card}(V)\), which follows from the injectivity of \(\mathrm{Sum.inl}\) and the cardinality of the universal finset.
For each original edge with \(G.\mathrm{Adj}(u, v)\), the two subdivided vertices \(\mathrm{inl}(u)\) and \(\mathrm{inl}(v)\) are distinct in \(V' \oplus E'\):
Suppose for contradiction that \(\mathrm{inl}(u) = \mathrm{inl}(v)\). By injectivity of \(\mathrm{inl}\), we get \(u = v\), contradicting \(G.\mathrm{ne\_ of\_ adj}(h_{\mathrm{adj}})\) which asserts \(u \neq v\) for adjacent vertices.
In the subdivided graph, every path between two original vertices must pass through a dummy vertex. Formally, the assumption \(\mathrm{subdivisionAdj}'(G)(\mathrm{inl}(u), \mathrm{inl}(v))\) leads to a contradiction.
This follows directly from \(\mathrm{no\_ original\_ original\_ adj}'(G)(u)(v)\) applied to the hypothesis.
The cost of subdivision is that the number of edge qubits doubles. For any \(n \in \mathbb {N}\):
This follows by integer arithmetic (omega).