LinearCodes: general Singleton bound + exact-MDS for RS and generators

[Praz314159]

"achieved with equality" from docstring is not matched by reality, where only lower bound is proved. Proving singleton bound generically so it can be inherited by codes wherever possible.

Add Generator.fnSingleton_bound (dim c + d ≤ |α| + 1 for any code c ⊆ α → F, via puncturing) and Generator.fn_exists_minWeight (Singleton attained ⇒ a nonzero codeword of weight exactly |α| − k + 1). Stated over a generic finite index type, so they cover Fin n → F and S → F uniformly.

Wire them into the repo's MDS-claiming codes, turning "achieved with equality" from docstring into theorem: reedSolomonSubmodule_minWeight_attained (RS), univariatePowers_minWeight_attained and affineLine_minWeight_attained (generators).

[z-tech]

Hi 👋, this is the first PR someone (I don't know) has opened up against my repo.

A non-blocking thought: the RS theorem seems to rely on hammingWeight and fnHammingWeight being definitionally equal on Fin n. Could we add an explicit bridge lemma, maybe fnHammingWeight_eq_hammingWeight, and use it here? That would make the dependency clearer and avoid brittle failures if either definition is refactored later.

Also, since fnSingleton_bound and fn_exists_minWeight are stated for arbitrary Submodule F (α → F), could they live in a more neutral namespace than Generator? They don’t seem generator-specific to me.

Do you plan to use this for something or just fun atm? Overall I'm happy to merge this.

[Praz314159]

Do you plan to use this for something or just fun atm? Overall I'm happy to merge this.

Hey what's up! Was just getting my feet wet, and realized that the MDS claims weren't tight. I am pretty interested in the work here, and am curious what you have planned (if anything) for it. I didn't have anything particular in mind, but I'm familiar with most of the papers referenced in the repo, so can probably be somewhat useful!