From 369f7bb3ae9406f7e04b7f63ca4723a6049fdfde Mon Sep 17 00:00:00 2001 From: Prashanth Ramakrishna Date: Tue, 23 Jun 2026 01:43:29 -0400 Subject: [PATCH 1/2] LinearCodes: general Singleton bound + exact-MDS for RS and generators MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). 0 sorry, 0 user axioms; lake build clean. --- LinearCodes/MCA/ConcreteMDS.lean | 35 +++++++++++ LinearCodes/MCA/InducedCode.lean | 98 +++++++++++++++++++++++++++++++ LinearCodes/MCA/RS/Submodule.lean | 23 ++++++++ 3 files changed, 156 insertions(+) diff --git a/LinearCodes/MCA/ConcreteMDS.lean b/LinearCodes/MCA/ConcreteMDS.lean index e45c477..9958947 100644 --- a/LinearCodes/MCA/ConcreteMDS.lean +++ b/LinearCodes/MCA/ConcreteMDS.lean @@ -450,5 +450,40 @@ example : (Generator.univariatePowers (ZMod 7) 3).IsMDS := end SanityChecks +/-! ### Exact MDS: the generator codes attain their Singleton distance + +`univariatePowers_IsMDS` / `affineLine_IsMDS` give the *lower* half of the +Singleton bound (`fnMinDistAtLeast` at the Singleton value). Feeding them into +the generic `fn_exists_minWeight` produces a nonzero codeword of *exactly* that +weight, so these codes meet the Singleton bound with equality. -/ + +/-- The univariate-powers generator's induced code attains the Singleton bound: +it contains a nonzero codeword of weight exactly `|F| − d` (its Singleton value +for `ℓ = d + 1`). -/ +theorem univariatePowers_minWeight_attained {F : Type*} [Field F] [DecidableEq F] + [Fintype F] {d : ℕ} (h_card : d + 1 ≤ Fintype.card F) : + ∃ w ∈ (univariatePowers F d).inducedCode, w ≠ 0 ∧ + fnHammingWeight w = Fintype.card F - d := by + have hmds := univariatePowers_IsMDS h_card + have h := fn_exists_minWeight (univariatePowers F d).inducedCode (d + 1) + hmds.inducedCode_finrank_eq (Nat.succ_pos d) hmds.inducedCode_minDist + obtain ⟨w, hw, hw0, hwt⟩ := h + refine ⟨w, hw, hw0, ?_⟩ + rw [hwt]; omega + +/-- The affine-line generator's induced code attains the Singleton bound: it +contains a nonzero codeword of weight exactly `|F| − 1` (its Singleton value for +`ℓ = 2`). -/ +theorem affineLine_minWeight_attained {F : Type*} [Field F] [DecidableEq F] + [Fintype F] (h_card : 2 ≤ Fintype.card F) : + ∃ w ∈ (affineLine F).inducedCode, w ≠ 0 ∧ + fnHammingWeight w = Fintype.card F - 1 := by + have hmds := affineLine_IsMDS h_card + have h := fn_exists_minWeight (affineLine F).inducedCode 2 + hmds.inducedCode_finrank_eq (by norm_num) hmds.inducedCode_minDist + obtain ⟨w, hw, hw0, hwt⟩ := h + refine ⟨w, hw, hw0, ?_⟩ + rw [hwt]; omega + end Generator end LinearCodes diff --git a/LinearCodes/MCA/InducedCode.lean b/LinearCodes/MCA/InducedCode.lean index 8d836af..04b08bf 100644 --- a/LinearCodes/MCA/InducedCode.lean +++ b/LinearCodes/MCA/InducedCode.lean @@ -183,4 +183,102 @@ theorem dotMap_injective_iff {F : Type*} [Field F] {S : Type*} {ℓ : ℕ} simpa only [Generator.dotMap_apply, Pi.zero_apply] using hx exact sub_eq_zero.mp huv0 + +/-! ### Singleton bound + +The Singleton bound `dim c + d ≤ |α| + 1` for any linear code `c ⊆ α → F`, +proved by puncturing: restricting codewords to `|α| − (d−1)` coordinates is +injective on `c` (two codewords agreeing there would differ on at most +`d − 1` coordinates, but a nonzero codeword has weight `≥ d`), so +`dim c ≤ |α| − (d−1)`. When the bound is met with equality the code is MDS; +`fn_exists_minWeight` extracts the attaining codeword. Both are stated over a +generic finite index type `α`, so they specialise to `Fin n → F` (Reed-Solomon) +and `S → F` (generator-induced codes) alike. -/ + +namespace Generator + +/-- **Singleton bound.** Any linear code `c ⊆ α → F` with minimum distance at +least `d` and positive dimension satisfies `dim c + d ≤ |α| + 1`. -/ +theorem fnSingleton_bound {F : Type*} [Field F] [DecidableEq F] {α : Type*} + [Fintype α] (c : Submodule F (α → F)) (d : ℕ) + (hc : 0 < Module.finrank F c) (hmd : fnMinDistAtLeast c d) : + Module.finrank F c + d ≤ Fintype.card α + 1 := by + classical + rcases Nat.eq_zero_or_pos d with hd0 | hd1 + · subst hd0 + have h := Submodule.finrank_le c + rw [Module.finrank_pi] at h + omega + · have hbot : c ≠ ⊥ := by + intro h; rw [h] at hc; simp at hc + obtain ⟨v, hv, hv0⟩ := (Submodule.ne_bot_iff c).mp hbot + have hdcard : d ≤ Fintype.card α := + le_trans (hmd v hv hv0) (fnHammingWeight_le_card v) + -- choose `d − 1` coordinates to drop; keep `T = Dᶜ` + obtain ⟨D, _hDsub, hDcard⟩ := + Finset.exists_subset_card_eq + (show d - 1 ≤ (Finset.univ : Finset α).card by rw [Finset.card_univ]; omega) + set T : Finset α := Dᶜ with hT + have hTcard : T.card = Fintype.card α - (d - 1) := by + rw [hT, Finset.card_compl, hDcard] + -- restriction to the kept coordinates is injective on `c` + let P : c →ₗ[F] (↥T → F) := + (LinearMap.funLeft F F (fun x : ↥T => (x : α))).comp c.subtype + have hPinj : Function.Injective P := by + rw [injective_iff_map_eq_zero] + rintro ⟨w, hw⟩ hPw + have hwT : ∀ x : α, x ∈ T → w x = 0 := by + intro x hxT + have := congrFun hPw (⟨x, hxT⟩ : ↥T) + simpa [P, LinearMap.funLeft_apply] using this + have hwle : fnHammingWeight w ≤ d - 1 := by + unfold fnHammingWeight + have hsub : (Finset.univ.filter fun i => w i ≠ 0) ⊆ D := by + intro i hi + rw [Finset.mem_filter] at hi + by_contra hiD + exact hi.2 (hwT i (by rw [hT, Finset.mem_compl]; exact hiD)) + calc (Finset.univ.filter fun i => w i ≠ 0).card + ≤ D.card := Finset.card_le_card hsub + _ = d - 1 := hDcard + have hw0 : w = 0 := by + by_contra hne + have := hmd w hw hne + omega + exact Subtype.ext hw0 + have hfr : Module.finrank F c ≤ T.card := by + have h := LinearMap.finrank_le_finrank_of_injective hPinj + rwa [Module.finrank_pi, Fintype.card_coe] at h + rw [hTcard] at hfr + omega + +/-- **Singleton bound attained ⇒ exact MDS.** A `k`-dimensional code +`c ⊆ α → F` whose minimum distance is at least the Singleton value +`|α| − k + 1` contains a nonzero codeword of weight *exactly* `|α| − k + 1`. +With the `fnMinDistAtLeast` hypothesis this pins the minimum distance to +exactly `|α| − k + 1` (the code is MDS, Singleton met with equality). -/ +theorem fn_exists_minWeight {F : Type*} [Field F] [DecidableEq F] {α : Type*} + [Fintype α] (c : Submodule F (α → F)) (k : ℕ) + (hfin : Module.finrank F c = k) (hk : 0 < k) + (hmd : fnMinDistAtLeast c (Fintype.card α - k + 1)) : + ∃ w ∈ c, w ≠ 0 ∧ fnHammingWeight w = Fintype.card α - k + 1 := by + classical + have hkn : k ≤ Fintype.card α := by + have h := Submodule.finrank_le c + rw [Module.finrank_pi, hfin] at h; exact h + by_contra hcon + push_neg at hcon + -- if no codeword has weight exactly `|α| − k + 1`, the distance is `≥ |α| − k + 2` + have hmd2 : fnMinDistAtLeast c (Fintype.card α - k + 1 + 1) := by + intro w hw hw0 + have hge := hmd w hw hw0 + have hne := hcon w hw hw0 + omega + have hpos : 0 < Module.finrank F c := by rw [hfin]; exact hk + have hb := fnSingleton_bound c (Fintype.card α - k + 1 + 1) hpos hmd2 + rw [hfin] at hb + omega + +end Generator + end LinearCodes diff --git a/LinearCodes/MCA/RS/Submodule.lean b/LinearCodes/MCA/RS/Submodule.lean index 1214ca4..c5db148 100644 --- a/LinearCodes/MCA/RS/Submodule.lean +++ b/LinearCodes/MCA/RS/Submodule.lean @@ -351,4 +351,27 @@ theorem reedSolomonSubmodule_isListDecodable_johnson h_johnson +/-- **Reed-Solomon attains the Singleton bound (exact MDS).** The RS code +contains a nonzero codeword of Hamming weight exactly `n − k + 1`. Together +with `reedSolomonSubmodule_minDist` (every nonzero codeword has weight +`≥ n − k + 1`) this pins the RS minimum distance to exactly `n − k + 1`: +Reed-Solomon meets the Singleton bound with equality. Proved by feeding +`reedSolomonSubmodule_isMDS` into the generic `Generator.fn_exists_minWeight`. -/ +theorem reedSolomonSubmodule_minWeight_attained [DecidableEq F] + (cfg : ReedSolomonConfig F) + (h_dom_size : cfg.domain.size = cfg.codeLength) + (h_distinct : ∀ i j : Fin cfg.domain.size, i ≠ j → + cfg.domain.getD i.val 0 ≠ cfg.domain.getD j.val 0) + (h_le : cfg.messageLength ≤ cfg.codeLength) + (h_pos : 0 < cfg.messageLength) : + ∃ w ∈ reedSolomonSubmodule cfg, w ≠ 0 ∧ + hammingWeight w = cfg.codeLength - cfg.messageLength + 1 := by + obtain ⟨hfin, hmd⟩ := reedSolomonSubmodule_isMDS cfg h_dom_size h_distinct h_le + have h := Generator.fn_exists_minWeight (reedSolomonSubmodule cfg) cfg.messageLength + hfin h_pos (by rw [Fintype.card_fin]; exact hmd) + obtain ⟨w, hw, hw0, hwt⟩ := h + rw [Fintype.card_fin] at hwt + exact ⟨w, hw, hw0, hwt⟩ + + end LinearCodes From 804aa699e8e51d80189341b906585211c6928a6b Mon Sep 17 00:00:00 2001 From: Prashanth Ramakrishna Date: Wed, 24 Jun 2026 12:44:16 -0400 Subject: [PATCH 2/2] Address review: explicit weight bridge + neutral namespace Add `fnHammingWeight_eq_hammingWeight` (rfl) and use it in `reedSolomonSubmodule_minWeight_attained` instead of relying on defeq. Move `fnSingleton_bound` / `fn_exists_minWeight` from `Generator` to the neutral `LinearCodes` namespace; update call sites. --- LinearCodes/MCA/InducedCode.lean | 20 +++++++++----------- LinearCodes/MCA/RS/Submodule.lean | 14 +++++++++++--- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/LinearCodes/MCA/InducedCode.lean b/LinearCodes/MCA/InducedCode.lean index 04b08bf..ea9c6d0 100644 --- a/LinearCodes/MCA/InducedCode.lean +++ b/LinearCodes/MCA/InducedCode.lean @@ -193,15 +193,15 @@ injective on `c` (two codewords agreeing there would differ on at most `dim c ≤ |α| − (d−1)`. When the bound is met with equality the code is MDS; `fn_exists_minWeight` extracts the attaining codeword. Both are stated over a generic finite index type `α`, so they specialise to `Fin n → F` (Reed-Solomon) -and `S → F` (generator-induced codes) alike. -/ - -namespace Generator +and `S → F` (generator-induced codes) alike. They are deliberately placed in +the neutral `LinearCodes` namespace (not `Generator`) since nothing here is +generator-specific. -/ /-- **Singleton bound.** Any linear code `c ⊆ α → F` with minimum distance at least `d` and positive dimension satisfies `dim c + d ≤ |α| + 1`. -/ theorem fnSingleton_bound {F : Type*} [Field F] [DecidableEq F] {α : Type*} [Fintype α] (c : Submodule F (α → F)) (d : ℕ) - (hc : 0 < Module.finrank F c) (hmd : fnMinDistAtLeast c d) : + (hc : 0 < Module.finrank F c) (hmd : Generator.fnMinDistAtLeast c d) : Module.finrank F c + d ≤ Fintype.card α + 1 := by classical rcases Nat.eq_zero_or_pos d with hd0 | hd1 @@ -231,8 +231,8 @@ theorem fnSingleton_bound {F : Type*} [Field F] [DecidableEq F] {α : Type*} intro x hxT have := congrFun hPw (⟨x, hxT⟩ : ↥T) simpa [P, LinearMap.funLeft_apply] using this - have hwle : fnHammingWeight w ≤ d - 1 := by - unfold fnHammingWeight + have hwle : Generator.fnHammingWeight w ≤ d - 1 := by + unfold Generator.fnHammingWeight have hsub : (Finset.univ.filter fun i => w i ≠ 0) ⊆ D := by intro i hi rw [Finset.mem_filter] at hi @@ -260,8 +260,8 @@ exactly `|α| − k + 1` (the code is MDS, Singleton met with equality). -/ theorem fn_exists_minWeight {F : Type*} [Field F] [DecidableEq F] {α : Type*} [Fintype α] (c : Submodule F (α → F)) (k : ℕ) (hfin : Module.finrank F c = k) (hk : 0 < k) - (hmd : fnMinDistAtLeast c (Fintype.card α - k + 1)) : - ∃ w ∈ c, w ≠ 0 ∧ fnHammingWeight w = Fintype.card α - k + 1 := by + (hmd : Generator.fnMinDistAtLeast c (Fintype.card α - k + 1)) : + ∃ w ∈ c, w ≠ 0 ∧ Generator.fnHammingWeight w = Fintype.card α - k + 1 := by classical have hkn : k ≤ Fintype.card α := by have h := Submodule.finrank_le c @@ -269,7 +269,7 @@ theorem fn_exists_minWeight {F : Type*} [Field F] [DecidableEq F] {α : Type*} by_contra hcon push_neg at hcon -- if no codeword has weight exactly `|α| − k + 1`, the distance is `≥ |α| − k + 2` - have hmd2 : fnMinDistAtLeast c (Fintype.card α - k + 1 + 1) := by + have hmd2 : Generator.fnMinDistAtLeast c (Fintype.card α - k + 1 + 1) := by intro w hw hw0 have hge := hmd w hw hw0 have hne := hcon w hw hw0 @@ -279,6 +279,4 @@ theorem fn_exists_minWeight {F : Type*} [Field F] [DecidableEq F] {α : Type*} rw [hfin] at hb omega -end Generator - end LinearCodes diff --git a/LinearCodes/MCA/RS/Submodule.lean b/LinearCodes/MCA/RS/Submodule.lean index c5db148..3ba1304 100644 --- a/LinearCodes/MCA/RS/Submodule.lean +++ b/LinearCodes/MCA/RS/Submodule.lean @@ -351,12 +351,20 @@ theorem reedSolomonSubmodule_isListDecodable_johnson h_johnson +/-- Bridge between the two Hamming-weight definitions on `Fin n`: the general +`Generator.fnHammingWeight` (over any finite index type) and the +`Fin n`-specific `hammingWeight` agree definitionally. Recorded explicitly so +that callers depend on a named lemma rather than on the two definitions +happening to be defeq, which would break silently if either is refactored. -/ +theorem fnHammingWeight_eq_hammingWeight [DecidableEq F] {n : ℕ} (v : Fin n → F) : + Generator.fnHammingWeight v = hammingWeight v := rfl + /-- **Reed-Solomon attains the Singleton bound (exact MDS).** The RS code contains a nonzero codeword of Hamming weight exactly `n − k + 1`. Together with `reedSolomonSubmodule_minDist` (every nonzero codeword has weight `≥ n − k + 1`) this pins the RS minimum distance to exactly `n − k + 1`: Reed-Solomon meets the Singleton bound with equality. Proved by feeding -`reedSolomonSubmodule_isMDS` into the generic `Generator.fn_exists_minWeight`. -/ +`reedSolomonSubmodule_isMDS` into the generic `fn_exists_minWeight`. -/ theorem reedSolomonSubmodule_minWeight_attained [DecidableEq F] (cfg : ReedSolomonConfig F) (h_dom_size : cfg.domain.size = cfg.codeLength) @@ -367,10 +375,10 @@ theorem reedSolomonSubmodule_minWeight_attained [DecidableEq F] ∃ w ∈ reedSolomonSubmodule cfg, w ≠ 0 ∧ hammingWeight w = cfg.codeLength - cfg.messageLength + 1 := by obtain ⟨hfin, hmd⟩ := reedSolomonSubmodule_isMDS cfg h_dom_size h_distinct h_le - have h := Generator.fn_exists_minWeight (reedSolomonSubmodule cfg) cfg.messageLength + have h := fn_exists_minWeight (reedSolomonSubmodule cfg) cfg.messageLength hfin h_pos (by rw [Fintype.card_fin]; exact hmd) obtain ⟨w, hw, hw0, hwt⟩ := h - rw [Fintype.card_fin] at hwt + rw [Fintype.card_fin, fnHammingWeight_eq_hammingWeight] at hwt exact ⟨w, hw, hw0, hwt⟩