feat(InformationTheory): linear codes over finite fields and minimum distance properties by cduenasnavarro · Pull Request #38014 · leanprover-community/mathlib4

cduenasnavarro · 2026-04-13T19:05:47Z

Define linear codes over a finite field F as finite-dimensional subspaces of Fin n → F,
together with their minimum Hamming distance.

Main definitions:

LinearCode
minDist
LinearCodeWithDist
hammingSphere

Main results:

minDist_eq_sInf_pairwiseDist: characterisation of the minimum distance via pairwise distances
disjoint_spheres: Hamming spheres of radius t around distinct codewords are disjoint
if 2 * t < d

Pending:

Choosing an adequate book reference

github-actions · 2026-04-13T19:05:58Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-04-13T19:06:47Z

PR summary 2a556ee342

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.InformationTheory.Coding.LinearCode` (new file)	1532

Declarations diff

+ LinearCode
+ LinearCodeWithDist
+ Word
+ disjoint_spheres
+ exists_pair_hammingDist_eq_minDist
+ hammingSphere
+ minDist
+ minDist_eq_sInf_pairwiseDist
+ minDist_le_hammingDist

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

github-actions · 2026-04-13T19:07:19Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

https://github.com/cduenasnavarro/mathlib4 into my-feature-branch fix pr

…/mathlib4 into my-feature-branch

vihdzp

Cursory remarks, not all too familiar with the maths.

vihdzp · 2026-04-13T22:35:20Z

+
+namespace InformationTheory
+
+variable (F : Type*) [Field F] [Fintype F] [DecidableEq F]


Why Fintype instead of Finite? And why DecidableEq?

Hi! Thank you for reviewing. Feel free to correct me if I'm missing anything; I'm quite new to lean.

I used Fintype because it seems to be what is used for finite fields:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Finite/Basic.html#FiniteField
Also, Mathlib's Fintype.finite states that Fintypes are Finite:

theorem Fintype.finite{α : Type u_4} (_inst : Fintype α) : Finite α

I added DecidableEq because minDist wouldn't compile otherwise due to the requirements of hammingNorm, showing this error:
failed to synthesize instance of type class Fin n → DecidableEq F

vihdzp · 2026-04-13T22:35:44Z

+/-- An **$[n, k]_q$-linear code** is a $k$-dimensional subspace of $\mathbb{F}_q^n$. -/
+structure LinearCode (n k : ℕ) where
+  /-- The underlying $k$-dimensional subspace of $\mathbb{F}_q^n$, encoded as `Fin n → F`. -/
+  space : Subspace F (Fin n → F)


I believe we might generally use carrier for something like this?

This reminds me of Module.Grassmannian, which is defined by restricting the rank on the quotient, but there is a TODO to recover the alternative definition that restricts the rank on the space itself. Perhaps this is too far but I would like to see a unified definition of "collection of submodules of the same rank"

@vihdzp Changing space to carrier
@wwylele Thanks for reviewing! Are there any other changes I should make then for consistency, apart from carrier?

I don't have concrete suggestion as the unification with Module.Grassmannian might be controversial and beyond the scope. I think it is fine to just change it to carrier for now

vihdzp · 2026-04-13T22:36:26Z

+/-- The **minimum distance** $d(C)$ of a code $C$ is the infimum of the Hamming weights of its
+non-zero elements. -/
+noncomputable def minDist {n k : ℕ} (C : LinearCode F n k) : ℕ :=
+  sInf {w | ∃ x : Fin n → F, x ∈ C.space ∧ x ≠ 0 ∧ w = hammingNorm x}


Suggested change

sInf {w | ∃ x : Fin n → F, x ∈ C.space ∧ x ≠ 0 ∧ w = hammingNorm x}

⨅ {x : Fin n → F // x ∈ C.space ∧ x ≠ 0}, hammingNorm x.1

The right syntax would be ⨅ x : {x : Fin n → F // x ∈ C.space ∧ x ≠ 0}, hammingNorm x.1, right? But when I change it to that, I can't use ext in the lemma.

vihdzp · 2026-04-13T22:36:51Z

+
+/-- An **$[n, k, d]$-linear code** is an $[n, k]$-linear code with minimum distance at least
+`d`. -/
+structure LinearCodeWithDist (n k d : ℕ) where


Does it make sense to extend LinearCode F n k?

Okay, I've managed to make that work. It does look cleaner!

vihdzp · 2026-04-13T22:38:25Z

+omit [Fintype F] in
+/-- The minimum distance of a code coincides with the infimum of pairwise Hamming distances
+between distinct codewords. -/
+lemma minDist_eq_sInf_pairwiseDist {n k : ℕ} (C : LinearCode F n k) :


Instead of a sInf theorem, I think it might be more reasonable to split this into two: a theorem minDist F C ≤ hammingDist x y, and a theorem ∃ x ∈ C.space, ∃ y ∈ C.space, x ≠ y ∧ hammingDist x y = minDist F C.

I think this theorem is useful for comparing the pairwise minimum (it's a minimum since the set is finite) and minDist. Anyhow, I'm adding these other two results, in case they are needed.

vihdzp · 2026-04-13T22:39:49Z

+    rw [hammingDist_eq_hammingNorm x y]
+    exact hammingDist_zero_right (-x + y)
+
+/-- The **Hamming sphere** $S_t(c)$ is the set of all vectors in $\mathbb{F}_q^n$ at Hamming


This seems suggestive of some kind of metric space... would it make sense to define a type alias for Fin n → F with the Hamming distance?

So would adding this

/-- A **word** of length `n` over the field `F`: an arbitrary vector in $\mathbb{F}_q^n$, equipped with the Hamming distance. -/ abbrev Word (n : ℕ) : Type _ := Hamming (fun _ : Fin n ↦ F)

for future usage be enough?

This should just be Hamming, right?

I think you need to specify the vector space, just Hamming doesn't compile, if that's what you mean

rkirov · 2026-04-14T00:11:14Z

Happy to provide second opinion on the theory of error-correcting codes if needed (also feel free to ignore me as I am not a mathlib contributor).

In terms of the theory these are the right first steps. Only questions to consider:

should we define non-linear codes, generally not studied as much because they are harder to encode and decode, but many books define them first.
shouldn't disjoint_spheres use https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Disjoint.html#Disjoint somehow.

I assume you are working up to hamming bound, which is also the first result in the theory usually.

rkirov · 2026-04-14T00:12:24Z

oh also, c₁ ∈ C.code.space could be c₁ ∈ C.code or even c₁ ∈ C if you add the right typeclass instances, leaving to the mathlib experts to decide what is more ideomatic, but it would read better.

wwylele · 2026-04-14T01:42:10Z

+
+## Main definitions
+
+* `LinearCode`: An $[n, k]_q$-linear code, i.e., a $k$-dimensional subspace of $\mathbb{F}_q^n$.


Suggested change

* `LinearCode`: An $[n, k]_q$-linear code, i.e., a $k$-dimensional subspace of $\mathbb{F}_q^n$.

* `LinearCode`: An $[n, k]_q$-linear code, i.e., a $k$-dimensional subspace of $\mathbb{F}_{q^n}$.

I've always seen it written as (F_q)^n, it's the vector space of n elements, with the elements belonging to F_q

Oh sorry, I misread this part. I think you are right. Please ignore this

wwylele · 2026-04-14T01:44:19Z

+namespace InformationTheory
+
+variable (F : Type*) [Field F] [Fintype F] [DecidableEq F]
+variable {q : ℕ} (hq : Fintype.card F = q)


It doesn't look like q and hq are used

They are not used (for now); I added it in case it is needed in the future. In the notation I've seen, it's a explicit parameter in the definition of linear code, so I thought I would explicitly define it

wwylele · 2026-04-14T01:50:22Z

+/-- An **$[n, k]_q$-linear code** is a $k$-dimensional subspace of $\mathbb{F}_q^n$. -/
+structure LinearCode (n k : ℕ) where
+  /-- The underlying $k$-dimensional subspace of $\mathbb{F}_q^n$, encoded as `Fin n → F`. -/
+  space : Subspace F (Fin n → F)


This reminds me of Module.Grassmannian, which is defined by restricting the rank on the quotient, but there is a TODO to recover the alternative definition that restricts the rank on the space itself. Perhaps this is too far but I would like to see a unified definition of "collection of submodules of the same rank"

cduenasnavarro · 2026-04-15T21:01:50Z

@rkirov

Happy to provide second opinion on the theory of error-correcting codes if needed (also feel free to ignore me as I am not a mathlib contributor).

In terms of the theory these are the right first steps. Only questions to consider:

should we define non-linear codes, generally not studied as much because they are harder to encode and decode, but many books define them first.

shouldn't disjoint_spheres use https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Disjoint.html#Disjoint somehow.

I assume you are working up to hamming bound, which is also the first result in the theory usually.

We should probably at least define them, but I personally have not studied general codes and I don't know which results apply to the general case.
I also don't know whether they would go in the same file. If so, the file might look a bit odd if we define general codes but define and prove most things for linear code. Although I'm not very knowledgeable of mathlib's structure.
Good idea, thanks! That simplifies the theorem a bit.
That's a good goal and I'll try to continue contributing to coding theory whenever I have the time (this is quite fun), but feel free to contribute too if you want :) I'll notify in the zulip thread before I start working on anything so we don't overlap.

oh also, c₁ ∈ C.code.space could be c₁ ∈ C.code or even c₁ ∈ C if you add the right typeclass instances, leaving to the mathlib experts to decide what is more ideomatic, but it would read better.

It now looks a bit better (C.carrier) thanks to extension as @vihdzp suggested

cduenasnavarro

Mostly changes from the comments I've received so far

cduenasnavarro added 2 commits April 13, 2026 20:49

add linear codes and minimum distance results

438ae00

Merge branch 'leanprover-community:master' into my-feature-branch

9eb895d

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 13, 2026

github-actions bot added the t-measure-probability Measure theory / Probability theory label Apr 13, 2026

cduenasnavarro changed the title ~~Creation of InformationTheory/Coding/LinearCode.lean~~ feat(InformationTheory): linear codes over finite fields and minimum distance properties Apr 13, 2026

cduenasnavarro added 6 commits April 13, 2026 21:23

Update Mathlib.lean

41b6629

Merge branch 'master' into my-feature-branch

8c30780

Merge branch 'my-feature-branch' of

4cfa5d1

https://github.com/cduenasnavarro/mathlib4 into my-feature-branch fix pr

Merge branch 'master' into my-feature-branch

fd385c8

Merge branch 'my-feature-branch' of https://github.com/cduenasnavarro…

4f50895

…/mathlib4 into my-feature-branch

Merge branch 'master' into my-feature-branch

88d6625

vihdzp reviewed Apr 13, 2026

View reviewed changes

mathlib-triage bot assigned RemyDegenne Apr 14, 2026

wwylele reviewed Apr 14, 2026

View reviewed changes

cduenasnavarro added 3 commits April 15, 2026 23:28

update PR after comments

9558cfa

update PR after comments

6a64567

Merge branch 'master' into my-feature-branch

60b383f

cduenasnavarro commented Apr 15, 2026

View reviewed changes

Ruben-VandeVelde requested a review from linesthatinterlace April 15, 2026 22:01


		namespace InformationTheory

		variable (F : Type*) [Field F] [Fintype F] [DecidableEq F]

	sInf {w \| ∃ x : Fin n → F, x ∈ C.space ∧ x ≠ 0 ∧ w = hammingNorm x}
	⨅ {x : Fin n → F // x ∈ C.space ∧ x ≠ 0}, hammingNorm x.1


		## Main definitions

		* `LinearCode`: An $[n, k]_q$-linear code, i.e., a $k$-dimensional subspace of $\mathbb{F}_q^n$.

Conversation

cduenasnavarro commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 13, 2026

Welcome new contributor!

Uh oh!

github-actions bot commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2a556ee342

Import changes for modified files

Declarations diff

Uh oh!

github-actions bot commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vihdzp Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cduenasnavarro Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cduenasnavarro Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rkirov commented Apr 14, 2026

Uh oh!

rkirov commented Apr 14, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cduenasnavarro Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cduenasnavarro commented Apr 13, 2026 •

edited

Loading

github-actions bot commented Apr 13, 2026 •

edited

Loading

github-actions bot commented Apr 13, 2026 •

edited

Loading

vihdzp Apr 13, 2026 •

edited

Loading

vihdzp Apr 13, 2026 •

edited

Loading

cduenasnavarro Apr 15, 2026 •

edited

Loading

cduenasnavarro Apr 15, 2026 •

edited

Loading

wwylele Apr 15, 2026 •

edited

Loading

cduenasnavarro Apr 15, 2026 •

edited

Loading