Linear-Code Constructions and Bounds

This module contains weight/projection lemmas, the singleton bound for arbitrary and linear codes, and basic constructions and dimension/rate facts for linear codes.

References

• [Guruswami, V., Rudra, A., Sudan M., Essential Coding Theory, online copy][GRS25]
• [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., All Polynomial Generators Preserve Distance with Mutual Correlated Agreement][BCGM25]

def Code.wt {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] (v : ι → F) : ℕ

theorem Code.wt_eq_hammingNorm {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] {v : ι → F} : wt v = ‖v‖₀

theorem Code.wt_eq_zero_iff {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] {v : ι → F} : wt v = 0 ↔ Fintype.card ι = 0 ∨ ∀ (i : ι), v i = 0

def projection {n : Type u_1} {R : Type u_2} (S : Finset n) (w : n → R) : ↥S → R

theorem projection_injective {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (nontriv : ‖C‖₀ ≥ 1) (S : Finset n) (hS : Fintype.card ↥S = Fintype.card n - (‖C‖₀ - 1)) (u v : n → R) (hu : u ∈ C) (hv : v ∈ C) : projection S u = projection S v → u = v

theorem singleton_bound {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [Finite R] (C : Set (n → R)) : Fintype.card ↑C ≤ Fintype.card R ^ (Fintype.card n - (‖C‖₀ - 1))

Singleton bound for arbitrary codes

@[reducible, inline]

abbrev ModuleCode (ι : Type u) (F : Type v) [Semiring F] (A : Type w) [AddCommMonoid A] [Module F A] : Type (max u w)

A ModuleCode ι F A is an F-linear code of length indexed by ι over the alphabet A, defined as an F-submodule of ι → A.

@[reducible, inline]

abbrev LinearCode (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] : Type (max u v)

theorem LinearCode_is_ModuleCode {ι : Type u} [Fintype ι] {F : Type v} [Semiring F] : LinearCode ι F = ModuleCode ι F F

noncomputable def LinearCode.disFromHammingNorm {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] [DecidableEq F] (LC : LinearCode ι F) : ℕ

The Hamming distance of a linear code can also be defined as the minimum Hamming norm of a non-zero vector in the code

theorem LinearCode.dist_eq_dist_from_HammingNorm {F : Type u_3} {ι : Type u_5} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : ‖LC.carrier‖₀ = LC.disFromHammingNorm

noncomputable def LinearCode.dim {F : Type u_3} {ι : Type u_5} [Semiring F] {A : Type u_7} [AddCommMonoid A] [Module F A] (MC : ModuleCode ι F A) : ℕ

The dimension of a linear code.

def LinearCode.length {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] {A : Type u_7} [AddCommMonoid A] [Module F A] : ModuleCode ι F A → ℕ

The length of a linear code.

noncomputable def LinearCode.rate {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] {A : Type u_7} [AddCommMonoid A] [Module F A] (MC : ModuleCode ι F A) : ℚ≥0

The rate of a linear code.

def LinearCode.termρ_ : Lean.ParserDescr

ρ LC is the rate of the linear code LC.

Uses & to make the notation non-reserved, allowing ρ to also be used as a variable name.

def LinearCode.projectedWord {F : Type u_3} {ι : Type u_5} [Fintype ι] (c : ι → F) (T : Finset ι) : ↥T → F

Let c be a word of length ι. For every finite ι-subset T , we define the projection of a word c to T as the word obtained by restricting the indexing set of c to T. We denote this by c|[T]. Definition 3.7 [BCGM25].

def LinearCode.«term_|[_]» : Lean.TrailingParserDescr

def LinearCode.projectedCode {F : Type u_3} {ι : Type u_5} [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (↥T → F)

Let C be a code of length ι. For every finite ι-subset T, we define the projected code C|[T] as the set of projected codewords c|[T], for c ∈ C. Definition 3.7 [BCGM25].

def LinearCode.«term_|[_]_1» : Lean.TrailingParserDescr

theorem LinearCode.projectedCode_linearCombination {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) (T : Finset ι) {α : Type} [Fintype α] (U : α → ι → F) (c : α → F) (hU : ∀ (j : α), U j|[T] ∈ LC.carrier|[T]) : (fun (k : ι) => ∑ j : α, c j * U j k)|[T] ∈ LC.carrier|[T]

Let T be a finite subset of ι. If every word in a collection lies in the projected code C|[T], then so do all F-linear combinations of these.

def LinearCode.IsMDS {F : Type u_3} {ι : Type} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop

A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound.

theorem LinearCode.linear_code_is_FG {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : Submodule.FG LC

Every linear code over a field F is a finitely generated F-module.

noncomputable def LinearCode.fromRowGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [Fintype κ] [Semiring F] (G : Matrix κ ι F) : LinearCode ι F

Module code defined by left multiplication by its generator matrix. For a matrix G : Matrix κ ι F (over field F) and module A over F, this generates the F-submodule of (ι → A) spanned by the rows of G acting on (κ → A). The matrix acts on vectors v : κ → A by : (G • v)(i) = ∑ k, G k i • v k where G k i : F is the scalar and v k : A is the module element.

noncomputable def LinearCode.fromColGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [Fintype κ] [CommRing F] (G : Matrix ι κ F) : LinearCode ι F

Linear code defined by right multiplication by a generator matrix.

noncomputable def LinearCode.byCheckMatrix {F : Type u_3} {ι : Type u_5} {κ : Type u_6} [Fintype κ] [CommRing F] (H : Matrix ι κ F) : LinearCode κ F

Define a linear code from its (parity) check matrix

theorem LinearCode.gen_matrix_exists {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : ∃ (G : Matrix (Fin (dim LC)) ι F), LC = fromRowGenMat G

Given a linear code of length ι and dimension dim over a field F, there exists a dim × ι matrix over F which generates the code. Theorem 2.2.7 [GRS25].

noncomputable def LinearCode.matrixFromBasis {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : Matrix (Fin (dim LC)) ι F

A matrix whose rows are a basis of a linear code over a field F.

theorem LinearCode.eq_span_rows {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : LC = Submodule.span F (Set.range LC.matrixFromBasis)

A linear code is equal to the submodule spanned by the rows of the matrix whose rows form a basis of the code.

theorem LinearCode.eq_fromRowGenMat_matrixFromBasis {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : LC = fromRowGenMat LC.matrixFromBasis

A linear code is equal to the code generated by the rows of the matrix constructed from a basis of the code. Note: eq_span_rows is good for linear-algebra-style reasoning, whereas eq_fromRowGenMat_matrixFromBasis is essentially a coding theory language restatement of it.

theorem LinearCode.rank_genMatrix_eq_dim {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : dim LC = LC.matrixFromBasis.rank

The rank of the generator matrix equals the dimension of the linear code.

theorem LinearCode.dim_fromRowGenMat {F : Type u_3} {k n : ℕ} [Field F] {G : Matrix (Fin k) (Fin n) F} : dim (fromRowGenMat G) = G.rank

The dimension of the linear code given by a generator matrix is the rank of the matrix.

noncomputable def LinearCode.genMatrixCols {F : Type u_3} {ι : Type u_5} [Fintype ι] [Field F] (LC : LinearCode ι F) : Matrix ι (Fin (dim LC)) F

Given a linear code of length ι and dimension dim over a field F, we define its ι × dim generator matrix as a matrix whose columns are an F-basis of the code.

theorem LinearCode.rank_eq_dim_fromColGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [Fintype κ] [CommRing F] {G : Matrix κ ι F} : G.rank = dim (fromColGenMat G)

The dimension of a linear code equals the rank of its associated generator matrix.

noncomputable def LinearCode.minWtCodewords {F : Type u_3} {ι : Type u_4} [Fintype ι] {A : Type u_5} [AddCommMonoid A] [DecidableEq A] [Semiring F] [Module F A] (MC : ModuleCode ι F A) : ℕ

The minimum taken over the weight of codewords in a linear code.

theorem LinearCode.hammingDist_eq_wt_sub {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [AddCommGroup F] {u v : ι → F} : Δ₀(u, v) = Code.wt (u - v)

The Hamming distance between codewords equals to the weight of their difference.

theorem LinearCode.dist_eq_minWtCodewords {F : Type u_3} {ι : Type u_4} [Fintype ι] [Ring F] {A : Type u_6} [DecidableEq A] [AddCommGroup A] [Module F A] {MC : ModuleCode ι F A} : Code.minDist ↑MC = minWtCodewords MC

The min distance of a linear code equals the minimum of the weights of non-zero codewords.

theorem LinearCode.dist_UB {F : Type u_3} {ι : Type u_4} [Fintype ι] [Ring F] {A : Type u_6} [DecidableEq A] [AddCommGroup A] [Module F A] {MC : ModuleCode ι F A} : Code.minDist ↑MC ≤ length MC

noncomputable def LinearCode.restrictLinear {F : Type u_3} {ι : Type u_4} {A : Type u_5} [AddCommMonoid A] [Semiring F] [Module F A] (S : Finset ι) : (ι → A) →ₗ[F] ↥S → A

theorem LinearCode.singletonBound {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] [StrongRankCondition F] (LC : LinearCode ι F) : dim LC ≤ length LC - Code.minDist ↑LC + 1

theorem LinearCode.singleton_bound_linear {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] [StrongRankCondition F] (LC : LinearCode ι F) : Module.finrank F ↥LC ≤ Fintype.card ι - ‖LC.carrier‖₀ + 1

Singleton bound for linear codes

def LinearCode.moduleCodeDist' {F : Type u_3} {A : Type u_4} {ι : Type u_5} [Fintype ι] [Semiring F] [Fintype A] [DecidableEq ι] [DecidableEq A] [AddCommMonoid A] [Module F A] (MC : ModuleCode ι F A) [DecidablePred fun (x : ι → A) => x ∈ MC] : ℕ∞

A computable version of the Hamming distance of a module code MC.

theorem poly_eq_zero_of_dist_lt {n k : ℕ} {F : Type u_3} [DecidableEq F] [CommRing F] [IsDomain F] {p : Polynomial F} {ωs : Fin n → F} (h_deg : p.natDegree < k) (hn : k ≤ n) (h_inj : Function.Injective ωs) (h_dist : Δ₀((fun (x : F) => Polynomial.eval x p) ∘ ωs, 0) < n - k + 1) : p = 0