- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Let \(G = (V, E)\) be a simple graph and \(S \subseteq V\) a finite subset. The induced edge set of \(S\) is
where \(S^{(2)}\) denotes the set of unordered pairs of elements of \(S\).
Let \(E \subseteq X_1\) be a set of edges in a simple graph \(G\) on vertex type \(V\). The set of vertices incident to \(E\) is defined as
That is, \(\Gamma (E)\) consists of all vertices that appear as an endpoint of some edge in \(E\).
Assume \(H\) is a finite group and \(|H|\) is invertible in \(\mathbb {F}_2\). The descended averaging map is the \(\mathbb {F}_2\)-linear map
defined by lifting the averaging map \(\operatorname {avg} : V \otimes _{\mathbb {F}_2} W \to (V \otimes _{\mathbb {F}_2} W)^H\),
through the coinvariants quotient. This is well-defined because the kernel of the coinvariants quotient is contained in the kernel of \(\operatorname {avg}\): if \(x = (\rho _V \otimes \rho _W)(g)(y) - y\) for some \(g \in H\), then \(\operatorname {avg}(x) = 0\) since the sum \(\sum _{h \in H} (\rho _V \otimes \rho _W)(hg)(y) = \sum _{h \in H} (\rho _V \otimes \rho _W)(h)(y)\) by re-indexing.
Let \(H\) be a group, let \(V\) and \(W\) be \(\mathbb {F}_2\)-modules equipped with \(H\)-representations \(\rho _V : H \to \operatorname {End}_{\mathbb {F}_2}(V)\) and \(\rho _W : H \to \operatorname {End}_{\mathbb {F}_2}(W)\). The balanced product \(V \otimes _H W\) is defined as the coinvariants of the diagonal \(H\)-action on \(V \otimes _{\mathbb {F}_2} W\):
where the diagonal action is \(h \cdot (v \otimes w) = \rho _V(h)(v) \otimes \rho _W(h)(w)\). Equivalently, this is the tensor product \(V \otimes _{\mathbb {F}_2[H]} W\) over the group algebra. Concretely,
The quotient map \(\operatorname {mk} : V \otimes _{\mathbb {F}_2} W \to V \otimes _H W\) is the canonical \(\mathbb {F}_2\)-linear surjection onto the balanced product, defined as the coinvariants quotient map of the diagonal representation \(\rho _V \otimes \rho _W\).
There is a canonical \(\mathbb {F}_2\)-linear equivalence
where \(\mathbf{1}\) denotes the trivial \(H\)-representation on \(\mathbb {F}_2\). In other words, \(V \otimes _H \mathbb {F}_2 \cong V_H\), identifying the balanced product of \(V\) with the trivial module \(\mathbb {F}_2\) with the coinvariant module of \(\rho _V\). This isomorphism is induced by the canonical \(\mathbb {F}_2\)-linear isomorphism \(\operatorname {rid} : V \otimes _{\mathbb {F}_2} \mathbb {F}_2 \xrightarrow {\sim } V\).
Assume \(H\) is a finite group and \(|H|\) is invertible in \(\mathbb {F}_2\) (i.e., \(|H|\) is odd). There is a canonical \(\mathbb {F}_2\)-linear equivalence
The forward map sends \([v \otimes w] \mapsto \frac{1}{|H|}\sum _{h \in H} \rho _V(h)(v) \otimes \rho _W(h)(w)\), and the inverse sends an invariant element \(x \in (V \otimes W)^H\) to its class \([x]\) in \(V \otimes _H W\).
The \(H\)-representation on \(C_0(X,\Lambda )\) is the \(\mathbb {F}_2\)-linear group action
defined by \((\rho _0(h) \cdot f)(v) = f(h^{-1} \cdot v)\) for \(h \in H\) and \(v \in C_0(X)\).
The \(H\)-representation on \(C_1(X,\Lambda )\) is the \(\mathbb {F}_2\)-linear group action
defined by \((\rho _1(h) \cdot c)(e) = c(h^{-1} \cdot e)\) for \(h \in H\) and \(e \in C_1(X)\). This is the standard permutation representation by precomposition with the inverse group action.
The balanced product Tanner cycle code is the chain complex
defined as the balanced product complex of the \(H\)-equivariant Tanner code complex and the \(H\)-equivariant cycle graph complex:
This requires \(\ell \geq 3\), \(\ell \) odd, an \(H\)-invariant labeling \(\Lambda \), and a cycle compatible \(H\)-action on \(\operatorname {Fin}(\ell )\).
The total complex has three non-trivial degrees:
where physical qubits correspond to \(C_1\), Z-checks are given by \(\partial _2 : C_2 \to C_1\), and X-checks are given by \(\partial _1 : C_1 \to C_0\).
Let \(H\) be a finite group acting on a graph with group action \(X\), and let \(\Lambda \) be a cell labeling of \(X\) with \(s\) labels. For a vertex \(v \in C_0(X)\) (a 0-cell of \(X\)), the cell local view at \(v\) is the linear map
defined by \(\operatorname {cellLocalView}(v)(c)(i) = c\! \left(\Lambda (v)^{-1}(i)\right)\), where \(\Lambda (v)^{-1}(i)\) denotes the preimage of \(i\) under the labeling bijection at \(v\).
The cycle chain \(H\)-representation is the \(\mathbb {F}_2\)-linear group action
defined by \((\rho _C(h) \cdot f)(i) = f(h^{-1} \cdot i)\) for \(h \in H\) and \(i \in \operatorname {Fin}(\ell )\).
A cycle compatible \(H\)-action on \(\operatorname {Fin}(\ell )\) is an \(H\)-action satisfying the compatibility condition: for all \(h \in H\) and \(i \in \operatorname {Fin}(\ell )\),
where \(\langle k \rangle \) denotes the element of \(\operatorname {Fin}(\ell )\) with value \(k\). In other words, the \(H\)-action commutes with taking the predecessor modulo \(\ell \).
For \(\ell \geq 1\), the cycle graph chain complex \(C(C_\ell )\) is the chain complex over \(\mathbb {F}_2\) defined by:
where both degree-\(1\) and degree-\(0\) components equal \((\operatorname {Fin}(\ell ) \to \mathbb {F}_2)\), the differential at \((1,0)\) is the cycle graph differential \(\partial _{C_\ell }\), and all modules outside degrees \(0\) and \(1\) are the trivial module.
Given a cycle compatible \(H\)-action on \(\operatorname {Fin}(\ell )\), the cycle graph chain complex \(C(C_\ell )\) equipped with the \(H\)-representation \(\rho _C\) on both degrees \(0\) and \(1\) forms an \(H\)-equivariant chain complex \(\widetilde{C}(C_\ell ) \in \operatorname {HEquivariantChainComplex}(H)\).
The equivariance condition requires \(\partial _{C_\ell } \circ \rho _C(h) = \rho _C(h) \circ \partial _{C_\ell }\) for all \(h \in H\), which follows from the cycle compatible action hypothesis.
The canonical inclusion map
is the map into the total complex at degree \(0\) corresponding to the \((0,0)\)-summand of the balanced product double complex.
The canonical inclusion map
is the map into the total complex at degree \(1\) corresponding to the \((0,1)\)-summand of the balanced product double complex.
The canonical inclusion map
is the map into the total complex at degree \(1\) corresponding to the \((1,0)\)-summand of the balanced product double complex.
The canonical inclusion map
is the map into the total complex at degree \(2\) corresponding to the \((1,1)\)-summand of the balanced product double complex.
The Tanner code chain complex \(C(X, \Lambda )\) is the chain complex over \(\mathbb {F}_2\) defined by:
where
\(C_1(X,\Lambda ) = (C_1(X) \to \mathbb {F}_2)\), the \(\mathbb {F}_2\)-module of functions on 1-cells of \(X\),
\(C_0(X,\Lambda ) = (C_0(X) \to \operatorname {Fin}(s) \to \mathbb {F}_2)\), the \(\mathbb {F}_2\)-module of labeled functions on 0-cells,
the differential at degrees \((1,0)\) is \(\partial ^{\mathrm{Tan}}\), and all other differentials are zero,
all modules outside degrees \(0\) and \(1\) are the trivial module \(\{ *\} \).
The chain complex condition \(\partial ^{\mathrm{Tan}} \circ \partial ^{\mathrm{Tan}} = 0\) holds trivially since the complex is concentrated in two consecutive degrees.
Given an \(H\)-invariant labeling \(\Lambda \) (i.e., \(\Lambda \) satisfies the invariance condition \(\operatorname {IsInvariantLabeling}(\Lambda )\)), the Tanner code chain complex \(C(X, \Lambda )\) equipped with the \(H\)-representations \(\rho _1\) on \(C_1\) and \(\rho _0\) on \(C_0\) forms an \(H\)-equivariant chain complex \(\widetilde{C}(X,\Lambda ) \in \operatorname {HEquivariantChainComplex}(H)\).
The equivariance condition requires that \(\partial ^{\mathrm{Tan}} \circ \rho _1(h) = \rho _0(h) \circ \partial ^{\mathrm{Tan}}\) for all \(h \in H\), i.e., the Tanner differential commutes with the \(H\)-action.
The Tanner differential is the linear map
defined by \(\partial ^{\mathrm{Tan}}(c)(v) = \operatorname {cellLocalView}(v)(c)\), i.e.,
This map assembles the local views at all vertices.
The X-check map of the balanced product Tanner cycle code is the differential
i.e., the chain complex differential from degree \(1\) to degree \(0\). X-errors are detected by this map.
The Z-check map of the balanced product Tanner cycle code is the differential
i.e., the chain complex differential from degree \(2\) to degree \(1\). Z-errors are detected by this map.
The binary entropy function \(H_2 : \mathbb {R} \to \mathbb {R}\) is defined by
For \(\delta \in (0,1)\), this gives the Shannon entropy of a Bernoulli\((\delta )\) distribution measured in bits. Outside \((0,1)\), the function extends by continuity, with \(\log _2(0) = 0\) by Mathlib’s convention.
Let \(G\) be a finite group with decidable equality, and let \(S\) be a symmetric generating set for \(G\). The Cayley graph \(\operatorname {Cay}(G, S)\) is the simple graph with vertex set \(G\), where two vertices \(g, g' \in G\) are adjacent if and only if there exists \(s \in S\) such that \(g' = s \cdot g\).
Well-definedness as a simple graph follows from:
Symmetry: If \(g' = s \cdot g\) for some \(s \in S\), then \(g = s^{-1} \cdot g'\) and \(s^{-1} \in S\) by the inverse-closure of \(S\).
Looplessness: If \(g = s \cdot g\) for some \(s \in S\), then \(s = 1\), contradicting \(1 \notin S\).
A symmetric generating set for a group \(G\) is a structure consisting of:
A finite set of generators \(S \subseteq G\) (the carrier),
A proof that the identity \(1 \notin S\),
A proof that \(S\) is closed under inverses: for all \(s \in S\), \(s^{-1} \in S\).
A regular cell complex \(X\) consists of:
A family of types \(X_n\) (for each \(n \in \mathbb {Z}\)), whose elements are called \(n\)-cells, each equipped with a Fintype instance and a DecidableEq instance.
A boundary map \(\partial \): for each \(n\)-cell \(\sigma \in X_n\), a finite set \(\partial \sigma \subseteq X_{n-1}\) of \((n-1)\)-cells in the boundary of \(\sigma \).
The chain complex condition: for every \(n \in \mathbb {Z}\), every \(n\)-cell \(\sigma \in X_n\), and every \((n-2)\)-cell \(\rho \in X_{n-2}\), the cardinality
\[ \left|\{ \, \tau \in \partial \sigma \mid \rho \in \partial \tau \, \} \right| \]is even (i.e., \(\equiv 0 \pmod{2}\)).
Let \(X\) be a cell complex. The homology of \(X\) in degree \(i \in \mathbb {Z}\) is
where \(H_i(C(X))\) is the \(i\)-th homology of the associated chain complex \(C(X)\) (as defined in the chain complex homology construction of Definition 1).
Let \(X\) be a cell complex. The associated chain complex \(C(X) = (C_\bullet (X), \partial )\) is the \(\mathbb {F}_2\)-chain complex defined as follows:
In degree \(i \in \mathbb {Z}\), the chain module is \(C_i(X) = (X_i \to \mathbb {F}_2)\), the free \(\mathbb {F}_2\)-vector space on the \(i\)-cells.
The differential \(d_{i,j} : C_i(X) \to C_j(X)\) is the linear map \(\partial _{j+1}\) when \(j + 1 = i\), and zero otherwise.
The chain complex condition \(d_{j} \circ d_{j+1} = 0\) is verified by composing the differentials and applying differentialMap_comp, after cancelling the coherence isomorphisms (eqToHom) that arise from the ModuleCat packaging.
Let \(X\) be a cell complex and let \(C_i(X) = (X_i \to \mathbb {F}_2)\) denote the free \(\mathbb {F}_2\)-vector space on the \(i\)-cells (i.e., functions from \(X_i\) to \(\mathbb {F}_2\)). The differential
is the \(\mathbb {F}_2\)-linear map defined for \(f \in C_n(X)\) and \(\tau \in X_{n-1}\) by
Equivalently, on a basis element \(e_\sigma \) (the indicator function of \(\sigma \)), we have \(\partial _n(e_\sigma ) = \sum _{\tau \in \partial \sigma } e_\tau \), extended linearly.
Let \(X\) be a cell complex and let \(S \subseteq X_0\) be a subset of vertices (0-cells). The edge boundary of \(S\) is the set
That is, an edge \(e \in X_1\) belongs to \(\delta S\) if and only if its boundary \(\partial _1 e\) intersects both \(S\) and its complement \(S^c\).
Let \(X\) be a cell complex, \(S \subseteq X_0\), and \(v \in X_0\). The edge boundary of \(S\) at vertex \(v\) is the intersection
A chain complex of \(\mathbb {F}_2\)-vector spaces indexed by \(\mathbb {Z}\) is defined as
The differential \(\partial _i : C_i \to C_{i-1}\) is given by \(\mathtt{d}\, i\, j\) in Mathlib where the complex shape satisfies \(j + 1 = i\) (i.e. \(j = i - 1\)). This corresponds to the paper’s \((C_\bullet , \partial )\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The boundaries at degree \(i\) are
defined as the image (range) submodule of the incoming differential \(\partial _{i+1} : C_{i+1} \to C_i\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The boundaries \(B_i(C)\), viewed as a submodule of the cycles \(Z_i(C)\), are defined as the preimage of \(B_i(C) \subseteq C_i\) under the canonical subtype embedding \(Z_i(C) \hookrightarrow C_i\). Concretely,
Let \(C\) be a chain complex over \(\mathbb {F}_2\). The coboundaries in degree \(i\) are the image (range) of the incoming coboundary map \(\delta ^{i-1}\):
viewed as a submodule of \(\operatorname {Dual}(C_i)\) over \(\mathbb {F}_2\).
Since \(B^i(C) \subseteq Z^i(C)\), we define \(B^i(C)\) as a submodule of \(Z^i(C)\) by taking the preimage of \(B^i(C)\) under the subtype embedding \(Z^i(C) \hookrightarrow \operatorname {Dual}(C_i)\):
where \(\iota _{Z^i} : Z^i(C) \to \operatorname {Dual}(C_i)\) is the canonical inclusion.
Let \(C = (C_\bullet , \partial )\) be a chain complex over \(\mathbb {F}_2\). For each \(i \in \mathbb {Z}\), the coboundary map \(\delta ^i : \operatorname {Dual}(C_i) \to \operatorname {Dual}(C_{i+1})\) is defined as the dual (transpose) of the incoming differential \(\partial _{i+1} : C_{i+1} \to C_i\):
Let \(C\) be a chain complex over \(\mathbb {F}_2\). The cocycles in degree \(i\) are the kernel of the coboundary map \(\delta ^i\):
viewed as a submodule of \(\operatorname {Dual}(C_i)\) over \(\mathbb {F}_2\).
Let \(C\) be a chain complex over \(\mathbb {F}_2\). The \(i\)-th cohomology of \(C\) is the quotient \(\mathbb {F}_2\)-vector space:
More precisely, it is the quotient of \(Z^i(C)\) by the submodule \(B^i(C)|_{Z^i}\) of \(Z^i(C)\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The differential \(\partial _i : C_i \to C_{i-1}\) is the \(\mathbb {F}_2\)-linear map obtained from the Mathlib differential \(C.d\, i\, (i-1)\) (with respect to the descending complex shape on \(\mathbb {Z}\)) by extracting its underlying linear map via the forgetful functor from \(\mathbf{Mod}_{\mathbb {F}_2}\) to \(\mathbb {F}_2\)-linear maps.
Let \(C\) be a chain complex over \(\mathbb {F}_2\) with \(C_i\), \(C_{i-1}\), and \(C_{i+1}\) finite-dimensional. There is a linear isomorphism of \(\mathbb {F}_2\)-vector spaces:
This isomorphism is constructed via LinearEquiv.ofFinrankEq, using the fact that both spaces are finite-dimensional \(\mathbb {F}_2\)-vector spaces of equal dimension, as established by finrank_homology_eq_finrank_cohomology.
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The \(i\)-th homology of \(C\) is the quotient \(\mathbb {F}_2\)-module
where \(B_i^{Z}(C)\) is the boundaries viewed as a submodule of the cycles \(Z_i(C)\).
Let \(n_1, m_1, n_2, m_2 \in \mathbb {N}\), and let
be linear maps over \(\mathbb {F}_2\) (parity-check matrices of two classical codes). The hypergraph product code is the chain complex
i.e., the tensor product complex of the parity-check complexes associated to \(\partial ^C\) and \(\partial ^D\). Concretely, the underlying 1-complexes are
and their tensor product double complex has three nontrivial degrees:
Degree \(2\): \(\mathbb {F}_2^{n_1} \otimes \mathbb {F}_2^{n_2}\),
Degree \(1\): \((\mathbb {F}_2^{n_1} \otimes \mathbb {F}_2^{m_2}) \oplus (\mathbb {F}_2^{m_1} \otimes \mathbb {F}_2^{n_2})\),
Degree \(0\): \(\mathbb {F}_2^{m_1} \otimes \mathbb {F}_2^{m_2}\).
The differential from degree \(2\) to degree \(1\) plays the role of \(H_Z^\top \), and the differential from degree \(1\) to degree \(0\) plays the role of \(H_X\) in the CSS code convention. The CSS code structure is read off from the total complex shifted by \(1\) to match the convention \(C_1 \xrightarrow {H_Z^\top } C_0 \xrightarrow {H_X} C_{-1}\).
Let \(C = (C_\bullet , \partial )\) be a chain complex over \(\mathbb {F}_2\). For each \(i \in \mathbb {Z}\), the incoming coboundary map \(\delta ^{i-1} : \operatorname {Dual}(C_{i-1}) \to \operatorname {Dual}(C_i)\) is defined as the dual (transpose) of the differential \(\partial _i : C_i \to C_{i-1}\):
This formulation avoids index-arithmetic issues by using \(C.\operatorname {differential}(i)\) directly.
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. The incoming differential at degree \(i\) is the \(\mathbb {F}_2\)-linear map \(\partial _{i+1} : C_{i+1} \to C_i\) extracted from the Mathlib differential \(C.d\, (i+1)\, i\). This formulation avoids definitional issues with \((i+1)-1\) vs. \(i\) in integer arithmetic.
Let \(C\) and \(D\) be chain complexes over \(\mathbb {F}_2\), and let \(p, q, n \in \mathbb {Z}\) with \(p + q = n\). The canonical inclusion of the summand \(C_p \otimes D_q\) into \((C \otimes D)_n\) is the map
defined as the total complex inclusion \(\iota _{p,q,n}\) applied to the tensor product double complex \(C \boxtimes D\).
Let \(C\) and \(D\) be chain complexes over \(\mathbb {F}_2\). The tensor product complex \(C \otimes D\) is defined as the total complex of the tensor product double complex:
Concretely, its degree-\(n\) component is
and its differential is \(\partial = \partial ^C \otimes \operatorname {id} + \operatorname {id} \otimes \partial ^D\). Over \(\mathbb {F}_2\), the usual sign factor \((-1)^p\) is trivial since \(-1 = 1\).
Let \(C\) and \(D\) be chain complexes over \(\mathbb {F}_2\). The horizontal differential
is defined by
that is, it applies the differential \(\partial ^C\) of \(C\) in the first (horizontal, \(p\)-)direction and the identity on \(D_q\).
Let \(C\) and \(D\) be chain complexes over \(\mathbb {F}_2\). The tensor product double complex \(C \boxtimes D\) is the double complex (in the sense of \(\operatorname {DoubleComplex}_{\mathbb {F}_2}\)) defined as follows:
Objects: \((C \boxtimes D)_{p,q} = C_p \otimes _{\mathbb {F}_2} D_q\) for all \(p, q \in \mathbb {Z}\).
Horizontal differential: \(\partial ^h_{p,q} = \partial ^C_p \otimes \operatorname {id}_{D_q} : C_p \otimes D_q \to C_{p-1} \otimes D_q\).
Vertical differential: \(\partial ^v_{p,q} = \operatorname {id}_{C_p} \otimes \partial ^D_q : C_p \otimes D_q \to C_p \otimes D_{q-1}\).
The double complex conditions are verified as follows. When the complex shape relation \(\operatorname {Rel}(p, p')\) (respectively \(\operatorname {Rel}(q, q')\)) does not hold, the corresponding differential vanishes. The horizontal and vertical differentials each square to zero: \(\partial ^h \circ \partial ^h = 0\) and \(\partial ^v \circ \partial ^v = 0\). Moreover, the horizontal and vertical differentials commute: \(\partial ^h \circ \partial ^v = \partial ^v \circ \partial ^h\), which over \(\mathbb {F}_2\) replaces the usual anticommutativity requirement. This is a consequence of the whisker exchange identity \((\partial ^C \otimes \operatorname {id}) \circ (\operatorname {id} \otimes \partial ^D) = (\operatorname {id} \otimes \partial ^D) \circ (\partial ^C \otimes \operatorname {id})\) in any monoidal category.
The double complex is assembled via HomologicalComplex2.ofGradedObject using the descending complex shape on \(\mathbb {Z}\) in both directions.
Let \(C\) and \(D\) be chain complexes over \(\mathbb {F}_2\). The vertical differential
is defined by
that is, it applies the identity on \(C_p\) and the differential \(\partial ^D\) of \(D\) in the second (vertical, \(q\)-)direction.
Let \(C\) and \(D\) be chain complexes over \(\mathbb {F}_2\). The graded object underlying the tensor product double complex is defined, for integers \(p, q \in \mathbb {Z}\), by
where \(\otimes _{\mathbb {F}_2}\) denotes the tensor product of \(\mathbb {F}_2\)-modules.
Let \(G\) be a finite simple graph with decidable adjacency. The Cheeger constant (or isoperimetric number) of \(G\) is
where the infimum is taken over all eligible subsets \(S\) (nonempty subsets with \(2|S| \leq |V|\)). When no eligible subset exists (i.e., \(|V| {\lt} 2\)), the set is empty and \(h(G) = 0\) by the convention \(\operatorname {sInf}\, \emptyset = 0\) for \(\mathbb {R}\).
Let \(G = (V, E)\) be a finite simple graph with a decidable adjacency relation, and let \(S \subseteq V\) be a finite subset of vertices. The edge boundary \(\delta S\) is the finite set of edges in \(G\) that cross the cut determined by \(S\):
Formally, using the quotient representation \(\operatorname {Sym2}(V)\) for unordered pairs, we set
A finite subset \(S \subseteq V\) is called eligible (for the Cheeger constant) if:
\(S\) is nonempty: \(S \neq \emptyset \), and
\(S\) is at most half the vertex set: \(2|S| \leq |V|\).
Formally, \(\operatorname {EligibleSubset}(S) \; \Longleftrightarrow \; S.\operatorname {Nonempty} \land 2 \cdot |S| \leq |V|\).
Let \(G\) be a finite simple graph with decidable adjacency, and let \(S \subseteq V\) be a finite subset. The isoperimetric ratio of \(S\) is
where \(|\delta S|\) denotes the cardinality of the edge boundary and \(|S|\) the cardinality of \(S\).
A classical linear binary code of block length \(n\) is a subspace \(\mathcal{C} \subseteq \mathbb {F}_2^n\). Formally, it is a structure wrapping a submodule
where \(\mathbb {F}_2^n\) is viewed as the \(\mathbb {F}_2\)-module of functions \(\operatorname {Fin}(n) \to \mathbb {F}_2\).
Let \(\mathcal{C}\) be a classical code of block length \(n\). The dimension of \(\mathcal{C}\) is
the finite rank of \(\mathcal{C}\) as an \(\mathbb {F}_2\)-module. This equals the number of encodable bits.
Let \(\mathcal{C}\) be a classical code of block length \(n\). The distance of \(\mathcal{C}\) is
where \(\operatorname {wt}(x)\) denotes the Hamming weight of \(x\). Here \(\inf \) is taken over \(\mathbb {N}\), and by convention \(\inf \emptyset = 0\), which gives \(d = 0\) for the trivial code \(\mathcal{C} = \{ 0\} \).
Let \(\mathcal{C}\) be a classical code, i.e. a subspace \(L \subseteq \mathbb {F}_2^n\). The dual code is
where \(\langle w, c \rangle = \sum _i w_i c_i\) is the standard \(\mathbb {F}_2\)-dot product. Concretely, \(L^\perp \) is defined as the pullback of the dual annihilator \(L^{\circ } \subseteq \operatorname {Dual}(\mathbb {F}_2^n)\) through the canonical linear isomorphism
There is a \(\mathbb {F}_2\)-linear equivalence
between the dual code \(L^\perp \) and the dual annihilator \(L^{\circ } \subseteq \operatorname {Dual}(\mathbb {F}_2^n)\), induced by the canonical isomorphism \(\operatorname {dotProductEquiv}\). Since \((L^\perp ).\mathtt{code} = L^{\circ }.\operatorname {comap}(\operatorname {dotProductEquiv})\), the restriction of \(\operatorname {dotProductEquiv}^{-1}\) to \(L^{\circ }\) gives the desired equivalence.
Given an \(\mathbb {F}_2\)-linear map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\) (the parity check map), we construct a classical code of block length \(n\) by taking the kernel:
Given an \(\mathbb {F}_2\)-linear parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), the associated two-term chain complex is
where \(C_1 = \mathbb {F}_2^n\) sits in degree \(1\) and \(C_0 = \mathbb {F}_2^m\) sits in degree \(0\). This is constructed via \(\operatorname {HomologicalComplex.double}\) applied to the morphism \(\partial ^C\) in the category of \(\mathbb {F}_2\)-modules, using the complex shape relation \(1 \to 0\).
For a parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), there is a canonical isomorphism
between the degree-\(1\) object of the parity check complex \(C\) and \(\mathbb {F}_2^n\), given by \(\operatorname {HomologicalComplex.doubleXIso_0}\).
A cochain complex of \(\mathbb {F}_2\)-vector spaces indexed by \(\mathbb {Z}\) is defined as
The differential \(\delta ^i : C^i \to C^{i+1}\) is given by \(\mathtt{d}\, i\, j\) in Mathlib where \(i + 1 = j\). In the paper, the coboundary \(\delta ^i\) is the transpose of \(\partial _{i+1}\).
Let \(H\) be a finite group, \(X\) a graph with \(H\)-action, and \(\Lambda \) a cell labeling of \(X\) with \(s\) labels. The coboundary map (or transpose Tanner differential)
is the linear map \(\delta : (X_0 \to \operatorname {Fin}(s) \to \mathbb {F}_2) \to (X_1 \to \mathbb {F}_2)\) defined by
Here \(X_0\) denotes the \(0\)-cells (vertices) and \(X_1\) the \(1\)-cells (edges) of \(X\). This map is \(\mathbb {F}_2\)-linear, being the transpose of the Tanner differential \(\partial : C_1(X,\Lambda ) \to C_0(X,\Lambda )\).
Let \(A\), \(B\), \(C\) be finite types with decidable equality, and let \(f : (A \to B \to \mathbb {F}_2) \to _{\mathbb {F}_2} (C \to \mathbb {F}_2)\) be a linear map over \(\mathbb {F}_2\). We say \(f\) is \((\alpha , \beta )\)-expanding (written \(\operatorname {IsExpandingCoboundary}(f, \alpha , \beta )\)) if:
\(0 {\lt} \alpha \leq 1\) and \(0 {\lt} \beta \),
For every \(x : A \to B \to \mathbb {F}_2\) with
\[ \bigl|\{ (a,b) \in A \times B \mid x(a,b) \neq 0\} \bigr| \leq \alpha \cdot |A| \cdot |B|, \]we have
\[ \bigl|\{ c \in C \mid f(x)(c) \neq 0\} \bigr| \geq \beta \cdot \bigl|\{ (a,b) \in A \times B \mid x(a,b) \neq 0\} \bigr|. \]
This is the expanding property for a map whose domain is a matrix-shaped space \((A \to B \to \mathbb {F}_2)\), dual to the \(\operatorname {IsExpandingLinMap}\) condition of Definition 653.
For a linear map \(f : (\operatorname {Fin} n \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin} m \to \mathbb {F}_2)\) and an index \(j : \operatorname {Fin} n\), the column weight of column \(j\) of the matrix representation of \(f\) is defined as
i.e., the number of row indices \(i\) such that the \((i,j)\)-entry of the matrix is nonzero.
A CSS (Calderbank–Shor–Steane) quantum code of parameters \((n, r_X, r_Z)\) consists of:
An X-type parity check matrix \(H_X : \mathbb {F}_2^n \to \mathbb {F}_2^{r_X}\), a linear map over \(\mathbb {F}_2\).
A Z-type parity check matrix transpose \(H_Z^T : \mathbb {F}_2^{r_Z} \to \mathbb {F}_2^n\), a linear map over \(\mathbb {F}_2\).
The CSS condition: \(H_X \circ H_Z^T = 0\).
The map \(H_Z^T\) serves as the differential from degree \(1\) to degree \(0\) in the associated chain complex \(C_1 \xrightarrow {H_Z^T} C_0 \xrightarrow {H_X} C_{-1}\).
Let \(Q\) be a CSS code with parity check matrices \(H_X\) and \(H_Z^T\). The submodule of boundaries inside cycles is
viewed as a submodule of \(\ker (H_X)\) via the comap of the subtype inclusion. Formally, it is the \(\mathbb {F}_2\)-submodule
The submodule of coboundaries inside cocycles is
where \(H_Z = (H_Z^T)^T = \operatorname {dualMap}(H_Z^T)\) and \(H_X^T = \operatorname {dualMap}(H_X)\), viewed as a submodule of \(\ker (H_Z)\). Formally, it is
The cohomology type of a CSS code \(Q\) is the quotient \(\mathbb {F}_2\)-vector space
i.e., the quotient of \(\ker (\operatorname {dualMap}(H_Z^T))\) by the submodule of coboundaries in cocycles.
Let \(Q = (H_X, H_Z^T)\) be a CSS code with parameters \((n, r_X, r_Z)\). The associated chain complex \(\operatorname {complex}(Q)\) is the three-term chain complex in \(\operatorname {Mod}_{\mathbb {F}_2}\) of the form
where the objects are
and the differentials are \(d_{1,0} = H_Z^T\) and \(d_{0,-1} = H_X\), with all other differentials zero. This is well-defined as a chain complex because \(\partial ^2 = 0\), which follows from the CSS condition \(H_X \circ H_Z^T = 0\).
Let \(Q = (H_X, H_Z^T)\) be a CSS code. The X-distance is the minimum Hamming weight of a vector in \(\ker H_X\) that does not lie in \(\operatorname {im}(H_Z^T)\):
where \(\operatorname {wt}(x) = |\operatorname {supp}(x)|\) is the Hamming weight. By convention, \(d_X = 0\) when \(\ker H_X = \operatorname {im}(H_Z^T)\) (trivial homology), since the infimum of the empty set is \(0\).
Let \(Q = (H_X, H_Z^T)\) be a CSS code. The Z-distance is defined using the dual maps. Since \(H_Z = (H_Z^T)^T\), the kernel of \(H_Z\) corresponds to the kernel of the dual map \((H_Z^T)^\vee : ({\mathbb {F}_2^n})^\vee \to ({\mathbb {F}_2^{r_Z}})^\vee \), and the image of \(H_X^T\) corresponds to the range of the dual map \(H_X^\vee : ({\mathbb {F}_2^{r_X}})^\vee \to ({\mathbb {F}_2^n})^\vee \). Over \(\mathbb {F}_2\) with canonical bases, \((\mathbb {F}_2^n)^\vee \cong \mathbb {F}_2^n\) via the dot product equivalence. Using this identification, the Z-distance is
where \(\operatorname {wt}(\varphi )\) is the Hamming weight of \(\varphi \) viewed as a vector in \(\mathbb {F}_2^n\) via the dot product isomorphism. By convention, \(d_Z = 0\) when the cohomology is trivial.
A family of CSS codes indexed by a type \(\iota \), say \(\{ C_\alpha \} _{\alpha \in \iota }\) where each \(C_\alpha \) is a CSS code with parameters \((n(\alpha ),\, r_X(\alpha ),\, r_Z(\alpha ))\), is called low-density parity-check (LDPC) if there exists a uniform bound \(w \in \mathbb {N}\) such that for every \(\alpha \in \iota \), both the parity-check matrix \(H_X\) and the transposed parity-check matrix \(H_Z^T\) (as stored in the CSS code structure) have bounded weight \(w\):
Note: Since the CSS code structure stores \(H_Z^T\) rather than \(H_Z\) directly, and since the weight bound \(w\) applies symmetrically to both rows and columns, the condition \(\operatorname {HasBoundedWeight}(H_Z^T, w)\) is equivalent to requiring that \(H_Z\) itself has all row weights and column weights bounded by \(w\).
Let \(Q\) be a CSS code and let \(k, d_X, d_Z \in \mathbb {N}\). We say \(Q\) is an \([\! [n,k,d_X,d_Z]\! ]\)-code if
This predicate is used when the X- and Z-distances are distinct and one wishes to record both separately.
Let \(Q = (H_X, H_Z^T)\) be a CSS code. The number of logical qubits is the dimension of the degree-\(0\) homology of the chain complex:
More precisely, \(k(Q) = \operatorname {finrank}_{\mathbb {F}_2}\bigl(\ker H_X \, /\, (\operatorname {range}(H_Z^T))^{-1}(\ker H_X)\bigr)\), where the quotient is taken of the subspace of \(\ker H_X\) by the image of \(H_Z^T\) within \(\ker H_X\).
The boundary map for the cycle graph \(C_\ell \) assigns to each cell its boundary:
For a 1-cell \(\sigma _i\) (with \(i \in \operatorname {Fin}(\ell )\)): \(\partial \sigma _i = \{ \tau _i,\, \tau _{(i+1)\bmod \ell }\} \subseteq \operatorname {Fin}(\ell )\), encoding the incidence relation of each edge with its two endpoint vertices.
For a 0-cell: \(\partial \tau _i = \varnothing \) (the boundary of a vertex is empty, valued in \(\operatorname {cellType}(\ell ,-1) = \varnothing \)).
For cells in all other dimensions: the boundary is vacuously empty (the cell type is \(\varnothing \)).
The cell type function for the cycle graph assigns to each integer dimension \(n\) the type of \(n\)-cells:
Thus the cycle graph has \(\ell \) vertices (0-cells) and \(\ell \) edges (1-cells), and no cells in any other dimension.
The cycle graph \(C_\ell \) is the cell complex (Definition 81) with:
cells given by \(\operatorname {cellType}(\ell )\): \(\ell \) vertices (0-cells) and \(\ell \) edges (1-cells), all indexed by \(\operatorname {Fin}(\ell )\);
boundary map given by \(\operatorname {cellBdry}(\ell )\): \(\partial \sigma _i = \{ \tau _i, \tau _{(i+1)\bmod \ell }\} \);
the chain complex condition \(\partial \circ \partial = 0\) verified by \(\mathtt{cellBdry\_ bdry}\).
Let \(\ell \geq 1\) be a natural number. The differential \(\partial _1 : \mathbb {F}_2^\ell \to \mathbb {F}_2^\ell \) of the cycle graph is the linear map defined by
for \(f : \operatorname {Fin}(\ell ) \to \mathbb {F}_2\) and \(i \in \operatorname {Fin}(\ell )\). On basis vectors \(e_j\), one has \(\partial _1(e_j) = e_j + e_{(j+1) \bmod \ell }\), so column \(j\) of the corresponding matrix has \(1\)-entries in rows \(j\) and \((j+1) \bmod \ell \), encoding the boundary relation \(\partial \sigma _j = \{ \tau _j, \tau _{(j+1) \bmod \ell }\} \).
The repetition code of length \(\ell \) is the classical code (Definition 41) defined by
i.e., it is the classical code whose codeword space is \(\ker (\partial _1) = \operatorname {span}\{ \mathbf{1}\} \subseteq \mathbb {F}_2^\ell \).
Let \(m \in \mathbb {N}\) and let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. The differential
is defined by
This is the component form of the differential \(\partial : C_1(X) \to C_0(X) \otimes L_0\) from the paper, using the canonical isomorphism \((V \to \mathbb {F}_2) \otimes (\operatorname {Fin}(m) \to \mathbb {F}_2) \cong V \to \operatorname {Fin}(m) \to \mathbb {F}_2\). For an edge \(e = \{ v,w\} \), the formula \(\partial (e) = e_v \otimes \partial ^L(e_{\Lambda _v(w)}) + e_w \otimes \partial ^L(e_{\Lambda _w(v)})\) becomes \(\partial (e)(v) = \partial ^L(e_{\Lambda _v(w)})\) and \(\partial (e)(w) = \partial ^L(e_{\Lambda _w(v)})\).
For a valid prime \(vp\), a balanced code datum is a structure bundling:
row counts \(r_X, r_Z \in \mathbb {N}\) for the X- and Z-type parity checks,
a CSS code \(\mathcal{C}\) of block length \(N = \operatorname {balancedCodeLength}(vp)\),
a weight bound \(w \in \mathbb {N}\) such that the X-parity check matrix \(H_X\) and the transposed Z-parity check matrix \(H_{ZT}\) both have bounded row and column weight at most \(w\) (LDPC property),
a lower bound on logical qubits: \(K \geq K_0 \cdot \lfloor n_c/2 \rfloor + 1\), where \(K_0\) is the logical qubit count of the subsystem code from Theorem 15 and \(n_c = q^2\) is the classical code length,
a lower bound on X-distance: \(D_X \geq D_{X,0} \cdot \lfloor n_c / 10 \rfloor \), where \(D_{X,0}\) is the X-distance of the subsystem code,
an upper bound on logical qubits: \(K \leq K_0 \cdot n_c\),
a lower bound on Z-distance: \(D_Z \geq D_{Z,0}\), where \(D_{Z,0}\) is the Z-distance of the subsystem code.
A double complex of \(\mathbb {F}_2\)-vector spaces is an array of \(\mathbb {F}_2\)-vector spaces \(E_{p,q}\) indexed by \((p,q) \in \mathbb {Z} \times \mathbb {Z}\), equipped with:
a vertical differential \(\partial ^v_{p,q} : E_{p,q} \to E_{p,q-1}\) (decreasing \(q\)),
a horizontal differential \(\partial ^h_{p,q} : E_{p,q} \to E_{p-1,q}\) (decreasing \(p\)),
satisfying:
\(\partial ^v_{p,q-1} \circ \partial ^v_{p,q} = 0\) for all \(p, q\),
\(\partial ^h_{p-1,q} \circ \partial ^h_{p,q} = 0\) for all \(p, q\),
\(\partial ^v_{p-1,q} \circ \partial ^h_{p,q} = \partial ^h_{p,q-1} \circ \partial ^v_{p,q}\) for all \(p, q\) (commutativity).
Over \(\mathbb {F}_2\), commutativity and anticommutativity coincide since \(-1 = 1\) in characteristic \(2\).
Formally, \(\operatorname {DoubleComplex}_{\mathbb {F}_2}\) is defined as \(\operatorname {HomologicalComplex}_2(\operatorname {ModuleCat}\ \mathbb {F}_2,\ \operatorname {ComplexShape.down}\ \mathbb {Z},\ \operatorname {ComplexShape.down}\ \mathbb {Z})\), where the first \(\operatorname {ComplexShape.down}\ \mathbb {Z}\) is the horizontal direction and the second is the vertical direction.
Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). The horizontal differential at position \((p,q)\) is the \(\mathbb {F}_2\)-linear map
defined as the underlying linear map of the \(q\)-th component of the horizontal chain map \(E.d_{p,p-1}\).
Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). The vertical differential at position \((p,q)\) is the \(\mathbb {F}_2\)-linear map
defined as the underlying linear map of the chain complex differential \((E_p).d_{q,q-1}\).
Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces. For integers \(p, q, n\) with \(p + q = n\), the inclusion map
is the canonical injection of the summand \(E_{p,q}\) into the coproduct \(\operatorname {Tot}(E)_n = \bigoplus _{p'+q'=n} E_{p',q'}\).
Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). The \(\mathbb {F}_2\)-vector space at position \((p, q) \in \mathbb {Z} \times \mathbb {Z}\) is defined by
where \(E_p\) denotes the \(p\)-th column complex and \((E_p)_q\) its \(q\)-th component.
Let \(E = (E_{\bullet ,\bullet }, \partial ^v, \partial ^h)\) be a double complex of \(\mathbb {F}_2\)-vector spaces (see Definition 112). The total complex \(\operatorname {Tot}(E)\) is the chain complex over \(\mathbb {F}_2\) indexed by \(\mathbb {Z}\) defined as follows:
The \(n\)-th object is the direct sum
\[ \operatorname {Tot}(E)_n \; =\; \bigoplus _{p+q=n} E_{p,q}, \]taken over all pairs of integers \((p,q)\) with \(p + q = n\).
The differential \(\partial _n \colon \operatorname {Tot}(E)_n \to \operatorname {Tot}(E)_{n-1}\) restricts to each summand \(E_{p,q}\) as
\[ \partial _n\big|_{E_{p,q}} \; =\; \partial ^v_{p,q} + \partial ^h_{p,q}, \]where \(\partial ^v_{p,q} \colon E_{p,q} \to E_{p,q-1}\) maps into the \((p, q-1)\)-summand and \(\partial ^h_{p,q} \colon E_{p,q} \to E_{p-1,q}\) maps into the \((p-1,q)\)-summand of \(\operatorname {Tot}(E)_{n-1}\).
Since \(\operatorname {ModuleCat}(\mathbb {F}_2)\) has all coproducts, the total complex exists. This construction is realized via Mathlib’s HomologicalComplex2.total with the descending complex shape on \(\mathbb {Z}\).
Sign convention: Mathlib uses sign maps \(\varepsilon (n) = (-1)^n\) (implemented by Int.negOnePow) for the TensorSigns instance on ComplexShape.down \(\mathbb {Z}\), satisfying: for \(p + q + 1 = n\), the sign condition \(\varepsilon '_{\mathrm{succ}}\) gives \(\varepsilon (p+1) = -\varepsilon (p)\), verified by simplification using Int.negOnePow_succ and \(-(-x)=x\). Over \(\mathbb {F}_2\) these signs are trivial (since \(-1 = 1\)), so Mathlib’s construction agrees with the sign-free definition in the paper.
Let \(s, \lambda _2, a \in \mathbb {R}\). The quadratic inverse is defined by
This is the solution \(g\) to the equation \(a = g^2 + \tfrac {\lambda _2}{s}\, g(1-g)\).
For \(n, r \in \mathbb {N}\) and a vector \(v \in \mathbb {F}_2^n\), the evaluation map at \(v\) is the linear map
This is given by \(\texttt{LinearMap.apply$_l$}\; v\).
Let \(G\) be a simple graph on \(V\), \(\Lambda \) a labeling of \(G\) with parameter \(s\), and \(H : \mathbb {F}_2^s \to \mathbb {F}_2^m\) a parity-check linear map. The coboundary map \(\delta \) applied to \(y : V \to \mathbb {F}_2^m\) is the function on edge-set of \(G\) given by
where \(\mathbf{1}_e\) denotes the indicator of edge \(e\) and \(\partial _\Lambda ^H\) is the Tanner differential.
Let \(H : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be a linear map. The transpose \(H^\top : \mathbb {F}_2^m \to \mathbb {F}_2^s\) is defined by
for \(j \in \{ 0,\ldots ,s-1\} \), where \(e_j = \mathbf{1}_j\) denotes the \(j\)-th standard basis vector. This is a linear map: additivity follows since the dot product is \(\mathbb {F}_2\)-bilinear, and scalar compatibility follows since \(\mathbb {F}_2\) is a field of characteristic 2.
Let \(V\) be a finite type and \(m \in \mathbb {N}\). For a vector \(y : V \to (\operatorname {Fin} m \to \mathbb {F}_2)\), the total Hamming weight is
where \(\operatorname {wt}(y_v)\) denotes the Hamming weight of the fiber \(y_v \in \mathbb {F}_2^m\).
The edge-to-vertex expansion parameter \(\beta '\) is defined as
which is equal to \(\operatorname {betaParam}(s, \lambda _2, \alpha )\).
The vertex-to-edge-boundary expansion parameter \(\beta ''\) is defined as
This arises from applying the relative vertex-to-edge expansion lemma with \(b = d_L - 1\) and \(\alpha ' = \alpha s\), ensuring that all high-expansion vertices have violated local checks.
Let \(G\) be a simple graph, \(\Lambda \) a labeling of \(G\) of degree \(s\), and \(\operatorname {parityCheck} : \mathbb {F}_2^s \to \mathbb {F}_2^m\) a linear map. The differential weight of a vector \(c : G.\operatorname {edgeSet} \to \mathbb {F}_2\) is
counting the number of vertices at which the local parity check is violated.
For a graph \(G\), a vector \(c : G.\operatorname {edgeSet} \to \mathbb {F}_2\), and a vertex \(v \in V\), the support edges at \(v\) is
For a valid prime \(q\), the code length is
This equals \(3|X_1|\) where \(|X_1| = \tfrac {s}{2} \cdot |\operatorname {PGL}(2,q)| = 201 \cdot q(q^2-1)\) is the number of edges of the LPS graph, obtained by the handshaking lemma for \(s\)-regular graphs with \(|X_0| = |\operatorname {PGL}(2,q)| = q(q^2-1)\) vertices and \(s = 402\).
For a valid prime \(q\), the LPS code data is a structure consisting of:
The number of \(X\)-type check rows \(r_X \in \mathbb {N}\),
The number of \(Z\)-type check rows \(r_Z \in \mathbb {N}\),
A subsystem CSS code of length \(N = \operatorname {codeLength}(q)\).
For a valid prime \(q\), the LPS construction data is a structure consisting of:
The number of \(X\)-type check rows \(r_X \in \mathbb {N}\),
The number of \(Z\)-type check rows \(r_Z \in \mathbb {N}\),
A subsystem CSS code of length \(N = \operatorname {codeLength}(q)\),
A proof that the \(X\)-type parity check matrix \(H_X\) has bounded weight \(\leq 2s = 804\) (LDPC property),
A proof that the \(Z\)-type parity check matrix \(H_{ZT}\) has bounded weight \(\leq 2s = 804\) (LDPC property).
The bound \(2s = 804\) arises from the Kronecker product structure: the Tanner code differential has weight \(\leq s\) (from \(s\)-regularity) and the cycle graph differential has weight \(2\), giving total weight \(\leq 2s\) after the balanced product quotient.
A valid prime for the LPS construction with \(p = 401\) is a structure consisting of:
A prime \(q \in \mathbb {N}\) with \(q\) odd, \(q \neq 401\), and \(q {\gt} 2\sqrt{401}\),
Elements \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfying \(x^2 + y^2 + 1 = 0\).
The condition \(x^2 + y^2 + 1 = 0\) witnesses that \(-1\) is not a quadratic residue mod \(q\), i.e., the Legendre symbol \((p/q) = -1\).
Let \(d_B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\) and \(d_F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) be linear maps, and let \(\varphi \) be a connection of type \(\operatorname {Connection}(n_1, m_1, n_2, m_2, d_F)\).
We say \(\varphi \) acts as identity on homology if for every basis element \(b^1 \in \operatorname {Fin}(n_1)\) and every \(b^0 \in \operatorname {Fin}(m_1)\) such that \(d_B(e_{b^1})(b^0) \neq 0\), the chain automorphism \(\varphi (b^1, b^0)\) acts as the identity on the homology of \(F\).
Formally:
Given a differential \(\partial ^F : (\operatorname {Fin} n_2 \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin} m_2 \to \mathbb {F}_2)\) and an augmented complex \(\mathtt{aug}\), the augmentation map at fiber degree \(q \in \mathbb {Z}\) is defined as:
This defines a linear map \((\operatorname {Fin}(\operatorname {fiberSize}(n_2, m_2, q)) \to \mathbb {F}_2) \to _{\mathbb {F}_2} \mathbb {F}_2\), corresponding to \(\pi _0 = \varepsilon \) and \(\pi _q = 0\) for \(q \ne 0\).
A complex \(F = (F_1 \xrightarrow {\partial ^F} F_0)\) is augmented if there exists a linear map \(\varepsilon : F_0 \to \mathbb {F}_2\) such that \(\varepsilon \circ \partial ^F = 0\). Concretely, for fixed natural numbers \(n_2, m_2\) and a linear map \(\partial ^F : (\operatorname {Fin} n_2 \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin} m_2 \to \mathbb {F}_2)\), an AugmentedComplex consists of:
A linear map \(\varepsilon : (\operatorname {Fin} m_2 \to \mathbb {F}_2) \to _{\mathbb {F}_2} \mathbb {F}_2\) (the augmentation map),
A proof that \(\varepsilon \circ \partial ^F = 0\) (the chain map condition).
Given a connection \(\varphi \) and a fiber degree \(q \in \mathbb {Z}\), the automorphism component at degree \(q\) is the family of linear endomorphisms
For \(n, n' \in \mathbb {Z}\), the base differential is:
as a linear map \((\operatorname {Fin}(\operatorname {baseSize}(n_1,m_1,n)) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(\operatorname {baseSize}(n_1,m_1,n')) \to \mathbb {F}_2)\).
The base size function assigns dimensions to degrees:
This encodes the graded structure of the base 1-complex \(B = (\mathbb {F}_2^{n_1} \xrightarrow {\partial ^B} \mathbb {F}_2^{m_1})\).
Let \(n_2, m_2 \in \mathbb {N}\) and let \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) be a linear map (the differential of a 1-complex \(F\) over \(\mathbb {F}_2\)). A chain automorphism of \(F\) is a structure consisting of:
an invertible linear map \(\alpha _1 : \mathbb {F}_2^{n_2} \xrightarrow {\sim } \mathbb {F}_2^{n_2}\) (automorphism on \(F_1\)),
an invertible linear map \(\alpha _0 : \mathbb {F}_2^{m_2} \xrightarrow {\sim } \mathbb {F}_2^{m_2}\) (automorphism on \(F_0\)),
the chain map condition: \(\partial ^F \circ \alpha _1 = \alpha _0 \circ \partial ^F\).
Let \(d_F : (\mathbb {F}_2^{n_2}) \to (\mathbb {F}_2^{m_2})\) be a linear map and let \(\psi \) be a chain automorphism of the chain complex \(F = (F^1 \xrightarrow {d_F} F^0)\). We say \(\psi \) acts as the identity on homology if:
Degree 1: For every \(f \in \ker (d_F)\), we have \(\alpha _1(f) = f\) (i.e., \(\alpha _1\) fixes cycles).
Degree 0: For every \(y \in \mathbb {F}_2^{m_2}\), we have \(\alpha _0(y) - y \in \operatorname {im}(d_F)\) (i.e., \([\alpha _0(y)] = [y]\) in \(H_0(F) = \mathbb {F}_2^{m_2}/\operatorname {im}(d_F)\)).
Given a differential \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), the identity chain automorphism \(\operatorname {id}_F\) is the chain automorphism with \(\alpha _1 = \operatorname {id}_{\mathbb {F}_2^{n_2}}\) and \(\alpha _0 = \operatorname {id}_{\mathbb {F}_2^{m_2}}\).
The cochain map \(\pi ^* : B^*_n \to \operatorname {Tot}(B \boxtimes _\varphi F)^*_n\) at degree \(n\) is defined as the \(\mathbb {F}_2\)-dual (transpose) of the chain map \(\pi _*\):
which is a linear map
On a cochain \(\beta \in B^*_p\), this gives \(\pi ^*(\beta )(b \otimes f) = \beta (b) \cdot \varepsilon (f)\) for \(f \in F_0\), and \(\pi ^*(\beta )(b \otimes f) = 0\) for \(f \in F_1\).
A connection for a fiber bundle with base dimensions \(n_1, m_1\) and fiber differential \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) is a function
That is, to each pair \((b^1, b^0) \in \operatorname {Fin}(n_1) \times \operatorname {Fin}(m_1)\), the connection assigns a chain automorphism of \(F\). Values outside the support of \(\partial ^B(e_{b^1})\) are irrelevant.
The twisted horizontal differential is the morphism in \(\operatorname {Mod}_{\mathbb {F}_2}\):
where \(\partial ^h_\varphi = \operatorname {twistedDhLin}(\partial ^B, (b_1, b_0) \mapsto \operatorname {autAtDeg}(\partial ^F, \varphi , q, b_1, b_0))\) is the connection-twisted horizontal differential.
The vertical differential \(\partial ^v = \operatorname {id}_B \otimes \partial ^F\) is the morphism in \(\operatorname {Mod}_{\mathbb {F}_2}\):
defined via \(\operatorname {LinearMap.lTensor}\).
The graded object underlying the fiber bundle double complex is the functor
The fiber bundle complex \(B \otimes _\varphi F = \operatorname {Tot}(B \boxtimes _\varphi F)\) is the total complex of the fiber bundle double complex:
It is the chain complex over \(\mathbb {F}_2\) obtained by taking the direct sum totalization of the double complex \(B \boxtimes _\varphi F\), with differential given by \(\partial ^h_\varphi + \partial ^v\) (summing the horizontal and vertical differentials in each total degree). The existence of the total complex is guaranteed because each graded piece is a finitely-generated \(\mathbb {F}_2\)-module, so all necessary coproducts exist and the \(\operatorname {HasTotal}\) instance holds by type class inference.
Let \(\partial ^B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\), \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), and \(\varphi \) a connection. The fiber bundle double complex \(B \boxtimes _\varphi F\) is the double complex over \(\mathbb {F}_2\) with:
Objects: \((p, q) \mapsto \mathbb {F}_2^{\operatorname {baseSize}(p)} \otimes _{\mathbb {F}_2} \mathbb {F}_2^{\operatorname {fiberSize}(q)}\),
Horizontal differential: \(\partial ^h_\varphi = \operatorname {fbDh}(p, p', q)\) (the connection-twisted map),
Vertical differential: \(\partial ^v = \operatorname {fbDv}(p, q, q') = \operatorname {id}_B \otimes \partial ^F\).
This is constructed using \(\operatorname {HomologicalComplex}_2.\operatorname {ofGradedObject}\) with the descending complex shape on \(\mathbb {Z}\). The double complex axioms are verified by the following conditions:
\((\partial ^h)^2 = 0\): since \(\operatorname {fbDh}(p, p', q) \circ \operatorname {fbDh}(p', p'', q) = 0\) (at most one factor can be nonzero, as \(p = 1, p' = 0\) and \(p' = 1, p'' = 0\) cannot both hold),
\((\partial ^v)^2 = 0\): since \(\operatorname {fbDv}(p, q', q'') \circ \operatorname {fbDv}(p, q, q') = 0\) (similarly),
Commutativity \(\partial ^h \circ \partial ^v = \partial ^v \circ \partial ^h\): by Lemma 184, since each \(\varphi (b_1, b_0)\) is a chain automorphism.
Given linear maps \(d_B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\) and \(d_F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), and a connection \(\varphi \), the fiber bundle small double complex is the \(2\times 2\) double complex \(E = B \otimes _\varphi F\) with:
with vertical differentials \(d_v^i = \operatorname {id} \otimes d_F\) (left-tensored), and horizontal twisted differentials:
where \(\alpha _k^\varphi (b^1, b^0) = \operatorname {autAtDeg}(d_F, \varphi , k, b^1, b^0)\). The anticommutativity condition \(d_h \circ d_v = d_v \circ d_h\) is supplied by \(\operatorname {twistedDh_comm_dv}\).
Given \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), the fiber differential at degrees \((q, q')\) is the linear map
The fiber size function assigns dimensions to degrees:
This encodes the graded structure of the fiber 1-complex \(F = (\mathbb {F}_2^{n_2} \xrightarrow {\partial ^F} \mathbb {F}_2^{m_2})\).
Suppose \(e_1 : M_1 \simeq N_1\) and \(e_2 : M_2 \simeq N_2\) are linear equivalences, \(f : M_1 \to M_2\) and \(g : N_1 \to N_2\) are linear maps, and the diagram
commutes (i.e., \(e_2 \circ f = g \circ e_1\)). Then there is a canonical linear equivalence \(\ker (f) \simeq \ker (g)\).
Let \(M\) be a free \(\mathbb {F}_2\)-module and \(f : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) a linear map. Since \(M\) is free over a field it is flat, so there is a canonical linear equivalence:
Let \(M\) be an \(\mathbb {F}_2\)-module and \(f : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\). There is a canonical linear equivalence:
Let \(\varepsilon : (\mathbb {F}_2^{m_2}) \to \mathbb {F}_2\) be a linear map (the augmentation of \(F_0\)). The projection \(\pi _*\) at degree 1 is the linear map
defined by
where \(\operatorname {rid}\) denotes the right-unit isomorphism \(V \otimes \mathbb {F}_2 \simeq V\). Concretely, on simple tensors \(\pi _*^{(1)}(b \otimes f,\, 0) = \varepsilon (f) \cdot b\), and \(\pi _*^{(1)}\) is zero on the \(\mathbb {F}_2^{m_1} \otimes \mathbb {F}_2^{n_2}\) component.
The map induced by \(\pi _*\) on degree-1 homology,
defined as the quotient lift
Under the same hypotheses as Theorem 235, the map \(H_1(\pi _*)\) is packaged as a linear equivalence
constructed via LinearEquiv.ofBijective applied to the bijection of Theorem 235.
The chain map \(\pi _* : \operatorname {Tot}(B \boxtimes _\varphi F)_n \to \mathbb {F}_2^{\operatorname {baseSize}(n_1,m_1,n)}\) at degree \(n\) is assembled from the summand maps using \(\operatorname {totalDesc}\):
given by summing the contributions \(\operatorname {piStarSummandMor}(\partial ^F, \mathtt{aug}, n, p, q)\) over all \((p, q)\) with \(p + q = n\).
The restriction of \(\pi _*^{(1)}\) to \(\operatorname {totZ}_1\), landing in \(\ker (d_B)\):
This is a well-defined \(\mathbb {F}_2\)-linear map by Lemma 229.
For integers \(p, q \in \mathbb {Z}\), the linear map underlying the \((p,q)\)-summand of \(\pi _*\) is:
given by \(b \otimes f \mapsto \pi _q(f) \cdot b\), where \(\pi _q = \operatorname {augMap}(\partial ^F, \mathtt{aug}, q)\). Concretely, this is the composition
For \(n, p, q \in \mathbb {Z}\) with \(p + q = n\), the \((p,q)\)-component of \(\pi _*\) is a morphism in \(\operatorname {ModuleCat}_{\mathbb {F}_2}\):
defined by:
If \(q = 0\): the map \(b \otimes f \mapsto \varepsilon (f) \cdot b\), composed with a type transport via \(\operatorname {Fin.cast}\) using the equality \(p = n\) (from \(p + 0 = n\)),
If \(q \ne 0\): the zero morphism.
Under the same hypotheses, and assuming \(\operatorname {totH}_1\) and \(\ker (d_B)\) are finite-dimensional, the dual of the isomorphism \(H_1(\pi _*)^{\simeq }\) yields a linear equivalence
Explicitly, for \(f \in \operatorname {Hom}(\ker (d_B), \mathbb {F}_2)\), we set \(H^1(\pi ^*)(f) = f \circ H_1(\pi _*)^{\simeq }\), and the inverse sends \(g \mapsto g \circ (H_1(\pi _*)^{\simeq })^{-1}\).
Let \(M\) be a free \(\mathbb {F}_2\)-module and \(f : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\). There is a canonical linear equivalence:
Let \(M\) be an \(\mathbb {F}_2\)-module and \(f : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\). There is a canonical linear equivalence:
Let \(V\) be an \(\mathbb {F}_2\)-module, let \(\partial ^B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\) be a linear map, and let \(\operatorname {autComp} : \operatorname {Fin}(n_1) \to \operatorname {Fin}(m_1) \to (V \to _{\mathbb {F}_2} V)\) be a family of linear endomorphisms. The twisted horizontal differential
is the linear map defined via the universal property of the tensor product (via \(\operatorname {TensorProduct.lift}\)): on a pure tensor \(b \otimes f\) (with \(b : \mathbb {F}_2^{n_1}\), \(f : V\)), it acts as
where \(e_{b_1}\) and \(e_{b_0}\) denote the standard basis vectors. This is well-defined as a bilinear map and extends to a linear map on the tensor product.
Let \(G\) be a simple graph on a finite vertex type \(V\) with decidable adjacency, and write \(n = |V|\). The adjacency eigenvalues of \(G\) are the function
defined as the eigenvalues \(\lambda _0 \geq \lambda _1 \geq \cdots \geq \lambda _{n-1}\) of \(G.\operatorname {adjMatrix}(\mathbb {R})\), sorted in decreasing order. Concretely, this is (adjMatrix_isHermitian G).eigenvalues\(_0\).
Let \(\iota \) be an index type, \(n : \iota \to \mathbb {N}\) a family of sizes, \(s \in \mathbb {N}\) a uniform regularity degree, and \(G_i\) a simple \(s\)-regular graph on \(\operatorname {Fin}(n(i))\) for each \(i \in \iota \), with \(n(i) \geq 2\) for all \(i\). The family \(\{ G_i\} _{i \in \iota }\) is an expander family if there exists \(\varepsilon {\gt} 0\) such that
i.e. the spectral gap of every graph in the family is uniformly bounded below by \(\varepsilon \).
Let \(G\) be a finite \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\). The graph \(G\) is Ramanujan if every eigenvalue \(\lambda \) of the adjacency matrix satisfying \(|\lambda | {\lt} s\) also satisfies
Formally, \(G\) is Ramanujan if for all \(i \in \operatorname {Fin}(|V|)\),
This is the optimal spectral bound for \(s\)-regular graphs.
Let \(G\) be a simple graph on a finite vertex type \(V\) with decidable adjacency, and suppose \(|V| \geq 2\). The second-largest eigenvalue \(\lambda _2\) of \(G\) is
i.e. the eigenvalue at index \(1\) in the decreasing sequence \(\lambda _0 \geq \lambda _1 \geq \cdots \).
Let \(G\) be a finite \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\). The spectral gap of \(G\) is
where \(\lambda _2(G)\) is the second-largest eigenvalue of \(G\). A larger spectral gap indicates better expansion properties.
A graph with group action consists of a finite graph \(X\) (given as a 1-dimensional cell complex, i.e., a CellComplex) equipped with a free right action of a finite group \(H\) on both vertices \(X_0\) and edges \(X_1\), compatible with the boundary map, and satisfying a quotient condition.
Formally, it is a structure \(\mathtt{GraphWithGroupAction}(H)\) for a group \(H\) with \(|H| {\lt} \infty \), comprising:
A cell complex \(\mathtt{graph} : \mathtt{CellComplex}\) (the underlying graph).
A right \(H\)-action \(\mathtt{vertexAction}\) on the vertices \(X.\mathtt{graph}.\mathtt{cells}(0)\), modeled as a left MulAction via \(h \cdot v = v \cdot h^{-1}\).
A right \(H\)-action \(\mathtt{edgeAction}\) on the edges \(X.\mathtt{graph}.\mathtt{cells}(1)\).
Freeness of the vertex action: for all \(h \in H\) and \(v \in X_0\), if \(h \cdot v = v\) then \(h = 1\).
Freeness of the edge action: for all \(h \in H\) and \(e \in X_1\), if \(h \cdot e = e\) then \(h = 1\).
Boundary equivariance: for all \(e \in X_1\), \(h \in H\), and \(\tau \in X_0\),
\[ \tau \in \partial (h \cdot e) \iff h^{-1} \cdot \tau \in \partial e. \]Quotient condition: for all \(e \in X_1\), \(v \in X_0\), and \(h \in H\), if \(v \in \partial e\) and \(h \cdot v \in \partial e\), then \(h = 1\). (No edge connects a vertex to a nontrivially translated copy of itself.)
Let \(X\) be a graph with a group action by \(H\). The set of edges incident to a vertex \(v \in X_0\) in the cell complex is defined as
Formally, \(\operatorname {cellIncidentEdges}(v) = \{ e \in X_1 \mid v \in X.\operatorname {graph}.\operatorname {bdry}(e) \} \).
A cell complex labeling of degree \(s\) on \(X\) is a family \(\Lambda = \{ \Lambda _v\} _{v \in X_0}\) assigning to each vertex \(v \in X_0\) a bijection
Formally, \(\operatorname {CellLabeling}(s) = \prod _{v : X_0} (\delta v \simeq \operatorname {Fin}(s))\).
Given a trivialization \(R\), an edge \(e \in X_1\), and two boundary vertices \(\tau _1, \tau _2 \in \partial e\) lying in distinct vertex orbits (\(\pi _0(\tau _1) \neq \pi _0(\tau _2)\)), the connection of \(e\) relative to \(\tau _1\) and \(\tau _2\) is the group element
where \(g_{\tau _i} = \mathtt{vertexGroupElement}(R, \tau _i)\) is the unique element satisfying \(g_{\tau _i} \cdot R(\pi _0(\tau _i)) = \tau _i\).
Given a trivialization \(R\) of \(X\), the induced connection is a map
defined as follows. For an edge orbit \(E \in (X/H)_1\), let \(e = \mathtt{out}(E)\) be a chosen representative edge with boundary \(\partial e\). If there exist \(\tau _1, \tau _2 \in \partial e\) with \(\pi _0(\tau _1) \neq \pi _0(\tau _2)\), we set
where \(\tau _1, \tau _2\) are chosen witnesses and \(g_{\tau _i} = \mathtt{vertexGroupElement}(R,\tau _i)\). Otherwise (all boundary vertices are in the same orbit, or the boundary is small), we set \(\phi _R(E) := 1\).
By the orbit compatibility lemma, this is independent of the choice of representative edge.
A cell complex labeling \(\Lambda \) is \(H\)-invariant if for all vertices \(v \in X_0\), all group elements \(h \in H\), and all incident edges \(e \in \delta v\),
Formally, \(\operatorname {IsInvariantLabeling}(\Lambda )\) is the proposition
The quotient boundary map on the quotient graph assigns to each edge orbit \(E \in (X/H)_1\) a finite set of vertex orbits:
where \(e\) is any representative of \(E\). This is well-defined: if \(e_1, e_2\) represent the same orbit, so \(\exists \, g \in H,\; g \cdot e_2 = e_1\), then for any \(\tau \in \partial e_1\), we have \(g^{-1} \cdot \tau \in \partial e_2\) by boundary equivariance, and \(\pi _0(g^{-1} \cdot \tau ) = \pi _0(\tau )\) since they are in the same \(H\)-orbit; and vice versa.
For a vertex orbit \([v] \in X/H\), the quotient incident edges are the edge orbits \([e] \in X_1/H\) such that some representative edge has a boundary vertex in the orbit of \([v]\):
Given an \(H\)-invariant labeling \(\Lambda \) (i.e., \(\operatorname {IsInvariantLabeling}(\Lambda )\) holds), the quotient labeling \(\bar{\Lambda }\) is a well-defined bijection
for each vertex orbit \([v] \in X/H\), defined by \(\bar{\Lambda }_{[v]}([e]) = \Lambda _v(e)\) for any representatives \(v \in [v]\) and \(e \in [e]\) with \(e \in \delta v\).
For a vertex \(v \in X_0\), a group element \(h \in H\), and an incident edge \(e \in \delta v\), define the transported incident edge
as the pair \(\langle h \cdot e.{\operatorname {val}},\, \operatorname {smul_incident_of_incident}(v, e.{\operatorname {val}}, h, e.{\operatorname {prop}})\rangle \).
A trivialization of the vertex quotient map \(\pi _0 : X_0 \to (X/H)_0\) is a section, i.e., a function
such that for every vertex orbit \(V \in (X/H)_0\), the representative \(R(V)\) lies in \(V\):
The set \(\{ R(V) \mid V \in (X/H)_0\} \subseteq X_0\) contains exactly one representative from each \(H\)-orbit of vertices.
Given a trivialization \(R\) of \(X\) and a vertex \(v \in X_0\), the vertex group element \(g_v \in H\) is the unique group element such that
Since \(\pi _0(R(\pi _0(v))) = \pi _0(v)\), the vertices \(R(\pi _0(v))\) and \(v\) lie in the same \(H\)-orbit, so such a \(g_v\) exists (chosen via the axiom of choice).
The Hamming ball of radius \(r \in \mathbb {R}\) centered at the origin in \(\mathbb {F}_2^n\) is the finset
where \(\operatorname {wt}(v)\) denotes the Hamming weight of \(v\). When \(r {\lt} 0\), the ball is empty.
A linear map \(f : (\operatorname {Fin} n \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin} m \to \mathbb {F}_2)\) is said to have bounded weight \(w\) (for some \(w \in \mathbb {N}\)) if every row and every column of its matrix representation has Hamming weight at most \(w\):
Let \(H\) be a group. An \(H\)-equivariant chain complex over \(\mathbb {F}_2\) consists of:
an underlying chain complex \(C_\bullet \) over \(\mathbb {F}_2\),
for each degree \(i \in \mathbb {Z}\), a representation \(\rho _i : H \to \operatorname {GL}_{\mathbb {F}_2}(C_i)\) (i.e., a left \(\mathbb {F}_2[H]\)-module structure on \(C_i\)),
an equivariance condition: for all \(i, j \in \mathbb {Z}\) and \(h \in H\),
\[ \partial ^{i \to j} \circ \rho _i(h) = \rho _j(h) \circ \partial ^{i \to j}, \]i.e., the differential \(\partial : C_i \to C_j\) intertwines the \(H\)-actions.
Let \(H\) be a finite group and \(C\), \(D\) \(H\)-equivariant chain complexes over \(\mathbb {F}_2\). For \(n \in \mathbb {Z}\), the balanced Künneth sum is
the direct sum of all balanced Künneth summands.
Let \(H\) be a finite group and \(C\), \(D\) \(H\)-equivariant chain complexes over \(\mathbb {F}_2\). For \(n, p \in \mathbb {Z}\), the balanced Künneth summand at index \(p\) is
defined as the coinvariants of the tensor product representation \(\rho ^{H_p}_C \otimes \rho ^{H_{n-p}}_D\) of \(H\) on \(H_p(C) \otimes _{\mathbb {F}_2} H_{n-p}(D)\).
Let \(C\) and \(D\) be \(H\)-equivariant chain complexes. The balanced product double complex \(C \boxtimes _H D\) is the double complex over \(\mathbb {F}_2\) with:
objects \((C \boxtimes _H D)_{p,q} = C_p \otimes _H D_q\),
horizontal differential \(\partial ^h = \partial ^C \otimes _H \operatorname {id}_D\) (decreasing \(p\)),
vertical differential \(\partial ^v = \operatorname {id}_C \otimes _H \partial ^D\) (decreasing \(q\)).
This forms a valid double complex: \((\partial ^h)^2 = 0\), \((\partial ^v)^2 = 0\), and \(\partial ^h \circ \partial ^v = \partial ^v \circ \partial ^h\).
Let \(H\) be a finite group and \(C\) an \(H\)-equivariant chain complex over \(\mathbb {F}_2\). For each \(p \in \mathbb {Z}\), the group \(H\) acts on the boundaries \(B_p(C) = \operatorname {im} \partial _{p+1}\) by the boundaries action
using \(H\)-equivariance of \(\partial _{p+1}\).
Let \(H\) be a finite group and \(C\) an \(H\)-equivariant chain complex over \(\mathbb {F}_2\). For each \(p \in \mathbb {Z}\), the group \(H\) acts on the submodule \(B_p(C) \subseteq Z_p(C)\) (boundaries viewed inside cycles) by the boundaries-sub-cycles action, induced from \(\rho ^Z_p\) and \(\rho ^B_p\) compatibly: for \(z \in Z_p(C)\) with \(z \in B_p(C)\), one sets \(h \cdot z = \rho _p(h)(z)\), which lies in both \(Z_p(C)\) and \(B_p(C)\).
Let \(C\) and \(D\) be \(H\)-equivariant chain complexes. The horizontal differential
is induced by \(\partial ^C_{p \to p'} \otimes \operatorname {id}_{D_q}\) on the balanced product. This is well-defined on coinvariants by the \(H\)-equivariance of \(\partial ^C\).
Let \(C\) and \(D\) be \(H\)-equivariant chain complexes. The vertical differential
is induced by \(\operatorname {id}_{C_p} \otimes \partial ^D_{q \to q'}\) on the balanced product. This is well-defined on coinvariants by the \(H\)-equivariance of \(\partial ^D\).
Let \(C\) and \(D\) be \(H\)-equivariant chain complexes. For integers \(p, q \in \mathbb {Z}\), the balanced product object at \((p,q)\) is
the balanced product (coinvariants of \(C_p \otimes _{\mathbb {F}_2} D_q\) under the diagonal \(H\)-action) of the representations \(\rho ^C_p\) and \(\rho ^D_q\).
Let \(H\) be a finite group and \(C\) an \(H\)-equivariant chain complex over \(\mathbb {F}_2\). For each \(p \in \mathbb {Z}\), the group \(H\) acts on the cycles \(Z_p(C) = \ker \partial _p\) by the cycles action
where \(\rho _p\) is the given \(H\)-action on \(C_p\). This is well-defined: if \(z \in \ker \partial _p\) then \(\partial _p(\rho _p(h)(z)) = \rho _{p-1}(h)(\partial _p(z)) = \rho _{p-1}(h)(0) = 0\), using the \(H\)-equivariance of \(\partial _p\).
Let \(H\) be a finite group and \(C\) an \(H\)-equivariant chain complex over \(\mathbb {F}_2\). For each \(p \in \mathbb {Z}\), the induced \(H\)-action on homology \(H_p(C) = Z_p(C)/B_p(C)\) is the representation
defined via the quotient map \(\operatorname {mapQ}\) applied to the cycles action \(\rho ^Z_p(h)\), using the fact that \(\rho _p(h)\) preserves \(B_p(C)\).
Let \(A\), \(B\), \(C\) be finite types with decidable equality. A linear map \(f : (A \to \mathbb {F}_2) \to _{\mathbb {F}_2} (B \to C \to \mathbb {F}_2)\) is \((\alpha , \beta )\)-expanding (written \(\operatorname {IsExpandingLinMap}(f, \alpha , \beta )\)) if:
\(0 {\lt} \alpha \leq 1\) and \(0 {\lt} \beta \);
For every \(x : A \to \mathbb {F}_2\) with \(\operatorname {wt}(x) \leq \alpha \cdot |A|\), we have
\[ \bigl|\{ (b,c) \in B \times C \mid f(x)(b,c) \neq 0\} \bigr| \; \geq \; \beta \cdot \operatorname {wt}(x). \]
The horizontal embedding is the \(\mathbb {F}_2\)-linear map
defined as the composition
where \(\kappa : H_1 \xrightarrow {\sim } \bigoplus _p H_p(\mathcal{C}(X,\Lambda )) \otimes _H H_{1-p}(\mathcal{C}_\ell )\) is the Künneth isomorphism (Def. 27).
The vertical embedding is the \(\mathbb {F}_2\)-linear map
defined as the composition
where \(\kappa \) is the Künneth isomorphism.
The gauge submodule \(H_1^G \subseteq H_1\) is defined as the image of the vertical embedding:
Gauge \(Z\)-operators correspond to elements of the vertical homology \(H_1^v\).
The logical submodule \(H_1^L \subseteq H_1\) is defined as the image of the horizontal embedding:
Logical \(Z\)-operators of the subsystem code correspond to nontrivial elements of the horizontal homology \(H_1^h\).
Let \(H\) be a finite group acting on a graph-with-group-action \(X\) with cell labeling \(\Lambda \), and let \(\ell \geq 3\) be an odd integer with a compatible cycle action. The horizontal Künneth inclusion is the \(\mathbb {F}_2\)-linear map
defined as the direct sum inclusion at index \(p = 1\). Here \(H_1^h\) denotes the horizontal homology summand of the balanced product complex.
The vertical Künneth inclusion is the \(\mathbb {F}_2\)-linear map
defined as the direct sum inclusion at index \(p = 0\). Here \(H_1^v\) denotes the vertical homology summand of the balanced product complex.
The balanced product complex \(C(X, \Lambda ) \otimes _H C(C_\ell )\) is defined as
the balanced product of the Tanner code complex and the cycle graph complex over \(H\).
The horizontal cohomology is the balanced Künneth summand at indices \(p = 1\), \(q = 0\):
By the homology-cohomology equivalence over \(\mathbb {F}_2\), this coincides with \(H_1^h\).
The vertical cohomology is the balanced Künneth summand at indices \(p = 0\), \(q = 1\):
By the homology-cohomology equivalence over \(\mathbb {F}_2\), this coincides with \(H_1^v\).
Let \(\ell \geq 3\) be an odd natural number with \(H\) acting on \(\operatorname {Fin}(\ell )\) via a cycle-compatible action \(h_{\mathrm{compat}}\). The cycle graph \(H\)-equivariant chain complex is defined as
the \(H\)-equivariant chain complex associated to the cycle graph \(C_\ell \).
For each integer \(p \in \mathbb {Z}\), the canonical inclusion of the \(p\)-th summand into the direct sum is the \(\mathbb {F}_2\)-linear map
defined as \(\iota _p := \operatorname {DirectSum.lof}_{\mathbb {F}_2}(-)(p)\).
For each integer \(p \in \mathbb {Z}\), the canonical projection onto the \(p\)-th summand is the \(\mathbb {F}_2\)-linear map
defined as \(\pi _p := \operatorname {DirectSum.component}_{\mathbb {F}_2}(-)(p)\).
The degree-1 homology of the balanced product complex is defined as
the first homology group of \(C(X, \Lambda ) \otimes _H C(C_\ell )\) over \(\mathbb {F}_2\).
The horizontal homology is the balanced Künneth summand at indices \(p = 1\), \(q = 0\):
The vertical homology is the balanced Künneth summand at indices \(p = 0\), \(q = 1\):
A homology class \(x \in H_1\) is horizontal if its vertical projection vanishes:
Equivalently, under the Künneth isomorphism, \(x\) lies entirely in the horizontal summand \(H_1^h \oplus \{ 0\} \).
A homology class \(x \in H_1\) is vertical if its horizontal projection vanishes:
Equivalently, under the Künneth isomorphism, \(x\) lies entirely in the vertical summand \(\{ 0\} \oplus H_1^v\).
Assuming \(|H|\) is odd, the Künneth isomorphism at degree \(1\) is the \(\mathbb {F}_2\)-linear equivalence
defined as \(\phi := \operatorname {kunnethBalancedProduct}\! \bigl(\operatorname {tannerHEq}(X, \Lambda , h_\Lambda ),\; \operatorname {cycleHEq}(\ell , h_{\mathrm{compat}}),\; h_{\mathrm{odd}},\; 1\bigr)\).
The horizontal projection \(p^h : H_1 \to H_1^h\) is the \(\mathbb {F}_2\)-linear map defined as the composition of the Künneth isomorphism with the canonical projection onto the \(p = 1\) summand:
where \(\phi : H_1 \xrightarrow {\sim } \bigoplus _p H_p \otimes _H H_{1-p}\) is the Künneth isomorphism and \(\pi _1\) is the projection onto the \(p = 1\) component.
The vertical projection \(p^v : H_1 \to H_1^v\) is the \(\mathbb {F}_2\)-linear map defined as the composition of the Künneth isomorphism with the canonical projection onto the \(p = 0\) summand:
where \(\phi : H_1 \xrightarrow {\sim } \bigoplus _p H_p \otimes _H H_{1-p}\) is the Künneth isomorphism and \(\pi _0\) is the projection onto the \(p = 0\) component.
Let \(H\) be a finite group acting on a graph \(X\) with cell labeling \(\Lambda \) that is invariant under the action. The Tanner code \(H\)-equivariant chain complex is defined as
the \(H\)-equivariant chain complex associated to the Tanner code on the graph with group action \(X\) and labeling \(\Lambda \).
The inclusion map is the \(\mathbb {F}_2\)-linear map
defined as the composition of the submodule inclusion \((V \otimes _{\mathbb {F}_2} W)^H \hookrightarrow V \otimes _{\mathbb {F}_2} W\) followed by the quotient map \(\operatorname {mk} : V \otimes _{\mathbb {F}_2} W \to V \otimes _H W\).
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\iota \) is a linear isomorphism:
This equivalence \(\iota ^{\equiv }\) is constructed via \(\operatorname {LinearEquiv.ofBijective}(\iota , \langle h_{\mathrm{inj}}, h_{\mathrm{surj}}\rangle )\), where \(h_{\mathrm{inj}}\) is from iotaMap_injective and \(h_{\mathrm{surj}}\) from iotaMap_surjective.
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\pi \) is a linear isomorphism:
This equivalence \(\pi ^{\equiv }\) is constructed via \(\operatorname {LinearEquiv.ofBijective}(\pi , \langle h_{\mathrm{inj}}, h_{\mathrm{surj}}\rangle )\), where \(h_{\mathrm{inj}}\) is from piMap_injective and \(h_{\mathrm{surj}}\) from piMap_surjective.
Let \(X\) be a finite graph with a free right \(H\)-action, \(\Lambda \) a cell labeling with \(s\) local code bits, and \(h_\Lambda \) a proof that \(\Lambda \) is \(H\)-invariant. For a vertex orbit \(V \in X_0/H\), the quotient local view is the \(\mathbb {F}_2\)-linear map
defined by \(c \mapsto \bigl(i \mapsto c\bigl((\Lambda ^{X/H}_V)^{-1}(i)\bigr)\bigr)\), where \(\Lambda ^{X/H}_V\) is the quotient labeling bijection at \(V\).
Linearity follows: for \(c_1, c_2 : X_1/H \to \mathbb {F}_2\) and \(r \in \mathbb {F}_2\),
Both properties follow by extensionality and simplification of the pointwise operations.
The quotient Tanner code complex \(C(X/H, L)\) is the chain complex over \(\mathbb {F}_2\) with chain spaces
and \(C_i = 0\) for \(i \geq 2\) or \(i {\lt} 0\). The differential is
(the quotient Tanner differential), and all other differentials are zero.
The chain complex condition \(d \circ d = 0\) is verified:
For the pair \((i,j,k) = (1,0,k)\): we have \(d_{1,0} \circ 0 = 0\) by the zero postcomposition rule.
For \(i = 0\): the outgoing differential is zero, so the composition vanishes.
For \(i \geq 2\) or \(i {\lt} 0\): the incoming differential is zero, so the composition vanishes by the zero precomposition rule.
All cases with non-adjacent indices satisfy the shape condition vacuously (the shape predicate fails, verified by positivity or simplification).
The homology in degree 1 is denoted \(H_1(C(X/H, L)) := \ker (d_{1,0}) / \operatorname {im}(0) = \ker (\partial )\).
The quotient Tanner differential is the \(\mathbb {F}_2\)-linear map
defined by \(c \mapsto (V \mapsto \operatorname {quotientLocalView}(V)(c))\).
Linearity: for \(c_1, c_2 : X_1/H \to \mathbb {F}_2\) and \(r \in \mathbb {F}_2\), the result follows by extensionality over vertex orbits \(V\) and local indices \(i\), together with simplification of the pointwise addition and scalar multiplication.
The witness graph is a trivial graph with a single vertex and a single edge, equipped with the trivial \(\mathrm{Unit}\)-action: the group \(H = \mathrm{Unit}\) acts on both vertices and edges as the identity. The cell sets are \(\mathrm{cells}(n) = \mathrm{Unit}\) for all \(n\), with empty boundary maps (satisfying \(\partial \circ \partial = 0\) vacuously). Both the vertex and edge actions are free (since the only element of \(\mathrm{Unit}\) fixing a cell is the identity). This provides a non-trivial graph with at least one vertex and one edge on which all required hypotheses hold.
The witness labeling is a cell labeling \(\Lambda : \operatorname {witnessGraph}.\operatorname {CellLabeling}(0)\) with \(s = 0\) local code bits. Since \(s = 0\), the labeling map at any vertex is a bijection from the empty set of incident edges to \(\operatorname {Fin}(0) = \emptyset \). It is defined by: for each vertex, the labeling bijection sends any element \(e\) with \(e \in \emptyset \) to its absurdity (by Finset.notMem_empty), and the inverse sends any element of \(\operatorname {Fin}(0)\) to its absurdity (by Fin.elim0).
The witness \(\mathrm{Unit}\) action on \(\operatorname {Fin}(3)\) is the trivial \(\mathrm{MulAction}\) where the unique group element \(() \in \mathrm{Unit}\) acts on every \(i \in \operatorname {Fin}(3)\) as the identity: \(() \cdot i = i\). The axioms \(\mathtt{one\_ smul}\) and \(\mathtt{mul\_ smul}\) hold by reflexivity.
A matrix \(A \in \mathbb {F}_2^{m \times n}\) is called \((\alpha , \beta )\)-expanding, where \(\alpha , \beta \in \mathbb {R}\), if the following conditions hold:
\(0 {\lt} \alpha \leq 1\),
\(0 {\lt} \beta \),
for every vector \(x \in \mathbb {F}_2^n\) satisfying \(|x| \leq \alpha \cdot n\), we have \(|Ax| \geq \beta \cdot |x|\),
where \(|\cdot |\) denotes the Hamming weight, and \(Ax\) denotes the matrix-vector product \(A \cdot x\) over \(\mathbb {F}_2\).
Formally, \(\operatorname {IsExpanding}(A, \alpha , \beta )\) holds if and only if
Let \(G\) be a simple graph on a finite vertex type \(V\), and let \(s \in \mathbb {N}\). A labeling for the Tanner code on \(G\) is a collection
where \(N(v) = G.\operatorname {neighborSet}(v)\) is the set of neighbors of \(v\) and \(\Lambda _v\) is a bijection. The neighbor \((\Lambda _v)^{-1}(i)\) corresponds to the \(i\)-th position in the local code. The existence of such a labeling requires \(|N(v)| = s\) for all \(v\), which holds when \(G\) is \(s\)-regular.
Let \(\Lambda \) be a labeling, \(v \in V\) a vertex, and \(c \in C_1(X) = (G.\operatorname {edgeSet} \to \mathbb {F}_2)\) a 1-chain. The local view at \(v\) is the \(\mathbb {F}_2\)-linear map
defined by
where \((\Lambda _v)^{-1}(i) \in N(v)\) is the neighbor of \(v\) labeled \(i\). This gives the restriction of \(c\) to the star of \(v\), viewed as an element of \(\mathbb {F}_2^s\) via the labeling.
For distinct odd primes \(p, q\) with Legendre symbol \(\left(\frac{p}{q}\right) = 1\), the element \(\operatorname {legendreSqrt}(q, p) \in \mathbb {Z}/q\mathbb {Z}\) is the square root of \(p\) in \(\mathbb {Z}/q\mathbb {Z}\), obtained via ZMod.isSquare_of_jacobiSym_eq_one.
For distinct odd primes \(p, q\) with \(q {\gt} 2\sqrt{p}\) and \(x, y \in \mathbb {Z}/q\mathbb {Z}\) with \(x^2+y^2+1=0\), the LPS generating set in \(\operatorname {PGL}_2(q)\) is the symmetric generating set
This is a SymmGenSet (i.e. closed under inverses and not containing the identity), verified by:
\(1 \notin S_{p,q}^{\operatorname {PGL}}\): If \(\pi _{\operatorname {PGL}}(\operatorname {tupleToGL}(t)) = 1\), then \(\operatorname {tupleToGL}(t) \in Z(\operatorname {GL})\), contradicting lpsMatrix_not_in_center.
Closure under inverses: For \(t \in S_p\) with \(a {\gt} 0\), use \(\bar{t} \in S_p\) and \(\pi _{\operatorname {PGL}}(\operatorname {tupleToGL}(\bar{t})) = \pi _{\operatorname {PGL}}(\operatorname {tupleToGL}(t))^{-1}\). For \(a = 0\), the element is its own inverse.
For distinct odd primes \(p, q\) with \(q {\gt} 2\sqrt{p}\) and \(\left(\frac{p}{q}\right) = 1\), and \(x, y \in \mathbb {Z}/q\mathbb {Z}\) with \(x^2+y^2+1=0\), the LPS generating set in \(\operatorname {PSL}_2(q)\) is the symmetric generating set
This is a SymmGenSet, verified by the same argument as for \(\operatorname {PGL}_2(q)\) but using the \(\operatorname {SL}\) variants of the matrix lemmas.
The LPS graph on \(\operatorname {PGL}_2(q)\) is the Cayley graph
When \(\left(\frac{p}{q}\right) = -1\) (i.e. the Legendre symbol is \(-1\)), this is the LPS expander graph on the group \(\operatorname {PGL}_2(q)\).
The LPS graph on \(\operatorname {PSL}_2(q)\) is the Cayley graph
When \(\left(\frac{p}{q}\right) = 1\) (i.e. the Legendre symbol is \(1\)), this is the LPS expander graph on the group \(\operatorname {PSL}_2(q)\).
Given \(x, y \in \mathbb {Z}/q\mathbb {Z}\) and a tuple \(t = (a,b,c,d) \in \mathbb {Z}^4\), the LPS matrix is the \(2 \times 2\) matrix over \(\mathbb {Z}/q\mathbb {Z}\) defined by
where \(\iota : \mathbb {Z} \to \mathbb {Z}/q\mathbb {Z}\) denotes the canonical ring homomorphism.
For a prime \(q\) and a matrix \(M \in M_2(\mathbb {Z}/q\mathbb {Z})\) with \(\det M \neq 0\), the element \(\operatorname {matToGL}(M) \in \operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z})\) is the unit corresponding to \(M\) (using the fact that invertibility of matrices over a field is equivalent to nonzero determinant).
For a prime \(q\), a matrix \(M \in M_2(\mathbb {Z}/q\mathbb {Z})\), and \(r \in \mathbb {Z}/q\mathbb {Z}\) with \(r \neq 0\) and \(r^2 = \det M\), define
This has determinant \(1\) since \(\det (r^{-1} M) = (r^{-1})^2 \det M = r^{-2} r^2 = 1\).
The projective general linear group \(\operatorname {PGL}(2, q) = \operatorname {GL}(2, \mathbb {F}_q) / Z(\operatorname {GL}(2, \mathbb {F}_q))\) is defined as the quotient of \(\operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z})\) by its center:
The projective special linear group \(\operatorname {PSL}(2, q) = \operatorname {SL}(2, \mathbb {F}_q) / Z(\operatorname {SL}(2, \mathbb {F}_q))\) is defined as the quotient of \(\operatorname {SL}(2, \mathbb {Z}/q\mathbb {Z})\) by its center:
For an odd prime \(p\) (i.e. \(p \equiv 1\) or \(3 \pmod{4}\)), the normalized subset \(S_p \subseteq \widetilde{S}_p\) is the finite set of integer \(4\)-tuples \((a,b,c,d)\) with \(a^2+b^2+c^2+d^2 = p\) satisfying the normalization condition:
If \(p \equiv 1 \pmod{4}\): \(a {\gt} 0\) and \(a\) is odd.
If \(p \equiv 3 \pmod{4}\): \(a\) is even and the first nonzero coordinate among \((a,b,c,d)\) is positive.
Concretely, \(S_p\) is obtained by filtering \(\{ -p, \ldots , p\} ^4\) by the predicate \(\operatorname {SpPred}(p)\).
For distinct odd primes \(p, q\), \(x, y \in \mathbb {Z}/q\mathbb {Z}\) with \(x^2 + y^2 + 1 = 0\), and \(t \in \widetilde{S}_p\), define
using \(\det M(t) \neq 0\) from lpsMatrixVal_det_ne_zero.
For distinct odd primes \(p, q\) with \(\left(\frac{p}{q}\right) = 1\), \(x, y \in \mathbb {Z}/q\mathbb {Z}\) with \(x^2+y^2+1=0\), and \(t \in \widetilde{S}_p\), define
where \(r = \operatorname {legendreSqrt}(q,p)\) satisfies \(r^2 = \det M(t) = (p : \mathbb {Z}/q\mathbb {Z})\).
For a prime \(q\) and \(x \in \mathbb {Z}/q\mathbb {Z}\), the unipotent GL element is the upper triangular unipotent matrix
with inverse \(\begin{pmatrix} 1 & -x \\ 0 & 1 \end{pmatrix}\).
For \(x \in \mathbb {Z}/q\mathbb {Z}\), the unipotent PGL element is the image of \(\operatorname {unipotentGL}(q,x)\) under the projection:
The unipotent homomorphism is the group homomorphism
defined by \(x \mapsto \operatorname {unipotentPGL}(q, \operatorname {toAdd}(x))\).
The map-one property holds because \(\operatorname {unipotentGL}(q, 0) = 1\), and the map-mul property holds because \(\operatorname {unipotentGL}(q, a+b) = \operatorname {unipotentGL}(q,a) \cdot \operatorname {unipotentGL}(q,b)\) and \(\operatorname {projPGL}\) is a group homomorphism.
The unipotent subgroup is the image of the unipotent homomorphism:
It consists of all elements of the form \(\begin{pmatrix} 1 & x \\ 0 & 1 \end{pmatrix}\) for \(x \in \mathbb {F}_q\), and is isomorphic to \((\mathbb {F}_q, +) \cong \mathbb {Z}/q\mathbb {Z}\).
For a chain complex \(C \in \operatorname {ChainComplex}_{\mathbb {F}_2}\) and indices \(i, j \in \mathbb {Z}\), the boundary map \(\partial _i : C_i \to C_{i-1}\) is defined as
This is the paper’s differential \(\partial \) accessed via the Mathlib API HomologicalComplex.d.
For a cochain complex \(C \in \operatorname {CochainComplex}_{\mathbb {F}_2}\) and indices \(i, j \in \mathbb {Z}\), the coboundary map \(\delta ^i : C^i \to C^{i+1}\) is defined as
This corresponds to the paper’s coboundary \(\delta \), accessed via HomologicalComplex.d on cochain complexes.
For \(\mathbb {F}_2\)-modules \(M\) and \(N\) and a linear map \(f : M \to _{\mathbb {F}_2} N\), the transpose (dual) of \(f\) is defined as
In the paper, the coboundary satisfies \(\delta = \partial ^\top \).
Let \(G = (V, E)\) be a simple graph and \(S \subseteq V\). For a vertex \(v \in V\), the edge boundary at \(v\) is the set of edges in the edge boundary \(\delta S\) that are incident to \(v\):
Let \(G = (V, E)\) be a simple graph, \(S \subseteq V\), \(s \in \mathbb {N}\), and \(b \in \mathbb {R}\). The set of high expansion vertices is
i.e., the vertices in \(S\) whose local boundary degree is at least \(s - b\).
For a linear map \(f : (\operatorname {Fin} n \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin} m \to \mathbb {F}_2)\) and an index \(i : \operatorname {Fin} m\), the row weight of row \(i\) of the matrix representation of \(f\) is defined as
i.e., the number of column indices \(j\) such that the \((i,j)\)-entry of the matrix is nonzero.
Let \(R\) be a commutative semiring, \(M\) an \(R\)-module, and \(\iota \) an index type. Given a submodule \(p \leq M\), there is a linear equivalence
The forward map sends \(x : \iota \to M\) (with \(x_i \in p\) for all \(i\)) to the function \(i \mapsto \langle x_i,\, x.\text{prop}\, i\rangle \), and the inverse sends \(f : \iota \to p\) to \(\langle \lambda \, i \mapsto f_i,\, \lambda \, i\, \_ \mapsto (f_i).\text{prop}\rangle \).
Let \(\Lambda \) be a labeling of \(G\) with degree \(s\) and \(c : G.\operatorname {edgeSet} \to \mathbb {F}_2\). The support degree of \(c\) at vertex \(v\) is
the number of edges in \(\operatorname {supp}(c)\) incident to \(v\).
A small double complex \(E\) over \(\mathbb {F}_2\) is a \(2 \times 2\) double complex consisting of four \(\mathbb {F}_2\)-modules \(A_{0,0}\), \(A_{0,1}\), \(A_{1,0}\), \(A_{1,1}\) together with vertical linear maps
and horizontal linear maps
satisfying the commutativity condition
This is the data of a double complex supported in bi-degrees \((p,q) \in \{ 0,1\} ^2\).
Since \(\partial ^h_0\) maps \(\operatorname {im}(\partial ^v_1)\) into \(\operatorname {im}(\partial ^v_0)\) (Lemma 149), it descends to a well-defined \(\mathbb {F}_2\)-linear map on vertical homology:
This is constructed as a quotient map \(\operatorname {mapQ}\) applied to \(\partial ^h_0\).
Since \(\partial ^h_1\) maps \(\ker (\partial ^v_1)\) into \(\ker (\partial ^v_0)\) (Lemma 151), it restricts to a well-defined \(\mathbb {F}_2\)-linear map on vertical homology:
This is constructed by codomain restriction of the domain-restricted map \(\partial ^h_1|_{\ker (\partial ^v_1)}\).
Given a small double complex \(E\), define the degree-1 total complex differential
This is the coproduct (direct sum) map \([\partial ^h_0,\, \partial ^v_0]\).
Given a small double complex \(E\), define the degree-2 total complex differential
This is the product map \(\partial ^v_1 \times \partial ^h_1\).
Since \(q \circ \iota \) vanishes on \(\operatorname {im}(\bar{\partial }^h_1)\) (Lemma 170), the map descends to
Define the inclusion \(\iota : H^v_{0,1} = \ker (\partial ^v_0) \to Z_1\) by sending \(b \mapsto (0, b)\):
This is well-defined because \(\partial _1(0,b) = \partial ^h_0(0) + \partial ^v_0(b) = 0 + 0 = 0\) for \(b \in \ker (\partial ^v_0)\).
Define the projection \(\pi : Z_1 \to H^v_{1,0}\) by composing the inclusion \(Z_1 \hookrightarrow A_{1,0} \times A_{0,1}\), the first projection \(\operatorname {fst} : A_{1,0} \times A_{0,1} \to A_{1,0}\), and the quotient map \(\pi _0 : A_{1,0} \to H^v_{1,0}\):
By Lemma 165, \(\pi \) lands in \(\ker (\bar{\partial }^h_0) = \mathcal{H}_{1,\text{fst}}\). Define the codomain-restricted map:
The vertical homology groups of \(E\) are:
Here \(H^v_{p,0}\) is the degree-0 vertical homology in column \(p\), and \(H^v_{p,1}\) is the degree-1 vertical homology in column \(p\).
A subsystem CSS code with parameters \(n, r_X, r_Z \in \mathbb {N}\) is a CSS code \(Q\) (Definition 50) together with the following data:
A logical subspace \(H_0^L \subseteq H_0\): an \(\mathbb {F}_2\)-submodule of the homology \(H_0 = \ker (H_X)/\operatorname {im}(H_Z^T)\).
A gauge subspace \(H_0^G \subseteq H_0\): an \(\mathbb {F}_2\)-submodule of the homology.
A direct sum decomposition \(H_0 = H_0^L \oplus H_0^G\): the pair \((H_0^L, H_0^G)\) satisfies \(\operatorname {IsCompl}(H_0^L, H_0^G)\), meaning \(H_0^L \cap H_0^G = 0\) and \(H_0^L + H_0^G = H_0\).
A linear equivalence \(\phi : H_0 \xrightarrow {\; \sim \; } H^0\) between the homology and cohomology, encoding the nondegenerate pairing. The cohomology splitting is induced by \(\phi \): \(H^0_L = \phi (H_0^L)\) and \(H^0_G = \phi (H_0^G)\), ensuring that \(H_0^L\) pairs nondegenerately with \(H^0_L\), \(H_0^G\) pairs nondegenerately with \(H^0_G\), and the cross-pairings vanish.
The logical cohomology projection is the \(\mathbb {F}_2\)-linear map
defined as the linear projection onto \(H^0_L\) along \(H^0_G\), using the induced cohomology direct sum decomposition \(H^0 = H^0_L \oplus H^0_G\) (via \(\operatorname {Submodule.linearProjOfIsCompl}\) and \(\operatorname {cohcompl}\)).
The X-distance \(d_X\) of a subsystem CSS code \(S\) is the minimum Hamming weight (under the identification \(\operatorname {dotProductEquiv} : (\mathbb {F}_2^n)^* \cong \mathbb {F}_2^n\)) of a representative \(\zeta \in \ker (H_Z)\) of a cohomology class \([\zeta ] \in H^0\) whose projection onto \(H^0_L\) is nonzero:
where \(\phi : \mathbb {F}_2^n \xrightarrow {\; \sim \; } (\mathbb {F}_2^n)^*\) is the dot-product equivalence, \([\zeta ] = \pi _{H^0}(\zeta )\) is the image under the cohomology quotient map, and \(\pi _L^* : H^0 \to H^0_L\) is the logical cohomology projection. By convention, \(d_X = 0\) when \(H^0_L = 0\).
The Z-distance \(d_Z\) of a subsystem CSS code \(S\) is the minimum Hamming weight of a representative \(z \in \ker (H_X)\) of a homology class \([z] \in H_0\) whose projection onto the logical subspace is nonzero:
where \(\operatorname {wt}(z) = \operatorname {hammingWeight}(z)\) denotes the Hamming weight of \(z \in \mathbb {F}_2^n\), \([z] = \pi _H(z)\) is the image under the homology quotient map, and \(\pi _L : H_0 \to H_0^L\) is the logical projection. By convention, \(d_Z = 0\) when no such class exists (i.e., \(H_0^L = 0\)).
A subsystem CSS code \(S\) is an \([\! [n,k,d]\! ]\)-code (written \(\operatorname {IsNKDCode}(k, d)\)) if
i.e., it encodes \(k\) logical qubits with overall distance \(d\).
A subsystem CSS code \(S\) is an \([\! [n,k,d_X,d_Z]\! ]\)-code (written \(\operatorname {IsNKDXZCode}(k, d_X, d_Z)\)) if
i.e., it encodes \(k\) logical qubits with X-distance \(d_X\) and Z-distance \(d_Z\) separately specified.
The number of logical qubits of a subsystem CSS code \(S\) is
i.e., the \(\mathbb {F}_2\)-dimension (finrank) of the logical subspace \(H_0^L\). In a subsystem code, only \(H_0^L\) encodes logical information, while \(H_0^G\) corresponds to gauge degrees of freedom.
The logical projection is the \(\mathbb {F}_2\)-linear map
defined as the linear projection onto \(H_0^L\) along \(H_0^G\), using the direct sum decomposition \(H_0 = H_0^L \oplus H_0^G\) (via \(\operatorname {Submodule.linearProjOfIsCompl}\)).
Let \(m \in \mathbb {N}\) and \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. The Tanner code is the submodule
where \(C_1(X) = G.\operatorname {edgeSet} \to \mathbb {F}_2\) is the space of 1-chains. A 1-chain \(c = \sum _e a_e \cdot e\) is a codeword if and only if for every vertex \(v\), the restriction of the \(a_e\) to edges incident to \(v\), read via \(\Lambda _v\), is a codeword of the local code \(L = \ker (H)\).
Let \(G\) be \(s\)-regular with \(s \geq 1\), \(|V| \geq 2\). Let \(n = |V|\), \(\gamma = |S|/n\), and \(\lambda _2 = \lambda _2(A(G))\). Then
Let \(A\) be a Hermitian matrix on \(V\) with orthonormal eigenvector basis \((v_j)_{j \in V}\) and corresponding real eigenvalues \((\lambda _j)\). For any \(x : V \to \mathbb {R}\),
Let \(C\) be a chain complex over \(\mathbb {F}_2\) with \(C_i\) and \(C_{i+1}\) finite-dimensional. Then:
Let \(C\) be a chain complex over \(\mathbb {F}_2\) with \(C_i\), \(C_{i-1}\), and \(C_{i+1}\) finite-dimensional. Then:
For \(\ell \geq 2\) and \(i \in \operatorname {Fin}(\ell )\), letting \(j = \langle (i + \ell - 1)\bmod \ell ,\, \cdot \rangle \), the set of 1-cells \(\sigma \) of \(C_\ell \) whose boundary contains \(i\) equals \(\{ i, j\} \):
Let \(\mathcal{C}\) be a classical code of length \(n\), let \(t \in \mathbb {R}\). Suppose every nonzero codeword \(v \in \mathcal{C}\) satisfies \(\operatorname {wt}(v) \geq t\), and suppose \(\mathcal{C}\) contains at least one nonzero element. Then \(d(\mathcal{C}) \geq t\).
Let \(s, \lambda _2, \alpha , \tilde{\alpha } \in \mathbb {R}\) with \(0 {\lt} s\), \(\lambda _2 {\lt} s\), \(0 {\lt} \alpha \), \(0 \leq \tilde{\alpha }\), and \(\tilde{\alpha } \leq \alpha \). Then
Let \(G\) be a finite connected \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\) and second-largest eigenvalue \(\lambda _2 {\lt} s\). Let \(E \subseteq E(G)\) be a nonempty set of edges, and set \(\tilde{\alpha } = |E|/|E(G)|\). Then
where \(\Gamma (E) = \operatorname {incidentVertices}(E)\) is the set of vertices incident to some edge in \(E\).
The premises of encodingRateCircle are satisfiable: there exist a finite group \(H\), a graph with \(H\)-action \(X\), an \(H\)-invariant cell labeling \(\Lambda \), a positive natural number \(\ell \) with an \(H\)-action on \(\operatorname {Fin}(\ell )\), a compatible cycle action, \(\ell \) odd, and \(|H|\) odd, such that \(\top \) holds.
Let \(\delta \in \mathbb {R}\) with \(0 {\lt} \delta \leq 1/2\), and \(n, k \in \mathbb {N}\) with \(0 {\lt} n\), \(0 {\lt} k\), \(k {\lt} n\). Suppose
Then there exists a classical code \(\mathcal{C}\) of length \(n\) with \(\dim (\mathcal{C}) = k\), \(d(\mathcal{C}) \geq \delta n\), and \(d(\mathcal{C}^\perp ) \geq \delta n\).
There exist \(\delta \in \mathbb {R}\) and \(n, k \in \mathbb {N}\) satisfying all premises of Lemma 445: \(0 {\lt} \delta \), \(\delta \leq 1/2\), \(0 {\lt} n\), \(0 {\lt} k\), \(k {\lt} n\), \(k + 1 {\lt} (1-h(\delta ))n\), and \(n - k + 1 {\lt} (1-h(\delta ))n\).
Let \(\delta \in \mathbb {R}\) with \(0 {\lt} \delta \leq 1/2\), and \(n, k \in \mathbb {N}\) with \(0 {\lt} n\), \(0 {\lt} k\), \(k {\lt} n\), and
Then there exists a classical code \(\mathcal{C}\) of length \(n\) with \(\dim (\mathcal{C}) = k\) and \(d(\mathcal{C}) \geq \delta n\).
Let \(\delta \in \mathbb {R}\) with \(0 {\lt} \delta \leq 1/2\), and \(n, k \in \mathbb {N}\) with \(0 {\lt} n\), \(0 {\lt} k\), \(k {\lt} n\), and
Then there exists a classical code \(\mathcal{C}\) of length \(n\) with \(\dim (\mathcal{C}) = k\) and \(d(\mathcal{C}^\perp ) \geq \delta n\).
There exist \(\delta \in \mathbb {R}\) and \(n, k \in \mathbb {N}\) satisfying all premises of Lemma 438: \(0 {\lt} \delta \), \(\delta \leq 1/2\), \(0 {\lt} n\), \(0 {\lt} k\), \(k {\lt} n\), and \(n - k + 1 {\lt} (1-h(\delta )) \cdot n\).
Let \(G\) be \(s\)-regular with labeling \(\Lambda \), and let \(S \subseteq V\), \(v \in S\). Define the set of label positions corresponding to \(S\)-neighbors:
Then
where \((\partial _e S)_v\) is the set of edges in \(\partial _e S\) incident to \(v\).
Let \(H : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be surjective, and let \(d_{L^\perp }\) be the minimum distance of the dual code \(C^\perp \). For any nonzero \(y \in \mathbb {F}_2^m\),
Let \(G\) be \(s\)-regular, \(\Lambda \) a labeling, \(\operatorname {parityCheck}\) a linear map with local code distance \(d_L {\gt} 0\), and \(c : G.\operatorname {edgeSet} \to \mathbb {F}_2\). Setting \(S = \operatorname {incidentToSupport}(G, c)\) and \(A = \operatorname {highExpansionVertices}(G, S, s, d_L - 1)\), we have
Let \(G\) be a graph with labeling \(\Lambda \) of degree \(s\), \(c : G.\operatorname {edgeSet} \to \mathbb {F}_2\), and \(S \subseteq V\) such that every edge \(e\) with \(c(e) \neq 0\) has both endpoints in \(S\). Then for every \(v \in V\),
Let \(\operatorname {parityCheck} : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be a linear map, \(d_L\) the minimum distance of \(\operatorname {ClassicalCode.ofParityCheck}(\operatorname {parityCheck})\), with \(d_L {\gt} 0\). If \(x \in \mathbb {F}_2^s\) satisfies \(x \neq 0\) and \(\operatorname {wt}(x) \leq d_L - 1\), then \(\operatorname {parityCheck}(x) \neq 0\).
Let \(G\) be an \(s\)-regular graph, \(S \subseteq V\), and \(v \in S\). Then
where \((\partial _E S)_v\) denotes the edges in the boundary of \(S\) incident to \(v\).
Let \(\psi \) be a chain automorphism of \(F\) and suppose \(\psi \) acts as the identity on homology (i.e., \(\psi .\operatorname {ActsAsIdOnHomology}\) holds). Then
where \(\alpha _0 = \psi .\alpha _0\) is the degree-\(0\) component of \(\psi \).
Let \(\varphi \) be a connection and suppose \(\varphi \) acts as the identity on homology (i.e., \(\operatorname {ActsAsIdentityOnHomology}(\partial ^B, \partial ^F, \varphi )\) holds). For any \(b_1 : \operatorname {Fin}(n_1)\) and \(b_0 : \operatorname {Fin}(m_1)\) with \(\partial ^B(\delta _{b_1})(b_0) \ne 0\),
red[UNPROVEN – sorry in Lean source]
Let \(E = \operatorname {fiberBundleSmallDC}(d_B, d_F, \varphi )\) and assume \(\varphi \) acts as identity on homology. Then:
where \(q_k : (\mathbb {F}_2^{n_k} \otimes \mathbb {F}_2^{m_2}) / \operatorname {im}(\operatorname {id} \otimes d_F) \xrightarrow {\sim } \mathbb {F}_2^{n_k} \otimes \operatorname {coker}(d_F)\) are the flatness quotient equivalences (Definition 198).
Note: This lemma is left with sorry in the formalization. The analogous result for \(\bar{d}_h^1\) is fully proved (Lemma 206); the degree-0 case requires additional diagram chasing on the quotient that remains to be completed.
Let \(d_F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\) be a linear map, let \(\psi \) be a chain automorphism of \(d_F\), and let \(\varepsilon : \mathbb {F}_2^{m_2} \to \mathbb {F}_2\) be a linear map satisfying \(\varepsilon \circ d_F = 0\). If \(\psi \) acts as the identity on the homology of \(d_F\) (i.e. \(\psi .\operatorname {ActsAsIdOnHomology}\)), then
Let \(E = \operatorname {fiberBundleSmallDC}(d_B, d_F, \varphi )\) and assume \(\varphi \) acts as identity on homology. Then:
where \(e_k : \mathbb {F}_2^{n_k} \otimes \ker (d_F) \xrightarrow {\sim } \ker (\operatorname {id}_{\mathbb {F}_2^{n_k}} \otimes d_F)\) are the flatness equivalences (Definition 197) for \(k=1,2\).
That is, \(\bar{d}_h^1\) (the restriction of \(d_h^1\) to the kernel of \(d_v^1\)) is conjugate to \(d_B \otimes \operatorname {id}_{\ker (d_F)}\) via these equivalences.
Assume:
\(\varphi \) acts as the identity on the homology of \(F\),
the augmentation induces an isomorphism \(\bar{\varepsilon } : H_0(F) = (\mathbb {F}_2^{m_2} / \operatorname {im}(d_F)) \xrightarrow {\sim } \mathbb {F}_2\),
\(H_0(B) = 0\), i.e. \(\operatorname {im}(d_B) = \mathbb {F}_2^{m_1}\) (surjectivity).
Then
Let \(V\) be an \(\mathbb {F}_2\)-module, \(n \in \mathbb {N}\), \(g : \operatorname {Fin}(n) \to \mathbb {F}_2\), and \(v \in V\). Then:
where \(e_i = \operatorname {Pi.single}\, i\, 1\).
Let \(d_B\), \(d_F\), and \(\varphi \) be given, and let \(\varepsilon \) satisfy \(\varepsilon \circ d_F = 0\), with \(\varphi \) acting as the identity on homology. For any \(x \in \mathbb {F}_2^{n_1} \otimes \mathbb {F}_2^{m_2}\),
where \(\widetilde{d}_h^0\) is the twisted horizontal differential at bidegree \((1,0)\). That is, \(\pi _*^{(1)}\) intertwines \(\widetilde{d}_h^0\) with \(d_B\).
Assume \(\operatorname {ActsAsIdentityOnHomology}(\partial ^B, \partial ^F, \varphi )\). On the \((p,0)\)-summand, \(\pi _*\) intertwines the horizontal twisted differential with the base differential:
The composition of \(\pi _*\) on the \((p,0)\)-summand with \(\operatorname {id} \otimes \partial ^F\) (the vertical differential from degree \((p,1)\)) is zero:
For any \(b : \operatorname {Fin}(\operatorname {baseSize}(n_1,m_1,p)) \to \mathbb {F}_2\) and \(f : \operatorname {Fin}(\operatorname {fiberSize}(n_2,m_2,0)) \to \mathbb {F}_2\),
Assume \(\varphi \) acts as identity on homology. Then:
i.e., the following diagram commutes:
Assume \(\varphi \) acts as identity on homology. For any \(e_i \in \mathbb {F}_2^{n_1}\) and \(f \in \mathbb {F}_2^{m_2}\):
where \(\pi : \mathbb {F}_2^{m_2} \to \mathbb {F}_2^{m_2}/\operatorname {im}(d_F)\) is the quotient map.
Assume \(\varphi \) acts as identity on homology. Then:
i.e., the following diagram commutes:
Let \(\varphi \) act as identity on homology. For any basis element \(e_i \in \mathbb {F}_2^{n_1}\) and any \(f \in \ker (d_F)\):
That is, the twisted horizontal differential \(d_h^1\) acts on \(B_1 \otimes \ker (d_F)\) as the untwisted \(d_B \otimes \operatorname {id}\).
Let \(\partial ^B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\), \(\partial ^F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), and \(\varphi \) a connection. The twisted horizontal differential commutes with the vertical differential \(\operatorname {id} \otimes \partial ^F\):
where \(\partial ^h_{\varphi ,\alpha _q}\) denotes the twisted horizontal differential using the automorphism component \(\alpha _q\) from the connection.
For any \(b : \mathbb {F}_2^{n_1}\) and \(f : V\),
Let \(R\) be a trivialization, \(e \in X_1\), \(g \in H\), and \(\tau _1, \tau _2 \in \partial e\) with \(\pi _0(\tau _1) \neq \pi _0(\tau _2)\). Then the connection is invariant under the \(H\)-action:
There exist a group \(H\), a graph with \(H\)-action \(X\), a degree \(s \in \mathbb {N}\), a cell labeling \(\Lambda : X.\operatorname {CellLabeling}(s)\), and a proof that \(\Lambda \) is \(H\)-invariant. In other words, the invariance premises are satisfiable.
Let \(X : \mathtt{GraphWithGroupAction}(H)\), and suppose every edge has at least one boundary vertex: \(\forall \, e \in X_1,\; \partial e \neq \emptyset \). Then for every edge orbit \(E \in (X/H)_1\), the quotient boundary \(\partial _{X/H}(E)\) is nonempty.
Let \(\delta \in \mathbb {R}\) with \(0 {\lt} \delta {\lt} 11/100\), and let \(n \in \mathbb {N}\) with \(n {\gt} 2/(1/2 - h(\delta ))\). Then there exists \(k \in \mathbb {N}\) such that:
The premises of the iota map are satisfiable: there exist a group \(H\), a graph with \(H\)-action \(X\), a cell labeling \(\Lambda \), a natural number \(\ell \), a group action of \(H\) on \(\operatorname {Fin}(\ell )\), invariance \(h_\Lambda \), and cycle-compatibility \(h_{\mathrm{compat}}\), such that the underlying graph has at least one vertex and one edge.
With the witness \(\mathrm{Unit}\)-action on \(\operatorname {Fin}(3)\), the cycle-compatible action condition holds for \(H = \mathrm{Unit}\) and \(\ell = 3\):
Let \(p, q\) be distinct odd primes with \(q {\gt} 2\sqrt{p}\), and let \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfy \(x^2 + y^2 + 1 = 0\). For any \(t \in \widetilde{S}_p\), the element \(\operatorname {tupleToGL}(t)\) does not lie in the center \(Z(\operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z}))\).
For distinct odd primes \(p, q\), \(x, y\) with \(x^2+y^2+1=0\), and \(t \in \widetilde{S}_p\):
Let \(G = (V, E)\) be a finite, connected simple graph with \(|V| \geq 2\). Then there exists a finset \(S \subseteq V\) with \(0 {\lt} |S|\) and \(|S| {\lt} |V|\), confirming that the hypotheses of the spectral Laplacian bound axiom are satisfiable.
Let \(G\) be a finite, connected, \(s\)-regular graph on \(|V| \geq 2\) vertices with second-largest eigenvalue \(\lambda _2\). For \(\alpha \in (0,1)\) and \(S \subseteq V\) with \(0 {\lt} |S|\) and \(|S| \leq \alpha |V|\),
Let \(\operatorname {parityCheck} : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be a linear map whose associated local code has positive distance. Then
Let \(R\) be a commutative semiring satisfying the strong rank condition, \(M\) an \(R\)-module, \(\iota \) a finite index type, and \(p \leq M\) a free finite-rank submodule. Then
Let \(G\), \(\Lambda \), and \(\operatorname {parityCheck}\) be as above. Then
Let \(c \in C(G, \Lambda , \operatorname {parityCheck})\) be a codeword, \(d_L = \operatorname {dist}(C_L)\) the local code distance, and \(v \in V\) a vertex such that \(\operatorname {localView}_\Lambda (v, c) \neq 0\). Then
Let \(G\) be a simple graph on \(V\), \(\Lambda \) a labeling of \(G\) with degree \(s\), and \(\operatorname {parityCheck} : (\mathbb {F}_2^s \to _{\mathbb {F}_2} \mathbb {F}_2^m)\) a linear map. Then
The image of \(\bar{\partial }^h_0\) in \(H^v_{0,0} = A_{0,0}/\operatorname {im}(\partial ^v_0)\) equals the image of \(\operatorname {im}(\partial ^h_0) + \operatorname {im}(\partial ^v_0)\) under the quotient map:
The map \(\partial ^h_0\) sends \(\operatorname {im}(\partial ^v_1)\) into \(\operatorname {im}(\partial ^v_0)\):
i.e., for every \(x = \partial ^v_1(z)\) in the image of \(\partial ^v_1\), we have \(\partial ^h_0(x) \in \operatorname {im}(\partial ^v_0)\).
red[UNPROVEN AXIOM]
Let \(s \geq 3\), let \(n : \mathbb {N} \to \mathbb {N}\), and let \(G_i\) be a connected \(s\)-regular simple graph on \(\operatorname {Fin}(n(i))\) for each \(i\), with \(|\operatorname {Fin}(n(i))| \geq 2\) for all \(i\). If \(n(i) \to \infty \), then
where \(\lambda _2(G_i)\) denotes the second-largest eigenvalue of the adjacency matrix of \(G_i\).
Note: This follows conceptually from alonBoppanaBound and diam_lower_bound: since \(n(i) \to \infty \), the Moore bound gives \(\operatorname {diam}(G_i) \to \infty \), so for large \(i\) the correction term \((2\sqrt{s-1} - 1)/\lfloor D_i/2 \rfloor \to 0\) and the bound approaches \(2\sqrt{s-1}\). It is stated as an axiom because connecting SimpleGraph.diam growth with Filter.liminf through logarithmic estimates requires infrastructure not directly available for SimpleGraph in Mathlib.
red[UNPROVEN AXIOM]
Let \(G\) be a finite, connected \(s\)-regular simple graph on a finite vertex type \(V\) with \(s \geq 3\) and diameter \(D = \operatorname {diam}(G) \geq 2\). Let \(\lambda _2\) denote the second-largest eigenvalue of the adjacency matrix of \(G\). Then
Note: This is stated as an axiom because the full proof (using Nilli’s edge-based Laplacian approach, constructing test vectors supported on BFS layers and bounding the Rayleigh quotient) was not completed in the formalization.
There exist a finite vertex type \(V\), a simple graph \(G\) on \(V\), and \(s \geq 3\) such that \(G\) is connected, \(s\)-regular, and \(\operatorname {diam}(G) \geq 2\). In particular, the hypotheses of alonBoppanaBound are satisfiable.
Let \(s \geq 3\), let \(n : \mathbb {N} \to \mathbb {N}\), and let \(G_i\) be a connected \(s\)-regular simple graph on \(\operatorname {Fin}(n(i))\) for each \(i\), with \(|\operatorname {Fin}(n(i))| \geq 2\) and \(n(i) \to \infty \). Suppose that there exists \(\varepsilon {\gt} 0\) such that
Then \(\varepsilon \leq s - 2\sqrt{s-1}\). In particular, any uniform spectral gap for an expander family cannot exceed \(s - 2\sqrt{s-1}\), so the Ramanujan bound \(\lambda _2 \leq 2\sqrt{s-1}\) is best possible.
Let \(G\) be a finite \(s\)-regular simple graph with \(s \geq 1\) and \(|V| \geq 2\). Let \(\lambda _2 = \lambda _2(A(G))\) be the second-largest eigenvalue of the adjacency matrix. For any nonempty proper subset \(S \subsetneq V\), set \(n = |V|\), \(\gamma = |S|/n\), and
Then the number of edges in the induced subgraph on \(S\) satisfies
red[UNPROVEN AXIOM]
Let \(G\) be an \(s\)-regular graph with \(s \geq 1\) and \(|V| \geq 2\). Suppose the largest eigenvalue \(\lambda _1\) is strictly larger than the second-largest:
If \(v : V \to \mathbb {R}\) satisfies \(A(G)\, v = s\cdot v\), then \(v\) is globally constant, i.e. there exists \(c \in \mathbb {R}\) such that \(v = c\, \mathbf{1}\).
Note: This is stated as an axiom because the required infrastructure (harmonic function theory on graphs and eigenspace dimension theory) is not currently available in Mathlib. The result combines two classical facts: (1) the discrete maximum principle shows eigenvectors for eigenvalue \(s\) are constant on connected components, and (2) a simple top eigenvalue implies the graph is connected (otherwise each component contributes an independent eigenvector, giving multiplicity \(\geq 2\)).
Let \(G\) be a \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\) and \(s \geq 1\). Let \(\lambda _2 \geq 0\) be the second-largest adjacency eigenvalue. Let \(E \subseteq \operatorname {edgeFinset}(G)\) and \(0 {\lt} \gamma {\lt} 1\). Set \(\alpha = \gamma ^2 + \tfrac {\lambda _2}{s}\, \gamma (1-\gamma )\). If
then
In other words, if \(E\) is a large fraction of edges, then \(E\) is incident to many vertices.
Let \(G\) be a \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\) and \(s \geq 1\). Let \(\lambda _2\) denote the second-largest adjacency eigenvalue of \(G\) with \(\lambda _2 \geq 0\). Let \(E \subseteq \operatorname {edgeFinset}(G)\) and \(0 {\lt} \gamma {\lt} 1\). If
then
For all \(h \in H\), \(v \in V\), \(w \in W\), the following equality holds in \(V \otimes _H W\):
In right-action notation, this is the familiar relation \([v h \otimes w] = [v \otimes h w]\).
Let \(X\) be an \(\mathbb {F}_2\)-module and let \(f, g : V \otimes _H W \to _{\mathbb {F}_2} X\) be \(\mathbb {F}_2\)-linear maps. If
then \(f = g\).
The degree-\((0,0)\) entry of the balanced product double complex equals the balanced product object at \((0,0)\):
The degree-\((1,1)\) entry of the balanced product double complex equals the balanced product object at \((1,1)\):
The composition of the Z-check map and the X-check map is zero:
This is the fundamental CSS condition ensuring that Z-stabilizers are orthogonal to X-stabilizers, making the balanced product Tanner cycle code a valid quantum CSS code.
Let \(X\) be a cell complex, \(S \subseteq X_0\), \(v \in X_0\), and \(e \in X_1\). Then
Let \(C\) be a chain complex over \(\mathbb {F}_2\), and assume \(C_i\) and \(C_{i-1}\) are finite-dimensional over \(\mathbb {F}_2\). For each \(i \in \mathbb {Z}\):
where \(Z_i(C)^{\mathrm{ann}} \subseteq \operatorname {Dual}(C_i)\) is the dual annihilator of the homological cycles \(Z_i(C) = \ker \, \partial _i\).
Let \(C\) be a chain complex over \(\mathbb {F}_2\). For each \(i \in \mathbb {Z}\), the composition of coboundary maps satisfies:
Let \(C\) be a chain complex over \(\mathbb {F}_2\). For each \(i \in \mathbb {Z}\):
where \(B_i(C)^{\mathrm{ann}} \subseteq \operatorname {Dual}(C_i)\) denotes the dual annihilator of the homological boundaries \(B_i(C) = \operatorname {im}\, \partial _{i+1}\).
Let \(C\) be a chain complex of \(\mathbb {F}_2\)-vector spaces. For every \(i \in \mathbb {Z}\),
as a composition of \(\mathbb {F}_2\)-linear maps \(C_{i+1} \to C_{i-1}\).
Let \(C\) be a chain complex over \(\mathbb {F}_2\) with \(C_i\), \(C_{i-1}\), and \(C_{i+1}\) finite-dimensional. Then:
where \(H_i(C) = Z_i(C)/B_i(C)\) is homology and \(H^i(C) = Z^i(C)/B^i(C)\) is cohomology.
Let \(C, D\) be chain complexes over \(\mathbb {F}_2\) and let \(p, q \in \mathbb {Z}\). The horizontal differential of \(C \boxtimes D\) from column \(p\) to column \(p-1\) at row \(q\) is
Let \(C, D\) be chain complexes over \(\mathbb {F}_2\) and let \(p, q \in \mathbb {Z}\). The vertical differential of \(C \boxtimes D\) at position \((p,q)\) is
Let \(G\) be a finite simple graph with decidable adjacency, \(S \subseteq V\) a finite subset, and \(e \in \operatorname {Sym2}(V)\). Then
red[UNPROVEN AXIOM]
Let \(G\) be a connected \(s\)-regular finite simple graph on vertex set \(V\) with \(|V| \geq 2\). Let \(\lambda _2 = \lambda _2(G)\) denote the second-largest adjacency eigenvalue of \(G\) (Definition 242), and let \(h(G)\) be the Cheeger constant of \(G\) (Definition 283). Then the following Cheeger inequalities hold:
The lower bound follows from the variational characterization of \(\lambda _2\) via the Courant–Fischer min-max theorem, and the upper bound follows from a sweep-cut argument applied to the second eigenvector.
Note: This is stated as an axiom because the proof requires spectral theory infrastructure (the Courant–Fischer min-max theorem and sweep-cut analysis) that is not available in Mathlib.
For any \(\mathbb {F}_2\)-linear parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), the code \(\mathcal{C} = \ker (\partial ^C)\) equals the image of the degree-\(1\) cycles of the parity check complex \(C\) under the canonical isomorphism \(\varphi : C(1) \xrightarrow {\sim } \mathbb {F}_2^n\):
where \(Z_1(C) = \ker (\partial ^C : C(1) \to C(0))\) is the submodule of \(1\)-cycles.
For any \(\mathbb {F}_2\)-linear parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), the underlying submodule of the code constructed from \(\partial ^C\) equals the kernel of \(\partial ^C\):
red[UNPROVEN AXIOM]
Let \(H\), \(X\), \(\Lambda \), \(\ell \), \(\alpha _{\mathrm{co}}\), \(\beta _{\mathrm{co}}\) be as in Theorem 668, with the additional assumption \(s \geq 1\). Let \([x] \in H^1\) be a nontrivial cohomology class with trivial vertical projection: \(p^v([x]) = 0\) (i.e. \([x]\) is purely horizontal).
Then
Note: This is stated as an axiom because the full proof was not completed in the formalization. It is the cohomological dual of Theorem 659, with the coboundary expansion applied fiber-by-fiber along the \(\ell \) edges of \(C_\ell \).
red[UNPROVEN AXIOM]
The hypotheses of Theorem 669 are jointly satisfiable. That is, there exist a finite group \(H\), a graph \(X\) with \(H\)-action, integers \(s \geq 1\) and \(\ell \geq 3\) odd, a cell labeling \(\Lambda \), cycle-compatible \(H\)-action on \(\operatorname {Fin}(\ell )\), invariant labeling, odd \(|H|\), parameters \(\alpha _{\mathrm{co}}, \beta _{\mathrm{co}} {\gt} 0\) with the coboundary \(\delta \) being \((\alpha _{\mathrm{co}}, \beta _{\mathrm{co}})\)-expanding, and a nonzero cohomology class \(x \in H^1\) with \(p^v(x) = 0\) (purely horizontal), such that
Note: This axiom serves as a satisfiability witness confirming the premises of the horizontal cohomological distance bound are consistent, including the requirement \(s \geq 1\) needed for the \(\frac{1}{4s}\) factors.
red[UNPROVEN AXIOM]
Let \(H\) be a finite group, \(X\) a graph with \(H\)-action, \(\Lambda \) a cell labeling with \(s\) labels, \(\ell \geq 3\) an odd integer with \(H \curvearrowright \operatorname {Fin}(\ell )\), \(\Lambda \) invariant, the action cycle-compatible, and \(|H|\) odd. Let \(\alpha _{\mathrm{co}}, \beta _{\mathrm{co}} \in \mathbb {R}\) be such that the coboundary map \(\delta = \partial ^T\) is \((\alpha _{\mathrm{co}}, \beta _{\mathrm{co}})\)-expanding. Let \([x] \in H^1\) be a nontrivial cohomology class (i.e. \(x \neq 0\)) with nontrivial vertical cohomological projection: \(p^v([x]) \neq 0\).
Then the minimum Hamming weight of a cycle representative satisfies
Note: This is stated as an axiom because the full proof was not completed in the formalization. It is the cohomological dual of Theorem 660, obtained by transposing the roles of boundary and coboundary. The factor \(|X_0| \cdot s\) arises because the domain of \(\delta \) is \(C_0(X,\Lambda ) \cong \mathbb {F}_2^{X_0 \times [s]}\).
red[UNPROVEN AXIOM]
The hypotheses of Theorem 668 are jointly satisfiable. That is, there exist a finite group \(H\), a graph \(X\) with \(H\)-action, a cell labeling \(\Lambda \) with \(s\) labels, an odd \(\ell \geq 3\) with cycle-compatible \(H\)-action on \(\operatorname {Fin}(\ell )\), invariant labeling, odd \(|H|\), parameters \(\alpha _{\mathrm{co}}, \beta _{\mathrm{co}} {\gt} 0\) with the coboundary \(\delta \) being \((\alpha _{\mathrm{co}}, \beta _{\mathrm{co}})\)-expanding, and a nonzero cohomology class \(x \in H^1\) with \(p^v(x) \neq 0\), such that
Note: This axiom serves as a satisfiability witness confirming the premises of the vertical cohomological distance bound are consistent.
For \(\ell \geq 2\), the cell complex differential \(\partial _1^{\mathrm{cell}} : \mathbb {F}_2^{C_1} \to \mathbb {F}_2^{C_0}\) of \(C_\ell \) (as defined in Definition 81) equals the algebraic map \(\partial _1\) of Definition 86:
There exists an explicit construction of an infinite family of \([[N, K, D]]\) LDPC quantum CSS codes such that:
(LDPC existence) For each valid prime \(vp\), there exists an LDPC CSS code of block length \(N = \operatorname {balancedCodeLength}(vp)\) with parity check matrices of bounded weight.
(Infinitely many) For every \(M \in \mathbb {N}\), there exists a valid prime \(vp\) with \(\operatorname {balancedCodeLength}(vp) {\gt} M\).
(\(K \in \Theta (N^{4/5})\)) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(vp\),
\[ c \cdot q^4 \; \leq \; K \; \leq \; C \cdot q^4, \]where \(K\) is the logical qubit count of the balanced code and \(N \in \Theta (q^5)\) gives \(q \in \Theta (N^{1/5})\).
(\(D \in \Omega (N^{3/5})\)) There exists a constant \(c {\gt} 0\) such that for every valid prime \(vp\),
\[ c \cdot q^3 \; \leq \; \min (D_X, D_Z), \]so \(D = \min (D_X, D_Z) \in \Omega (q^3) = \Omega (N^{3/5})\).
(\(N \in \Theta (q^5)\)) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(vp\),
\[ c \cdot q^5 \; \leq \; N \; \leq \; C \cdot q^5. \]
red[UNPROVEN AXIOM]
For every valid prime \(vp\), there exists a balanced code datum \(\operatorname {BalancedCodeData}(vp)\).
That is, given the subsystem CSS code from Theorem 15 (with parameters \([[N_0, K_0, D_{X,0}, D_{Z,0}]]\)) and the Gilbert–Varshamov classical code of length \(n_c = q^2\) (Theorem 10), the Evra–Kaufman–Zemor distance balancing procedure (EKZ22, Theorem 1) produces a (non-subsystem) CSS code with:
Block length \(N = N_0 \cdot n_c\),
Logical qubits \(K \geq K_0 \cdot k_c\) where \(k_c \geq n_c/2\),
X-distance \(D_X \geq D_{X,0} \cdot d_c\) where \(d_c \geq n_c/10\),
Z-distance \(D_Z \geq D_{Z,0}\),
LDPC property preserved (row and column weights bounded by a constant).
Note: This is stated as an axiom because the full proof was not completed in the formalization. The EKZ result is from: Evra, Kaufman, Zemor, “Decodable quantum LDPC codes beyond the \(\sqrt{n}\) distance barrier using high-dimensional expanders”, FOCS 2022.
Let \(E : \operatorname {DoubleComplex}_{\mathbb {F}_2}\). For all \(p, q \in \mathbb {Z}\), the anticommutativity condition holds:
That is, over \(\mathbb {F}_2\), anticommutativity and commutativity of the differentials coincide, since \(-1 = 1\) in characteristic \(2\).
Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces. For all integers \(n, m, k\), the composition of consecutive differentials of \(\operatorname {Tot}(E)\) vanishes:
Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces, let \(A\) be an \(\mathbb {F}_2\)-module, and let \(n \in \mathbb {Z}\). Suppose \(f, g \colon \operatorname {Tot}(E)_n \to A\) are two morphisms such that for all integers \(p, q\) with \(p + q = n\),
Then \(f = g\).
Let \(E\) be a double complex of \(\mathbb {F}_2\)-vector spaces. For each integer \(n\), the \(n\)-th object of the total complex equals the coproduct
where \(E^{\mathrm{gr}}\) denotes the underlying graded object of \(E\) and the superscript denotes the graded-object mapping along the complex-shape projection \(\pi \colon \mathbb {Z} \times \mathbb {Z} \to \mathbb {Z}\), \((p,q) \mapsto p+q\).
Let \(G\) be a finite connected \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\) and second-largest eigenvalue \(\lambda _2 {\lt} s\). Let \(0 {\lt} \alpha \leq 1\) and let \(E \subseteq E(G)\) be a set of edges with \(|E| \leq \alpha \, |E(G)|\). Then
where \(\beta (s, \lambda _2, \alpha ) = \dfrac {\sqrt{\lambda _2^2 + 4s(s-\lambda _2)\alpha } - \lambda _2}{s(s-\lambda _2)\alpha }\).
Let \(H\) be a finite group with \(\operatorname {DecidableEq}\) instance, let \(X\) be a graph with \(H\)-action, let \(\Lambda \) be an \(H\)-invariant cell labeling of \(X\) of width \(s\), let \(\ell \in \mathbb {N}\) with \(\ell \neq 0\) and \(H \curvearrowright \operatorname {Fin}(\ell )\). Assume \(\ell \) is odd (i.e., \(\ell \equiv 1 \pmod{2}\)) and \(|H|\) is odd. Then the horizontal homology of the balanced product Tanner cycle code has the same \(\mathbb {F}_2\)-dimension as the quotient Tanner code homology:
red[UNPROVEN AXIOM]
Let \(n, r \in \mathbb {N}\) with \(0 {\lt} r \leq n\), and let \(t \in \mathbb {R}\). Suppose
Then there exists a linear map \(\phi : \mathbb {F}_2^n \to \mathbb {F}_2^r\) such that for every nonzero \(v \in \mathbb {F}_2^n\) with \(\operatorname {wt}(v) {\lt} t\), we have \(\phi (v) \neq 0\).
Note: This is stated as an axiom because the full probabilistic counting argument was not completed in the formalization. The argument follows the probabilistic method: a uniformly random linear map avoids each bad vector \(v\) with probability \(1 - 2^{-r}\), and a union bound over the \(|\operatorname {Ball}(n,t-1)|\) bad vectors yields existence of a good map when the ball is smaller than \(2^r\).
red[UNPROVEN AXIOM]
Let \(n, r \in \mathbb {N}\) with \(0 {\lt} r \leq n\), and let \(t \in \mathbb {R}\). Suppose
Then there exists a surjective linear map \(\phi : \mathbb {F}_2^n \to \mathbb {F}_2^r\) such that:
For every nonzero \(v \in \mathbb {F}_2^n\) with \(\operatorname {wt}(v) {\lt} t\), we have \(\phi (v) \neq 0\).
For every \(w \in (\ker \phi )^\perp \) with \(w \neq 0\), we have \(\operatorname {wt}(w) \geq t\).
Note: This extends exists_good_map by simultaneously bounding both the distance and the dual-distance conditions via a union bound: the probability of a bad distance event plus the probability of a bad dual-distance event is less than \(1\), and any map satisfying the dual condition is automatically surjective (otherwise some nonzero \(y\) has \(\phi ^\top (y) = 0\), which has weight \(0 {\lt} t\)).
Let \(G\) be a connected \(s\)-regular simple graph on a finite vertex set \(V\) with \(|V| \geq 2\) and \(s \geq 1\). Let \(\lambda _2 = \lambda _2(G)\) be its second largest eigenvalue. Let \(H : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be a surjective linear parity-check map, and let \(\Lambda \) be a labeling of \(G\). Write \(k_L + m = s\) (so \(k_L\) is the dimension of the local code \(\ker (H)\)).
Let \(d_{L^\perp } \geq 2\) be the minimum distance of the dual local code \(C^\perp \), with \(d_{L^\perp } \leq s\). Let \(\alpha {\gt} 0\) with \(\alpha m {\lt} 1\). Define \(b = d_{L^\perp } - 1 {\gt} 0\).
For any \(y : V \to \mathbb {F}_2^m\) with
setting
we have
Let \(G\) be a connected \(s\)-regular graph on \(|V| \geq 2\) vertices with second-largest eigenvalue \(\lambda _2 {\lt} s\). Let \(\operatorname {parityCheck} : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be a linear map, \(\Lambda \) a labeling of \(G\), and \(d_L\) the minimum distance of the local code, with \(0 {\lt} d_L \leq s\). For \(\alpha \in (0, 1]\) and \(x : G.\operatorname {edgeSet} \to \mathbb {F}_2\) satisfying
we have
where
red[UNPROVEN AXIOM]
For every valid prime \(q\), the balanced product \(C(X, L) \otimes _{\mathbb {Z}_q} C(C_q)\) yields a subsystem CSS code of length \(N = \operatorname {codeLength}(q)\), with the horizontal/vertical homology splitting providing the logical/gauge decomposition.
Note: This is stated as an axiom citing Panteleev–Kalachev [ , Def. 26 and Def. 29. The full formalization of the balanced product construction was not completed.
red[UNPROVEN AXIOM]
For every valid prime \(q\), the parity check matrices of the balanced product code have bounded weight:
Note: This is stated as an axiom citing Panteleev–Kalachev [ , §4.3, Step 8. The bound \(2s = 804\) follows from the Kronecker product structure.
orange[Uses unproven axioms: thm:ExplicitFamilyQuantumCodes.balanced_product_code, thm:ExplicitFamilyQuantumCodes.balanced_product_ldpc, thm:ExplicitFamilyQuantumCodes.infinitelyManyValidPrimes, thm:ExplicitFamilyQuantumCodes.lps_K_lower_bound, thm:ExplicitFamilyQuantumCodes.lps_K_upper_bound, thm:ExplicitFamilyQuantumCodes.lps_DZ_lower_bound, thm:ExplicitFamilyQuantumCodes.lps_DX_lower_bound]
There exists an explicit construction of an infinite family of \([\! [N, K, D_X, D_Z]\! ]\) LDPC subsystem CSS quantum codes satisfying the following simultaneously:
(Code existence) For each valid prime \(q\), there exist row counts \(r_X, r_Z \in \mathbb {N}\) and a subsystem CSS code of length \(N = 3 \cdot 201 \cdot q(q^2-1)\) whose parity check matrices \(H_X\) and \(H_{ZT}\) both have bounded weight \(\leq 804\).
(Infinite family) For any \(M \in \mathbb {N}\), there exists a valid prime \(q\) with \(N {\gt} M\).
(Logical qubit count) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(q\),
\[ c(q^2 - 1) \leq K \leq C(q^2 - 1), \]i.e., \(K \in \Theta (q^2) = \Theta (N^{2/3})\).
(X-distance) There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\),
\[ D_X \geq c \cdot q = \Omega (N^{1/3}). \](Z-distance) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(q\),
\[ c \cdot N \leq D_Z \leq C \cdot N, \]i.e., \(D_Z \in \Theta (N)\).
red[UNPROVEN AXIOM]
For any \(M \in \mathbb {N}\), there exists a valid prime \(q {\gt} M\).
Note: This is stated as an axiom appealing to Dirichlet’s theorem on primes in arithmetic progressions (Dirichlet 1837) and quadratic reciprocity for the Legendre symbol condition. The required Dirichlet theorem infrastructure was not formalized from scratch.
red[UNPROVEN AXIOM]
There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(D_X = D.\operatorname {code}.\operatorname {dX}\) is the \(X\)-distance of the subsystem code.
Note: This is stated as an axiom citing Panteleev–Kalachev [ , Theorem 14 (cohomological distance bound). Using \(|X_0|s = 2|X_1| \in \Theta (q^3)\) and \(\ell = q\), the minimum over horizontal and vertical contributions is \(\Theta (q)\). Expansion parameters \(\alpha _{co} = 10^{-5}\) and \(\beta _{co} {\gt} 0\) come from Theorem 9.
red[UNPROVEN AXIOM]
There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(D_Z = D.\operatorname {code}.\operatorname {dZ}\) is the \(Z\)-distance of the subsystem code.
Note: This is stated as an axiom citing Panteleev–Kalachev [ , Theorem 13 (homological distance bound). Since \(|X_1| = 201 \cdot q(q^2-1)\), the bound gives \(D_Z \geq c \cdot q(q^2-1)\) for a constant \(c {\gt} 0\) determined by the expansion parameters \(\alpha _{ho} = 10^{-3}\) and \(\beta _{ho} {\gt} 0\) from Theorem 8.
red[UNPROVEN AXIOM]
There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(K = \operatorname {logicalQubits}(D.\operatorname {code})\) is the number of logical qubits.
Note: This is stated as an axiom citing Sipser–Spielman 1996 (Theorem 7 in this work). Since \(k_L {\gt} s/2 = 201\) and \(|X_1|/\ell = 201(q^2-1)\), one obtains \(K \geq c(q^2-1)\) for a constant \(c {\gt} 0\).
red[UNPROVEN AXIOM]
There exists a constant \(C {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(K = \operatorname {logicalQubits}(D.\operatorname {code})\).
Note: This is stated as an axiom appealing to the Rank–Nullity Theorem (Axler, Linear Algebra Done Right, Thm. 3.22). The total chain module \(\operatorname {Tot}_1\) of the balanced product has dimension \(\in \Theta (q^3)\), giving \(K = \dim (H_1) \leq \dim (\operatorname {Tot}_1) \in O(q^2)\) after dividing by \(\ell = q\).
Let \(d_B\), \(d_F\), \(\varphi \) be as above with \(\varphi \) acting as identity on homology. Then:
i.e., \((\mathbb {F}_2^{m_1}/\operatorname {im}(d_B)) \otimes _{\mathbb {F}_2} (\mathbb {F}_2^{m_2}/\operatorname {im}(d_F))\).
Let \(d_B\), \(d_F\), \(\varphi \) be as above with \(\varphi \) acting as identity on homology. Then:
Let \(d_B : \mathbb {F}_2^{n_1} \to \mathbb {F}_2^{m_1}\), \(d_F : \mathbb {F}_2^{n_2} \to \mathbb {F}_2^{m_2}\), and let \(\varphi \) be a connection that acts as identity on homology. Then:
Under the following three hypotheses:
the connection \(\varphi \) acts as the identity on the homology of \(F\),
\(\bar{\varepsilon } : H_0(F) \xrightarrow {\sim } \mathbb {F}_2\) (the augmentation \(\varepsilon \) induces an isomorphism on \(H_0(F)\)),
\(\operatorname {im}(d_B) = \top \) (surjectivity of \(d_B\), equivalently \(H_0(B) = 0\)),
and assuming \(\varepsilon \) itself is surjective, the map
is a bijection (hence a linear isomorphism, since it is a linear map between finite-dimensional \(\mathbb {F}_2\)-vector spaces of equal dimension).
Let \(\delta \in \mathbb {R}\) with \(0 {\lt} \delta {\lt} 11/100\), and let \(n \in \mathbb {N}\) with \(0 {\lt} n\) and
Then there exists a classical code \(\mathcal{C}\) of length \(n\) such that:
\(\dim (\mathcal{C}) {\gt} n/2\),
\(d(\mathcal{C}) \geq \delta n\),
\(d(\mathcal{C}^\perp ) \geq \delta n\).
Let \(G\) be a simple graph on a finite vertex type \(V\) with decidable adjacency. The map \(\operatorname {adjEigenvalues}(G) : \operatorname {Fin}(|V|) \to \mathbb {R}\) is antitone: for all \(i \leq j\),
Let \(R\) be a trivialization of \(X\), let \(e \in X_1\), and let \(\tau _1, \tau _2 \in \partial e\) with \(\pi _0(\tau _1) \neq \pi _0(\tau _2)\). Then there exists an edge \(e' \in X_1\) such that:
\(\pi _1(e') = \pi _1(e)\) (i.e., \(e'\) is in the same orbit as \(e\)),
\(R(\pi _0(\tau _1)) \in \partial e'\),
\(\phi _R(e;\tau _1,\tau _2) \cdot R(\pi _0(\tau _2)) \in \partial e'\).
Let \(\Lambda \) be an \(H\)-invariant labeling. For any vertex \(v \in X_0\), edge \(e \in X_1\) with \(v \in \partial e\), and \(h \in H\) (so that \(h \cdot v \in \partial (h \cdot e)\)), the labeling value is independent of the representative:
For all \(p, q \in \mathbb {Z}\), the horizontal differential of the balanced product double complex satisfies
i.e., it is induced by \(\partial ^C_{p \to p-1} \otimes \operatorname {id}_{D_q}\).
For all \(p, q \in \mathbb {Z}\), the vertical differential of the balanced product double complex satisfies
i.e., it is induced by \(\operatorname {id}_{C_p} \otimes \partial ^D_{q \to q-1}\).
red[UNPROVEN AXIOM]
Let \(H\) be a finite group of odd order, and let \(C\), \(D\) be \(H\)-equivariant chain complexes over \(\mathbb {F}_2\). Then for every \(n \in \mathbb {Z}\) there is a linear isomorphism
Note: This is stated as an axiom because the full proof requires infrastructure not available in Mathlib: specifically, (1) identifying the balanced product complex \(C \otimes _H D\) (from \(\operatorname {balancedProductComplex}\), Def. 23) with the coinvariants of the tensor product complex \((C \otimes D)_H\) at the chain complex level; (2) showing that over \(\mathbb {F}_2\) with \(|H|\) odd the coinvariants functor \((-)_H\) is exact (so it commutes with homology); and (3) combining with the ordinary Künneth formula (Thm. 1) and the fact that \((-)_H\) commutes with finite direct sums. The proof sketch is: \(H_n(C \otimes _H D) \cong H_n((C \otimes D)_H) \cong (H_n(C \otimes D))_H \cong \bigoplus _{p+q=n}(H_p(C) \otimes H_q(D))_H = \bigoplus _{p+q=n} H_p(C) \otimes _H H_q(D)\).
red[UNPROVEN AXIOM]
Let \(H\) be a finite group, \(X\) a graph with \(H\)-action, \(\Lambda \) a cell labeling, \(\ell \geq 1\) an integer, \(\mu _H\) an \(H\)-action on \(\operatorname {Fin}(\ell )\), with \(\Lambda \) invariant and the cycle-compatible action condition satisfied, and \(|H|\) odd. There exists a function
assigning to each homology class \([x] \in H_1\) the minimum Hamming weight \(|u| + |v|\) over all cycle representatives \(x = (u, v) \in \operatorname {Tot}_1 = E_{1,0} \oplus E_{0,1}\) of that class, where the basis is the coinvariant basis of the balanced product modules.
Note: This is stated as an axiom because the full proof—constructing the coinvariant basis and transporting Hamming weight through balanced product quotients—requires infrastructure beyond Mathlib’s current scope. See van Lint, Introduction to Coding Theory, Ch. 1; MacWilliams–Sloane, The Theory of Error-Correcting Codes, §1.1; and Panteleev–Kalachev [PK22].
red[UNPROVEN AXIOM]
Under the same hypotheses, for any \(x \in H_1\) with \(x \neq 0\), we have \(\operatorname {cycleRepWeight}(x) {\gt} 0\). If \(x \neq 0\), then at least one coordinate is nonzero, so \(\operatorname {wt}(x) \geq 1 {\gt} 0\).
Note: This is stated as an axiom because it depends on the coinvariant basis infrastructure axiomatized in \(\operatorname {cycleRepWeight}\).
red[UNPROVEN AXIOM]
Under the same hypotheses, \(\operatorname {cycleRepWeight}(0) = 0\). The zero vector has no nonzero coordinates, so its Hamming weight is zero.
Note: This is stated as an axiom because it depends on the coinvariant basis infrastructure axiomatized in \(\operatorname {cycleRepWeight}\).
red[UNPROVEN AXIOM]
Let \(H\) be a finite group of odd order, \(X\) a graph with \(H\)-action, \(\Lambda \) an \(H\)-invariant cell labeling, \(\ell \geq 3\) an odd integer with \(H\) acting on \(\operatorname {Fin}(\ell )\) compatibly, and suppose the Tanner differential \(\partial : C_1(X, \Lambda ) \to C_0(X, \Lambda )\) is \((\alpha _{\mathrm{ho}}, \beta _{\mathrm{ho}})\)-expanding. If \(x \in H_1\) is a nonzero homology class with nontrivial horizontal projection \(p^h([x]) \neq 0\), then the minimum Hamming weight of a cycle representative satisfies:
Note: This is Theorem 5, Case 1 of Panteleev–Kalachev [PK22]. The proof proceeds by case analysis on \(|u|\) relative to \(\alpha _{\mathrm{ho}}|X_1|/2\): if \(|u| \geq \alpha _{\mathrm{ho}}|X_1|/2\) the bound follows directly; if \(|u| {\lt} \alpha _{\mathrm{ho}}|X_1|/2\) the expansion of \(\partial \) applied fiber-by-fiber gives \(|\partial u_{\mathrm{fiber}}| \geq \beta _{\mathrm{ho}}|u_{\mathrm{fiber}}|\), and the cycle condition \(\partial ^h u + \partial ^v v = 0\) forces \(|v| \geq \beta _{\mathrm{ho}}|u|/s\). It is axiomatized because the coinvariant basis and fiber decomposition infrastructure is beyond Mathlib’s current scope.
red[UNPROVEN AXIOM]
Under the same hypotheses as the horizontal bound (with additionally \(s \geq 1\)), if \(x \in H_1\) is a nonzero homology class with trivial horizontal projection \(p^h([x]) = 0\) (purely vertical class), then:
Note: This is Theorem 5, Case 2 of Panteleev–Kalachev [PK22]. The proof decomposes \(v\) into \(\ell \) slices along the cycle graph edges. The cycle condition forces \(\partial (v_j - v_{j+1}) = 0\), and expansion applied to consecutive differences with a pigeonhole argument over slices yields the bound. It is axiomatized for the same reasons as Case 1.
The cohomological logical submodule \(H^1_L\) and gauge submodule \(H^1_G\) are complementary:
Over \(\mathbb {F}_2\), the cohomology and homology splitting are identified via Def. 2 and Def. 27, so \(H^1_L = H_1^L\) and \(H^1_G = H_1^G\) definitionally.
Suppose \(H_0(\mathcal{C}(X,\Lambda ))\) is trivial (i.e., a subsingleton). Then the gauge submodule vanishes: \(H_1^G = \{ 0\} \).
Note: The paper derives this from the weaker condition \(H_0(\mathcal{C}(X/H,\Lambda )) = 0\) (surjectivity of the quotient differential). The present formalization uses the stronger hypothesis \(H_0(\mathcal{C}(X,\Lambda )) = 0\) because the degree-0 iota/pi maps connecting quotient \(H_0\) to equivariant \(H_0\) coinvariants are not yet formalized.
Suppose \(\ell \) is odd (\(\ell \equiv 1 \pmod{2}\)) and \(|H|\) is odd. If the kernel of the quotient Tanner differential \(\partial : C_1(X/H, \Lambda ) \to C_0(X/H, \Lambda )\) is trivial, i.e.,
then the logical submodule vanishes: \(H_1^L = \{ 0\} \).
red[UNPROVEN AXIOM]
There exists an \(\mathbb {F}_2\)-linear map
where \(H_1^h = H_1^h(X, \Lambda , \ell , h_\Lambda , h_{\mathrm{compat}})\) is the horizontal homology of the balanced product Tanner cycle code from Definition 27.
The map \(\iota \) is defined on homology classes as follows: given \([\sum _{\mathcal{E}} a_{\mathcal{E}} \mathcal{E}] \in H_1(C(X/H,L))\) (where \(\mathcal{E} = eH\) ranges over edge orbits), set
where \(y_0\) is a fixed \(0\)-cell of the cycle graph \(C_\ell \).
Well-definedness: the orbit indicator \(\sum _{e \in \mathcal{E}} \delta _e\) is \(H\)-invariant in \(C_1(X,L)\), so tensoring with \(\delta _{y_0} \in C_0(C_\ell )\) gives a well-defined element of \(C_1(X,L) \otimes _H C_0(C_\ell )\). The map sends cycles to cycles (the quotient differential is compatible with the balanced product differential) and boundaries to boundaries (well-defined on homology).
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, we have
For a horizontal class \([(\sum _e a_e\, e \otimes y_0, 0)]\) with \(a_e\) constant on orbits, \(\pi \) sends it to \([\sum _e a_e\, eH]\), and \(\iota \) lifts back to \([(\sum _e a_e \sum _{e' \in eH} e' \otimes y_0, 0)]\). Since each orbit of size \(\ell \) contributes \(\ell \) copies and \(\ell \equiv 1 \pmod{2}\), this equals the original class.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
There exists an \(\mathbb {F}_2\)-linear map
The map \(\pi \) projects from horizontal homology to quotient Tanner code homology by collapsing orbits. By the Künneth decomposition, elements of \(H_1^h = H_1(C(X,L)) \otimes _H H_0(C_\ell )\) are represented by cycles of the form \((\sum _e a_e\, e \otimes y_0, 0)\) with coefficients \(a_e\) constant on \(H\)-orbits. The map sends this class to
Well-definedness: since \(a_e\) is constant on orbits, each orbit \(\mathcal{E} = eH\) contributes \(a_{\mathcal{E}} \cdot \mathcal{E}\), and the quotient differential is compatible with the balanced product differential.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, we have
Each orbit \(\mathcal{E} = eH\) has \(|H| = \ell \) elements. Applying \(\iota \) to \([\mathcal{E}]\) gives \([\sum _{e \in \mathcal{E}} e \otimes y_0]\), and then \(\pi \) maps each \(e \otimes y_0\) back to \(\mathcal{E}\), yielding \(\ell \cdot [\mathcal{E}]\). Since \(\ell \) is odd, \(\ell \equiv 1 \pmod{2}\), so \(\ell \cdot [\mathcal{E}] = [\mathcal{E}]\) in \(\mathbb {F}_2\).
Note: This is stated as an axiom because the full proof was not completed in the formalization.
Let \(p, q\) be distinct odd primes with \((q : \mathbb {R}) {\gt} 2\sqrt{p}\), \(x,y \in \mathbb {F}_q\) satisfying \(x^2 + y^2 + 1 = 0\), and \(\operatorname {legendreSym}(q, p) = -1\). Then \(S_{p,q} \cap H = \emptyset \), i.e., no generator lies in the unipotent subgroup \(H\).
red[UNPROVEN AXIOM]
\(|S_{p,q}^{\operatorname {PGL}}| = p + 1\).
Note: The injectivity of the map \(S_p \to \operatorname {PGL}_2(q)\) (distinct tuples give distinct projective classes) requires deep number-theoretic arguments about quaternion arithmetic modulo \(q\). Together with \(|S_p| = p+1\), this gives \(|S_{p,q}^{\operatorname {PGL}}| = p+1\). This is stated as an axiom because the required infrastructure is not available in Mathlib.
red[UNPROVEN AXIOM]
The subgroup generated by \(S_{p,q}^{\operatorname {PGL}}\) equals all of \(\operatorname {PGL}_2(q)\):
Note: This deep result follows from the strong approximation theorem for quaternion algebras (Lubotzky–Phillips–Sarnak), which is far beyond current Mathlib infrastructure.
red[UNPROVEN AXIOM]
\(|S_{p,q}^{\operatorname {PSL}}| = p + 1\).
Note: As with \(\operatorname {PGL}\), the injectivity of \(S_p \to \operatorname {PSL}_2(q)\) via scaled matrices requires the same quaternion-arithmetic arguments. This is stated as an axiom.
red[UNPROVEN AXIOM]
The subgroup generated by \(S_{p,q}^{\operatorname {PSL}}\) equals all of \(\operatorname {PSL}_2(q)\):
Note: Follows from the same strong approximation theorem for quaternion algebras (Lubotzky–Phillips–Sarnak).
red[UNPROVEN AXIOM]
For any two pairs \((x_1, y_1)\) and \((x_2, y_2)\) in \(\mathbb {Z}/q\mathbb {Z}\) both satisfying \(x_i^2 + y_i^2 + 1 = 0\), the LPS graphs \(\operatorname {Cay}(\operatorname {PGL}_2(q), S_{p,q}^{\operatorname {PGL}}(x_1,y_1))\) and \(\operatorname {Cay}(\operatorname {PGL}_2(q), S_{p,q}^{\operatorname {PGL}}(x_2,y_2))\) are isomorphic as simple graphs.
Note: The proof requires constructing an explicit element of the orthogonal group of the norm form \(x^2 + y^2 + 1\) over \(\mathbb {F}_q\), conjugating one quaternion embedding to the other. This algebraic infrastructure is not available in Mathlib.
red[UNPROVEN AXIOM]
For any two pairs \((x_1, y_1)\) and \((x_2, y_2)\) in \(\mathbb {Z}/q\mathbb {Z}\) both satisfying \(x_i^2 + y_i^2 + 1 = 0\), the LPS graphs \(\operatorname {Cay}(\operatorname {PSL}_2(q), S_{p,q}^{\operatorname {PSL}}(x_1,y_1))\) and \(\operatorname {Cay}(\operatorname {PSL}_2(q), S_{p,q}^{\operatorname {PSL}}(x_2,y_2))\) are isomorphic as simple graphs.
Note: The conjugation by \(g \in \operatorname {GL}(2, \mathbb {F}_q)\) preserves \(\operatorname {SL}(2, \mathbb {F}_q)\) up to scaling, hence descends to \(\operatorname {PSL}_2(q)\). Requires the same orthogonal group infrastructure as the \(\operatorname {PGL}\) case.
red[UNPROVEN AXIOM]
For every odd prime \(p\),
Note: This follows from Jacobi’s four-square theorem: the number of representations of an odd prime \(p\) as a sum of four integer squares is \(r_4(p) = 8(p+1)\), and the normalization conditions select exactly \(p+1\) representatives. Jacobi’s four-square theorem is not available in Mathlib, so this is stated as an axiom.
blue[Hypothesis-based] The following result is proved under explicit assumptions on the Ramanujan property and a spectral bound, which are deep results requiring algebraic geometry not available in Mathlib.
Let \(p, q\) be distinct odd primes with \(q {\gt} 2\sqrt{p}\), and let \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfy \(x^2 + y^2 + 1 = 0\). Let \(G = X_{p,q}^{\operatorname {PGL}}\) be the LPS graph on \(\operatorname {PGL}(2,q)\). Suppose:
(Ramanujan hypothesis) \(G\) is a Ramanujan graph of degree \(p+1\), i.e., every eigenvalue \(\lambda _i\) with \(|\lambda _i| {\lt} p+1\) satisfies \(|\lambda _i| \leq 2\sqrt{p}\).
(Spectral bound hypothesis) \(|\lambda _2(G)| {\lt} p+1\), where \(\lambda _2\) denotes the second-largest eigenvalue.
Then
blue[Hypothesis-based] The following result is proved under explicit assumptions on the Ramanujan property and a spectral bound.
Let \(p, q\) be distinct odd primes with \(q {\gt} 2\sqrt{p}\) and \(\left(\frac{p}{q}\right) = 1\) (i.e., \(p\) is a quadratic residue mod \(q\)), and let \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfy \(x^2 + y^2 + 1 = 0\). Let \(G = X_{p,q}^{\operatorname {PSL}}\) be the LPS graph on \(\operatorname {PSL}(2,q)\). Given:
(Ramanujan hypothesis) \(G\) is Ramanujan of degree \(p+1\).
(Spectral bound hypothesis) \(|\lambda _2(G)| {\lt} p+1\).
Then
blue[Hypothesis-based] The following combined result is proved under the hypotheses of connectedness and the Ramanujan property, which are deep results from Lubotzky–Phillips–Sarnak requiring algebraic geometry not available in Mathlib.
Let \(p, q\) be distinct odd primes with \(q {\gt} 2\sqrt{p}\), and let \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfy \(x^2 + y^2 + 1 = 0\). Let \(G = X_{p,q}^{\operatorname {PGL}}\) be the LPS graph on \(\operatorname {PGL}(2,q)\). Given:
(Connectedness hypothesis) \(G\) is connected.
(Ramanujan hypothesis) \(G\) is Ramanujan of degree \(p+1\).
Then simultaneously:
\(G\) is connected,
\(G\) is \((p+1)\)-regular,
\(|\operatorname {PGL}(2,q)| \geq 2\), and
\(G\) is a Ramanujan graph of degree \(p+1\).
blue[Hypothesis-based] Let \(p, q\) be distinct odd primes with \(q {\gt} 2\sqrt{p}\) and \(\left(\frac{p}{q}\right) = 1\), and let \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfy \(x^2 + y^2 + 1 = 0\). Let \(G = X_{p,q}^{\operatorname {PSL}}\) be the LPS graph on \(\operatorname {PSL}(2,q)\). Given:
(Connectedness hypothesis) \(G\) is connected.
(Ramanujan hypothesis) \(G\) is Ramanujan of degree \(p+1\).
Then simultaneously:
\(G\) is connected,
\(G\) is \((p+1)\)-regular,
\(|\operatorname {PSL}(2,q)| \geq 2\), and
\(G\) is a Ramanujan graph of degree \(p+1\).
Let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. A 1-chain \(c \in C_1(X)\) belongs to the Tanner code if and only if for every vertex \(v \in V\),
Let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. A 1-chain \(c \in C_1(X)\) belongs to the Tanner code if and only if for every vertex \(v \in V\),
where \(\operatorname {ofParityCheck}(H)\) is the classical code (Definition 41) associated to the parity-check matrix \(H\).
Let \(G = (V, E)\) be a finite, connected, \(s\)-regular simple graph, and let \(\lambda _2\) denote its second-largest adjacency eigenvalue (well-defined since \(|V| \geq 2\)). Let \(\alpha \in (0,1)\) and let \(S \subseteq V\) with \(0 {\lt} |S|\) and \(|S| {\lt} \alpha \cdot |V|\). Then:
red[UNPROVEN AXIOM]
Let \(G = (V, E)\) be a finite, connected, \(s\)-regular simple graph with \(|V| \geq 2\), and let \(\lambda _2\) denote its second-largest adjacency eigenvalue. For any nonempty proper subset \(S \subsetneq V\) (i.e., \(0 {\lt} |S| {\lt} |V|\)), the edge boundary \(\delta S\) satisfies:
Note: This is stated as an axiom because the proof requires eigenvalue decomposition and the Courant–Fischer variational characterization of \(\lambda _2\), which are not currently available in Mathlib. The proof strategy is: (Step 1) Set \(f = \mathbf{1}_S\), decompose \(f = \bar{f}\cdot \mathbf{1} + g\) where \(\bar{f} = |S|/|V|\); (Step 2) By the spectral theorem, \(g^\top (sI - M)g \geq (s - \lambda _2)\, g^\top g\); (Step 3) Compute \(g^\top g = |S|(1 - |S|/|V|)\) and \(f^\top (sI-M)f = |\delta S|\); (Step 4) Since \((sI-M)\cdot \mathbf{1} = 0\), we have \(g^\top (sI-M)g = f^\top (sI-M)f\), completing the bound. This follows the same convention as cheegerInequalities in the Cheeger constant file.
Let \(G\) be a finite, connected, \(s\)-regular graph on vertex set \(V\) with \(|V| \geq 2\) and second-largest eigenvalue \(\lambda _2\). Let \(\alpha \in (0,1)\), \(b \in \mathbb {R}\) with \(0 {\lt} b \leq s\), and \(S \subseteq V\) with \(|S| \leq \alpha |V|\). Define
Then
Let \(G\) be a simple graph on \(V\) that is \(s\)-regular with \(s \geq 1\) and \(|V| \geq 2\). Let \(\Lambda \) be a labeling of \(G\) with degree \(s\), and let \(\operatorname {parityCheck} : \mathbb {F}_2^s \to \mathbb {F}_2^m\) be a linear map with \(k_L = \operatorname {finrank}_{\mathbb {F}_2}(\ker (\operatorname {parityCheck}))\). Then the Tanner code \(C(G, \Lambda , \operatorname {parityCheck})\) satisfies
where \(|X_1| = |E(G)|\) denotes the number of edges.
Let \(G\) be a connected \(s\)-regular simple graph on \(V\) with \(s \geq 1\) and \(|V| \geq 2\). Let \(\Lambda \) be a labeling of \(G\) with degree \(s\), \(\operatorname {parityCheck} : \mathbb {F}_2^s \to \mathbb {F}_2^m\) a linear map, \(d_L = \operatorname {dist}(C_L)\) the local code distance, and \(\lambda _2\) the second largest eigenvalue of \(G\) with \(\lambda _2 \geq 0\) and \(d_L {\gt} \lambda _2\). Then every nonzero codeword \(c \in C(G, \Lambda , \operatorname {parityCheck})\) satisfies
where \(|X_1| = |E(G)|\).
There is a canonical \(\mathbb {F}_2\)-linear isomorphism
Let \(H\) be a finite group acting on \(\mathbb {F}_\ell \) for some \(\ell \geq 3\) odd, let \(X\) be a graph with \(H\)-action, let \(\Lambda \) be an \(s\)-regular \(H\)-invariant cell labeling, and let the action be cycle-compatible. Suppose:
\(\operatorname {hdim_components}\): \(\dim _{\mathbb {F}_2}(\operatorname {Tot}_1) = |X_1| + s \cdot |X_0|\), where \(\operatorname {Tot}_1\) denotes the degree-\(1\) component of the balanced product Tanner cycle complex;
\(\operatorname {hreg}\): \(2|X_1| = s \cdot |X_0|\) (i.e. the graph \(X\) is \(s\)-regular).
Then
Let \(\alpha _{\mathrm{co}}, \beta _{\mathrm{co}} {\gt} 0\), \(s \geq 1\), and suppose the coboundary map is \((\alpha _{\mathrm{co}}, \beta _{\mathrm{co}})\)-expanding. For every nontrivial homology class \(x \in H_1 \setminus \{ 0\} \),
Using \(s\)-regularity \(s \cdot |X_0| = 2|X_1|\), this gives
Under the same hypotheses as Theorem 678, for every nontrivial homology class \(x \in H_1 \setminus \{ 0\} \),
Note: The existence of nontrivial homology classes for specific graph families (Cayley expanders) is a constructive combinatorial result from the balanced product code construction [ .
Let \(\alpha _{\mathrm{co}}, \beta _{\mathrm{co}} {\gt} 0\), \(s \geq 1\), and suppose the coboundary map is \((\alpha _{\mathrm{co}}, \beta _{\mathrm{co}})\)-expanding. For every nontrivial cohomology class \(x \in H_1 \setminus \{ 0\} \) whose vertical co-projection satisfies \(\tilde{\pi }_V(x) = 0\) (purely horizontal class),
Let \(\alpha _{\mathrm{co}}, \beta _{\mathrm{co}} {\gt} 0\) and suppose the coboundary map is \((\alpha _{\mathrm{co}}, \beta _{\mathrm{co}})\)-expanding. For every nontrivial cohomology class \(x \in H_1 \setminus \{ 0\} \) whose vertical co-projection \(\tilde{\pi }_V(x) \neq 0\),
Since \(s\)-regularity gives \(s \cdot |X_0| = 2|X_1|\), this is equivalent to
Let \(\alpha _{\mathrm{ho}}, \beta _{\mathrm{ho}} {\gt} 0\) and suppose the Tanner differential \(\partial ^{\mathrm{Tanner}}\) is \((\alpha _{\mathrm{ho}}, \beta _{\mathrm{ho}})\)-expanding. For every nontrivial homology class \(x \in H_1 \setminus \{ 0\} \) whose horizontal projection \(\pi _H(x) \neq 0\),
Let \(k_L = \dim _{\mathbb {F}_2}(\ker (\partial ^{\mathrm{quot}}))\) be the local code dimension, and let \(m = |(X/H)_1|\) be the number of edges of the quotient graph, satisfying \(m = |X_1|/\ell \) (the free action hypothesis). Assume \(s \geq 1\) and that the quotient Tanner code homology satisfies the Sipser–Spielman bound
Then
Let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. The Tanner code equals the intersection of pullbacks of the local code along all local views: