Buiding a Coding Theory Library

Stream: new members

[Allan Li]

I am new to lean4 and am starting a project on building a coding theory library. I am having trouble on defining the distance of a code, which is $\min_{x, y\in C, x\neq y}HammingDist(x, y)$. Here is my code:

import Mathlib.Logic.Equiv.Fin
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.InformationTheory.Hamming
import Mathlib.Data.Finset.Basic
import Mathlib.Init.Set

open Set Filter Asymptotics Finset

namespace CodingTheory

variable {𝔽 : Type*} [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽]
variable {α : Type} [Fintype 𝔽] [DecidableEq α]
variable {n k : ℕ}


/-- A type that represents the set of symbols in the code -/
abbrev Alphabet := Set α


/-- An element of 𝔽ⁿ. -/
abbrev Codeword (n : ℕ) (𝔽 : Type*) [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽] := Fin n → 𝔽


/-- Code `Code n 𝔽` is a subset of 𝔽ⁿ. -/
abbrev Code (n : ℕ) (𝔽 : Type*) [Field 𝔽] [Fintype 𝔽] [DecidableEq 𝔽] := Finset (Codeword n 𝔽)


def hamming_distance (c1 c2 : Codeword n 𝔽) : ℕ :=
  hammingDist c1 c2

/-- This gives me an error. -/
def distance {n : ℕ} (C : Code n 𝔽) : ℕ :=
  Finset.min' {d : Fin n | ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ hamming_distance x y = d}

I am happy to take any comments/suggestions on the code.

[ohhaimark]

Disclaimer, I'm a mathlib noob but:
{d : Fin n | ∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ hamming_distance x y = d} is a Set, not a FinSet. I think you can use Finset.range and Finset.filter to get a finset of what you want.

Another problem is that Finset.min' takes two arguments, a finset and a proof that it is non-empty, but I think if n is 0, there is only one codeword, but you need two distinct codewords for an element of your FinSet and it can therefore be empty.

[Ruben Van de Velde]

^ I can confirm this is correct :)

[Martin Dvořák]

I don't think d : Fin n is a good idea.

[Martin Dvořák]

Not a direct answer to your question, but I think this definition might be useful:

def separated {n : ℕ} (C : Code n 𝔽) (d : ℕ) : Prop :=
  ∀ x ∈ C, ∀ y ∈ C, x ≠ y → hamming_distance x y ≥ d

[Martin Dvořák]

My last comment: I don't see what Alphabet should do in your code.

[ohhaimark]

To elaborate, perhaps unnecesarily, separated C 0 is always true since x ≥ 0 is always true and since ℕ is well founded, you can find the minimum d such that separated C d. I think that'll translate fairly straightforwardly in mathlib.

[Martin Dvořák]

The interesting question is the maximum d such that...

[ohhaimark]

Oh. I should refrain from commenting with my airheadedness

[Bolton Bailey]

If you are interested in coding theory you might be interested in talking to @Wrenna Robson

[Wrenna Robson]

Hi. @Allan Li we already have the hamming metric defined

[Wrenna Robson]

We also have a construct called infsup (I think) which is designed to be used for exactly this

[Bolton Bailey]

Yeah, I was going to say, if you want spoilers, you can see how mathlib defines the hamming distance at docs#hammingDist

[Wrenna Robson]

docs#Set.infsep

[Wrenna Robson]

However yeah I had a go at defining linear codes a year or two ago and I never really got anywhere with it. I know Dan Bernstein has done some formalisation in this area too but his work hasn't made it to Mathlib in any form.

[Wrenna Robson]

Ah I see you have already imported the hamming distance file

[Wrenna Robson]

What you want to do is define Codeword as Hamming (Fin n -> alpha)

[Wrenna Robson]

And then the hamming distance of a set of codewords is given by s.infsep

[Wrenna Robson]

(because that's the ambient metric on the space)

[Wrenna Robson]

The design intent was always to use this for codes but I never got round to putting infsep and hamming together!

[Wrenna Robson]

But yeah above people are trying to go down the path I already went down when I made infsep. You don't need to do this again!

[Wrenna Robson]

The only thing we could ARGUABLY do with is a definition of Finset.infsep but I think we decided that wasn't strictly necessary. You'd want it if you wanted a computable version I guess.

[Wrenna Robson]

What's interesting actually is that the hamming distance has a very well-behaved infsep even not on final steps because it takes integer values. I don't think we ever worked out quite how to formalise that property.

[Wrenna Robson]

By well behaved I mean "a set is non-trivial if and only if its infsep is positive" - that's true for finite sets, and we have that, but what we don't have is a notion of, I guess, a "discrete metric" (in the sense of a metric that gives rise to the discrete topology, rather than the usual sense of discrete metric).

[Wrenna Robson]

Or I guess, specifically, a metric where non-equal things have some minimum distance.

[Wrenna Robson]

So actually it's univ.infsep > 0 isn't it

[Wrenna Robson]

Which is somewhat the relatively discrete stuff in there, but it's very limited and could do with extending.

[Wrenna Robson]

Also I feel like maybe that ought to be "uniformly discrete"

[Wrenna Robson]

Based on https://en.m.wikipedia.org/wiki/Delone_set

[Wrenna Robson]

I think I got as far as suggesting that we ought to have a notion of uniformly discrete metric spaces but no further.

[Wrenna Robson]

I still think this!

[Wrenna Robson]

We should define UniformlyDiscrete and RelativelyDense as predicates on sets with a metric, and then we could also define Delone, and then we could define a UniformlyDiscrete(E)Metric as a metric for which univ is a UniformlyDiscrete set.

[Wrenna Robson]

All of which would help with coding theory but isn't directly related to it, but this was kind of what I found: you end up having to do a lot of stuff in specific that really you want to define in general and then be specific about.

[Wrenna Robson]

We might also want to define covering radius and packing radius which are related but not the same.

[Wrenna Robson]

It all needs a plan, basically, and I was only one person working on my own so it was hard to get any engagement with it.

[Wrenna Robson]

@Allan Li i would be interested to help out if and when you take this further

[Allan Li]

@Wrenna Robson I am thinking about taking this project further. I have already set up the blueprint and documentation for the project https://shilun-allan-li.github.io/tcslib/ I am thinking about following lectures notes on coding theory and implementing the blueprint of the theorems first.

[Wrenna Robson]

Sounds great.

[Wrenna Robson]

Was the above useful?

[Allan Li]

Yeah, thanks for the advice

[Wrenna Robson]

I think the definition of code there is as good as any. For what it's worth I think it might be good to have this stuff in mathlib but I guess it could be downstream.

[Allan Li]

I'm creating a new library since I'm also trying to formalize other TCS results (for example complexity theory). I'm note sure if these results would fit into mathlib

[Edward van de Meent]

i tried to replicate these definitions, while extending it to define all Codes instead of just linear codes and got a decent way, even defining the minimal distance, dimension, and rate of a code.
i'd like to also formalise the hamming bound and possibly even prove it, but i'm having a bit of trouble integrating with the Hamming distance and metric.

Wrenna Robson said:

What you want to do is define Codeword as Hamming (Fin n -> alpha)

i tried defining CodeWord the way that was suggested, but it doesn't seem to work? i don't quite get the type of Hamming either, it seems to say it needs some kind of dependent type?

this is what i tried:

import Mathlib.Data.Fintype.Basic
import Mathlib.InformationTheory.Hamming
abbrev CodeWord (ι:Type) [Fintype ι] (Ω:Type) [DecidableEq Ω] : Type := Hamming (ι → Ω)

and this is the error i got:

application type mismatch
  Hamming (ι → Ω)
argument
  ι → Ω
has type
  Type : Type 1
but is expected to have type
  ?m.1224 ι Ω → Type : Type 1

[Wrenna Robson]

Hmm, I can't quite remember how it's defined

[Wrenna Robson]

docs#Hamming

[Wrenna Robson]

Right yes I see - you're putting in the type \iota -> \omega. But actually you want something like this: const \iota \omega

[Wrenna Robson]

The other day after chatting about this I was playing around with definitions of the various delone quantities. I think I'm intending to redefine infsep to be the packing diameter at some point, and also define covering radius

[Edward van de Meent]

this seemed to work: @Hamming ι (fun x => Ω)

[Wrenna Robson]

Yes that's essentially the same

[Edward van de Meent]

sadly const doesn't seem to be a built-in

[Wrenna Robson]

Function.const maybe?

[Wrenna Robson]

Sorry I just got back from a week of house hunting, I'm pretty pooped ;_;

[Edward van de Meent]

Wrenna Robson said:

Function.const maybe?

you're right, that does work! and that way i don't need to specify the implicit context parameter too! thanks!

[Wrenna Robson]

Nw

[Wrenna Robson]

One thing I got stuck on was that not all codes use the hamming metric

[Wrenna Robson]

But I'm interested to see where you get to

[Edward van de Meent]

the plan is to define linear codes afterward, along with isomorphisms of linear codes...
speaking of, is there some reason why those are defined to conserve distance on the entire vectorspace, rather than just on the code? i couldn't figure it out, and there didn't seem to be some obvious proof that those are the same...

[Wrenna Robson]

How do you mean?

[Wrenna Robson]

Which distance?

[Wrenna Robson]

Anyway, an isometry of the space preserves distances.

[Wrenna Robson]

It would be strange to define an isometry only on a set...

[Wrenna Robson]

But of course you could define some notion of isometryOn...

[Edward van de Meent]

i see my mistake now... a key aspect of a Code is its embedding in the space of all possible codewords, since that's the space from where you want to be able to correct. i thought that it (for a linear code at least) was just some set with a notion of adding, scalar multiplying, and a notion of hamming distance on that set.

[Wrenna Robson]

Indeed, but it is not - the embedding is important

[Wrenna Robson]

It's a subset, or subspace in the case of a linear code

[Wrenna Robson]

But as I say not all codes use the hamming distance

[Wrenna Robson]

https://arxiv.org/abs/2203.12384#:~:text=The%20rank%20metric%20measures%20the,by%20a%20variety%20of%20applications.

[Wrenna Robson]

Indeed it's not even necessary in theory that they be finite

[Wrenna Robson]

At least the underlying space - I think in practice you would always want a code to be finite, and of course in any practical application infinity doesn't exist

[Edward van de Meent]

right... i'm not sure how i would have to extend the definition that i have now though... something i (or someone else) will have to figure out later

[Wrenna Robson]

Broadly speaking, a "code" can be thought of as just some set in an arbitrary type, such that the set is sufficiently separated that I can distinguish members of the code, and so that sufficiently large balls around the codewords cover the set

[Wrenna Robson]

That is, really, a delone set. Many theorems about "codes" are actually theorems in that much more general setting

[Wrenna Robson]

But yes - what you should do is continue your work and hopefully someone will generalise it later

[Wrenna Robson]

https://en.m.wikipedia.org/wiki/Hamming_bound#:~:text=In%20mathematics%20and%20computer%20science,space%20of%20all%20possible%20words.

[Wrenna Robson]

Proving the hamming bound would be a good test

[Wrenna Robson]

And then proving facts about perfect codes is the natural next step

[Wrenna Robson]

If you could prove this result it would be a very fine thing indeed: https://epubs.siam.org/doi/abs/10.1137/0124010?journalCode=smjmap

[Edward van de Meent]

i'm afraid i might fall short of those last two... the main reason i'm developing this part of the library is because i'd like a rigorous notion of code automorphisms, as the construction of the sporadic Mathieu-12 group depends in part on it (, or at least in the book i'm reading it does). i might give it a shot though

[Wrenna Robson]

Oh exciting

[Wrenna Robson]

The reason I suggest it is just that testing your definitions actually work for proving things is a great way to see if they're any good

[Edward van de Meent]

i'm having a bit of trouble... the packing distance in a metric space is half the smallest distance between points... however, for codes with the hamming distance, the packing distance is rounded down... is there a good way to unify this? if there isn't, which definition should i use?

there might be several options:

• the largest radius such that all open balls around points in the subset are disjoint
  • this one would suggest rounding up
• the largest radius such that there is a all closed balls around points in the subset are disjoint, and there is some point where the shortest distance to a point in the subset is that radius
  • this one agrees with the definition saying to round down.
  • however, it only works in the discrete case, in the continuous case the limsup might give a value for which the property doesn't hold
• keep it as-is, half the smallest distance

[Edward van de Meent]

i feel the key to this problem is that in the discrete case, looking at a closed set makes more sense. in particular because it is sensible to only consider packing distances where there actually is some point with that distance to the subset

[Edward van de Meent]

somehow you'd want to look at both open and closed balls, and look at which combination of open/closed and radius fits the maximum amount of points in balls, while keeping the property that the balls around points in the subset are disjoint

[Edward van de Meent]

is there some mathematical concept that describes this?

[Johan Commelin]

It might help to write down a bunch of such statements in Lean, and prove them with sorry. And then at some point the API might suggest what the optimal definition is.

[Johan Commelin]

Or you make all 3 definitions, and some implications between them...

[Edward van de Meent]

i was kindof thinking of somehow generalising this notion of "picking the largest radius that exists, such that all closed or all open balls are disjoint"

[Edward van de Meent]

but that will make properties a bit harder, because you don't necessarily know if you are talking about opens or closeds

[Wrenna Robson]

Yeah I know the issue you're talking about

[Wrenna Robson]

The easiest way to think about it I think is: the hamming metric is integer-valued, so "half" rounds down

[Edward van de Meent]

yes... except that when you use s.infsep, it becomes real-valued automatically

[Wrenna Robson]

Yes, it's because we have no notion really of an integer-valued distance

[Wrenna Robson]

but

[Wrenna Robson]

https://en.m.wikipedia.org/wiki/Delone_set

[Wrenna Robson]

I think you want to use the definition here

[Wrenna Robson]

Like it's still true that open balls of radius infsep/2 won't intersect

[Wrenna Robson]

But - ah yeah right sorry, this is why one rounds up I think...

[Wrenna Robson]

If it's t-error correcting, then closed balls of radius t won't intersect. So in other words, the infsep has to be at least 2t + 1, right? If it was 2t, then there would be some pair with 2t coordinates different, but then if you change t of one to the coordinates of the other, that's t away from two codewords, and we can't correct it

[Wrenna Robson]

I think infsep/2 is the only sensible definition of packing radius. But it might mean that some of the literature doesn't quite line up. What I found was that defining it in terms of the balls isn't the way to go - you kinda want to treat that as a property you prove

[Wrenna Robson]

Especially because you can then say "ah well if e > packing radius, balls of that radius intersect", and that's true for I think both open and closed balls

[Wrenna Robson]

I recently tried writing some of this down - if you search on Zulip I think I posted some of it?

[Edward van de Meent]

Wrenna Robson said:

Especially because you can then say "ah well if e > packing radius, balls of that radius intersect", and that's true for I think both open and closed balls

this is not the case though?

[Wrenna Robson]

Is it not? I suppose it might not be

[Edward van de Meent]

if you take the entire space as your code, infsep will be 1. so then the packing radius is 1/2, but open balls of size 3/4 don't intersect

[Edward van de Meent]

even open balls of radius 1 don't

[Wrenna Robson]

Around each point in the space?

[Edward van de Meent]

yes

[Edward van de Meent]

in the discrete case

[Wrenna Robson]

Yeah.

[Wrenna Robson]

Oh yes of course because there's no "points in-between"

[Wrenna Robson]

Which is why my geometric intuition is messing up

[Wrenna Robson]

Whereas in lattice theory obviously they embed in a larger space... hmm

[Wrenna Robson]

What I suppose is true is that closed balls with radius infsep around a point in the space will always contain another point in the space

[Wrenna Robson]

I think that's true in the continuous and discrete cases?

[Edward van de Meent]

yes, by definition of infsep

[Edward van de Meent]

it gives you the pair of points in the subset of that distance

[Wrenna Robson]

The abstract of this paper looks interesting and promising

[Wrenna Robson]

https://link.springer.com/article/10.1007/s10623-012-9623-4

[Wrenna Robson]

Yeah here is a neat but troubling example

[Wrenna Robson]

f867cdc2-dbbf-4e4e-a6cb-02cc3cf9f5e1.jpg

[Wrenna Robson]

(note this is using the language of permutation codes)

[Wrenna Robson]

But the idea is - you can construct two codes, both with min distance 6, but one of them can decode 3 errors and one can't.

[Edward van de Meent]

yea, i got that much

[Wrenna Robson]

If the min distance is 3, you can guarantee you can decode 2 errors, but you might not be able to decode 3

[Wrenna Robson]

It suggests that in fact you do want to define the packing radius distinctly to infsep - it's that the minimum distance of the code is closely related to the packing radius, but I think it might be the case that you can't actually determine one from the other

