The MDS conjecture over finite fields of even order
A Lean 4 proof of the linear MDS conjecture for every finite field of even order. For a finite field K with an even number q of elements and 2 ≤ k ≤ q, the maximum length of a k-dimensional linear maximum distance separable (MDS) code over K is q + 2 when k = 3 or k = q − 1, and q + 1 otherwise; codes are subspaces of K^N and an MDS code is one whose minimum Hamming distance equals N − k + 1. The upper bound is proved through the correspondence between MDS codes and arcs: after puncturing and duality it suffices to exclude arcs of q + 2 vectors in K^r for 4 ≤ r ≤ q/2 + 1. A hypothetical such…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-15-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000014/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'