Theorem 13: Homological Distance Bound #
For the balanced product Tanner cycle code C(X,L) ⊗_{ℤ_ℓ} C(C_ℓ) (Def_26),
if the Tanner code boundary map ∂ : C₁(X,L) → C₀(X,L) is (α_ho, β_ho)-expanding
(Rem_3), then any nontrivial homology class [x] ∈ H₁ with cycle representative
x = (u,v) has Hamming weight |x| = |u| + |v| bounded below:
(1) If pʰ([x]) ≠ 0 (nontrivial horizontal projection):
|x| ≥ |X₁| · min(α_ho/2, α_ho·β_ho/4)
(2) If pʰ([x]) = 0 (purely vertical class):
|x| ≥ ℓ · min(α_ho/(4s), α_ho·β_ho/(4s))
This is Theorem 5 of Panteleev–Kalachev [PK22].
Main Results #
hammingWeight— Hamming weight for𝔽₂-valued functionsexpanding_ker_weight_bound— classical expander code distance bound (proved)homologicalDistanceBound_horizontal— Case 1 bound (axiom, deep PK22 result)homologicalDistanceBound_vertical— Case 2 bound (axiom, deep PK22 result)
Hamming weight for 𝔽₂-valued functions #
The Hamming weight |x| of a vector x : A → 𝔽₂ is the number of nonzero
coordinates, i.e., |{a ∈ A | x(a) ≠ 0}|. This is the standard notion used
in coding theory (Rem_3).
The Hamming weight of an 𝔽₂-valued function: the number of coordinates
where x(a) ≠ 0.
Equations
- HomologicalDistanceBound.hammingWeight x = {a : A | x a ≠ 0}.card
Instances For
Expanding matrix condition #
The (α, β)-expanding property for the Tanner differential viewed as a linear map.
A linear map f : (A → 𝔽₂) →ₗ[𝔽₂] (B → C → 𝔽₂) is (α, β)-expanding if
for any x with |x| ≤ α · |A|, we have |f(x)| ≥ β · |x|.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Classical expander code distance bound #
Any nonzero vector in the kernel of an (α, β)-expanding linear map has
Hamming weight strictly greater than α · |domain|. This is the fundamental
distance bound for expander codes (Sipser–Spielman), from which the quantum
balanced product distance bound follows via fiber-by-fiber analysis.
Classical expander distance bound. If f is (α, β)-expanding and
x ∈ ker(f) is nonzero, then the Hamming weight of x exceeds α · |A|.
Proof: If |x| ≤ α·|A|, the expansion property gives |f(x)| ≥ β·|x| > 0
(since β > 0 and |x| ≥ 1), contradicting f(x) = 0.
Balanced product complex abbreviations #
Cycle representative weight #
A nontrivial homology class [x] ∈ H₁(C(X,L) ⊗_H C(C_ℓ)) is represented by a
cycle x = (u, v) ∈ Tot₁ = E_{1,0} ⊕ E_{0,1}. The Hamming weight of the
representative is |x| = |u| + |v|, where |u| counts nonzero entries of u
in the edge basis of E_{1,0} and |v| counts nonzero entries in the vertex
basis of E_{0,1}.
Since the chain modules of the balanced product are abstract ModuleCat 𝔽₂
objects (coinvariants of tensor products), directly defining Hamming weight on
them requires building the coinvariant basis infrastructure. We axiomatize the
existence of a weight function on cycle representatives that satisfies the
standard properties of Hamming weight (cf. van Lint, Introduction to Coding
Theory, Ch. 1; MacWilliams–Sloane, The Theory of Error-Correcting Codes,
§1.1).
Hamming weight on cycle representatives (standard construction in coding
theory, cf. van Lint, Introduction to Coding Theory, Ch. 1; used as wt(·)
in Panteleev–Kalachev [PK22, §3]).
This assigns to each element of H₁ the minimum Hamming weight |u| + |v|
over all cycle representatives x = (u,v) ∈ Tot₁ of the homology class.
The Hamming weight on 𝔽₂-vector spaces with a distinguished basis is a
standard notion; here the basis is the coinvariant basis of the balanced
product modules E_{1,0} ⊕ E_{0,1}.
Hamming weight of zero is zero (standard property of Hamming weight,
cf. van Lint, Introduction to Coding Theory, Ch. 1; MacWilliams–Sloane,
The Theory of Error-Correcting Codes, §1.1). The zero vector has no nonzero
coordinates, so wt(0) = 0.
Nonzero vectors have positive Hamming weight (standard property of
Hamming weight, cf. van Lint, Introduction to Coding Theory, Ch. 1;
MacWilliams–Sloane, The Theory of Error-Correcting Codes, §1.1).
If x ≠ 0, then at least one coordinate is nonzero, so wt(x) ≥ 1.
Satisfiability of cycleRepWeight axioms #
We verify that the axiom premises are satisfiable: the type
HorizontalVerticalHomologySplitting.H1 X Λ ℓ hΛ hcompat is inhabited
(it has a zero element), so the axioms are non-vacuous.
Main Theorems #
The homological distance bound (Theorem 5 of [PK22]) derives minimum weight
bounds from the (α, β)-expanding property of the Tanner differential.
The proof involves:
- The Künneth splitting
H₁ ≅ H₁ʰ ⊕ H₁ᵛ(Def_27) - Fiber-by-fiber analysis of cycle representatives over the cycle graph
- The classical expander distance bound applied to each fiber
- Case analysis on
|u|vsα|X₁|/2
This requires infrastructure (coinvariant bases, fiber decompositions, transport of Hamming weight through balanced product quotients) that is beyond Mathlib's current scope. We axiomatize the final bound following Panteleev–Kalachev [PK22], Theorem 5.
Homological Distance Bound, Case 1 (Horizontal).
If [x] ∈ H₁ has nontrivial horizontal projection pʰ([x]) ≠ 0, and the
Tanner differential is (α_ho, β_ho)-expanding, then the minimum Hamming
weight of a cycle representative satisfies
|x| ≥ |X₁| · min(α_ho/2, α_ho·β_ho/4).
The proof (Theorem 5, Case 1 of [PK22]) proceeds by case analysis:
- If
|u| ≥ α_ho·|X₁|/2, the bound follows directly. - If
|u| < α_ho·|X₁|/2, the expansion of∂applied fiber-by-fiber gives|∂u_fiber| ≥ β_ho·|u_fiber|, and the cycle condition∂ʰu + ∂ᵛv = 0forces|v| ≥ β_ho·|u|/s. Optimizing the threshold yields the bound.
Homological Distance Bound, Case 2 (Vertical).
If [x] ∈ H₁ is nontrivial with pʰ([x]) = 0 (purely vertical), and the
Tanner differential is (α_ho, β_ho)-expanding, then
|x| ≥ ℓ · min(α_ho/(4s), α_ho·β_ho/(4s)).
The proof (Theorem 5, Case 2 of [PK22]) decomposes v into ℓ slices along
the cycle graph edges. The cycle condition forces ∂(v_j - v_{j+1}) = 0, and
expansion applied to consecutive differences with a pigeonhole argument over
slices yields the bound.
Satisfiability witnesses for axiom premises #
We verify that the expansion parameters yield nontrivial bounds.