33 Cor 2: Cheeger Optimality
This corollary establishes that choosing a graph \(G\) with Cheeger constant \(h(G) = 1\) is optimal for code distance preservation in the deformed code construction. When \(h(G) = 1\), the deformed code distance satisfies \(d^* = d\) (no distance reduction). A Cheeger constant larger than 1 does not further improve the distance, and a Cheeger constant smaller than 1 causes distance reduction by factor \(h(G)\).
The trivial extension of an original code operator to the deformed system. Given an operator \(\mathrm{op}\) with support only on vertices, the trivial extension \(\mathrm{op} \otimes I_E\) is defined as a deformed Pauli operator with:
\(X\)-support on vertices: \(\mathrm{op}.\mathrm{xSupport}\),
\(Z\)-support on vertices: \(\mathrm{op}.\mathrm{zSupport}\),
\(X\)-support on edges: \(\emptyset \),
\(Z\)-support on edges: \(\emptyset \),
phase: \(0\).
The weight of a trivially extended operator equals the weight of the original operator:
By simplification using the definitions of trivialExtension, DeformedPauliOperator.totalWeight, and OriginalCodeOperator.weight, together with the facts that the empty set union yields the original set and \(|\emptyset | + 0 = 0\), the result follows directly.
The trivial extension has no edge \(X\)-support:
This holds by reflexivity (definitional equality).
The trivial extension has no edge \(Z\)-support:
This holds by reflexivity (definitional equality).
A trivially extended nontrivial operator is nontrivial in the deformed code. If \(\mathrm{op}\) is nontrivial (i.e., \(\mathrm{op}.\mathrm{isNontrivial}\) holds), then \(\mathrm{trivialExtension}(\mathrm{op}).\mathrm{isNontrivial}\) holds.
By simplification using the definitions of trivialExtension and DeformedPauliOperator.isNontrivial, the nontriviality of the original operator directly implies nontriviality of the extension via the left disjunct (\(\mathrm{Or.inl}\)).
The trivial extension of an operator with empty \(X\)-support on edges is a \(1\)-cocycle. Every cycle has even (zero) intersection with the empty edge set:
Let \(p\) be an arbitrary cycle. By simplification using the definitions of fluxCommutationCount and the fact that the \(X\)-support on edges of the trivial extension is empty, we have \(\emptyset \cap p = \emptyset \) and \(|\emptyset | = 0\), so the cocycle condition holds.
A trivially extendable logical for a graph \(G\) with cycles and an original code distance specification consists of:
An original logical operator \(\mathrm{op}\),
A proof that \(\mathrm{op}\) is a logical of the original code (\(\mathrm{code}.\mathrm{isLogical}(\mathrm{op})\)),
A proof that \(\mathrm{op}\) is nontrivial (\(\mathrm{op}.\mathrm{isNontrivial}\)),
A proof that \(\mathrm{op}\) has the minimum weight \(d\) (\(\mathrm{op}.\mathrm{weight} = \mathrm{code}.d\)),
A proof that the trivial extension commutes with all Gauss law operators \(A_v\): for all vertices \(v\), \(|\mathrm{op}.\mathrm{zSupport} \cap \{ v\} | \equiv 0 \pmod{2}\).
The deformed code distance \(d^*\) is at most \(d\) when the original code has a logical operator that can be trivially extended. Specifically, if \(\ell \) is a trivially extendable logical, then
Rewriting using trivialExtension_totalWeight, the total weight of the trivial extension equals \(\mathrm{op}.\mathrm{weight}\). The result then follows directly from the hypothesis \(\ell .\mathrm{has\_ weight\_ d}\) which states \(\mathrm{op}.\mathrm{weight} = \mathrm{code}.d\).
When \(h(G) = 1\), the lower bound from Lemma 2 gives \(d^* \geq d\). Specifically, for any deformed logical operator \(L\):
We apply SpaceDistanceBound_logical with \(h(G) = 1\) and the hypothesis \(0 \leq 1\) (established by linarith), along with the Cheeger constant and weight bound hypotheses. This gives
Rewriting using \(\mathrm{minCheegerOne\_ eq\_ one}\) (applied to \(1 \leq 1\)), we obtain \(\min (1,1) = 1\), so \(|L| \geq 1 \cdot d = d\). The final step applies Nat.cast_le.mp to convert from a real inequality to a natural number inequality.
When the Cheeger constant is exactly 1, the deformed code distance satisfies \(d^* \geq d\) and there exists a deformed logical with weight exactly \(d\) (the trivial extension of an original minimum-weight logical). That is:
We prove each conjunct separately.
Lower bound (\(d^* \geq d\)): This follows directly from SpaceDistanceBound_strong_expander applied with \(h(G) = 1\) and \(1 \leq 1\), together with the Cheeger constant and weight bound hypotheses.
Upper bound (\(|\mathrm{trivialExtension}(\ell .\mathrm{op})| = d\)): This follows directly from trivial_extension_upper_bound.
Part 1 Main Result: When \(h(G) = 1\), the deformed code distance exactly equals the original code distance:
The equality follows from matching upper and lower bounds: the lower bound \(d^* \geq d\) comes from Lemma 2, and the upper bound \(d^* \leq d\) comes from the existence of a trivially extended logical operator of weight exactly \(d\) in the set of deformed logicals.
We apply \(\mathrm{Nat.le\_ antisymm}\) to establish equality from two inequalities.
Upper bound (\(d^* \leq d\)): From the hypothesis \(\mathrm{h\_ trivial\_ in\_ logicals}\), we obtain a deformed logical \(L_{\mathrm{triv}}\) in the set of logicals with \(|L_{\mathrm{triv}}| = d\). Unfolding the definition of \(\mathrm{DeformedCodeDistance}\) as an infimum, we apply \(\mathrm{Nat.sInf\_ le}\) to conclude \(d^* \leq d\).
Lower bound (\(d^* \geq d\)): This follows from SpaceDistanceBound_strong_expander applied with \(h(G) = 1\) and \(1 \leq 1\), together with the Cheeger constant and weight bound hypotheses.
When \(h(G) {\gt} 1\), the bound is still \(d^* \geq d\) (not better). Specifically, for any deformed logical operator \(L\):
The \(\min (h(G), 1)\) factor caps the improvement at \(d\).
From \(h(G) {\gt} 1\) we obtain \(h(G) \geq 1\). We then compute \(\min (h(G), 1) = 1\) using minCheegerOne_eq_one. We prove both conjuncts:
The weight bound \(|L| \geq \min (h(G), 1) \cdot d\) follows directly from SpaceDistanceBound_logical applied with \(h(G)\) and \(0 \leq h(G)\) (obtained by linarith from \(h(G) {\gt} 1\)).
The equality \(\min (h(G), 1) = 1\) is the result computed above.
For any \(h(G) \geq 1\), the effective bound factor is capped:
This follows directly from \(\mathrm{minCheegerOne\_ eq\_ one}\) applied to \(h(G) \geq 1\).
For all \(h(G) \geq 1\), the distance bound \(d^* \geq d\) holds.
This follows directly from SpaceDistanceBound_strong_expander applied with \(h(G)\) and \(h(G) \geq 1\).
When \(0 {\lt} h(G) {\lt} 1\), the lower bound from Lemma 2 gives \(|L| \geq h(G) \cdot d\), and furthermore \(h(G) \cdot d {\lt} d\), confirming that the distance is reduced. Formally:
From \(0 {\lt} h(G)\) we obtain \(0 \leq h(G)\). We compute \(\min (h(G), 1) = h(G)\) using minCheegerOne_eq_hG (since \(h(G) {\lt} 1\)). We prove both conjuncts:
The bound \(|L| \geq h(G) \cdot d\): We apply SpaceDistanceBound_logical with the hypotheses, obtaining \(|L| \geq \min (h(G), 1) \cdot d\). Rewriting \(\min (h(G), 1) = h(G)\) gives the result.
The strict inequality \(h(G) \cdot d {\lt} d\): Since \(d {\gt} 0\) (from \(\mathrm{code.d\_ pos}\), cast to \(\mathbb {R}\) via \(\mathrm{Nat.cast\_ pos}\)), and \(h(G) {\lt} 1\), we compute \(h(G) \cdot d {\lt} 1 \cdot d\) by nlinarith, and \(1 \cdot d = d\) by one_mul.
For \(h(G) {\lt} 1\), the factor \(\min (h(G), 1) = h(G)\).
This follows directly from \(\mathrm{minCheegerOne\_ eq\_ hG}\) applied to \(h(G) {\lt} 1\).
For \(0 {\lt} h(G) {\lt} 1\), the deformed code distance satisfies
We apply SpaceDistanceBound with \(h(G)\) and \(0 \leq h(G)\) (from \(0 {\lt} h(G)\)), obtaining \(d^* \geq \min (h(G), 1) \cdot d\). Rewriting using \(\mathrm{minCheegerOne\_ eq\_ hG}\) (since \(h(G) {\lt} 1\)) gives \(d^* \geq h(G) \cdot d\).
A Cheeger regime classifies the Cheeger constant \(h(G)\) into one of three cases:
Optimal: \(h(G) = 1\),
Above one: \(h(G) {\gt} 1\),
Below one: \(0 {\lt} h(G) {\lt} 1\).
The effective distance bound factor depends on the Cheeger regime. For \(h(G) {\gt} 0\):
We prove both conjuncts:
The first follows directly from \(\mathrm{minCheegerOne\_ eq\_ one}\).
The second follows directly from \(\mathrm{minCheegerOne\_ eq\_ hG}\).
Main Optimality Theorem: \(h(G) = 1\) is optimal for code distance preservation. Given a graph \(G\) with exactness condition, Cheeger constant \(h(G) {\gt} 0\), original code distance \(d\), and a nonempty set of deformed logicals satisfying the Cheeger and weight bound hypotheses:
When \(h(G) \geq 1\): \(d^* \geq d\) (distance preserved).
When \(h(G) {\lt} 1\): \(d^* \geq h(G) \cdot d\) (distance reduced by factor \(h(G)\)).
In all cases: \(d^* \geq \min (h(G), 1) \cdot d\).
We prove each of the three parts using \(\mathrm{refine} \langle ?, ?, ? \rangle \):
Part 1 & 2 (\(h(G) \geq 1 \implies d^* \geq d\)): Assume \(h(G) \geq 1\). This follows directly from cheeger_ge_one_preserves_distance applied with all hypotheses.
Part 3 (\(h(G) {\lt} 1 \implies d^* \geq h(G) \cdot d\)): Assume \(h(G) {\lt} 1\). This follows directly from cheeger_lt_one_bound applied with \(h(G)\), \(0 {\lt} h(G)\), \(h(G) {\lt} 1\), and the remaining hypotheses.
General bound (\(d^* \geq \min (h(G), 1) \cdot d\)): This follows directly from SpaceDistanceBound applied with \(h(G)\) and \(0 \leq h(G)\) (from \(0 {\lt} h(G)\)).
For all \(h(G) {\gt} 0\), we have \(\min (h(G), 1) \leq 1\). That is, \(h(G) = 1\) achieves the best possible distance guarantee.
This follows directly from minCheegerOne_le_one.
The distance factor \(\min (h(G), 1)\) is nonnegative when \(h(G) \geq 0\):
This follows directly from minCheegerOne_nonneg.
For \(h(G) = 1\), we have \(\min (1, 1) = 1\).
This follows from \(\mathrm{minCheegerOne\_ eq\_ one}\) applied to \(1 \leq 1\).
The distance bound is monotonic in \(h(G)\) up to \(1\): if \(0 \leq h_1 \leq h_2 \leq 1\), then
We consider two cases.
Case \(h_2 = 1\): Then \(\min (h_2, 1) = 1\) by minCheegerOne_eq_one applied to \(1 \leq 1\). We have \(\min (h_1, 1) \leq 1\) by minCheegerOne_le_one, giving the result.
Case \(h_2 {\lt} 1\): Since \(h_2 \leq 1\) and \(h_2 \neq 1\), we have \(h_2 {\lt} 1\). Then \(h_1 {\lt} 1\) as well (since \(h_1 \leq h_2 {\lt} 1\)). Rewriting both sides using \(\mathrm{minCheegerOne\_ eq\_ hG}\), we need \(h_1 \leq h_2\), which holds by hypothesis.
The distance bound is constant for \(h(G) \geq 1\): if \(h_1 \geq 1\) and \(h_2 \geq 1\), then
Rewriting both sides using \(\mathrm{minCheegerOne\_ eq\_ one}\) (applied to \(1 \leq h_1\) and \(1 \leq h_2\) respectively), both equal \(1\).
Summary of optimality:
\(\min (1, 1) = 1\) (factor is exactly 1 at \(h(G) = 1\)),
For all \(h(G) {\gt} 1\): \(\min (h(G), 1) = 1\) (no improvement),
For all \(h(G) {\lt} 1\): \(\min (h(G), 1) = h(G)\) (reduction by factor \(h(G)\)).
We use \(\mathrm{refine} \langle \mathrm{minCheegerOne\_ at\_ one'}, ?, ? \rangle \) and prove the remaining two parts:
For \(h(G) {\gt} 1\): we apply \(\mathrm{minCheegerOne\_ eq\_ one}\) to \(h(G) \geq 1\) (obtained from \(h(G) {\gt} 1\)).
For \(h(G) {\lt} 1\): we apply \(\mathrm{minCheegerOne\_ eq\_ hG}\) to \(h(G) {\lt} 1\).