[Wrenna Robson]

Annoying!!

[Wrenna Robson]

Also, making this definition in a way that is nicely compatible with the continuous case will be a pain, and it's never fun to be taking minimums.

[Edward van de Meent]

i think in general i'd need to formalise these notions:
class GMetricSpace A Codomain
def packing_radius (...) : (OpenOrClosed \x Codomain)with OpenOrClosed an enum.

[Wrenna Robson]

Maybe - there was certainly some talk of doing generalised metric spaces at some point

[Wrenna Robson]

Basically all this is why I gave up before - it felt like the kind of thing that was too big to do alone, because you end up with a bunch of different ways of doing a bunch of stuff, and you want some coordination

[Edward van de Meent]

in that case, you can determine the radius simply by taking the supremum of radii that work in the closed case, while the enum is determined afterwards by checking wether a counterexample to the edge case exists

[Wrenna Robson]

Yeah no I just mean that you end up wanting a lot of general API

[Wrenna Robson]

That approach sounds hacky but if it lets you move forward it's better than nothing

[Edward van de Meent]

the question is if i should keep calling such a space a DeloneSet or not...

[Wrenna Robson]

Yeah. Possibly not!

[Wrenna Robson]

But it feels like a useful notion to have and tantalisingly close to what you actually want

[Wrenna Robson]

I think possibly, as @Yaël Dillies has observed at some point, part of the issue is that "packing radius" is kinda less useful than "packing diameter".

[Edward van de Meent]

what's packing diameter?

[Edward van de Meent]

twice the radius of the largest sphere that does not contain an element of the subset?

[Wrenna Robson]

Infsep, probably.

[Wrenna Robson]

It's sort of like, intuitively, we can expand out to that diameter without hitting another codeword

[Wrenna Robson]

Or rather I suppose, that's the first time when we might

[Wrenna Robson]

Or when another codeword is an infinitesimal distance away?

[Wrenna Robson]

It doesn't help we don't even have a notion of discrete metric...

[Edward van de Meent]

right... let me get a start with general metrics, see how that goes

[Edward van de Meent]

i'm guessing the best general case for a notion of distance is a linear ordering with a lowest element?

[Edward van de Meent]

where we'd like the distance between an element and itself to be that lowest element?

[Wrenna Robson]

Uh. Well, you don't need the second part. I guess that would be a generalised pseudometric?

[Edward van de Meent]

so just any linear ordering?

[Wrenna Robson]

Well, for the dist function it can be anything, in a sense that's just notation.

[Edward van de Meent]

ah, there is a slight hiccup as we would like to be able to add distances to define the triangle inequality

[Notification Bot]

A message was moved here from #new members > How to get the least element of a set of natural numbers? by Edward van de Meent.

[Edward van de Meent]

i'm guessing we should like it to be a monoid which respects ordering? as in, adding only increases its value?

[Yaël Dillies]

Wrenna Robson said:

I think possibly, as Yaël Dillies has observed at some point, part of the issue is that "packing radius" is kinda less useful than "packing diameter".

I'm not sure I said this exactly, but I do agree that you can't just take the packing radius to be half the packing diameter.

[Yaël Dillies]

I will also point out that, just as we have both docs#Int.floor and docs#Int.ceil, you will very likely need both the left and right adjoint to some map (which I think is ε ↦ ball x ε, but I'm not sure)

[Edward van de Meent]

the first hurdle has been cleared: writing a definition for a general equivalent to a PseudoMetricSpace.

it turns out you can easily extend it. The construction of a Bornology (whatever that is) still works. However, i was unable to extend the mapping to a Uniform space

[Wrenna Robson]

Yaël Dillies said:

I will also point out that, just as we have both docs#Int.floor and docs#Int.ceil, you will very likely need both the left and right adjoint to some map (which I think is ε ↦ ball x ε, but I'm not sure)

Oh this is a nice observation.

[Edward van de Meent]

i think that's precisely what will happen when i add the option between open or closed... not exactly sure, but i think so

[Edward van de Meent]

