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 00dbc4ec64

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)	1531

Declarations diff

+ LinearCode
+ LinearCodeWithDist
+ disjoint_spheres
+ hammingSphere
+ minDist
+ minDist_eq_sInf_pairwiseDist

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

Mathlib/InformationTheory/Coding/LinearCode.lean

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


Why Fintype instead of Finite? And why DecidableEq?

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+/-- 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 · 2026-04-13T22:36:26Z

Mathlib/InformationTheory/Coding/LinearCode.lean

+/-- 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

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+
+/-- 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?

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+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.

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+    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?

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+
+## 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}$.

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+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

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

Mathlib/InformationTheory/Coding/LinearCode.lean

+/-- 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 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


		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 00dbc4ec64

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!

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!

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!

rkirov commented Apr 14, 2026

Uh oh!

rkirov commented Apr 14, 2026

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

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