Theorem 10: Gilbert–Varshamov Plus

Main Results

• gilbertVarshamovPlus: the main existence theorem

Helper lemmas for the counting argument

theorem gv_threshold_pos {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 11 / 100) : 0 < 2 / (1 / 2 - binaryEntropy δ)

theorem gv_n_large {δ : ℝ} {n : ℕ} (hδ0 : 0 < δ) (hδ1 : δ < 11 / 100) (hn : ↑n > 2 / (1 / 2 - binaryEntropy δ)) : (1 / 2 - binaryEntropy δ) * ↑n > 2

theorem gv_k_exists {δ : ℝ} {n : ℕ} (hδ0 : 0 < δ) (hδ1 : δ < 11 / 100) (hn : ↑n > 2 / (1 / 2 - binaryEntropy δ)) : ∃ (k : ℕ), ↑n / 2 < ↑k ∧ ↑k + 1 < (1 - binaryEntropy δ) * ↑n ∧ k < n

Counting argument infrastructure

def evalMap (n r : ℕ) (v : Fin n → 𝔽₂) : ((Fin n → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂

The evaluation linear map φ ↦ φ(v) from Hom(𝔽₂^n, 𝔽₂^r) to 𝔽₂^r.

Equations

• evalMap n r v = LinearMap.applyₗ v

theorem evalMap_apply {n r : ℕ} (v : Fin n → 𝔽₂) (φ : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂) : (evalMap n r v) φ = φ v

theorem evalMap_surjective {n r : ℕ} {v : Fin n → 𝔽₂} (hv : v ≠ 0) : Function.Surjective ⇑(evalMap n r v)

For nonzero v, the evaluation map is surjective.

theorem evalMap_ker_finrank {n r : ℕ} {v : Fin n → 𝔽₂} (hv : v ≠ 0) : Module.finrank 𝔽₂ ↥(evalMap n r v).ker = n * r - r

The finrank of the kernel of the evaluation map.

theorem card_ker_evalMap {n r : ℕ} {v : Fin n → 𝔽₂} (hv : v ≠ 0) [Fintype ((Fin n → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂)] : Fintype.card ↥(evalMap n r v).ker * 2 ^ r = Fintype.card ((Fin n → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂)

Cardinality of {φ | φ(v) = 0} times 2^r equals total cardinality of Hom.

axiom exists_good_map {n r : ℕ} {t : ℝ} (hr : 0 < r) (hrn : r ≤ n) (hsmall : (hammingBall n (t - 1)).card < 2 ^ r) : ∃ (φ : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂), ∀ (v : Fin n → 𝔽₂), v ≠ 0 → ↑(hammingWeight v) < t → φ v ≠ 0

When the number of nonzero vectors with Hamming weight less than d is less than 2^r, there exists a linear map φ : 𝔽₂^n → 𝔽₂^r such that φ v ≠ 0 for all nonzero v of weight < d. This is the counting/probabilistic method argument.

axiom exists_good_surjective_map {n r : ℕ} {t : ℝ} (hr : 0 < r) (hrn : r ≤ n) (hsmall_dist : (hammingBall n (t - 1)).card < 2 ^ r) (hsmall_dual : (hammingBall n (t - 1)).card < 2 ^ (n - r)) : ∃ (φ : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin r → 𝔽₂), Function.Surjective ⇑φ ∧ (∀ (v : Fin n → 𝔽₂), v ≠ 0 → ↑(hammingWeight v) < t → φ v ≠ 0) ∧ ∀ w ∈ (ClassicalCode.ofParityCheck φ).dualCode.code, w ≠ 0 → ↑(hammingWeight w) ≥ t

Combined counting argument: when both the distance and dual-distance Hamming ball bounds hold, there exists a surjective linear map φ : 𝔽₂^n → 𝔽₂^r whose kernel code has good distance AND whose dual code also has good distance. This extends exists_good_map by simultaneously bounding both bad-distance and bad-dual-distance events via a union bound: P(bad dist) + P(bad dual) < 1, and observing that any map satisfying the dual condition is automatically surjective (otherwise some nonzero y has φᵀ(y) = 0, weight 0 < t).

theorem distance_ge_of_no_lowweight {n : ℕ} (𝒞 : ClassicalCode n) {t : ℝ} (h : ∀ v ∈ 𝒞.code, v ≠ 0 → ↑(hammingWeight v) ≥ t) (hne_code : ∃ v ∈ 𝒞.code, v ≠ 0) : ↑𝒞.distance ≥ t

Distance of a code ≥ t if no nonzero codeword has weight < t and the code has a nonzero element.

theorem exists_submodule_of_finrank {n k : ℕ} (W : Submodule 𝔽₂ (Fin n → 𝔽₂)) (hk : k ≤ Module.finrank 𝔽₂ ↥W) : ∃ W' ≤ W, Module.finrank 𝔽₂ ↥W' = k

Submodule of prescribed finrank inside a larger submodule.

Existence of codes with good distance

theorem exists_code_with_good_distance {δ : ℝ} (hδ0 : 0 < δ) (hδhalf : δ ≤ 1 / 2) {n k : ℕ} (hn : 0 < n) (hk_pos : 0 < k) (hkn : k < n) (hk_bound : ↑k + 1 < (1 - binaryEntropy δ) * ↑n) : ∃ (𝒞 : ClassicalCode n), 𝒞.dimension = k ∧ ↑𝒞.distance ≥ δ * ↑n

theorem exists_code_with_good_distance_premises_satisfiable : ∃ (δ : ℝ) (n : ℕ) (k : ℕ), 0 < δ ∧ δ ≤ 1 / 2 ∧ 0 < n ∧ 0 < k ∧ k < n ∧ ↑k + 1 < (1 - binaryEntropy δ) * ↑n

theorem dualCode_dualCode_eq {n : ℕ} (𝒞 : ClassicalCode n) : 𝒞.dualCode.dualCode.code = 𝒞.code

Double dual identity for codes: (dualCode (dualCode 𝒞)).code = 𝒞.code. Over a finite-dimensional space, the double annihilator equals the original subspace.

theorem distance_dualCode_dualCode {n : ℕ} (𝒞 : ClassicalCode n) : 𝒞.dualCode.dualCode.distance = 𝒞.distance

The distance of a code equals the distance of its double dual.

theorem exists_code_with_good_dual_distance {δ : ℝ} (hδ0 : 0 < δ) (hδhalf : δ ≤ 1 / 2) {n k : ℕ} (hn : 0 < n) (hk_pos : 0 < k) (hkn : k < n) (hk_bound : ↑n - ↑k + 1 < (1 - binaryEntropy δ) * ↑n) : ∃ (𝒞 : ClassicalCode n), 𝒞.dimension = k ∧ ↑𝒞.dualCode.distance ≥ δ * ↑n

theorem exists_code_with_good_dual_distance_premises_satisfiable : ∃ (δ : ℝ) (n : ℕ) (k : ℕ), 0 < δ ∧ δ ≤ 1 / 2 ∧ 0 < n ∧ 0 < k ∧ k < n ∧ ↑n - ↑k + 1 < (1 - binaryEntropy δ) * ↑n

Binary entropy bound at 1/100

theorem key_nat_ineq_hundredth : 100 ^ 100 < 2 ^ 10 * 99 ^ 99

theorem key_frac_ineq_hundredth : 100 * (100 / 99) ^ 99 < 2 ^ 10

theorem binaryEntropy_at_one_hundredth : binaryEntropy (1 / 100) < 1 / 10

theorem binaryEntropy_at_one_hundredth_tight : binaryEntropy (1 / 100) < 499 / 1000

Combined existence and main theorem

theorem hammingBall_lt_pow {δ : ℝ} {n m : ℕ} (hδ0 : 0 < δ) (hδhalf : δ ≤ 1 / 2) (hn : 0 < n) (hHn : binaryEntropy δ * ↑n < ↑m) : ↑(hammingBall n (δ * ↑n - 1)).card < 2 ^ m

Helper for the Hamming ball bound used in both distance and dual distance arguments.

theorem exists_code_with_both_distances {δ : ℝ} (hδ0 : 0 < δ) (hδhalf : δ ≤ 1 / 2) {n k : ℕ} (hn : 0 < n) (hk_pos : 0 < k) (hkn : k < n) (hk_upper : ↑k + 1 < (1 - binaryEntropy δ) * ↑n) (hk_lower : ↑n - ↑k + 1 < (1 - binaryEntropy δ) * ↑n) : ∃ (𝒞 : ClassicalCode n), 𝒞.dimension = k ∧ ↑𝒞.distance ≥ δ * ↑n ∧ ↑𝒞.dualCode.distance ≥ δ * ↑n

theorem exists_code_with_both_distances_premises_satisfiable : ∃ (δ : ℝ) (n : ℕ) (k : ℕ), 0 < δ ∧ δ ≤ 1 / 2 ∧ 0 < n ∧ 0 < k ∧ k < n ∧ ↑k + 1 < (1 - binaryEntropy δ) * ↑n ∧ ↑n - ↑k + 1 < (1 - binaryEntropy δ) * ↑n

Main Theorem

theorem gilbertVarshamovPlus {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 11 / 100) {n : ℕ} (hn : 0 < n) (hn_large : ↑n > 2 / (1 / 2 - binaryEntropy δ)) : ∃ (𝒞 : ClassicalCode n), ↑𝒞.dimension > ↑n / 2 ∧ ↑𝒞.distance ≥ δ * ↑n ∧ ↑𝒞.dualCode.distance ≥ δ * ↑n