right now, i've defined the generalised metric to have domain β with [LinearOrderedAddCommMonoid β], however in copying some lemmas of PseudoMetricSpace i often come across instances where i'd like to prove something like (a < b) -> (a + c < b + c), and the original proofs make use of some lemmas (in docs#Mathlib.Algebra.Order.Monoid.Lemmas) which require an instance [CovariantClass β β (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1]... i'm not exactly sure how i should fix something like this, other than explicitly adding the instance and continuing... is there some single stronger requirement i could ask of β? the trouble of expanding to something like [Group β] is that you'd probably have to allow negative distances...

[Yaël Dillies]

Look up docs#LinearOrderedAddCommMonoid

[Yaël Dillies]

See that it is extended by docs#LinearOrderedCancelAddCommMonoid

[Edward van de Meent]

Thanks!

[Edward van de Meent]

i'd like some advice...

right now i've defined a notion of generalised DeloneSet, and have a definition for a "general" Linear Code, i.e. a subspace of some vectorspace that is also a DeloneSet... however, now i'm not sure if there really is a difference between a DeloneSet and a code. furthermore, i'm not certain if i should add more requirements to Linear Codes, as the current notion really seems like the best definition that does not necessarily use the Hamming distance. i could of course add a requirement that the vectorspace must be a finite disjoint union of a finite field (or something like that), but that seems unnecessarily restrictive... what is the best course going forward?

[Wrenna Robson]

I'm not sure if there's a meaningful rather than contextual difference.

[Wrenna Robson]

Honestly what I would do is try to free yourself from definition hell by picking some simple theorems and trying to prove them.

[Wrenna Robson]

In my experience that is the best guide.

[Wrenna Robson]

Trying to remember what we call a module equipped with a compatible norm... There's a word for this. Anyway, all subspaces of the suitable vector space are linear codes - so it must be a property of the space, not the individual code

[Wrenna Robson]

Like there's something about the space that means all subspaces are delone, right?

[Wrenna Robson]

And that's weird. It's certainly not true of all subsets! But I wonder if it is the essential thing you need to capture

[Edward van de Meent]

Wrenna Robson said:

I'm not sure if there's a meaningful rather than contextual difference.

the differences that i can think of of the top of my head are twofold: the first difference is that right now, the vectorspace can have any number of dimensions (even infinite). secondly, as of yet there is no restriction on the "size" of the scalar field, so each of the dimensions can stretch on forever in every direction you'd like, which most certainly isn't the case for products of finite fields.

[Wrenna Robson]

But is this actually important for anything in the actual definition?

[Wrenna Robson]

Rather than an extra hypothesis you will introduce in certain theorems?

[Edward van de Meent]

well... if i want to at least be somewhat consistent with existing literature....

[Wrenna Robson]

I agree that there's a few finiteness constraints that you need for coding theory

[Wrenna Robson]

Edward van de Meent said:

well... if i want to at least be somewhat consistent with existing literature....

In my experience - I don't think I'm entirely wrong about this - the definitions in existing literature don't always match up with the natural way to formalise things, and it's very easy to unnecessarily introduce constraints into your definitions that aren't actually necessary for them.

[Wrenna Robson]

I personally take a formalisation philosophy that things should minimally use preconditions, only when they are necessary.

[Wrenna Robson]

Like in the literature sometimes a code is defined as a map and sometimes it's defined as the image of that map

[Wrenna Robson]

You literally can't be fully consistent.

[Edward van de Meent]

it can be a map :melting_face:

[Edward van de Meent]

welp

[Wrenna Robson]

And in my experience if you make your definitions too specialised, it becomes challenging to go on and use your definitions

[Wrenna Robson]

Well yeah of course

[Wrenna Robson]

Like another way of thinking about a linear code is that it's an injective linear map, right?

[Wrenna Robson]

Say from a space with dimension n to a space with dimension k

[Wrenna Robson]

And maybe we have a metric on the spaces which is, essentially, the hamming metric according to a particular basis for both of them

[Wrenna Robson]

Then the image of the map is the set of codewords.

[Edward van de Meent]

i hadn't thought about it that way, i had only come across the "it's a subset with those distance properties" part...

[Wrenna Robson]

OR it could be a surjective linear map from a space with dimension n to a space with dimension n - k, and the kernel is the set of codewords

[Wrenna Robson]

Because linear codes (well, any subspace, but in this context) are simultaneously images or kernels, and when they're images we think of them as codewords, and when they're kernels we think of them as sets with null syndromes

[Edward van de Meent]

the thing is, i think the requirements you pose on automorphisms make a lot more sense when you look at a Code (not necessarily a linear one) as a map, rather than a subset, as it makes it obvious that the "superspace" is important

[Wrenna Robson]

Yes. But the trouble is the choice of map is not unique

[Wrenna Robson]

Different encodings can give rise to the same codewords

[Wrenna Robson]

Which is why one makes the equation of the linear codes with the subspaces/subsets

[Wrenna Robson]

The trouble being that it does somewhat obscure these other properties/perspectives

[Wrenna Robson]

And the issue is that in formalisation, we really have to care about what things actually are, rather than making these kind of elisions where we equate stuff

[Edward van de Meent]

the main problem that i'm understanding from this is that given some distance function and set of codewords on some space, the mapping is not unique?

[Wrenna Robson]

Yes

[Wrenna Robson]

Another way of thinking about this is - you have many different generating sets for the same code

[Wrenna Robson]

Or sometimes you want to take one code and permute it to obscure its structure (this is relevant in cryptography).

[Edward van de Meent]

i don't think that different generating sets should be a problem the way i've linear codes right now... and i think permuting a code can be done by simply applying the permutation before both parameters of the metric and before the correcting map? that should still work, right?

[Wrenna Robson]

Correcting map?

[Edward van de Meent]

the mapping from the entire space to the codewords?

[Wrenna Robson]

Why is it called that?

[Edward van de Meent]

that's how i describe it. i'm not very familiar with coding theory, but that's what i'd call it. if it's not obvious or if there is a better/more common name for such a map, i do apologise, i didn't know.

[Edward van de Meent]

because the map corrects

[Wrenna Robson]

Oh I see, as in, the map that - right

[Wrenna Robson]

But you don't explicitly have such a map, right?

[Wrenna Robson]

I would call this operation "decoding", incidentally

[Edward van de Meent]

ah right, i remember seeing that somewhere...

[Edward van de Meent]

Wrenna Robson said:

But you don't explicitly have such a map, right?

no, i don't... but i'm thinking about it...

[Edward van de Meent]

i should at the very least consider it, before discarding such an idea

[Wrenna Robson]

You can certainly define such a map

[Wrenna Robson]

But you won't have a general explicit definition I think

[Wrenna Robson]

Not a computable one anyway

[Edward van de Meent]

yes, and extensionality would also be a weaker tool, precisely because there might be multiple decoding maps

[Wrenna Robson]

Well ideally it is unambiguous what they decode to, so from a function extensionality pov they're all the same, but I think one can certainly say of a function "this function decodes that code"

[Edward van de Meent]

yes, i can certainly write such a statement... something along the lines of "the function maps all closed balls of a certain radius around some codepont to that codepoint if they don't intersect with some other ball with that radius around another codepoint"

[Wrenna Robson]

Yeah the issue I guess is that you do have a limit to how much you can correct

[Wrenna Robson]

And Ithink that when it's not a perfect code, there will be things that cannot be corrected to anything

[Edward van de Meent]

yes, that does seem right

[Edward van de Meent]

i suppose you could construct a decoding map in general by doing axiom of choice on the family of sets of closest codewords for each point... but it wouldn't exactly be canonical

[Edward van de Meent]

by the way, is there a name for the union of those closed balls i was talking about? or can i give it a name like "sphere of influence" or something?

[Wrenna Robson]

Crucially I think decoding is NP hard in general

[Wrenna Robson]

Hmm not sure. Name it and it can be renamed later.

[Edward van de Meent]

def Separates (c:GDeloneSet α₁ β) (δ : β): Prop :=
  ∀ cw ∈ c, ∀ cw' ∈ c, cw ≠ cw' → closedBall cw δ ∩ closedBall cw' δ = ∅

def IsDecodingMap (c : GDeloneSet α₁ β) (DecFun : α₁ → c):Prop :=
  ∀ x : α₁, ∀ cw ∈ c, Separates β c (GDist.gdist x cw) → DecFun x = cw

sneak peek

[Edward van de Meent]

here beta is the type of the codomain of the metric we're using. it gets passed because lean doesn't always naturally infer the type we're going for

[Edward van de Meent]

i'm having some trouble with defining the covering radius... according to the source that was mentioned before, it is the smallest distance such that closed balls around elements of some set X cover the entire space, however it seems to me that when you choose X={1/n | n∈ℕ} and the entire space X∪ {-1}, the infimum of distances which cover {-1} is equal to 1, however closed balls around elements of X with radius 1 all don't contain the element {-1}... so there is no such smallest distance...
is this just a bad description or definition of covering radius? or is there some assumption i'm missing?

[Wrenna Robson]

Just so you know, @Newell Jensen is also interested in some of these things and is pursuing a patch to add some of these concepts

[Wrenna Robson]

Yeah I think it is the infimum of something, but it may not imply that it does cover the space

[Wrenna Robson]

You might need an extra assumption on the space (completeness?)

[Edward van de Meent]

i think that would fix it yea.... or maybe something like the subset of elements closer than some radius is finite, maybe?

[Edward van de Meent]

i'm not completely sure

[Wrenna Robson]

Perhaps.

[Newell Jensen]

@Edward van de Meent feel free to contribute to #10641 if you see fit.

[Edward van de Meent]

thanks... although i did use my own definitions and stuff, so it might not exactly be compatible... in particular i generalised it so discrete metrics and anything inbetween could be used...

[Edward van de Meent]

most of my definitions parametrise over some codomain β which is a CompleteLinearOrder and a AddCommMonoid, along with a mixin which says that they work together nice...

[Edward van de Meent]

that way, some distances come out a bit better

[Wrenna Robson]

It might be good to state some goals: I think broadly what we are looking for here is, aside from the specific context of coding theory, to get concepts such as Delone sets, packing radii, minimum distance and so forth to a) lie flat together, b) be defined in Mathlib to an appropriate degree of generality i.e. for as arbitrary a metric space as possible.

