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

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

LinearCodes/MCA/InducedCode.lean

@@ -183,4 +183,100 @@ 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. 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 : Generator.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 : 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
+          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 : 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
+    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 : 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
+    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 LinearCodes

LinearCodes/MCA/RS/Submodule.lean

@@ -351,4 +351,35 @@ 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 `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 := 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, fnHammingWeight_eq_hammingWeight] at hwt
+  exact ⟨w, hw, hw0, hwt⟩
+
+
 end LinearCodes