50 Thm 14: Cohomological Distance Bound
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.
Let \(H\) be a finite group and \(X\) a graph with \(H\)-action. The number of \(0\)-cells (vertices) of \(X\) is
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]
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 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.
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.