[Wrenna Robson]

The wrinkles come in because in the literature, different definitions are sometimes used, and in general settings they might not be equivalent.

[Wrenna Robson]

Does that reflect both your understandings?

[Wrenna Robson]

Actually I should post this in the other thread...

[Nurrin]

Hi everyone,
I am currently interested in starting a project in sphere-packing bound. I'd like to ask what is the current status of Information Theory in Mathlib. Are there any existing ongoing projects related to this area that I should be aware of before starting ? So far as I know, there is already a formalisation of the Hamming distance, but I'm unsure about the overall state of the field in Mathlib.
I'd greatly appreciate any feedback. Thank you in advance for your time and insights.
Best regards,
Nurrin

[Sidharth Hariharan]

Hi Nurrin,
I am currently working with several others on a project to formalise the solution to the sphere packing problem in dimension 8. We have built a nontrivial amount of machinery, including definitions and lemmas on things like sphere packing density, which might be of interest to you. You can read the blueprint and look at our documentation, but the repo itself is still private. Is this the sort of thing you had in mind? (I know close to nothing about information theory.)

[Nurrin]

Hi Sidharth,
Thank you for letting me know. I would want to work on the sphere-packing bound in coding theory, using the Hamming metric. I believe it is quite a different topic.

[Junyan Xu]

