49 Thm 13: Homological Distance Bound
Let \(A\) be a finite type with decidable equality. The Hamming weight of a vector \(x : A \to \mathbb {F}_2\) is the number of coordinates where \(x\) is nonzero:
Let \(A\) be a finite type with decidable equality. If \(x : A \to \mathbb {F}_2\) satisfies \(x \neq 0\), then \(\operatorname {wt}(x) {\gt} 0\).
We proceed by contradiction. Suppose \(\operatorname {wt}(x) = 0\), i.e., the filter set \(\{ a \in A \mid x(a) \neq 0\} \) has cardinality zero. By pushing negations and rewriting via \(\operatorname {Finset.card_pos}\), the emptiness of the filter set means that for all \(a \in A\), \(x(a) = 0\). By function extensionality, this gives \(x = 0\), contradicting \(x \neq 0\).
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). \]
Let \(f : (A \to \mathbb {F}_2) \to _{\mathbb {F}_2} (B \to C \to \mathbb {F}_2)\) be an \((\alpha , \beta )\)-expanding linear map. If \(x \neq 0\) and \(f(x) = 0\), then
We proceed by contradiction. Suppose \(\operatorname {wt}(x) \leq \alpha \cdot |A|\). From the \((\alpha , \beta )\)-expanding property (decomposing \(\operatorname {hexp}\) into its components \(0 {\lt} \alpha \), \(\alpha \leq 1\), \(0 {\lt} \beta \), and the expansion inequality), we apply the expansion to \(x\) and \(h\) to obtain:
Since \(f(x) = 0\), the output filter is empty: \(|\{ (b,c) \mid f(x)(b,c) \neq 0\} | = 0\). Indeed, for any \((b,c)\), we have \(f(x)(b,c) = (f(x))(b)(c)\), and rewriting using \(f(x) = 0\) gives \(f(x)(b)(c) = 0\). Thus after rewriting with \(\operatorname {hout}\), we obtain \(0 \geq \beta \cdot \operatorname {wt}(x)\).
We then establish that \(\operatorname {wt}(x) {\gt} 0\) as a real number: since \(\operatorname {wt}(x) = |\{ a \mid x(a) \neq 0\} |\) and the filter set is nonempty (if it were empty, every \(x(a) = 0\) and function extensionality would yield \(x = 0\), contradicting \(x \neq 0\)), we have \(\operatorname {wt}(x) \geq 1 {\gt} 0\). Together with \(\beta {\gt} 0\), this gives \(\beta \cdot \operatorname {wt}(x) {\gt} 0\), contradicting \(0 \geq \beta \cdot \operatorname {wt}(x)\) by nonlinear arithmetic.
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, \(\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]
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}\).
The type \(H_1(C(X,\Lambda ) \otimes _H C(C_\ell ))\) is inhabited: there exists an element \(x\) (namely \(x = 0\)) with \(x = x\).
We exhibit the witness \(x := 0\) and note that \(0 = 0\) holds by reflexivity.
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.
For valid expansion parameters \(0 {\lt} \alpha \leq 1\) and \(0 {\lt} \beta \):
We apply \(\min \_ le\_ of\_ left\_ le\) to reduce to showing \(\alpha /2 \leq 1\). Since \(\alpha \leq 1\), we have \(\alpha /2 \leq 1/2 \leq 1\) by linear arithmetic.
For valid expansion parameters \(0 {\lt} \alpha \leq 1\), \(0 {\lt} \beta \), and integer \(s \geq 1\):
We apply \(\min \_ le\_ of\_ left\_ le\) to reduce to \(\alpha /(4s) \leq 1\). We establish \(0 {\lt} s\) as a real number via \(\operatorname {Nat.cast_pos}\) (since \(s \geq 1\) by \(\omega \)), and \((1 : \mathbb {R}) \leq s\) via exact casting of the natural number hypothesis. Rewriting \(\alpha /(4s) \leq 1\) as \(\alpha \leq 4s\) via \(\operatorname {div_le_one}\) (using positivity of \(4s\)), the conclusion follows by linear arithmetic from \(\alpha \leq 1 \leq s\).
For valid expansion parameters \(0 {\lt} \alpha \), \(0 {\lt} \beta \), and any edge count \(n_E \geq 1\):
We apply \(\operatorname {mul_pos}\). The factor \(n_E {\gt} 0\) follows from \(\operatorname {Nat.cast_pos}\) applied to \(hn_E\). For the minimum factor, we apply \(\operatorname {lt_min}\) and use positivity to establish \(0 {\lt} \alpha /2\) and \(0 {\lt} \alpha \beta /4\) from \(\alpha {\gt} 0\) and \(\beta {\gt} 0\).
For valid expansion parameters \(0 {\lt} \alpha \), \(0 {\lt} \beta \), integer \(s \geq 1\), and cycle length \(0 {\lt} \ell \):
We apply \(\operatorname {mul_pos}\). The factor \(\ell {\gt} 0\) as a real number follows from \(\operatorname {Nat.cast_pos}\) applied to \(h\ell \). For the minimum factor, we establish \(0 {\lt} s\) as a real number via \(\operatorname {Nat.cast_pos}\) (using \(s \geq 1\) by \(\omega \)), then apply \(\operatorname {lt_min}\) and use positivity to establish \(0 {\lt} \alpha /(4s)\) and \(0 {\lt} \alpha \beta /(4s)\) from \(\alpha {\gt} 0\), \(\beta {\gt} 0\), and \(s {\gt} 0\).