{"schema_version":1,"revision":444,"release":"a12870861c6830312d0fc13d40b47ec34023dab1287e8638076c9597f9f29082","totals":{"results":691,"projects":558},"entries":[{"abbreviated":false,"abstract":"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 arc gives one plane arc together with r − 3 lifts that, with three coordinate rows, form r linearly independent vectors; the formalization proves that all lifts of a plane arc lie in one common subspace of dimension at most r − 1. The proof uses an exactly normalized form of Segre's envelope of the tangents, a characteristic-two derivative obstruction, and a dimension bound for a colon ideal of (X^n, Y^n, Z^n) with n = q/2. Extended Reed–Solomon codes and the regular hyperoval show that the bound is attained.","authors":[{"name":"Pranava Kumar"}],"classification":{"arxiv":["math.CO","cs.IT"],"msc2020":["94B05","94B65","51E21","51E20","13H10","68V20"]},"formalization":{"theorem_names":["EvenOrderMDS.maximum_length_of_MDS_code"]},"id":"PALOMAR-2026-10-15-000014","path":"entries/PALOMAR-2026-10-15-000014-v1.json","preservation":{"repositories":[{"commit":"1e7d9f0fc719de64230edd473411b23e2a8ed72b","fork_repository":"PalomarArchive/PranavaKCode--EvenOrderMDS--5612d0673af7","source_repository":"PranavaKCode/EvenOrderMDS"}]},"preview":{"artifact_tree_sha256":"eaa570609ddecf3d13417c622dca901c254bb76a50507418476c3dd019978ec3","version":1},"published_at":"2026-10-15T19:52:55Z","source":{"commit":"1e7d9f0fc719de64230edd473411b23e2a8ed72b","project_path":null,"repository":"PranavaKCode/EvenOrderMDS"},"source_omitted":false,"status":"registered","title":"The MDS conjecture over finite fields of even order","trust":{"level":"high"},"version":1,"versions":1}],"previous":null,"next":null,"dropped":[],"message":null}