There are definitely connections, e.g. between the binary Golay code and the Leech lattice. This chapter of SPLAG has more details.

[Junyan Xu]

Glad to learn that the E8 project is now in progress! I think @Seewoo Lee would also be pleased to be informed. People have been discussing multivariate Poisson summation here because I made a comment about the linear programming bound (Theorem 4.7/5.1 in the blueprint). Is LinearProgrammingBound already sorry free? (Update: I found the answer here: looks like its derivation from the Poisson summation formula is formalized but the Possion formula is not.)

By the way, I believe the sphere-packing bound in coding theory is this one: https://en.wikipedia.org/wiki/Hamming_bound#Statement_of_the_bound

[Seewoo Lee]

@Junyan Xu Yes I'm actually in the Sidharth's group too :) But as Nurrin said, it seems that the one for coding theory and Viazovska's result are different things.

[Sidharth Hariharan]

Nurrin said:

Hi Sidharth,
Thank you for letting me know. I would want to work on the sphere-packing bound in coding theory, using the Hamming metric. I believe it is quite a different topic.

I see, never mind then :)
I don't know any information theory at all :D
That being said, thanks @Junyan Xu for sharing the link to the book. One of my friends was coincidentally just talking to me about something he did with Hamming metrics (not in Lean or anything), and it definitely does sound interesting. I'll def read about it if I get a chance.