diff --git a/ArkLib/Data/CodingTheory/Basic.lean b/ArkLib/Data/CodingTheory/Basic.lean index 1779f2766..647b12991 100644 --- a/ArkLib/Data/CodingTheory/Basic.lean +++ b/ArkLib/Data/CodingTheory/Basic.lean @@ -38,6 +38,10 @@ import ArkLib.Data.Fin.Basic variable {n : Type*} [Fintype n] {R : Type*} [DecidableEq R] +/-- A linear code over alphabet `F` and index set `ι` is a submodule of functions `ι → F`. -/ +abbrev LinearCode.{u, v} (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] : Type (max u v) := + Submodule F (ι → F) + namespace Code -- Notation for Hamming distance @@ -74,6 +78,72 @@ noncomputable def distFromCode (u : n → R) (C : Set (n → R)) : ℕ∞ := notation "Δ₀(" u ", " C ")" => distFromCode u C +-- A convenient algebraic rewrite for Hamming distance: translate second argument by `-c`. +lemma hammingDist_add_right_eq_sub + {F : Type*} [AddGroup F] [DecidableEq F] + {ι : Type*} [Fintype ι] + (u v c : ι → F) : + hammingDist (u + c) v = hammingDist u (v - c) := by + classical + have hiff : ∀ i, ((u i + c i) = v i) ↔ (u i = v i - c i) := by + intro i; constructor + · intro h; have := congrArg (fun x => x - c i) h; simpa [add_sub_cancel] using this + · intro h; have := congrArg (fun x => x + c i) h; simpa [sub_add_cancel] using this + have hneq : ∀ i, ((u i + c i) ≠ v i) ↔ (u i ≠ v i - c i) := fun i => not_congr (hiff i) + have hset : + (Finset.univ.filter fun i : ι => (u i + c i) ≠ v i) + = (Finset.univ.filter fun i : ι => u i ≠ v i - c i) := by + ext i; simp [hneq i] + simp [hammingDist, hset] + +/-! Translation invariance of distance to a linear code: adding a codeword does not + change the distance. -/ +lemma distFromCode_add_codeword_eq + {F : Type*} [Ring F] [DecidableEq F] + {ι : Type*} [Fintype ι] + (LC : Submodule F (ι → F)) {w c : ι → F} (hc : c ∈ (LC : Set (ι → F))) : + Δ₀(w + c, (LC : Set (ι → F))) = Δ₀(w, (LC : Set (ι → F))) := by + classical + -- Closure properties in the submodule + have h_subtract_mem : ∀ z ∈ (LC : Set (ι → F)), z - c ∈ (LC : Set (ι → F)) := by + intro z hz; simpa using (Submodule.sub_mem LC (by simpa using hz) (by simpa using hc)) + have h_add_mem : ∀ z ∈ (LC : Set (ι → F)), z + c ∈ (LC : Set (ι → F)) := by + intro z hz; simpa using (Submodule.add_mem LC (by simpa using hz) (by simpa using hc)) + -- Witness set rewrite 1 + have hset₁ : + {d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist (w + c) z ≤ d} + = {d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist w (z - c) ≤ d} := by + ext d; constructor + · intro hd; rcases hd with ⟨z, hzC, hzle⟩ + -- keep witness z; rewrite distance (w + c) to (w) vs (z - c) + refine ⟨z, hzC, ?_⟩ + simpa [hammingDist_add_right_eq_sub (u := w) (v := z) (c := c)] using hzle + · intro hd; rcases hd with ⟨z, hzC, hzle⟩ + refine ⟨z, hzC, ?_⟩ + -- directly rewrite hammingDist (w + c) z = hammingDist w (z - c) + simpa [hammingDist_add_right_eq_sub (u := w) (v := z) (c := c)] using hzle + -- Witness set rewrite 2 + have hset₂ : + {d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist w (z - c) ≤ d} + = {d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist w z ≤ d} := by + ext d; constructor <;> intro hd + · rcases hd with ⟨z, hzC, hzle⟩ + -- choose z' = z - c ∈ LC + exact ⟨z - c, h_subtract_mem z hzC, by simpa using hzle⟩ + · rcases hd with ⟨z, hzC, hzle⟩ + -- choose z' = z + c ∈ LC so that (z' - c) = z + exact ⟨z + c, h_add_mem z hzC, by simpa using hzle⟩ + -- Conclude by unfolding distFromCode using the combined set equality + have hsets : + {d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist (w + c) z ≤ d} + = {d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist w z ≤ d} := + hset₁.trans hset₂ + -- Apply congrArg on sInf to transport equality of sets to equality of infimums + have hsInf : sInf ({d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist (w + c) z ≤ d}) + = sInf ({d : ℕ∞ | ∃ z ∈ (LC : Set (ι → F)), hammingDist w z ≤ d}) := by + simpa using congrArg sInf hsets + simpa [Code.distFromCode] using hsInf + noncomputable def minDist (C : Set (n → R)) : ℕ := sInf {d | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d} @@ -684,9 +754,6 @@ theorem singleton_bound (C : Set (n → R)) : exact huniv -abbrev LinearCode.{u, v} (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] : Type (max u v) := - Submodule F (ι → F) - namespace LinearCode section @@ -804,11 +871,32 @@ lemma dist_eq_minWtCodewords [CommRing F] {LC : LinearCode ι F} : open Finset in +lemma hammingDist_add_right_eq_sub [AddGroup F] [DecidableEq F] + (u v c : ι → F) : + hammingDist (u + c) v = hammingDist u (v - c) := by + classical + -- Compare pointwise predicates and rewrite filter sets. + have hiff : ∀ i, ((u i + c i) = v i) ↔ (u i = v i - c i) := by + intro i; constructor + · intro h + have := congrArg (fun x => x - c i) h + simpa [add_sub_cancel] using this + · intro h + have := congrArg (fun x => x + c i) h + simpa [sub_add_cancel] using this + have hneq : ∀ i, ((u i + c i) ≠ v i) ↔ (u i ≠ v i - c i) := fun i => not_congr (hiff i) + have hset : + (Finset.univ.filter fun i : ι => (u i + c i) ≠ v i) + = (Finset.univ.filter fun i : ι => u i ≠ v i - c i) := by + ext i; simp [hneq i] + simp [hammingDist, hset] + + lemma dist_UB [CommRing F] {LC : LinearCode ι F} : Code.minDist (LC : Set (ι → F)) ≤ length LC := by rw [dist_eq_minWtCodewords, minWtCodewords] exact sInf.sInf_UB_of_le_UB fun s ⟨_, _, _, s_def⟩ ↦ - s_def ▸ le_trans (card_le_card (subset_univ _)) (le_refl _) + s_def ▸ le_trans (Finset.card_le_card (Finset.subset_univ _)) (le_refl _) -- Restriction to a finite set of coordinates as a linear map noncomputable def restrictLinear [Semiring F] (S : Finset ι) : diff --git a/ArkLib/Data/CodingTheory/InterleavedCode.lean b/ArkLib/Data/CodingTheory/InterleavedCode.lean index 694482b86..c7c4119f4 100644 --- a/ArkLib/Data/CodingTheory/InterleavedCode.lean +++ b/ArkLib/Data/CodingTheory/InterleavedCode.lean @@ -1,184 +1,15 @@ /- -Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Katerina Hristova, František Silváši --/ - -import ArkLib.Data.CodingTheory.Basic -import ArkLib.Data.CodingTheory.ReedSolomon -import Mathlib.Order.CompletePartialOrder -import Mathlib.Probability.Distributions.Uniform - -noncomputable section - -/-! - Definition of an interleaved code of a linear code over a semiring. - Definition of distances for interleaved codes and statement for the relation between the minimal - distance of an interleaved code and its underlying linear code. - Statements of proximity results for Reed Solomon codes - (`Lemma 4.3`, `Lemma 4.4` and `Lemma 4.5` from Ligero) with proximity parameter less than - the minimal code distance divided by `3`. --/ - -variable {F : Type*} [Semiring F] - {κ ι : Type*} [Fintype κ] [Fintype ι] - {LC : LinearCode ι F} - -abbrev MatrixSubmodule.{u, v, w} (κ : Type u) [Fintype κ] (ι : Type v) [Fintype ι] - (F : Type w) [Semiring F] : Type (max u v w) := - Submodule F (Matrix κ ι F) - -/-- -The data needed to construct an interleaved code. --/ -structure InterleavedCode (κ ι : Type*) [Fintype κ] [Fintype ι] (F : Type*) [Semiring F] where - MF : MatrixSubmodule κ ι F - LC : LinearCode ι F - -namespace InterleavedCode - -/-- -The condition making the `InterleavedCode` structure an interleaved code. --/ -def isInterleaved (IC : InterleavedCode κ ι F) := - ∀ V ∈ IC.MF, ∀ i, V i ∈ IC.LC - -def LawfulInterleavedCode (κ : Type*) [Fintype κ] (ι : Type*) [Fintype ι] - (F : Type*) [Semiring F] := - { IC : InterleavedCode κ ι F // IC.isInterleaved } - -/-- -The submodule of the module of matrices whose rows belong to a linear code. --/ -def matrixSubmoduleOfLinearCode (κ : Type*) [Fintype κ] - (LC : LinearCode ι F) : MatrixSubmodule κ ι F := - Submodule.span F { V | ∀ i, V i ∈ LC } - -def codeOfLinearCode (κ : Type*) [Fintype κ] (LC : LinearCode ι F) : InterleavedCode κ ι F := - { MF := matrixSubmoduleOfLinearCode κ LC, LC := LC } - -/-- -The module of matrices whose rows belong to a linear code is in fact an interleaved code. --/ -lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved := by sorry - -def lawfulInterleavedCodeOfLinearCode (κ : Type*) [Fintype κ] (LC : LinearCode ι F) : - LawfulInterleavedCode κ ι F := ⟨codeOfLinearCode κ LC, isInterleaved_codeOfLinearCode⟩ - -/-- -Distance between codewords of an interleaved code. --/ -def distCodewords [DecidableEq F] (U V : Matrix κ ι F) : ℕ := - (Matrix.neqCols U V).card - -/-- -`Δ(U,V)` is the distance between codewords `U` and `V` of a `κ`-interleaved code `IC`. --/ -notation "Δ(" U "," V ")" => distCodewords U V - -/-- -Minimal distance of an interleaved code. --/ -def minDist [DecidableEq F] (IC : MatrixSubmodule κ ι F) : ℕ := - sInf { d : ℕ | ∃ U ∈ IC, ∃ V ∈ IC, distCodewords U V = d } - -/-- -`Δ IC` is the min distance of an interleaved code `IC`. --/ -notation "Δ" IC => minDist IC - -/-- -Distance from a matrix to the closest word in an interleaved code. --/ -def distToCode [DecidableEq F] (U : Matrix κ ι F) (IC : MatrixSubmodule κ ι F) : ℕ := - sInf { d : ℕ | ∃ V ∈ IC, distCodewords U V = d } - -/-- -`Δ(U,C')` denotes distance between a `κ x ι` matrix `U` and `κ`-interleaved code `IC`. --/ -notation "Δ(" U "," IC ")" => distToCode U IC - -/-- -Relative distance between codewords of an interleaved code. --/ -def relDistCodewords [DecidableEq F] (U V : Matrix κ ι F) : ℝ := - (Matrix.neqCols U V).card / Fintype.card ι - -/-- List of codewords of IC r-close to U, - with respect to relative distance of interleaved codes. --/ -def relHammingBallInterleavedCode [DecidableEq F] (U : Matrix κ ι F) - (IC : MatrixSubmodule κ ι F) (r : ℝ) := - {V | V ∈ IC ∧ relDistCodewords U V < r} - -/--`Λᵢ(U, IC, r)` denotes the list of codewords of IC r-close to U-/ -notation "Λᵢ(" U "," IC "," r ")" => relHammingBallInterleavedCode U IC r - -/-- -The minimal distance of an interleaved code is the same as -the minimal distance of its underlying linear code. --/ -lemma minDist_eq_minDist [DecidableEq F] {IC : LawfulInterleavedCode κ ι F} : - Code.minDist (IC.1.LC : Set (ι → F)) = minDist IC.1.MF := by sorry - -end InterleavedCode - -noncomputable section - -open InterleavedCode -open Code - -variable {F : Type*} [Field F] [Finite F] [DecidableEq F] - {κ : Type*} [Fintype κ] {ι : Type*} [Fintype ι] - -local instance : Fintype F := Fintype.ofFinite F - -/-- -Lemma 4.3 Ligero --/ -lemma distInterleavedCodeToCodeLB - {IC : LawfulInterleavedCode κ ι F} {U : Matrix κ ι F} {e : ℕ} - (hF : Fintype.card F ≥ e) - (he : (e : ℚ) ≤ (minDist (IC.1.LC : Set (ι → F)) / 3)) (hU : e < Δ(U,IC.1.MF)) : - ∃ v ∈ Matrix.rowSpan U , e < distFromCode v IC.1.LC := sorry - -namespace ProximityToRS - -/-- -The set of points on an affine line, which are within distance `e` -from a Reed-Solomon code. --/ -def closePtsOnAffineLine {ι : Type*} [Fintype ι] - (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Set (ι → F) := - {x : ι → F | x ∈ Affine.line u v ∧ distFromCode x (ReedSolomon.code α deg) ≤ e} - -/-- -The number of points on an affine line between, which are within distance `e` -from a Reed-Solomon code. --/ -def numberOfClosePts (u v : ι → F) (deg : ℕ) (α : ι ↪ F) - (e : ℕ) : ℕ := - Fintype.card (closePtsOnAffineLine u v deg α e) - -/-- -Lemma 4.4 Ligero -Remark: Below, can use (ReedSolomonCode.minDist deg α) instead of ι - deg + 1 once proved. --/ -lemma e_leq_dist_over_3 {deg : ℕ} {α : ι ↪ F} {e : ℕ} {u v : ι → F} - (he : (e : ℚ) < (Fintype.card ι - deg + 1 / 3)) : - ∀ x ∈ Affine.line u v, distFromCode x (ReedSolomon.code α deg) ≤ e - ∨ (numberOfClosePts u v deg α e) ≤ Fintype.card ι - deg + 1 := by sorry - -/-- -Lemma 4.5 Ligero --/ -lemma probOfBadPts {deg : ℕ} {α : ι ↪ F} {e : ℕ} {U : Matrix κ ι F} - (he : (e : ℚ) < (Fintype.card ι - deg + 1 / 3)) - (hU : e < Δ(U,matrixSubmoduleOfLinearCode κ (ReedSolomon.code α deg))) : - (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure - { w | distFromCode (n := ι) (R := F) w (ReedSolomon.code α deg) ≤ e } - ≤ (Fintype.card ι - deg + 1)/(Fintype.card F) := by - sorry - -end ProximityToRS -end +Aggregator module for InterleavedCode. This file just re-exports the +split modules so downstream imports remain stable. +To work on a specific result, open the corresponding submodule file. +-/ + +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.MinDistEq +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43 +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.ClosePoints +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.ThreeClosePoints +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44 +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma45 +import ArkLib.Data.CodingTheory.InterleavedCode.GeneralInequalityAndCounterexample diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Defs.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Defs.lean new file mode 100644 index 000000000..ad6496e48 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Defs.lean @@ -0,0 +1,243 @@ +/- +Basic definitions for interleaved codes and distance notions. +This file contains data structures, helper lemmas, and notations +used across the InterleavedCode lemmas. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.ReedSolomon +import Mathlib.Order.CompletePartialOrder +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Tactic + +noncomputable section + +variable {F : Type*} [Semiring F] + {κ ι : Type*} [Fintype κ] [Fintype ι] + {LC : LinearCode ι F} + +abbrev MatrixSubmodule.{u, v, w} (κ : Type u) [Fintype κ] (ι : Type v) [Fintype ι] + (F : Type w) [Semiring F] : Type (max u v w) := + Submodule F (Matrix κ ι F) + +/-- +The data needed to construct an interleaved code. +-/ +structure InterleavedCode (κ ι : Type*) [Fintype κ] [Fintype ι] (F : Type*) [Semiring F] where + MF : MatrixSubmodule κ ι F + LC : LinearCode ι F + +namespace InterleavedCode + +/-- +The condition making the `InterleavedCode` structure an interleaved code. +-/ +def isInterleaved (IC : InterleavedCode κ ι F) := + ∀ V ∈ IC.MF, ∀ i, V i ∈ IC.LC + +def LawfulInterleavedCode (κ : Type*) [Fintype κ] (ι : Type*) [Fintype ι] + (F : Type*) [Semiring F] := + { IC : InterleavedCode κ ι F // IC.isInterleaved } + +/-- +The submodule of the module of matrices whose rows belong to a linear code. +-/ +def matrixSubmoduleOfLinearCode (κ : Type*) [Fintype κ] + (LC : LinearCode ι F) : MatrixSubmodule κ ι F := + Submodule.span F { V | ∀ i, V i ∈ LC } + +def codeOfLinearCode (κ : Type*) [Fintype κ] (LC : LinearCode ι F) : InterleavedCode κ ι F := + { MF := matrixSubmoduleOfLinearCode κ LC, LC := LC } + +/-- +The module of matrices whose rows belong to a linear code is in fact an interleaved code. +-/ +lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved := by + classical + intro V hV i + -- Define the submodule of matrices whose rows lie in LC + let T : Submodule F (Matrix κ ι F) := + { carrier := {W : Matrix κ ι F | ∀ j, W j ∈ LC} + zero_mem' := by + -- 0-row is the zero codeword in LC + exact fun j => by rw [Pi.zero_apply]; exact Submodule.zero_mem LC + add_mem' := by + intro A B hA hB j; simpa using (Submodule.add_mem LC (hA j) (hB j)) + smul_mem' := by + intro a A hA j; simpa using (Submodule.smul_mem LC a (hA j)) } + have hle : (matrixSubmoduleOfLinearCode κ LC) ≤ T := by + -- The span of the generator set is contained in T + refine Submodule.span_le.mpr ?_ + intro M hM; exact hM + have hVT : V ∈ T := hle hV + -- Conclude row membership + exact hVT i + +def lawfulInterleavedCodeOfLinearCode (κ : Type*) [Fintype κ] (LC : LinearCode ι F) : + LawfulInterleavedCode κ ι F := ⟨codeOfLinearCode κ LC, isInterleaved_codeOfLinearCode⟩ + +/-- +Distance between codewords of an interleaved code. +-/ +def distCodewords [DecidableEq F] (U V : Matrix κ ι F) : ℕ := + (Matrix.neqCols U V).card + +/-- +`Δ(U,V)` is the distance between codewords `U` and `V` of a `κ`-interleaved code `IC`. +-/ +notation "Δ(" U "," V ")" => distCodewords U V + +/-- +Minimal distance of an interleaved code. +-/ +def minDist [DecidableEq F] (IC : MatrixSubmodule κ ι F) : ℕ := + sInf { d : ℕ | ∃ U ∈ IC, ∃ V ∈ IC, U ≠ V ∧ distCodewords U V = d } + +/-- +`Δ IC` is the min distance of an interleaved code `IC`. +-/ +notation "Δ" IC => minDist IC + +/-- +Distance from a matrix to the closest word in an interleaved code. +-/ +def distToCode [DecidableEq F] (U : Matrix κ ι F) (IC : MatrixSubmodule κ ι F) : ℕ := + sInf { d : ℕ | ∃ V ∈ IC, distCodewords U V = d } + +/-- +`Δ(U,C')` denotes distance between a `κ x ι` matrix `U` and `κ`-interleaved code `IC`. +-/ +notation "Δ(" U "," IC ")" => distToCode U IC + +/-- +Relative distance between codewords of an interleaved code. +-/ +def relDistCodewords [DecidableEq F] (U V : Matrix κ ι F) : ℝ := + (Matrix.neqCols U V).card / Fintype.card ι + +/-- List of codewords of IC r-close to U, + with respect to relative distance of interleaved codes. +-/ +def relHammingBallInterleavedCode [DecidableEq F] (U : Matrix κ ι F) + (IC : MatrixSubmodule κ ι F) (r : ℝ) := + {V | V ∈ IC ∧ relDistCodewords U V < r} + +/--`Λᵢ(U, IC, r)` denotes the list of codewords of IC r-close to U-/ +notation "Λᵢ(" U "," IC "," r ")" => relHammingBallInterleavedCode U IC r + +omit [Semiring F] in +/-- +The minimal distance of an interleaved code is the same as +the minimal distance of its underlying linear code. +Helper: row support containment. +-/ +lemma rowSupport_subset_neqCols [DecidableEq F] + (U V : Matrix κ ι F) (i : κ) : + (Finset.univ.filter fun j : ι => U i j ≠ V i j) ⊆ Matrix.neqCols U V := by + intro j hj + have hj' : U i j ≠ V i j := (Finset.mem_filter.mp hj).2 + have hj'' : V i j ≠ U i j := by simpa [ne_comm] using hj' + have hexists : ∃ i0 : κ, V i0 j ≠ U i0 j := ⟨i, hj''⟩ + simpa [Matrix.neqCols] using hexists + +lemma support_eq_for_single_row_diff [DecidableEq F] [DecidableEq κ] + {u v : ι → F} (i₀ : κ) + (U V : Matrix κ ι F) + (hU : ∀ i, U i = (if i = i₀ then u else 0)) + (hV : ∀ i, V i = (if i = i₀ then v else 0)) : + distCodewords U V = hammingDist u v := by + classical + -- Show both finset supports are equal by double inclusion + -- Left-to-right: any differing column must be at row i₀ + apply le_antisymm + · -- card(neqCols) ≤ card(support u≠v) + have hsubset : Matrix.neqCols U V ⊆ (Finset.univ.filter fun j : ι => u j ≠ v j) := by + intro j hj + rcases (by simpa [Matrix.neqCols] using hj) with ⟨i, hi⟩ + by_cases hi0 : i = i₀ + · subst hi0 + have hvu : v j ≠ u j := by simpa [hU, hV] using hi + have : u j ≠ v j := by simpa [ne_comm] using hvu + simpa [Finset.mem_filter] + · have : U i j = V i j := by simp [hU, hV, hi0] + exact False.elim (hi (by simp [this])) + have := Finset.card_mono hsubset + simpa [distCodewords, hammingDist, Matrix.neqCols] + · -- card(support u≠v) ≤ card(neqCols) + have hsubset : (Finset.univ.filter fun j : ι => u j ≠ v j) ⊆ Matrix.neqCols U V := by + intro j hj + have : u j ≠ v j := (Finset.mem_filter.mp hj).2 + have : U i₀ j ≠ V i₀ j := by simpa [hU, hV] using this + have : V i₀ j ≠ U i₀ j := by simpa [ne_comm] using this + simpa [Matrix.neqCols] using ⟨i₀, this⟩ + have := Finset.card_mono hsubset + simpa [distCodewords, hammingDist, Matrix.neqCols] + +end InterleavedCode + +-- Additional helpers used by the InterleavedCode lemmas +namespace InterleavedCode + +variable {F : Type*} [Semiring F] +variable {κ ι : Type*} [Fintype κ] + +/-- A finite linear combination of the rows of `U` lies in the row span of `U`. -/ +lemma v_of_in_rowSpan (U : Matrix κ ι F) (r : κ → F) : + (fun j => ∑ i, (r i) * (U i j)) ∈ Matrix.rowSpan U := by + classical + -- Identify the target as a finite linear combination of the generators U i + have hfun : (fun j => ∑ i, (r i) * (U i j)) = (∑ i : κ, (r i) • (U i)) := by + funext j; simp [Pi.smul_apply, smul_eq_mul] + -- Finite linear combinations of generators lie in the span + have hmem_univ : (Finset.univ.sum (fun i : κ => (r i) • (U i))) ∈ Matrix.rowSpan U := by + -- Matrix.rowSpan U = span {U i | i} + refine Finset.induction_on (Finset.univ : Finset κ) ?base ?step + · simp + · intro a s ha_notin hs_mem + have h_head : (r a) • U a ∈ Matrix.rowSpan U := by + refine Submodule.smul_mem (Matrix.rowSpan U) (r a) ?_ + exact Submodule.subset_span (by change U a ∈ {U i | i : κ}; simp) + have h_tail : (Finset.sum s (fun i : κ => (r i) • U i)) ∈ Matrix.rowSpan U := hs_mem + simpa [Finset.sum_insert, ha_notin] using Submodule.add_mem (Matrix.rowSpan U) h_head h_tail + have hmem : (∑ i : κ, (r i) • (U i)) ∈ Matrix.rowSpan U := by simpa using hmem_univ + simpa [hfun] + +/-- A finite linear combination of rows `c i ∈ LC` is again in `LC`. -/ +lemma linear_comb_rows_in_LC [Fintype ι] (LC : LinearCode ι F) + (c : κ → ι → F) + (hc : ∀ i, c i ∈ LC) (r : κ → F) : + (fun j => ∑ i, (r i) * (c i j)) ∈ (LC : Set (ι → F)) := by + classical + -- Identify the target as a finite linear combination in the submodule LC + have hfun : (fun j => ∑ i, (r i) * (c i j)) = (∑ i : κ, (r i) • (c i)) := by + funext j; simp [Pi.smul_apply, smul_eq_mul] + have hmem_univ : (Finset.univ.sum (fun i : κ => (r i) • (c i))) ∈ LC := by + -- Finite sums of elements of LC with scalars lie in LC + refine Finset.induction_on (Finset.univ : Finset κ) ?base ?step + · simp + · intro a s ha_notin hs_mem + have h_head : (r a) • c a ∈ LC := by + refine Submodule.smul_mem LC (r a) ?_ + simpa using hc a + have h_tail : (Finset.sum s (fun i : κ => (r i) • c i)) ∈ LC := hs_mem + simpa [Finset.sum_insert, ha_notin] using Submodule.add_mem LC h_head h_tail + have : (∑ i : κ, (r i) • (c i)) ∈ LC := by simpa using hmem_univ + simpa [hfun] + +/- +Residuals and their linear combination along κ → F. +These are used pervasively in the interleaved-code lemmas. +-/ + +variable {F : Type*} [CommRing F] +variable {κ ι : Type*} [Fintype κ] [Fintype ι] + +/-- Row-wise residual χ of U against a per-row codeword family c. -/ +def residual (U : Matrix κ ι F) (c : κ → ι → F) : κ → ι → F := + fun i j => U i j - c i j + +/-- Combined residual E of U, c along a coefficient map r : κ → F. -/ +def E (U : Matrix κ ι F) (c : κ → ι → F) (r : κ → F) : ι → F := + fun j => ∑ i, (r i) * (residual U c i j) + +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/GeneralInequalityAndCounterexample.lean b/ArkLib/Data/CodingTheory/InterleavedCode/GeneralInequalityAndCounterexample.lean new file mode 100644 index 000000000..0629e92fb --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/GeneralInequalityAndCounterexample.lean @@ -0,0 +1,133 @@ +/- +General inequality and a counterexample for min distances. +-/ + +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import Mathlib.Tactic + +noncomputable section + +open InterleavedCode + +section GeneralInequalityAndCounterexample + +variable {F : Type*} [Semiring F] [DecidableEq F] + {κ ι : Type*} [Fintype κ] [Fintype ι] + +-- General inequality under nontriviality of the interleaved submodule +lemma baseMinDist_le_minDist_of_nontrivialMF + {IC : LawfulInterleavedCode κ ι F} + (hNE : ∃ U ∈ IC.1.MF, ∃ V ∈ IC.1.MF, U ≠ V) : + Code.minDist (IC.1.LC : Set (ι → F)) ≤ InterleavedCode.minDist IC.1.MF := by + classical + let S := {d : ℕ | ∃ U ∈ IC.1.MF, ∃ V ∈ IC.1.MF, U ≠ V ∧ InterleavedCode.distCodewords U V = d} + -- Lower bound for each element of the witness set: base minDist ≤ Δ(U,V) + have hLB : ∀ s ∈ S, Code.minDist (IC.1.LC : Set (ι → F)) ≤ s := by + intro s hs; rcases hs with ⟨U, hU, V, hV, hNe, rfl⟩ + -- pick a row where they differ + have hex : ∃ i : κ, U i ≠ V i := by + by_contra hAll; push_neg at hAll; exact hNe (by funext i j; simp [hAll i]) + rcases hex with ⟨i, hi⟩ + -- rows are in LC by lawfulness + have hUi : U i ∈ IC.1.LC := IC.2 U hU i + have hVi : V i ∈ IC.1.LC := IC.2 V hV i + -- base ≤ row distance ≤ column distance + have hbase_le : Code.minDist (IC.1.LC : Set (ι → F)) ≤ hammingDist (U i) (V i) := by + refine Nat.sInf_le ?_; exact ⟨U i, hUi, V i, hVi, hi, rfl⟩ + have hrow_le_cols : hammingDist (U i) (V i) ≤ InterleavedCode.distCodewords U V := by + -- as finsets + simpa [hammingDist, InterleavedCode.distCodewords, Matrix.neqCols] using + (Finset.card_mono (rowSupport_subset_neqCols U V i)) + exact le_trans hbase_le hrow_le_cols + -- Nonempty witness set + have hneS : S.Nonempty := by + rcases hNE with ⟨U, hU, V, hV, hNe⟩ + exact ⟨InterleavedCode.distCodewords U V, ⟨U, hU, V, hV, hNe, rfl⟩⟩ + -- Conclude base ≤ sInf = minDist + simpa [InterleavedCode.minDist, Set.mem_setOf_eq] using (sInf.le_sInf_of_LB hneS hLB) + + +def IC0 : InterleavedCode (Fin 1) (Fin 1) (ZMod 2) := { MF := ⊥, LC := ⊤ } + +lemma IC0_isInterleaved : IC0.isInterleaved := by + intro V _ i + simp [IC0] + +def LC0 : LawfulInterleavedCode (Fin 1) (Fin 1) (ZMod 2) := ⟨IC0, IC0_isInterleaved⟩ + +example : + Code.minDist (LC0.1.LC : Set (Fin 1 → ZMod 2)) ≠ InterleavedCode.minDist LC0.1.MF := by + -- Right-hand side: Δ(⊥) = 0 (no distinct matrices in ⊥) + -- Compute minDist of ⊥ explicitly: witness set is empty + have hMF : InterleavedCode.minDist LC0.1.MF = 0 := by + unfold InterleavedCode.minDist + -- Show emptiness of the witness set + have hempty : {d : ℕ | ∃ U ∈ LC0.1.MF, ∃ V ∈ LC0.1.MF, + U ≠ V ∧ InterleavedCode.distCodewords U V = d} = (∅ : Set ℕ) := by + apply Set.eq_empty_iff_forall_notMem.mpr + intro d hd + rcases hd with ⟨U, hU, V, hV, hne, _⟩ + have hU0 : U = 0 := by simpa [IC0] using hU + have hV0 : V = 0 := by simpa [IC0] using hV + exact hne (by simp [hU0, hV0]) + simp [hempty] + -- Left-hand side: min distance of ⊤ on length-1 vectors over ZMod 2 is 1 + have hLC_le : Code.minDist (LC0.1.LC : Set (Fin 1 → ZMod 2)) ≤ 1 := by + -- Witness: u = 0, v = 1 + let u : Fin 1 → ZMod 2 := fun _ => 0 + let v : Fin 1 → ZMod 2 := fun _ => 1 + have hu : u ∈ (LC0.1.LC : Set (Fin 1 → ZMod 2)) := by simp [LC0, IC0] + have hv : v ∈ (LC0.1.LC : Set (Fin 1 → ZMod 2)) := by simp [LC0, IC0] + have hne : u ≠ v := by + intro h + have h0 : u 0 ≠ v 0 := by decide + exact h0 (congrArg (fun f => f 0) h) + -- minDist ≤ Δ₀(u,v) ≤ 1 via general bound + have h₁ : Code.minDist (LC0.1.LC : Set (Fin 1 → ZMod 2)) ≤ hammingDist u v := by + refine Nat.sInf_le ?_; + exact ⟨u, hu, v, hv, hne, rfl⟩ + have h₂' : hammingDist u v ≤ Fintype.card (Fin 1) := by + simpa using (hammingDist_le_card_fintype (ι := Fin 1)) + have h₂ : hammingDist u v ≤ 1 := by + simpa [Fintype.card_fin] using h₂' + exact le_trans h₁ h₂ + -- Lower bound: every distinct pair in ⊤ differs in the only coordinate ⇒ distance ≥ 1 + have hLC_ge : 1 ≤ Code.minDist (LC0.1.LC : Set (Fin 1 → ZMod 2)) := by + -- Use the general `le_sInf_of_LB` with the witness set for Code.minDist + let S := {d : ℕ | ∃ u ∈ (LC0.1.LC : Set (Fin 1 → ZMod 2)), + ∃ v ∈ (LC0.1.LC : Set (Fin 1 → ZMod 2)), + u ≠ v ∧ hammingDist u v = d} + -- S is nonempty: same witness as above + have hS_ne : S.Nonempty := by + let u : Fin 1 → ZMod 2 := fun _ => 0 + let v : Fin 1 → ZMod 2 := fun _ => 1 + have hu : u ∈ (LC0.1.LC : Set (Fin 1 → ZMod 2)) := by simp [LC0, IC0] + have hv : v ∈ (LC0.1.LC : Set (Fin 1 → ZMod 2)) := by simp [LC0, IC0] + have hne : u ≠ v := by + intro h + have h0 : u 0 ≠ v 0 := by decide + exact h0 (congrArg (fun f => f 0) h) + exact ⟨hammingDist u v, ⟨u, hu, v, hv, hne, rfl⟩⟩ + -- Every element of S is ≥ 1 + have hLB : ∀ s ∈ S, 1 ≤ s := by + intro s hs; rcases hs with ⟨u, hu, v, hv, hne, rfl⟩ + -- On Fin 1, distinct functions differ at 0, so distance is 1 + have h0neq : u 0 ≠ v 0 := by + by_contra hEq + apply hne; funext j; have : j = 0 := Fin.fin_one_eq_zero j; simp [this, hEq] + have hmem : (0 : Fin 1) ∈ (Finset.univ.filter fun j : Fin 1 => u j ≠ v j) := by + simp [h0neq] + have hpos : 0 < (Finset.univ.filter (fun j : Fin 1 => u j ≠ v j)).card := + Finset.card_pos.mpr ⟨0, hmem⟩ + have : 1 ≤ hammingDist u v := by + simpa [hammingDist] using Nat.succ_le_of_lt hpos + simpa using this + -- Apply the helper lemma from Prelims + have : 1 ≤ sInf S := sInf.le_sInf_of_LB hS_ne hLB + simpa [Code.minDist, Set.mem_setOf_eq] using this + -- Thus Code.minDist = 1, while Interleaved minDist = 0 + have hLC : Code.minDist (LC0.1.LC : Set (Fin 1 → ZMod 2)) = 1 := le_antisymm hLC_le hLC_ge + -- Conclude inequality 1 ≠ 0 + simp [hLC, hMF] + +end GeneralInequalityAndCounterexample diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43.lean new file mode 100644 index 000000000..eff91eb20 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43.lean @@ -0,0 +1,223 @@ +/- +Direct (paper-style) blueprint for Lemma 4.3: main assembly lemma only. +-/ + +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.Aux +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.Argmax +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.RowFreshCoord +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.BadAlpha +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.Gate3e +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import Mathlib.Tactic + +noncomputable section + +open InterleavedCode +open Code +open scoped BigOperators + +set_option linter.style.longLine false +set_option linter.unnecessarySimpa false + +namespace InterleavedCode +namespace Lemma43 + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {κ : Type*} [Fintype κ] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/- +Main assembly lemma: if `|F| ≥ e+2`, `3e < d(LC)`, and `Δ(U, MF) > e` with +`MF = matrixSubmoduleOfLinearCode κ LC`, then some row-combination of `U` +is strictly farther than `e` from `LC`. +-/ +lemma distInterleavedCodeToCodeLB + {IC : LawfulInterleavedCode κ ι F} {U : Matrix κ ι F} {e : ℕ} + (hF : Nat.card F ≥ e.succ.succ) + (he : 3 * e < Code.minDist (IC.1.LC : Set (ι → F))) + (hU : e < distToCode U IC.1.MF) + (hMF : IC.1.MF = matrixSubmoduleOfLinearCode κ IC.1.LC) : + ∃ v ∈ Matrix.rowSpan U , e < distFromCode v IC.1.LC := by + classical + -- Contradiction posture: assume no row-combination is > e far from LC. + by_contra hnone + have hAll : ∀ v ∈ Matrix.rowSpan U, distFromCode v IC.1.LC ≤ e := by + intro v hv; have : ¬ e < distFromCode v IC.1.LC := by exact fun hvgt => hnone ⟨v, hv, hvgt⟩ + simpa using (not_lt.mp this) + -- Pick v₀ maximizing distance in the row span. + rcases exists_argmax_dist_in_rowSpan (L := (IC.1.LC : Set (ι → F))) (U := U) with ⟨v0, hv0, hmax⟩ + -- Choose a codeword c₀ within ≤ e of v₀; set E₀ := Err v₀ c₀ and t := |E₀| with t ≤ e. + have hdist_v0 : distFromCode v0 IC.1.LC ≤ e := hAll v0 hv0 + rcases ProximityToRS.exists_codeword_close_of_dist_le + (u := v0) (C := (IC.1.LC : Set (ι → F))) (e := e) hdist_v0 with ⟨c0, hc0, hv0c0_le⟩ + let E0 : Finset ι := Err (ι := ι) v0 c0 + let t : ℕ := E0.card + have hE0_le : t ≤ e := by + -- t = E0.card = hammingDist v0 c0 ≤ e + simpa [E0, Err, hammingDist, errset_card_eq_hamming] using hv0c0_le + -- For each row, choose a codeword within ≤ e (by hAll applied to U i ∈ rowSpan U). + have hUi_in : ∀ i, (U i) ∈ Matrix.rowSpan U := by + intro i; exact Submodule.subset_span (by change U i ∈ {U k | k : κ}; simp) + have hex_row : ∀ i, ∃ ci ∈ (IC.1.LC : Set (ι → F)), hammingDist (U i) ci ≤ e := by + intro i + have hdist : distFromCode (U i) IC.1.LC ≤ e := hAll (U i) (hUi_in i) + simpa using + (ProximityToRS.exists_codeword_close_of_dist_le + (u := U i) (C := (IC.1.LC : Set (ι → F))) (e := e) hdist) + classical + choose c_row hcrow hrowle using hex_row + -- Build V' with rows equal to c_row; show V' ∈ MF by hMF + let V' : Matrix κ ι F := fun i j => c_row i j + have hV'_in : V' ∈ IC.1.MF := by + have hrows : ∀ i, V' i ∈ IC.1.LC := by intro i; simpa [V'] using (hcrow i) + have : V' ∈ matrixSubmoduleOfLinearCode κ IC.1.LC := by + have : V' ∈ {W : Matrix κ ι F | ∀ i, W i ∈ IC.1.LC} := by simpa [V'] + exact Submodule.subset_span this + simpa [hMF] using this + -- Use Δ(U,MF) ≤ distCodewords U V' to conclude many bad columns for V' + have hDist_le : Δ(U, IC.1.MF) ≤ distCodewords U V' := by + change sInf {d : ℕ | ∃ W ∈ IC.1.MF, distCodewords U W = d} ≤ distCodewords U V' + refine Nat.sInf_le ?_ + exact ⟨V', hV'_in, rfl⟩ + -- Therefore |neqCols U V'| > e + set S := Matrix.neqCols U V' with hSdef + have hScard_gt : e < S.card := by + have : Δ(U, IC.1.MF) ≤ distCodewords U V' := hDist_le + have : e < distCodewords U V' := lt_of_lt_of_le hU this + simpa [S, hSdef] using this + -- Pick a fresh column j ∈ S \ E0 and the corresponding row i + have hnot_subset : ¬ S ⊆ Err (ι := ι) v0 c0 := by + intro hsubset + have hmono := Finset.card_mono hsubset + have : S.card ≤ (Err (ι := ι) v0 c0).card := hmono + exact (not_lt_of_ge (le_trans this hE0_le)) hScard_gt + have hsel : ∃ j, j ∈ S ∧ j ∉ Err (ι := ι) v0 c0 := by + by_contra h + have : S ⊆ Err (ι := ι) v0 c0 := by + intro j hj + by_contra hjmem + exact h ⟨j, hj, hjmem⟩ + exact hnot_subset this + rcases hsel with ⟨j, hjS, hjNotE0⟩ + have hx' : ∃ i : κ, V' i j ≠ U i j := by + simpa [S, hSdef, Matrix.neqCols] using hjS + rcases hx' with ⟨i, hVU'⟩ + have hjUcr : j ∈ Err (ι := ι) (U i) (c_row i) := by + have hjuniv : j ∈ (Finset.univ : Finset ι) := by simp + have : U i j ≠ c_row i j := by simpa [V', ne_comm] using hVU' + simpa [Err, Finset.mem_filter, hjuniv] using this + -- j is fresh relative to E0 and differs in row i against c_row i + -- Choose α ∉ Bad with α ≠ 0; weight increases by ≥ 1 at the fresh coordinate j. + obtain ⟨α, hα0, hα_not_bad⟩ := + exists_good_alpha (ι := ι) (e := e) (hF := hF) (E0 := E0) + (χ0 := fun j => v0 j - c0 j) (χi := fun j => U i j - c_row i j) (t_le_e := hE0_le) + have hj_new : (U i j - c_row i j) ≠ 0 := by + -- j ∈ Err(U i, c_row i) ⇒ difference at j is nonzero + have : j ∈ Err (U i) (c_row i) := hjUcr + have : (U i j ≠ c_row i j) := by + have hjuniv : j ∈ (Finset.univ : Finset ι) := by simp + simpa [Err, Finset.mem_filter, hjuniv] using this + simpa [sub_eq_zero] using this + have hj_old : (v0 j - c0 j) = 0 := by + -- j ∉ E0 ⇒ v0 j = c0 j + have hjuniv : j ∈ (Finset.univ : Finset ι) := by simp + have hmem_iff : j ∈ (Finset.univ.filter fun t : ι => v0 t ≠ c0 t) ↔ v0 j ≠ c0 j := by + simpa [Finset.mem_filter, hjuniv] + have : ¬ v0 j ≠ c0 j := by + have hnotmem : j ∉ (Finset.univ.filter fun t : ι => v0 t ≠ c0 t) := by simpa [E0, Err] using hjNotE0 + have hnotiff : (j ∈ (Finset.univ.filter fun t : ι => v0 t ≠ c0 t)) ↔ (v0 j ≠ c0 j) := hmem_iff + have : ¬ (v0 j ≠ c0 j) := (not_congr hnotiff).mp hnotmem + exact this + exact sub_eq_zero.mpr (Classical.not_not.mp this) + have h_wt : t.succ ≤ hammingNorm (fun t => (v0 t - c0 t) + α * (U i t - c_row i t)) := by + have hbase : hammingNorm (fun j => v0 j - c0 j) = t := by + -- ‖v0 - c0‖₀ = hammingDist v0 c0 = E0.card = t + have : hammingNorm (fun j => v0 j - c0 j) = hammingDist v0 c0 := + hammingNorm_sub_eq_hamming _ _ + simpa [E0, t, Err, hammingDist, errset_card_eq_hamming] using this + have hw_ineq := + (weight_increase_by_one (E0 := E0) (χ0 := fun j => v0 j - c0 j) (χi := fun j => U i j - c_row i j) + (j := j) (hj_new := hj_new) (hj_old := hj_old) (α := α) (hα := hα_not_bad) + (hE0 := by + classical + ext k; simp [E0, Err, sub_eq_zero])) + simpa [hbase, Nat.add_comm] using hw_ineq + -- Gate identity: within radius e, the distance equals the distance to c0 + α·c_row i. + have hgate_eq : + distFromCode (fun j => v0 j + α * U i j) (IC.1.LC : Set (ι → F)) + = hammingDist (fun j => v0 j + α * U i j) (fun j => c0 j + α * c_row i j) := by + -- Use gate_distance_identity_3e with hv, hu and he + have hv' : hammingDist v0 c0 ≤ e := hv0c0_le + have hu' : hammingDist (U i) (c_row i) ≤ e := hrowle i + -- Apply gate + -- Establish membership of v0 + α • U i in the row span (closure under add/smul). + have hUi_span : (U i) ∈ Matrix.rowSpan U := hUi_in i + have hαUi_span : (fun j => α * U i j) ∈ Matrix.rowSpan U := by + exact (Submodule.smul_mem (Matrix.rowSpan U) α hUi_span) + have hsum_span : (fun j => v0 j + α * U i j) ∈ Matrix.rowSpan U := by + exact (Submodule.add_mem (Matrix.rowSpan U) hv0 hαUi_span) + have := gate_distance_identity_3e (L := IC.1.LC) (e := e) (he := he) + (hc0 := hc0) (hci := hcrow i) (hv := hv') (hu := hu') (α := α) + (hsmall := hAll (fun j => v0 j + α * U i j) hsum_span) + simpa using this + -- Combine with weight lower bound to obtain a strict inequality vs v0 by maximality + -- First, lower-bound the distance from code at wα by t+1 + have hge : (t.succ : ℕ∞) ≤ distFromCode (fun j => v0 j + α * U i j) (IC.1.LC : Set (ι → F)) := by + -- distFromCode equals hamming distance to c0 + α·c_row i + have : + distFromCode (fun j => v0 j + α * U i j) (IC.1.LC : Set (ι → F)) + = (hammingDist (fun j => v0 j + α * U i j) (fun j => c0 j + α * c_row i j) : ℕ∞) := by + simpa using hgate_eq + -- And that hamming distance equals the Hamming weight of (χ0 + α χi) + have hdiff_eq : + (fun j => (v0 j + α * U i j) - (c0 j + α * c_row i j)) + = (fun j => (v0 j - c0 j) + α * (U i j - c_row i j)) := by + funext j; ring + have hhd_eq : + hammingDist (fun j => v0 j + α * U i j) (fun j => c0 j + α * c_row i j) + = hammingNorm (fun j => (v0 j - c0 j) + α * (U i j - c_row i j)) := by + -- Step 1: Δ(wα,cα) = ‖(wα) - (cα)‖₀ + have hwteq1 : + hammingDist (fun j => v0 j + α * U i j) (fun j => c0 j + α * c_row i j) + = hammingNorm ((fun j => v0 j + α * U i j) - (fun j => c0 j + α * c_row i j)) := by + simpa using (hammingNorm_sub_eq_hamming (v := (fun j => v0 j + α * U i j)) (c := (fun j => c0 j + α * c_row i j))).symm + -- Step 2: rewrite difference pointwise to χ0 + α χi + have hwteq2 : + hammingNorm ((fun j => v0 j + α * U i j) - (fun j => c0 j + α * c_row i j)) + = hammingNorm (fun j => (v0 j - c0 j) + α * (U i j - c_row i j)) := by + -- transport equality through hammingNorm by congrArg + exact congrArg hammingNorm hdiff_eq + exact hwteq1.trans hwteq2 + -- So the distance-from-code is ≥ t+1 by h_wt + have hnat : (t.succ : ℕ) ≤ hammingDist (fun j => v0 j + α * U i j) (fun j => c0 j + α * c_row i j) := by + simpa [hhd_eq] using h_wt + have : (t.succ : ℕ∞) ≤ (hammingDist (fun j => v0 j + α * U i j) + (fun j => c0 j + α * c_row i j) : ℕ∞) := by + exact_mod_cast hnat + simpa [hgate_eq] using this + -- Also, upper-bound the distance from code at v0 by t using c0 as a witness + have hv0_le_t : distFromCode v0 (IC.1.LC : Set (ι → F)) ≤ (t : ℕ∞) := by + -- sInf ≤ distance to c0 and that equals t = hammingDist v0 c0 by definition + have hmem : (hammingDist v0 c0 : ℕ∞) ∈ {d : ℕ∞ | ∃ z ∈ (IC.1.LC : Set (ι → F)), hammingDist v0 z ≤ d} := by + exact ⟨c0, hc0, by exact_mod_cast (le_of_eq rfl)⟩ + have hsInf_le := sInf_le hmem + simpa [Code.distFromCode, t] using hsInf_le + -- Now: distFromCode v0 ≤ t < t+1 ≤ distFromCode wα gives strict inequality + have h_mem : (fun j => v0 j + α * U i j) ∈ Matrix.rowSpan U := by + exact Submodule.add_mem _ hv0 ((Submodule.smul_mem _ α) (hUi_in i)) + have h_lt_tsucc : distFromCode v0 (IC.1.LC : Set (ι → F)) < (t.succ : ℕ∞) := by + have : (distFromCode v0 (IC.1.LC : Set (ι → F))) ≤ (t : ℕ∞) := hv0_le_t + have : (distFromCode v0 (IC.1.LC : Set (ι → F))) < (t : ℕ∞) + 1 := + lt_of_le_of_lt this (by exact_mod_cast Nat.lt_succ_self t) + simpa using this + have h_strict : distFromCode v0 (IC.1.LC : Set (ι → F)) + < distFromCode (fun j => v0 j + α * U i j) (IC.1.LC : Set (ι → F)) := + lt_of_lt_of_le h_lt_tsucc hge + -- Contradiction with maximality of v0 over the row span + have h_le_all := hmax (fun j => v0 j + α * U i j) h_mem + exact (not_lt_of_ge h_le_all) h_strict + +end Lemma43 +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Argmax.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Argmax.lean new file mode 100644 index 000000000..ae10bde84 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Argmax.lean @@ -0,0 +1,48 @@ +/- +Argmax over the row span for the distance-to-code functional. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace InterleavedCode +namespace Lemma43 + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {κ : Type*} +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Existence of an argmax of `distFromCode · L` inside the finite `rowSpan U`. -/ +lemma exists_argmax_dist_in_rowSpan + (L : Set (ι → F)) (U : Matrix κ ι F) : + ∃ v ∈ Matrix.rowSpan U, + ∀ w ∈ Matrix.rowSpan U, distFromCode v L ≥ distFromCode w L := by + classical + let fFintype : Fintype F := Fintype.ofFinite F + -- Work over the finite type of elements of the row span as a subtype. + let S : Finset (Matrix.rowSpan U) := (Finset.univ : Finset (Matrix.rowSpan U)) + have hS_ne : S.Nonempty := by + refine ⟨⟨0, by simp⟩, ?_⟩ + simp [S] + -- Maximize the distance-to-code over S. + obtain ⟨vS, hvS, hmaxS⟩ := + Finset.exists_max_image (s := S) + (f := fun (x : Matrix.rowSpan U) => distFromCode (x : ι → F) L) + hS_ne + -- Project to an element v0 : ι → F in the row span. + refine ⟨(vS : ι → F), (vS.property), ?_⟩ + intro w hw + -- View w as a subtype element to apply maximality. + have hwS : (⟨w, hw⟩ : Matrix.rowSpan U) ∈ S := by simp [S] + have := hmaxS (⟨w, hw⟩) hwS + -- Conclude the inequality in the requested orientation. + simpa using this + +end Lemma43 +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Aux.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Aux.lean new file mode 100644 index 000000000..7efb64680 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Aux.lean @@ -0,0 +1,73 @@ +/- +Auxiliaries for Lemma 4.3: error sets and Hamming-norm helpers. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace InterleavedCode +namespace Lemma43 + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {κ : Type*} [Fintype κ] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/- A small finite-set helper. -/ +lemma exists_not_mem_of_card_lt_univ + {α : Type*} [Finite α] [DecidableEq α] + (s : Finset α) (h : s.card < Nat.card α) : ∃ a : α, a ∉ s := by + classical + by_contra hnone + push_neg at hnone + let fFintype : Fintype α := Fintype.ofFinite α + have : s = (Finset.univ : Finset α) := by + ext a; constructor <;> intro ha + · exact Finset.mem_univ a + · exact hnone a + have hc : s.card = Nat.card α := by simp [this] + have h' : s.card < s.card := by simpa [hc] using h + exact (lt_irrefl (s.card)).elim h' + +/-- Hamming distance equals the size of the error set. -/ +def Err (v c : ι → F) : Finset ι := Finset.univ.filter (fun j => v j ≠ c j) + +omit [Field F] [Fintype F] [DecidableEq ι] in +lemma errset_card_eq_hamming (v c : ι → F) : + hammingDist v c = (Err (ι := ι) v c).card := by + classical + simp [Err, hammingDist] + +/-- Error vector `χ(v,c)`. -/ +def chi (v c : ι → F) : ι → F := fun j => v j - c j + +omit [Fintype F] [DecidableEq ι] in +/-- Hamming norm of the difference equals Hamming distance. -/ +lemma hammingNorm_sub_eq_hamming (v c : ι → F) : + hammingNorm (fun j => v j - c j) = hammingDist v c := by + classical + -- (v j - c j) = 0 ↔ v j = c j + have hset : + (Finset.univ.filter fun j : ι => (v j - c j) ≠ 0) + = (Finset.univ.filter fun j : ι => v j ≠ c j) := by + ext j; simp [sub_eq_zero] + simp [hammingNorm, hammingDist, hset] + +omit [Fintype F] [DecidableEq ι] in +/-- Scaling by a nonzero does not change Hamming weight. -/ +lemma hammingNorm_smul_eq_of_ne_zero (α : F) (hα : α ≠ 0) (x : ι → F) : + hammingNorm (fun j => α * x j) = hammingNorm x := by + classical + have hset : + (Finset.univ.filter fun j : ι => α * x j ≠ 0) + = (Finset.univ.filter fun j : ι => x j ≠ 0) := by + ext j; simp [mul_eq_zero, hα] + simpa [hammingNorm] using congrArg Finset.card hset + +end Lemma43 +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/BadAlpha.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/BadAlpha.lean new file mode 100644 index 000000000..01fcec53a --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/BadAlpha.lean @@ -0,0 +1,176 @@ +/- +Bad-α control and weight growth lemmas for Lemma 4.3. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.Aux +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace InterleavedCode +namespace Lemma43 + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {κ : Type*} [Fintype κ] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- For fixed `a, b ≠ 0`, there is at most one `α` with `a + α*b = 0`. -/ +lemma one_cancellation_per_coordinate (a b : F) (hb : b ≠ 0) : + {α : F | a + α*b = 0}.Finite ∧ Nat.card {α : F | a + α*b = 0} ≤ 1 := by + classical + -- Finiteness since F is finite + have hfinite : ({α : F | a + α * b = 0} : Set F).Finite := by + simpa using (Set.finite_univ.subset (by intro x hx; simp)) + -- At most one solution: if a + α b = 0 and a + α' b = 0 then α = α' + have hsub : Subsingleton {α : F // a + α * b = 0} := by + refine ⟨?_⟩ + intro x y + apply Subtype.ext + have hx : a + x.val * b = 0 := x.property + have hy : a + y.val * b = 0 := y.property + -- (x - y) * b = 0 + have hxy : (x.val - y.val) * b = 0 := by + have hx' : x.val * b = -a := by simpa [add_comm, eq_neg_iff_add_eq_zero] using hx + have hy' : y.val * b = -a := by simpa [add_comm, eq_neg_iff_add_eq_zero] using hy + calc + (x.val - y.val) * b = x.val * b - y.val * b := by ring + _ = (-a) - (-a) := by simp [hx', hy'] + _ = 0 := by simp + -- From (x - y) * b = 0 and hb, deduce x - y = 0 + have hsubzero : x.val - y.val = 0 := by + have hdisj := mul_eq_zero.mp hxy + cases hdisj with + | inl h0 => exact h0 + | inr hb0 => exact (hb hb0).elim + -- conclude x.val = y.val + have : x.val = y.val := by + have := sub_eq_zero.mp hsubzero + exact this + simpa using this + have hcard_le : Nat.card {α : F // a + α * b = 0} ≤ 1 := + Finite.card_le_one_iff_subsingleton.mpr (by apply Subsingleton.intro; intro x y; exact hsub.elim x y) + exact ⟨hfinite, hcard_le⟩ + +/-- The finite set of “bad” α values that cause cancellations on `E₀`, plus α = 0. -/ +def Bad (E0 : Finset ι) (χ0 χi : ι → F) : Finset F := + insert 0 <| + (E0.filter (fun t => χi t ≠ 0)).image (fun t => - χ0 t / χi t) + +omit [Fintype F] [Fintype ι] [DecidableEq ι] in +lemma bad_alpha_card_le (E0 : Finset ι) (χ0 χi : ι → F) : + (Bad (ι := ι) E0 χ0 χi).card ≤ E0.card.succ := by + classical + set S := (E0.filter (fun t => χi t ≠ 0)).image (fun t => - χ0 t / χi t) with hS + have h1 : (insert (0:F) S).card ≤ S.card.succ := Finset.card_insert_le _ _ + have h2 : S.card ≤ (E0.filter (fun t => χi t ≠ 0)).card := by + have := Finset.card_image_le (s := E0.filter (fun t => χi t ≠ 0)) (f := fun t => - χ0 t / χi t) + simpa [hS] using this + have h3 : (E0.filter (fun t => χi t ≠ 0)).card ≤ E0.card := Finset.card_filter_le _ _ + have : (Bad (ι := ι) E0 χ0 χi).card ≤ S.card.succ := by + simpa [Bad, hS] using h1 + exact le_trans this (Nat.succ_le_succ (le_trans h2 h3)) + +omit [Fintype F] [DecidableEq ι] in +/-- Outside `Bad`, the Hamming weight of `χ0 + α • χi` is at least `weight χ0 + 1`. -/ +lemma weight_increase_by_one + (E0 : Finset ι) (χ0 χi : ι → F) + (j : ι) (hj_new : χi j ≠ 0) (hj_old : χ0 j = 0) + {α : F} (hα : α ∉ Bad (ι := ι) E0 χ0 χi) + (hE0 : E0 = (Finset.univ.filter fun t : ι => χ0 t ≠ 0)) : + hammingNorm (fun t => χ0 t + α * χi t) ≥ hammingNorm χ0 + 1 := by + classical + -- α ≠ 0 since 0 ∈ Bad + have hα_ne0 : α ≠ 0 := by + intro h; exact hα (by simpa [Bad, h] using Finset.mem_insert_self (0:F) _) + -- Define supports + let supp0 : Finset ι := Finset.univ.filter (fun t : ι => χ0 t ≠ 0) + let suppα : Finset ι := Finset.univ.filter (fun t : ι => χ0 t + α * χi t ≠ 0) + have hE0' : E0 = supp0 := hE0 + -- Claim 1: No cancellations on E0 = supp0 + have h_nocancel : supp0 ⊆ suppα := by + intro t ht + have ht_univ : t ∈ (Finset.univ : Finset ι) := by simp + have hχ0_ne : χ0 t ≠ 0 := by + have := (Finset.mem_filter.mp ht).2; simpa [supp0] using this + by_cases hχi0 : χi t = 0 + · have : χ0 t + α * χi t ≠ 0 := by simpa [hχi0] using hχ0_ne + exact (Finset.mem_filter.mpr ⟨ht_univ, by simpa [suppα]⟩) + · have ht_in_E0 : t ∈ E0 := by simpa [hE0', supp0] using ht + have h_in_image : (- χ0 t / χi t) ∈ (E0.filter (fun s => χi s ≠ 0)).image (fun s => - χ0 s / χi s) := by + have ht_in_filter : t ∈ E0.filter (fun s => χi s ≠ 0) := by + exact Finset.mem_filter.mpr ⟨ht_in_E0, hχi0⟩ + exact Finset.mem_image.mpr ⟨t, ht_in_filter, rfl⟩ + have hα_ne_forbid : α ≠ - χ0 t / χi t := by + intro h_eq + have hin : (- χ0 t / χi t) + ∈ insert (0:F) ((E0.filter (fun s => χi s ≠ 0)).image (fun s => - χ0 s / χi s)) := + Finset.mem_insert_of_mem h_in_image + have hα_in : α ∈ insert (0:F) ((E0.filter (fun s => χi s ≠ 0)).image (fun s => - χ0 s / χi s)) := by + simpa [h_eq] using hin + have : α ∈ Bad (ι := ι) E0 χ0 χi := by simpa [Bad] using hα_in + exact hα this + have : χ0 t + α * χi t ≠ 0 := by + intro hsum + have hαeq : α = - χ0 t / χi t := by + have hmul : α * χi t = - χ0 t := by + have : α * χi t + χ0 t = 0 := by simpa [add_comm] using hsum + exact (eq_neg_iff_add_eq_zero).mpr this + have := congrArg (fun z => z * (χi t)⁻¹) hmul + have hχ0 : χi t ≠ 0 := hχi0 + simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, hχ0] using this + exact hα_ne_forbid hαeq + exact (Finset.mem_filter.mpr ⟨ht_univ, by simpa [suppα]⟩) + -- Claim 2: j is newly nonzero in suppα and not in supp0 + have hj_not_in_supp0 : j ∉ supp0 := by + have : j ∈ (Finset.univ : Finset ι) := by simp + have : j ∈ Finset.univ.filter (fun t : ι => χ0 t = 0) := by + simp [Finset.mem_filter, this, hj_old] + by_contra hjin + have : χ0 j ≠ 0 := by + have := (Finset.mem_filter.mp hjin).2; simpa [supp0] using this + exact this hj_old + have hj_in_suppα : j ∈ suppα := by + have : χ0 j + α * χi j ≠ 0 := by + have : α * χi j ≠ 0 := mul_ne_zero hα_ne0 hj_new + simpa [hj_old, add_comm] using this + have hjuniv : j ∈ (Finset.univ : Finset ι) := by simp + exact (Finset.mem_filter.mpr ⟨hjuniv, by simpa [suppα]⟩) + -- Cardinality: supp0 ⊆ suppα and j ∈ suppα \ supp0 ⇒ |suppα| ≥ |supp0| + 1 + have hsubset : supp0 ⊆ suppα := by simpa [hE0'] using h_nocancel + have hstrict_lt : supp0.card < suppα.card := by + have hss : supp0 ⊂ suppα := by + refine Finset.ssubset_iff_subset_ne.mpr ?_ + refine And.intro hsubset ?_ + intro hEq; exact hj_not_in_supp0 (by simpa [hEq] using hj_in_suppα) + exact Finset.card_lt_card hss + have hstrict : (supp0.card + 1) ≤ suppα.card := Nat.succ_le_of_lt hstrict_lt + simpa [hammingNorm, supp0, suppα, Nat.add_comm] using hstrict + +omit [Fintype ι] [DecidableEq ι] in +lemma exists_good_alpha + {e : ℕ} + (hF : Nat.card F ≥ e.succ.succ) + (E0 : Finset ι) (χ0 χi : ι → F) + (t_le_e : E0.card ≤ e) : + ∃ α : F, α ≠ 0 ∧ α ∉ Bad (ι := ι) E0 χ0 χi := by + classical + have hBad_le : (Bad (ι := ι) E0 χ0 χi).card ≤ e.succ := + (bad_alpha_card_le (E0 := E0) (χ0 := χ0) (χi := χi)).trans (Nat.succ_le_succ t_le_e) + have : (Bad (ι := ι) E0 χ0 χi).card < Nat.card F := by + have h1 : e.succ < e.succ.succ := Nat.lt_succ_self _ + have h2 : e.succ.succ ≤ Nat.card F := by simpa using hF + exact lt_of_le_of_lt hBad_le (lt_of_lt_of_le h1 h2) + obtain ⟨α, hα_notin⟩ := + exists_not_mem_of_card_lt_univ (s := (Bad (ι := ι) E0 χ0 χi)) this + have hα_ne0 : α ≠ 0 := by + intro h0 + exact hα_notin (by simp [Bad, h0]) + exact ⟨α, hα_ne0, hα_notin⟩ + +end Lemma43 +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Gate3e.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Gate3e.lean new file mode 100644 index 000000000..a164c1974 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/Gate3e.lean @@ -0,0 +1,191 @@ +/- +3e-gate lemmas (uniqueness and identity) used in Lemma 4.3. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.Aux +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace InterleavedCode +namespace Lemma43 + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {κ : Type*} [Fintype κ] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- +3e-gate (uniqueness): if `dist v c0 ≤ e` and `dist u ci ≤ e` with `3e < d(L)`, +then for every `α` any codeword within `≤ e` of `v + α•u` must equal `c0 + α•ci`. +-/ +lemma gate_unique_close_codeword_3e + (L : LinearCode ι F) {e : ℕ} + (he : 3 * e < Code.minDist (L : Set (ι → F))) + {v u c0 ci : ι → F} (hc0 : c0 ∈ (L : Set (ι → F))) (hci : ci ∈ (L : Set (ι → F))) + (hv : hammingDist v c0 ≤ e) (hu : hammingDist u ci ≤ e) : + ∀ α : F, ∀ c ∈ (L : Set (ι → F)), hammingDist (v + fun j => α * u j) c ≤ e → + c = fun j => c0 j + α * ci j := by + classical + intro α c hcL hclose + -- Notation + let wα : ι → F := fun j => v j + α * u j + let cα : ι → F := fun j => c0 j + α * ci j + -- cα ∈ L by linearity + have hcα : cα ∈ (L : Set (ι → F)) := by + have hc0' : c0 ∈ L := by simpa using hc0 + have hci' : (fun j => α * ci j) ∈ L := by + simpa [Pi.smul_apply, smul_eq_mul] using (Submodule.smul_mem L α (by simpa using hci)) + simpa [cα, Pi.add_def] using (Submodule.add_mem L (by simpa using hc0') (by simpa using hci')) + -- Bound Δ(wα, cα) ≤ e + e + have hΔ_wα_cα_le : hammingDist wα cα ≤ e + e := by + have hv' : Code.wt (fun j => v j - c0 j) ≤ e := by simpa [LinearCode.hammingDist_eq_wt_sub] using hv + have hu' : Code.wt (fun j => u j - ci j) ≤ e := by simpa [LinearCode.hammingDist_eq_wt_sub] using hu + have hsub := + (ProximityToRS.wt_add_le (x := fun j => v j - c0 j) (y := fun j => α * (u j - ci j))) + have hsmul : Code.wt (fun j => α * (u j - ci j)) ≤ Code.wt (fun j => u j - ci j) := by + by_cases hα : α = 0 + · have hzero : (fun j : ι => α * (u j - ci j)) = 0 := by funext j; simpa [hα] + have : Code.wt (fun j : ι => α * (u j - ci j)) = 0 := by simp [Code.wt_eq_hammingNorm, hzero] + simpa [this] using (Nat.zero_le (Code.wt (fun j => u j - ci j))) + · have : hammingNorm (fun j => α * (u j - ci j)) = hammingNorm (fun j => u j - ci j) := + hammingNorm_smul_eq_of_ne_zero α hα (fun j => u j - ci j) + simpa [Code.wt_eq_hammingNorm] using le_of_eq this + have : Code.wt (fun j => (v j - c0 j) + α * (u j - ci j)) ≤ e + e := + (le_trans hsub (add_le_add hv' (le_trans hsmul hu'))) + -- Convert to Hamming distance bound via difference identity + have hdiff : (fun j => wα j - cα j) = (fun j => (v j - c0 j) + α * (u j - ci j)) := by + funext j; simp [wα, cα, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add] + have hwt_wαcα : Code.wt (wα - cα) ≤ e + e := by + simpa [Pi.sub_def, hdiff] using this + simpa [LinearCode.hammingDist_eq_wt_sub] using hwt_wαcα + -- Triangle: Δ(c, cα) ≤ Δ(c, wα) + Δ(wα, cα) ≤ 3e + have hΔ_ccα_lt : hammingDist c cα < Code.minDist (L : Set (ι → F)) := by + have htri := hammingDist_triangle c wα cα + have hclose' : hammingDist c wα ≤ e := by simpa [wα, hammingDist_comm] using hclose + have hbound : hammingDist c cα ≤ e + (e + e) := le_trans htri (by exact add_le_add hclose' hΔ_wα_cα_le) + have h3e_lt : e + (e + e) < Code.minDist (L : Set (ι → F)) := by + simpa [Nat.succ_mul, two_mul, add_comm, add_left_comm, add_assoc] using he + exact lt_of_le_of_lt hbound h3e_lt + -- Conclude equality + by_contra hneq + have hmin_le : Code.minDist (L : Set (ι → F)) ≤ hammingDist c cα := by + have hwit : ∃ u ∈ (L : Set (ι → F)), ∃ v ∈ (L : Set (ι → F)), u ≠ v ∧ hammingDist u v = hammingDist c cα := by + exact ⟨c, hcL, cα, hcα, hneq, rfl⟩ + exact Nat.sInf_le (Set.mem_setOf.mpr hwit) + exact (not_lt_of_ge hmin_le) hΔ_ccα_lt + +/-- +3e-gate (identity): under the hypotheses of the previous lemma, whenever +`distFromCode (v + α•u) L ≤ e` it must equal the distance to `c0 + α•ci`. +-/ +lemma gate_distance_identity_3e + (L : LinearCode ι F) {e : ℕ} + (he : 3 * e < Code.minDist (L : Set (ι → F))) + {v u c0 ci : ι → F} (hc0 : c0 ∈ (L : Set (ι → F))) (hci : ci ∈ (L : Set (ι → F))) + (hv : hammingDist v c0 ≤ e) (hu : hammingDist u ci ≤ e) + (α : F) + (hsmall : distFromCode (v + fun j => α * u j) (L : Set (ι → F)) ≤ e) : + distFromCode (v + fun j => α * u j) (L : Set (ι → F)) + = hammingDist (v + fun j => α * u j) (fun j => c0 j + α * ci j) := by + classical + -- Notation: wα and cα + let wα : ι → F := fun j => v j + α * u j + let cα : ι → F := fun j => c0 j + α * ci j + -- cα ∈ L by linearity + have hcα : cα ∈ (L : Set (ι → F)) := by + have hmem_add : (c0 + fun j => α * ci j) ∈ (L : Set (ι → F)) := by + have hc0' : c0 ∈ L := by simpa using hc0 + have hci' : (fun j => α * ci j) ∈ L := by + simpa [Pi.smul_apply, smul_eq_mul] using (Submodule.smul_mem L α (by simpa using hci)) + simpa using (Submodule.add_mem L (by simpa using hc0') (by simpa using hci')) + simpa [cα, Pi.add_def] using hmem_add + -- Pick a close codeword to wα within radius e + rcases ProximityToRS.exists_codeword_close_of_dist_le + (u := wα) (C := (L : Set (ι → F))) (e := e) hsmall + with ⟨c, hcL, hwαc_le⟩ + -- Bound Δ(wα, cα) ≤ 2e using subadditivity and scaling bound + have hΔ_wα_cα_le : hammingDist wα cα ≤ e + e := by + have hv' : Code.wt (fun j => v j - c0 j) ≤ e := by + simpa [LinearCode.hammingDist_eq_wt_sub] using hv + have hu' : Code.wt (fun j => u j - ci j) ≤ e := by + simpa [LinearCode.hammingDist_eq_wt_sub] using hu + have hsub : + Code.wt (fun j => (v j - c0 j) + α * (u j - ci j)) + ≤ Code.wt (fun j => v j - c0 j) + Code.wt (fun j => α * (u j - ci j)) := by + simpa using (ProximityToRS.wt_add_le (x := (fun j => v j - c0 j)) (y := (fun j => α * (u j - ci j)))) + have hsmul : Code.wt (fun j => α * (u j - ci j)) ≤ Code.wt (fun j => u j - ci j) := by + by_cases hα : α = 0 + · have hzero : (fun j : ι => α * (u j - ci j)) = 0 := by funext j; simpa [hα] + have : Code.wt (fun j : ι => α * (u j - ci j)) = 0 := by simp [Code.wt_eq_hammingNorm, hzero] + simpa [this] using (Nat.zero_le (Code.wt (fun j => u j - ci j))) + · have : hammingNorm (fun j => α * (u j - ci j)) = hammingNorm (fun j => u j - ci j) := + hammingNorm_smul_eq_of_ne_zero α hα (fun j => u j - ci j) + simpa [Code.wt_eq_hammingNorm] using le_of_eq this + have : Code.wt (fun j => (v j - c0 j) + α * (u j - ci j)) ≤ e + e := + (le_trans hsub (add_le_add hv' (le_trans hsmul hu'))) + have hdiff : (fun j => wα j - cα j) = (fun j => (v j - c0 j) + α * (u j - ci j)) := by + funext j; simp [wα, cα, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add] + have hwt_wαcα : Code.wt (wα - cα) ≤ e + e := by + simpa [Pi.sub_def, hdiff] using this + simpa [LinearCode.hammingDist_eq_wt_sub] using hwt_wαcα + -- Show distFromCode equals Δ(wα, v) for a minimizer v ∈ L + -- Work in the finite set of codewords + have hCfin : ((L : Set (ι → F)) : Set (ι → F)).Finite := Set.toFinite _ + -- pick a concrete element in L as a seed for min_image + let w0 := c + have hw0L : w0 ∈ (L : Set (ι → F)) := hcL + have hw0mem : w0 ∈ hCfin.toFinset := by simpa using hCfin.mem_toFinset.mpr hw0L + obtain ⟨vmin, hv_in, hmin⟩ := + Finset.exists_min_image (s := hCfin.toFinset) + (f := fun x : (ι → F) => hammingDist wα x) + ⟨w0, hw0mem⟩ + have hvL : vmin ∈ (L : Set (ι → F)) := hCfin.mem_toFinset.mp hv_in + -- distFromCode ≤ Δ(wα, v) + have h_le : distFromCode wα (L : Set (ι → F)) ≤ (hammingDist wα vmin : ℕ∞) := by + have hmem : (hammingDist wα vmin : ℕ∞) + ∈ {d : ℕ∞ | ∃ z ∈ (L : Set (ι → F)), hammingDist wα z ≤ d} := by + exact ⟨vmin, hvL, by simp⟩ + simpa [Code.distFromCode] using sInf_le hmem + -- (Δ(wα, v)) ≤ distFromCode via minimality + have h_ge : (hammingDist wα vmin : ℕ∞) ≤ distFromCode wα (L : Set (ι → F)) := by + -- Any element of the defining set is ≥ Δ(wα, v) + have hLB : ∀ d ∈ {d : ℕ∞ | ∃ z ∈ (L : Set (ι → F)), hammingDist wα z ≤ d}, + (hammingDist wα vmin : ℕ∞) ≤ d := by + intro d hd; rcases hd with ⟨z, hzL, hΔz_le_d⟩ + -- by minimality, Δ(wα, v) ≤ Δ(wα, z) + have hz_in : z ∈ hCfin.toFinset := hCfin.mem_toFinset.mpr hzL + have : hammingDist wα vmin ≤ hammingDist wα z := hmin z hz_in + exact le_trans (by exact_mod_cast this) hΔz_le_d + -- Apply le_csInf + have : (hammingDist wα vmin : ℕ∞) + ≤ sInf {d : ℕ∞ | ∃ z ∈ (L : Set (ι → F)), hammingDist wα z ≤ d} := by + apply le_csInf + · refine ⟨(hammingDist wα w0 : ℕ∞), ?_⟩; exact ⟨w0, hw0L, by simp⟩ + · intro d hd; exact hLB d hd + simpa [Code.distFromCode] using this + have h_eq_min : distFromCode wα (L : Set (ι → F)) = (hammingDist wα vmin : ℕ∞) := + le_antisymm h_le h_ge + -- Since distFromCode ≤ e, the minimizer v is within radius e and is unique, so v = cα + have hΔv_le_e : hammingDist wα vmin ≤ e := by + have hdist_le : distFromCode wα (L : Set (ι → F)) ≤ e := by + simpa [wα] using hsmall + have : (hammingDist wα vmin : ℕ∞) ≤ e := by simpa [h_eq_min] using hdist_le + exact (by exact_mod_cast this) + have hv_eq : vmin = cα := + gate_unique_close_codeword_3e (L := L) (e := e) (he := he) (hc0 := hc0) (hci := hci) + (hv := hv) (hu := hu) α vmin hvL hΔv_le_e + -- Conclude the desired identity by rewriting the minimizer to cα and unfolding notation + have h5 : + distFromCode (v + fun j => α * u j) (L : Set (ι → F)) + = (hammingDist (v + fun j => α * u j) cα : ℕ∞) := by + -- combine the minimizer identity and uniqueness (vmin = cα) + simpa [wα, hv_eq] using h_eq_min + simpa [cα] using h5 + +end Lemma43 +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/RowFreshCoord.lean b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/RowFreshCoord.lean new file mode 100644 index 000000000..a7ecf88e1 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/Lemma43/RowFreshCoord.lean @@ -0,0 +1,65 @@ +/- +Fresh error coordinate from column mismatch set. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43.Aux +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace InterleavedCode +namespace Lemma43 + +variable {F : Type*} [DecidableEq F] +variable {κ : Type*} [Fintype κ] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- +Fresh error with an explicit witness matrix: if `V` has each row in `L`, and +`distCodewords U V > e ≥ |E₀|`, then there is a row `i` and column `j` with +`j ∈ Err (U i) (V i)` but `j ∉ E₀`. +-/ +lemma exists_row_and_fresh_coord + {e : ℕ} + (U V : Matrix κ ι F) + (v0 c0 : ι → F) + (hE0_le : (Err (ι := ι) v0 c0).card ≤ e) + (hUV : e < distCodewords U V) : + ∃ i : κ, ∃ j : ι, j ∈ Err (ι := ι) (U i) (V i) ∧ j ∉ Err (ι := ι) v0 c0 := by + classical + -- Let S := Matrix.neqCols U V, with S.card = distCodewords U V > e. + set S := Matrix.neqCols U V + have hScard : S.card = distCodewords U V := by rfl + have hSgt : e < S.card := by simpa [hScard] + -- If every j ∈ S belongs to E0, then S.card ≤ E0.card ≤ e + have hnot_subset : ¬ S ⊆ Err (ι := ι) v0 c0 := by + intro hsubset + have hmono := Finset.card_mono hsubset + have : S.card ≤ (Err (ι := ι) v0 c0).card := hmono + exact (not_lt_of_ge (le_trans this hE0_le)) hSgt + -- So pick j ∈ S with j ∉ E0 + have hsel : ∃ j, j ∈ S ∧ j ∉ Err (ι := ι) v0 c0 := by + by_contra h + have : S ⊆ Err (ι := ι) v0 c0 := by + intro j hj + by_contra hjmem + exact h ⟨j, hj, hjmem⟩ + exact hnot_subset this + rcases hsel with ⟨j, hjS, hjNotE0⟩ + -- By definition of S, we get a row i with a mismatch at column j + have hx' : ∃ i : κ, V i j ≠ U i j := by simpa [S, Matrix.neqCols] using hjS + rcases hx' with ⟨i, hVU⟩ + have hi : U i j ≠ V i j := by simpa [ne_comm] using hVU + -- Conclude j ∈ Err(U i, V i) + have hjErr : j ∈ Err (ι := ι) (U i) (V i) := by + have hjuniv : j ∈ (Finset.univ : Finset ι) := by simp + simp [Err, Finset.mem_filter, hjuniv, hi] + exact ⟨i, j, hjErr, hjNotE0⟩ + +end Lemma43 +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/MinDistEq.lean b/ArkLib/Data/CodingTheory/InterleavedCode/MinDistEq.lean new file mode 100644 index 000000000..c46ee03d6 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/MinDistEq.lean @@ -0,0 +1,206 @@ +/- +Major lemma: equality of minimal distances between a linear code and +its associated interleaved-code row-span construction. +-/ + +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.Basic +import Mathlib.Tactic + +noncomputable section + +namespace InterleavedCode + +variable {F : Type*} [Semiring F] + {κ ι : Type*} [Fintype κ] [Fintype ι] + (LC : LinearCode ι F) + +lemma minDist_eq_minDist [DecidableEq F] [Nonempty κ] : + Code.minDist (LC : Set (ι → F)) = minDist (matrixSubmoduleOfLinearCode κ LC) := by + classical + -- Abbreviations + set C := (LC : Set (ι → F)) + set M := matrixSubmoduleOfLinearCode κ LC + -- We prove both inequalities and conclude by antisymmetry on `≤` for naturals. + apply le_antisymm + · -- Lower bound: `Code.minDist C ≤ minDist M`. + -- Split on whether there are any distinct base codewords. + by_cases hC_nontriv : ∃ u ∈ C, ∃ v ∈ C, u ≠ v + · -- Show that the witness set for `minDist M` is nonempty by constructing matrices + -- from `u ≠ v`. + rcases hC_nontriv with ⟨u, hu, v, hv, hne⟩ + obtain ⟨i₀⟩ := (inferInstance : Nonempty κ) + let U0 : Matrix κ ι F := fun i j => if i = i₀ then u j else 0 + let V0 : Matrix κ ι F := fun i j => if i = i₀ then v j else 0 + -- U0,V0 are in the generator set, thus in the span M + have h0mem : ∀ i, U0 i ∈ C := by + intro i; by_cases h : i = i₀ + · subst h; simpa [C, U0] + · have hzC : (0 : ι → F) ∈ C := by simp [C] + simpa [U0, h] using hzC + have h1mem : ∀ i, V0 i ∈ C := by + intro i; by_cases h : i = i₀ + · subst h; simpa [C, V0] + · have hzC : (0 : ι → F) ∈ C := by simp [C] + simpa [V0, h] using hzC + have hU0in : U0 ∈ M := by + have : U0 ∈ {W : Matrix κ ι F | ∀ i, W i ∈ LC} := by simpa [C] using h0mem + exact Submodule.subset_span this + have hV0in : V0 ∈ M := by + have : V0 ∈ {W : Matrix κ ι F | ∀ i, W i ∈ LC} := by simpa [C] using h1mem + exact Submodule.subset_span this + -- Lower bound for each element of the witness set: base minDist ≤ Δ(U,V) + have hLB : ∀ s ∈ {d : ℕ | ∃ U ∈ M, ∃ V ∈ M, U ≠ V ∧ InterleavedCode.distCodewords U V = d}, + Code.minDist C ≤ s := by + intro s hs + rcases hs with ⟨U, hU, V, hV, hNe', rfl⟩ + -- Pick a row where they differ + have hex : ∃ i : κ, U i ≠ V i := by + by_contra hAll + push_neg at hAll + exact hNe' (by funext i j; simp [hAll i]) + rcases hex with ⟨i, hi⟩ + -- rows are in LC by the construction of M + have hrows := isInterleaved_codeOfLinearCode (κ := κ) (LC := LC) + have hUi : U i ∈ LC := hrows U hU i + have hVi : V i ∈ LC := hrows V hV i + -- base ≤ row distance ≤ column distance + have hbase_le : Code.minDist C ≤ hammingDist (U i) (V i) := by + refine Nat.sInf_le ?_ + refine ⟨U i, ?_, V i, ?_, hi, rfl⟩ + · simpa [C] using hUi + · simpa [C] using hVi + have hrow_le_cols : + hammingDist (U i) (V i) ≤ InterleavedCode.distCodewords U V := by + -- as finsets + simpa [hammingDist, InterleavedCode.distCodewords, Matrix.neqCols] using + (Finset.card_mono (rowSupport_subset_neqCols U V i)) + exact le_trans hbase_le hrow_le_cols + -- Nonempty witness set for M (given u ≠ v we can take U0,V0) + have hneS : + {d : ℕ | ∃ U ∈ M, ∃ V ∈ M, U ≠ V ∧ InterleavedCode.distCodewords U V = d}.Nonempty := by + refine ⟨InterleavedCode.distCodewords U0 V0, ?_⟩ + exact ⟨U0, hU0in, V0, hV0in, by + intro hEq; apply hne; funext j + simpa [U0, V0] using congrArg (fun W => W i₀ j) hEq + , rfl⟩ + -- Conclude base ≤ sInf = minDist + simpa [InterleavedCode.minDist, Set.mem_setOf_eq, C, M] + using (sInf.le_sInf_of_LB hneS hLB) + · -- Base code has no distinct elements: both min distances are 0. + have hC0 : Code.minDist C = 0 := by + unfold Code.minDist + have hemptyC : {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d} = (∅ : Set ℕ) := by + apply Set.eq_empty_iff_forall_notMem.mpr + intro d hd; rcases hd with ⟨u, hu, v, hv, hne, _⟩ + exact hC_nontriv ⟨u, hu, v, hv, hne⟩ + simp [hemptyC] + -- The witness set for M is empty as well (every row is 0) + have hemptyM : + {d : ℕ | ∃ U ∈ M, ∃ V ∈ M, U ≠ V ∧ InterleavedCode.distCodewords U V = d} + = (∅ : Set ℕ) := by + apply Set.eq_empty_iff_forall_notMem.mpr + intro d hd + rcases hd with ⟨U, hU, V, hV, hne, _⟩ + have hrows := isInterleaved_codeOfLinearCode (κ := κ) (LC := LC) + -- Since LC has no distinct elements, every element of LC is 0 + have hOnlyZero : ∀ x ∈ LC, x = (0 : ι → F) := by + intro x hx; by_contra hx0 + exact hC_nontriv ⟨x, by simpa [C] using hx, 0, by simp [C], hx0⟩ + have hU0 : U = 0 := by + funext i j; have : U i ∈ LC := hrows U hU i; simp [hOnlyZero _ this] + have hV0 : V = 0 := by + funext i j; have : V i ∈ LC := hrows V hV i; simp [hOnlyZero _ this] + exact hne (by simp [hU0, hV0]) + have hM0 : minDist M = 0 := by + unfold minDist; simp [hemptyM] + simp [hM0, hC0, C, M] + · -- Upper bound: `minDist M ≤ Code.minDist C`. + -- It suffices to show `minDist M ≤ d` for each `d` realized by distinct base codewords. + -- Use `le_sInf_of_LB` with witness set for `Code.minDist C`. + have hLB : ∀ d ∈ {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d}, + minDist M ≤ d := by + intro d hd + rcases hd with ⟨u, hu, v, hv, hne, rfl⟩ + -- Build single-row matrices from u and v and relate their distance to hammingDist u v. + obtain ⟨i₀⟩ := (inferInstance : Nonempty κ) + let U : Matrix κ ι F := fun i j => if i = i₀ then u j else 0 + let V : Matrix κ ι F := fun i j => if i = i₀ then v j else 0 + -- Show each row lies in LC, then lift to membership in the span M + have hrowsU : ∀ i, U i ∈ LC := by + intro i; by_cases h : i = i₀ + · subst h; simpa [U, C] using hu + · have hUi0 : U i = 0 := by + ext j; simp [U, h] + simp [hUi0] + have hrowsV : ∀ i, V i ∈ LC := by + intro i; by_cases h : i = i₀ + · subst h; simpa [V, C] using hv + · have hVi0 : V i = 0 := by + ext j; simp [V, h] + simp [hVi0] + have hUin : U ∈ M := by + have : U ∈ {W : Matrix κ ι F | ∀ i, W i ∈ LC} := by simpa using hrowsU + exact Submodule.subset_span this + have hVin : V ∈ M := by + have : V ∈ {W : Matrix κ ι F | ∀ i, W i ∈ LC} := by simpa using hrowsV + exact Submodule.subset_span this + -- Distances coincide for these single-row matrices + have hdist_eq : InterleavedCode.distCodewords U V = hammingDist u v := + support_eq_for_single_row_diff (i₀ := i₀) U V + (by + intro i; by_cases h : i = i₀ + · subst h; ext j; simp [U] + · ext j; simp [U, h]) + (by + intro i; by_cases h : i = i₀ + · subst h; ext j; simp [V] + · ext j; simp [V, h]) + -- Conclude `minDist M ≤ distCodewords U V = hammingDist u v` + have hle : minDist M ≤ InterleavedCode.distCodewords U V := by + change sInf {d : ℕ | ∃ U' ∈ M, ∃ V' ∈ M, U' ≠ V' ∧ InterleavedCode.distCodewords U' V' = d} + ≤ InterleavedCode.distCodewords U V + refine Nat.sInf_le ?_ + exact ⟨U, hUin, V, hVin, by + intro h; apply hne; funext j + simpa [U, V] using congrArg (fun W => W i₀ j) h, rfl⟩ + -- rewrite the RHS using hdist_eq + have : minDist M ≤ hammingDist u v := by simpa [hdist_eq] using hle + exact this + -- Conclude + have : minDist M ≤ Code.minDist C := by + -- If base witness set nonempty, use hLB. + -- Else both sides are 0, so the inequality is trivial. + by_cases hC_nontriv' : ∃ u ∈ C, ∃ v ∈ C, u ≠ v + · have hneC : + {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d}.Nonempty := by + rcases hC_nontriv' with ⟨u, hu, v, hv, hne⟩ + exact ⟨hammingDist u v, ⟨u, hu, v, hv, hne, rfl⟩⟩ + have hineq := sInf.le_sInf_of_LB hneC (i := minDist M) hLB + simpa [Code.minDist, C] using hineq + · -- base set empty ⇒ Code.minDist C = 0, and also minDist M = 0 (as above), so ≤ holds + have hC0 : Code.minDist C = 0 := by + unfold Code.minDist + have hemptyC : {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d} = (∅ : Set ℕ) := by + apply Set.eq_empty_iff_forall_notMem.mpr + intro d hd; rcases hd with ⟨u, hu, v, hv, hne, _⟩; exact hC_nontriv' ⟨u, hu, v, hv, hne⟩ + simp [hemptyC] + have hemptyM : + {d : ℕ | ∃ U ∈ M, ∃ V ∈ M, U ≠ V ∧ InterleavedCode.distCodewords U V = d} + = (∅ : Set ℕ) := by + apply Set.eq_empty_iff_forall_notMem.mpr + intro d hd; rcases hd with ⟨U, hU, V, hV, hneUV, _⟩ + have hrows := isInterleaved_codeOfLinearCode (κ := κ) (LC := LC) + have hOnlyZero : ∀ x ∈ LC, x = (0 : ι → F) := by + intro x hx; by_contra hx0 + exact hC_nontriv' ⟨x, by simpa [C] using hx, 0, by simp [C], hx0⟩ + have hU0 : U = 0 := by + funext i j; have : U i ∈ LC := hrows U hU i; simp [hOnlyZero _ this] + have hV0 : V = 0 := by + funext i j; have : V i ∈ LC := hrows V hV i; simp [hOnlyZero _ this] + exact hneUV (by simp [hU0, hV0]) + have hM0 : minDist M = 0 := by unfold minDist; simp [hemptyM] + simp [hM0, hC0] + exact this + +end InterleavedCode diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Aux.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Aux.lean new file mode 100644 index 000000000..bc8da91aa --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Aux.lean @@ -0,0 +1,360 @@ +/- +Auxiliary lemmas for the Proximity-to-RS results. +Some are placeholders to be filled in subsequent iterations. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import Mathlib.Tactic +import Mathlib.Algebra.BigOperators.Ring.Finset + +noncomputable section +open scoped Polynomial BigOperators + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] +variable {deg : ℕ} {α : ι ↪ F} + +/-! Reindexing helpers -/ + +private def reindex {ι ι' F} (e : ι ≃ ι') (f : ι → F) : ι' → F := fun j => f (e.symm j) + +lemma wt_reindex_eq {ι ι' : Type*} [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] + {F : Type*} [Zero F] [DecidableEq F] (e : ι ≃ ι') (f : ι → F) : + Code.wt (reindex e f) = Code.wt f := by + classical + unfold Code.wt + -- Compare supports via map along the embedding of the equivalence. + have hset : + ({j : ι' | reindex e f j ≠ 0} : Finset ι') + = (Finset.map e.toEmbedding ({i : ι | f i ≠ 0} : Finset ι)) := by + ext j; constructor + · intro hj + refine Finset.mem_map.mpr ?_ + refine ⟨e.symm j, ?_, by simp⟩ + simpa [reindex] using hj + · intro hj + rcases Finset.mem_map.mp hj with ⟨i, hi, hij⟩ + -- From `hij : e.toEmbedding i = j`, derive `e.symm j = i`. + have h_ei : e i = j := by simpa using hij + have hsymm : e.symm j = i := by simpa [h_ei] using e.left_inv i + -- And `hi : f i ≠ 0` gives the desired predicate at `j`. + have hi' : f i ≠ 0 := by simpa using hi + simpa [reindex, hsymm] + -- Cardinalities of mapped finsets are equal to the source + simpa [hset] + using (Finset.card_map (s := ({i : ι | f i ≠ 0} : Finset ι)) (f := e.toEmbedding)) + +lemma hammingDist_reindex_eq {ι ι' : Type*} [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] + {F : Type*} [DecidableEq F] + (e : ι ≃ ι') (u v : ι → F) : + hammingDist (reindex e u) (reindex e v) = hammingDist u v := by + classical + -- Compare the filtered supports defining Hamming distance under reindexing + have hset : + (Finset.univ.filter fun j : ι' => reindex e u j ≠ reindex e v j) + = Finset.map e.toEmbedding + (Finset.univ.filter fun i : ι => u i ≠ v i) := by + ext j; constructor + · intro hj + refine Finset.mem_map.mpr ?_ + refine ⟨e.symm j, ?_, by simp⟩ + simpa [reindex] using hj + · intro hj + rcases Finset.mem_map.mp hj with ⟨i, hi, hij⟩ + have h_ei : e i = j := by simpa using hij + have hsymm : e.symm j = i := by simpa [h_ei] using e.left_inv i + have hi' : u i ≠ v i := by simpa using hi + simpa [reindex, hsymm, hi'] + -- Cardinalities of mapped finsets are equal to the source + simpa [hammingDist, hset] + using (Finset.card_map (s := (Finset.univ.filter fun i : ι => u i ≠ v i)) (f := e.toEmbedding)) + +/-- Translation invariance of distance to the RS code: adding a codeword does not change +the distance to the code. -/ +lemma translate_invariant_RS (w c : ι → F) + (hc : c ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F))) : + Code.distFromCode (w + c) (ReedSolomon.code α deg) + = Code.distFromCode w (ReedSolomon.code α deg) := by + classical + -- Direct application of the general translation invariance for linear codes + simpa using + Code.distFromCode_add_codeword_eq + (LC := ReedSolomon.code α deg) (w := w) (c := c) hc + +/-- If a vector is within distance `e` from a code `C`, there exists a codeword within +that distance. -/ +lemma exists_codeword_close_of_dist_le {u : ι → F} {C : Set (ι → F)} {e : ℕ} + (h : Code.distFromCode u C ≤ e) : ∃ w ∈ C, Δ₀(u, w) ≤ e := by + classical + -- If C were empty, Δ₀(u,C) = ⊤, contradicting h ≤ e. Hence C is nonempty. + have hCne : C.Nonempty := by + by_cases hCempty : C = (∅ : Set (ι → F)) + · have htop : Code.distFromCode u C = ⊤ := by + simpa [hCempty] using (Code.distFromCode_of_empty (u := u)) + have htople : (⊤ : ℕ∞) ≤ e := by simpa [htop] using h + -- ⊤ ≤ e is impossible + have : False := by simpa using htople + exact this.elim + · exact Set.nonempty_iff_ne_empty.mpr hCempty + -- Pick v ∈ C minimizing d(v) = hammingDist u v + have hCfin : (C : Set (ι → F)).Finite := Set.toFinite _ + obtain ⟨w0, hw0C⟩ := hCne + have hw0mem : w0 ∈ hCfin.toFinset := by simpa using hCfin.mem_toFinset.mpr hw0C + obtain ⟨v, hv_in, hmin⟩ := + Finset.exists_min_image (s := hCfin.toFinset) (f := fun x : (ι → F) => hammingDist u x) + (by exact ⟨w0, hw0mem⟩) + have hvC : v ∈ C := hCfin.mem_toFinset.mp hv_in + have hminC : ∀ w ∈ C, hammingDist u v ≤ hammingDist u w := by + intro w hwC + have hw_in : w ∈ hCfin.toFinset := hCfin.mem_toFinset.mpr hwC + exact hmin w hw_in + -- Let S be the witness set defining Δ₀(u,C); show (Δ₀(u,v)) is a lower bound of S. + let S : Set ℕ∞ := {d | ∃ w ∈ C, hammingDist u w ≤ d} + have hLB : ∀ d ∈ S, (hammingDist u v : ℕ∞) ≤ d := by + intro d hd; rcases hd with ⟨w, hwC, hdle⟩ + have : hammingDist u v ≤ hammingDist u w := hminC w hwC + exact le_trans (by exact_mod_cast this) hdle + -- Therefore (Δ₀(u,v)) ≤ sInf S = Δ₀(u,C) ≤ e + have hv_le_dist : (hammingDist u v : ℕ∞) ≤ Code.distFromCode u C := by + -- sInf S is the greatest lower bound of S + have hv_le_sInf : (hammingDist u v : ℕ∞) ≤ sInf S := by + apply le_csInf + · refine ⟨(hammingDist u w0 : ℕ∞), ?_⟩; exact ⟨w0, hw0C, by simpa⟩ + · intro d hd; exact hLB d hd + simpa [Code.distFromCode, S] using hv_le_sInf + have : (hammingDist u v : ℕ∞) ≤ e := le_trans hv_le_dist h + exact ⟨v, hvC, by exact_mod_cast this⟩ + +/-- Minimal distance of a Reed–Solomon code over a general index type `ι`. +This transports the known `Fin`-indexed statement via a reindexing equivalence. -/ +lemma minDist_RS_general [NeZero deg] [Nonempty ι] : + Code.minDist ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) + = Fintype.card ι - deg + 1 := by + classical + -- Reindex to `Fin m` and apply the Fin-indexed theorem. + let m := Fintype.card ι + let e : ι ≃ Fin m := Fintype.equivFin ι + -- Reindexed evaluation domain on `Fin m` as a function with injectivity. + let αfun' : Fin m → F := fun j => α (e.symm j) + have inj' : Function.Injective αfun' := by + intro i j h + have h' : α (e.symm i) = α (e.symm j) := h + have : e.symm i = e.symm j := by exact α.injective h' + simpa using congrArg e this + let αemb' : (Fin m) ↪ F := ⟨αfun', inj'⟩ + -- Transport codewords via the reindexing equivalence on coordinates. + let φ : (ι → F) → (Fin m → F) := fun f j => f (e.symm j) + have hφ_dist : ∀ u v, hammingDist (φ u) (φ v) = hammingDist u v := by + intro u v; classical + -- Specialize the general reindexing lemma to `e : ι ≃ Fin m`. + simpa [φ, reindex] using + (hammingDist_reindex_eq (ι := ι) (ι' := Fin m) (F := F) e u v) + -- Characterize membership under φ: RS over α maps to RS over α'. + have hmem : ∀ f, f ∈ (ReedSolomon.code α deg : Submodule F (ι → F)) + ↔ (φ f) ∈ (ReedSolomon.code αemb' deg : Submodule F (Fin m → F)) := by + intro f; constructor + · rintro ⟨p, hp, rfl⟩; exact ⟨p, hp, by ext j; rfl⟩ + · rintro ⟨p, hp, hfp⟩; refine ⟨p, hp, ?_⟩; ext i + have hx := congrArg (fun g => g (e i)) hfp + -- (φ f) (e i) = f i; RHS evaluates via αemb' + simpa [φ, ReedSolomon.evalOnPoints, αemb', αfun'] using hx + -- Distances are preserved by φ, hence minDist of the code equals that of the image code. + have hdist_eq : + Code.minDist ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) + = Code.minDist ((ReedSolomon.code αemb' deg : Submodule F (Fin m → F)) : Set (Fin m → F)) := by + -- Show the witness sets for sInf are the same via φ on pairs. + unfold Code.minDist + apply congrArg sInf + ext d; constructor <;> intro hd + · rcases hd with ⟨u, hu, v, hv, hne, hle⟩ + refine ⟨φ u, (hmem u).mp hu, φ v, (hmem v).mp hv, ?_, ?_⟩ + · intro h; apply hne; ext i + have := congrArg (fun g => g (e i)) h + simpa [φ] using this + · simpa [hφ_dist u v] using hle + · rcases hd with ⟨u, hu, v, hv, hne, hle⟩ + -- pull back witnesses by φ⁻¹ = precompose with e + refine ⟨(fun i => u (e i)), ?_, (fun i => v (e i)), ?_, ?_, ?_⟩ + · have hφu : φ (fun i => u (e i)) = u := by funext j; simp [φ] + have : (φ (fun i => u (e i))) ∈ (ReedSolomon.code αemb' deg : Submodule F (Fin m → F)) := by + simpa [hφu] using hu + exact (hmem (fun i => u (e i))).mpr this + · have hφv : φ (fun i => v (e i)) = v := by funext j; simp [φ] + have : (φ (fun i => v (e i))) ∈ (ReedSolomon.code αemb' deg : Submodule F (Fin m → F)) := by + simpa [hφv] using hv + exact (hmem (fun i => v (e i))).mpr this + · intro h; apply hne; ext j; simpa using congrArg (fun g => g (e.symm j)) h + · have hΔ := hammingDist_reindex_eq (ι := Fin m) (ι' := ι) (F := F) e.symm u v + have hΔ' : Δ₀((fun i => u (e i)), (fun i => v (e i))) = Δ₀(u, v) := by + simpa [reindex] using hΔ + calc + Δ₀((fun i => u (e i)), (fun i => v (e i))) = Δ₀(u, v) := hΔ' + _ = d := hle + -- Apply the Fin-indexed theorem. + -- Handle both cases uniformly: ReedSolomonCode.minDist expects `deg ≤ m`. + by_cases hle : deg ≤ m + · -- Use the Fin-indexed minDist theorem and transport back. + have hfin := + (ReedSolomonCode.minDist (F := F) (α := αfun') (inj := inj') (n := deg) (m := m) (h := hle)) + simpa [hdist_eq] using hfin + · -- deg > m: the code equals the full space, so minDist = 1 + -- We avoid reconstructing a basis; this follows from standard RS theory. + -- It also matches the right-hand side since m - deg + 1 = 1 in this case. + have hgt : m < deg := Nat.lt_of_not_ge hle + have hrhs : m - deg + 1 = 1 := by + have : m ≤ deg := le_of_lt hgt + simpa [m, Nat.sub_eq_zero_of_le this] + -- Show the RS code at degree m equals the full space, hence at degree deg (> m) as well. + have hdim_code_m : Module.finrank F (ReedSolomon.code αemb' m) = m := by + simpa using (ReedSolomonCode.dim_eq_deg_of_le (F := F) (α := αfun') (inj := inj') (n := m) + (m := m) (h := le_rfl)) + have hfinrank_ambient : Module.finrank F (Fin m → F) = m := by + classical + simpa using (Pi.finrank (Fin m) F) + have htop : (ReedSolomon.code αemb' m) = ⊤ := by + classical + -- both finranks are equal to m + have : Module.finrank F (ReedSolomon.code αemb' m) = Module.finrank F (Fin m → F) := by + simpa [hfinrank_ambient] using hdim_code_m + exact Submodule.eq_top_of_finrank_eq (K := F) (V := (Fin m → F)) this + -- Monotonicity in degree gives: code m ⊆ code deg, hence code deg = ⊤ as well + have htop_deg : (ReedSolomon.code αemb' deg : Submodule F (Fin m → F)) = ⊤ := by + -- `degreeLT _ m ≤ degreeLT _ deg` since m < deg + have hsub : (Polynomial.degreeLT F m) ≤ (Polynomial.degreeLT F deg) := by + intro p hp + have hp' : p.degree < (m : WithBot ℕ) := by simpa [Polynomial.mem_degreeLT] using hp + have hmle : ((m : ℕ) : WithBot ℕ) ≤ deg := by exact_mod_cast (le_of_lt hgt) + have : p.degree < deg := lt_of_lt_of_le hp' hmle + simpa [Polynomial.mem_degreeLT] using this + -- map preserves ≤, so codes are nested + have hle := Submodule.map_mono (f := ReedSolomon.evalOnPoints αemb') hsub + -- from code m = ⊤ and code m ≤ code deg, deduce code deg = ⊤ + apply top_unique + have : (ReedSolomon.code αemb' m : Submodule F (Fin m → F)) ≤ (ReedSolomon.code αemb' deg) := by + simpa [ReedSolomon.code] using hle + simpa [htop] using this + -- Full space has minimum distance 1 from the definition of Δ₀ + have hfin_eq : + Code.minDist ((ReedSolomon.code αemb' deg : Submodule F (Fin m → F)) : Set (Fin m → F)) = 1 := by + classical + -- Upper bound: exhibit 0 and a one-sparse delta vector at distance 1 + have hUB : Code.minDist ((⊤ : Submodule F (Fin m → F)) : Set (Fin m → F)) ≤ 1 := by + unfold Code.minDist + refine Nat.sInf_le ?_ + -- pick i0 and delta + let i0 : Fin m := ⟨0, by + have : 0 < m := by simpa [m] using Fintype.card_pos_iff.mpr (inferInstance : Nonempty ι) + simpa⟩ + let δ : Fin m → F := fun j => if j = i0 then 1 else 0 + have hδ_ne : (0 : Fin m → F) ≠ δ := by + intro h; have := congrArg (fun f => f i0) h; simpa [δ] using this + have hdist_delta : hammingDist (0 : Fin m → F) δ = 1 := by + unfold δ + -- Show directly that exactly one coordinate differs from zero + have hsetU : + (Finset.univ.filter + (fun i : Fin m => (0 : F) ≠ (if i = i0 then (1 : F) else 0))) + = {i0} := by + ext j; by_cases hji : j = i0 <;> simp [hji] + -- Also record the cardinality of the equality-locus set for simp's alternative normalization + have hEqCard : (({i : Fin m | i = i0} : Finset (Fin m)).card) = 1 := by + classical + have hEq : ({i : Fin m | i = i0} : Finset (Fin m)) = ({i0} : Finset (Fin m)) := by + ext j; by_cases hji : j = i0 <;> simp [hji] + simpa [hEq, Finset.card_singleton] + simpa [hammingDist, hsetU, Finset.card_singleton] + exact ⟨0, by simp, δ, by simp [δ], by exact hδ_ne, hdist_delta⟩ + -- Lower bound: any two distinct vectors differ in ≥ 1 coordinate + have hLB : 1 ≤ Code.minDist ((⊤ : Submodule F (Fin m → F)) : Set (Fin m → F)) := by + unfold Code.minDist + -- Nonempty set of distances (reuse delta witness) + let i0 : Fin m := ⟨0, by + have : 0 < m := by simpa [m] using Fintype.card_pos_iff.mpr (inferInstance : Nonempty ι) + simpa⟩ + let δ : Fin m → F := fun j => if j = i0 then 1 else 0 + have hδ_ne : (0 : Fin m → F) ≠ δ := by + intro h; have := congrArg (fun f => f i0) h; simpa [δ] using this + have hne : {d | ∃ u ∈ ((⊤ : Submodule F (Fin m → F)) : Set (Fin m → F)), ∃ v ∈ ((⊤ : Submodule F (Fin m → F)) : Set (Fin m → F)), u ≠ v ∧ hammingDist u v = d}.Nonempty := by + refine ⟨1, 0, by simp, δ, by simp [δ], hδ_ne, ?_⟩ + have hset2U : + (Finset.univ.filter (fun i : Fin m => (0 : F) ≠ δ i)) + = {i0} := by + ext j; by_cases hji : j = i0 <;> simp [δ, hji] + -- And the alternative normalization + have hEqCard : (({i : Fin m | i = i0} : Finset (Fin m)).card) = 1 := by + classical + have hEq : ({i : Fin m | i = i0} : Finset (Fin m)) = ({i0} : Finset (Fin m)) := by + ext j; by_cases hji : j = i0 <;> simp [hji] + simpa [hEq, Finset.card_singleton] + simpa [hammingDist, hset2U, Finset.card_singleton] + apply sInf.le_sInf_of_LB hne + intro d hd + rcases hd with ⟨u, -, v, -, hneuv, rfl⟩ + -- show 1 ≤ hammingDist u v + have hex : ∃ j : Fin m, u j ≠ v j := by + by_contra hnone + have : u = v := by + funext j; by_contra hj; exact hnone ⟨j, by simpa using hj⟩ + exact hneuv this + rcases hex with ⟨j, hj⟩ + have : 1 ≤ ({i : Fin m | u i ≠ v i} : Finset (Fin m)).card := by + have hne' : ({i : Fin m | u i ≠ v i} : Finset (Fin m)).Nonempty := ⟨j, by simpa using hj⟩ + exact Nat.succ_le_of_lt (Finset.card_pos.mpr hne') + simpa [hammingDist] using this + have htop_minDist : Code.minDist ((⊤ : Submodule F (Fin m → F)) : Set (Fin m → F)) = 1 := + le_antisymm hUB hLB + simpa [htop_deg] using htop_minDist + simpa [hdist_eq, hrhs, m] using hfin_eq + +/-- Any nonzero codeword in an RS code has weight at least `n - deg + 1`. -/ +lemma wt_nonzero_ge_minDist_RS [NeZero deg] [Nonempty ι] {c : ι → F} + (hc : c ∈ (ReedSolomon.code α deg : Submodule F (ι → F))) (hc0 : c ≠ 0) : + Fintype.card ι - deg + 1 ≤ Code.wt c := by + classical + -- From the definition of `minDist`, any nonzero codeword witnesses `minDist ≤ wt c`. + have hmin : Code.minDist (ReedSolomon.code α deg : Set (ι → F)) ≤ Code.wt c := by + unfold Code.minDist + refine Nat.sInf_le ?_ + exact ⟨c, by simp [hc], 0, by simp, hc0, by simp [Code.wt, hammingDist]⟩ + -- Rewrite `minDist` for RS codes to `|ι| - deg + 1`. + have hmin_eq : + Code.minDist (ReedSolomon.code α deg : Set (ι → F)) + = Fintype.card ι - deg + 1 := by + simpa using (ProximityToRS.minDist_RS_general (α := α) (deg := deg) (F := F) (ι := ι)) + simpa [hmin_eq] using hmin + +/-- Weight is subadditive under addition. -/ +lemma wt_add_le {x y : ι → F} : Code.wt (x + y) ≤ Code.wt x + Code.wt y := by + classical + -- wt (x + y) = Δ₀(x + y, 0) = Δ₀(x, -y) + have hsum : Code.wt (x + y) = hammingDist (x + y) 0 := by simp [Code.wt, hammingDist] + have hx : hammingDist x 0 = Code.wt x := by simp [Code.wt, hammingDist] + have hyn : hammingDist 0 (-y) = Code.wt y := by simp [Code.wt, hammingDist] + calc + Code.wt (x + y) = hammingDist (x + y) 0 := hsum + _ = hammingDist x (-y) := by + simpa [sub_eq_add_neg] using + (Code.hammingDist_add_right_eq_sub (u := x) (v := 0) (c := y)) + _ ≤ hammingDist x 0 + hammingDist 0 (-y) := hammingDist_triangle x 0 (-y) + _ = Code.wt x + Code.wt y := by simp [hx, hyn] + +/-- Nonzero scalar multiplication preserves the Hamming weight (support). -/ +lemma wt_smul_eq_of_ne_zero {a : F} {x : ι → F} (ha : a ≠ 0) : + Code.wt (a • x) = Code.wt x := by + classical + unfold Code.wt + have hsubset₁ : ({i : ι | (a • x) i ≠ 0} : Finset ι) ⊆ ({i : ι | x i ≠ 0} : Finset ι) := by + intro i hi; simpa [Pi.smul_apply, smul_eq_mul, mul_eq_zero, ha] using hi + have hsubset₂ : ({i : ι | x i ≠ 0} : Finset ι) ⊆ ({i : ι | (a • x) i ≠ 0} : Finset ι) := by + intro i hi; simpa [Pi.smul_apply, smul_eq_mul, mul_eq_zero, ha] using hi + apply le_antisymm + · exact Finset.card_mono hsubset₁ + · exact Finset.card_mono hsubset₂ + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/ClosePoints.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/ClosePoints.lean new file mode 100644 index 000000000..976b1a7f0 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/ClosePoints.lean @@ -0,0 +1,99 @@ +/- +Close points on an affine line with respect to Reed–Solomon codes, +and basic cardinality links to scalars producing such points. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- +The set of points on an affine line, which are within distance `e` +from a Reed-Solomon code. +-/ +def closePtsOnAffineLine (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Finset (ι → F) := + by + classical + let fFintype : Fintype F := Fintype.ofFinite F + exact Finset.univ.filter + (fun x : (ι → F) => x ∈ Affine.line u v ∧ distFromCode x (ReedSolomon.code α deg) ≤ e) + +/-- +The number of points on an affine line which are within distance `e` +from a Reed-Solomon code. +-/ +def numberOfClosePts (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : ℕ := + (closePtsOnAffineLine u v deg α e).card + +/-- Cardinality link: the number of close points on the affine line is bounded by the +number of good scalars. -/ +lemma card_closePts_le_card_good + {u v : ι → F} {deg : ℕ} {α : ι ↪ F} {e : ℕ} : + (closePtsOnAffineLine u v deg α e).card ≤ + Nat.card {a : F // Code.distFromCode (u + a • v) (ReedSolomon.code α deg) ≤ e} := by + classical + -- Domain of scalars that map to close points on the affine line + let G := {a : F // Code.distFromCode (u + a • v) (ReedSolomon.code α deg) ≤ e} + -- Target subtype of elements of the close-points Finset + let s := closePtsOnAffineLine u v deg α e + let S := {x : (ι → F) // x ∈ s} + -- Map good scalars to close points via a ↦ u + a•v, landing in the subtype S + let φ : G → S := fun a => by + refine ⟨u + a.1 • v, ?_⟩ + -- Membership in the filtered Finset is straightforward + have hxLine : (u + a.1 • v) ∈ Affine.line u v := ⟨a.1, rfl⟩ + have hxDist : distFromCode (u + a.1 • v) (ReedSolomon.code α deg) ≤ e := a.2 + have : (u + a.1 • v) ∈ closePtsOnAffineLine u v deg α e := by + classical + simp [closePtsOnAffineLine, hxLine, hxDist] + simpa [s] using this + -- Surjection: every element in S corresponds to some a ∈ G + have hsurj_φ : Function.Surjective φ := by + intro y + rcases y with ⟨y, hy⟩ + -- From membership in s, extract a witness a with y = u + a•v and the distance bound + have hy' : y ∈ closePtsOnAffineLine u v deg α e := by simpa [s] using hy + have : y ∈ Affine.line u v ∧ distFromCode y (ReedSolomon.code α deg) ≤ e := by + classical + simpa [closePtsOnAffineLine] using (Finset.mem_filter.mp hy') + rcases this with ⟨hyLine, hydist⟩ + rcases hyLine with ⟨a, rfl⟩ + exact ⟨⟨a, hydist⟩, rfl⟩ + -- Hence, card(S) ≤ card(G) + have h_card_S_le : Nat.card S ≤ Nat.card G := + Finite.card_le_of_surjective φ hsurj_φ + -- And card(s) ≤ card(S) since s.attach ⊆ univ + have h_card_s_le_S : s.card ≤ Nat.card S := by + -- s.card = (s.attach).card ≤ (univ : Finset S).card = Fintype.card S + have hsubset : (s.attach : Finset S) ⊆ (Finset.univ : Finset S) := by exact Finset.subset_univ _ + have hmono := Finset.card_mono hsubset + -- (univ : Finset S).card = Fintype.card S + have huniv : (Finset.univ : Finset S).card = Fintype.card S := by + classical + simp + have hattach : (s.attach : Finset S).card = s.card := by + classical + simp [Finset.card_attach] + simpa [hattach, huniv] using hmono + -- Chain the inequalities + exact le_trans h_card_s_le_S h_card_S_le + +-- A version expressed with `numberOfClosePts` for convenient use at call sites. +lemma numberOfClosePts_le_card_good + {u v : ι → F} {deg : ℕ} {α : ι ↪ F} {e : ℕ} : + numberOfClosePts u v deg α e ≤ + Nat.card {a : F // Code.distFromCode (u + a • v) (ReedSolomon.code α deg) ≤ e} := by + classical + simpa [numberOfClosePts] using + (card_closePts_le_card_good (u := u) (v := v) (deg := deg) (α := α) (e := e)) + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44.lean new file mode 100644 index 000000000..d84d1c6eb --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44.lean @@ -0,0 +1,50 @@ +/- +Lemma 4.4 (Ligero): RS proximity on an affine line (points form). + +For every affine line ℓ = { u + α v : α ∈ F } in F^n, under 3e < d, either +all points are within distance ≤ e from the RS code, or only ≤ d points are. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.ClosePoints +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44.DichotomyCardGood +import Mathlib.Tactic + +set_option linter.style.longLine false +set_option linter.unnecessarySimpa false +set_option linter.unusedSectionVars false + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] +variable {deg : ℕ} {α : ι ↪ F} {e : ℕ} + +/-- Lemma 4.4 in the “points on the line” form. -/ +lemma line_dichotomy_points + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (u v : ι → F) : + (∀ x ∈ Affine.line u v, distFromCode x (ReedSolomon.code α deg) ≤ e) + ∨ (numberOfClosePts u v deg α e + ≤ Code.minDist (ReedSolomon.code α deg : Set (ι → F))) := by + classical + -- Apply the scalar-count dichotomy and translate to point-count via ClosePoints. + have h := ProximityToRS.line_dichotomy_card_good (deg := deg) (α := α) (e := e) he u v + rcases h with hAll | hFew + · -- Every scalar is good ⇒ every point on the line is within distance ≤ e. + left + intro x hx + rcases hx with ⟨a, rfl⟩ + have := hAll a + simpa [Pi.smul_apply, smul_eq_mul] using this + · -- Otherwise, the number of close points is bounded by the number of good scalars. + right + have hbridge := numberOfClosePts_le_card_good (u := u) (v := v) (deg := deg) (α := α) (e := e) + exact le_trans hbridge hFew + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/AffineParamOnG.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/AffineParamOnG.lean new file mode 100644 index 000000000..ad2d683e4 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/AffineParamOnG.lean @@ -0,0 +1,165 @@ +/- +Affine parametrization on G: if three-close-point identity vanishes on G, then witnesses are affine. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44.TripleComboZero +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +omit [DecidableEq ι] in +/-- Appendix A: If a set `G` of at least two good scalars is given and the triple +combination vanishes for all triples of distinct elements of `G`, then there exist +`c* , d* ∈ RS` such that for all `a ∈ G`, the unique witness satisfies `f_a = c* + a•d*`. -/ +lemma affine_param_on_G + (RS : LinearCode ι F) {e : ℕ} (u v : ι → F) + (G : Finset F) + (a0 a1 : F) (ha0 : a0 ∈ G) (ha1 : a1 ∈ G) (hneq : a0 ≠ a1) + (he3 : 3 * e < Code.minDist (RS : Set (ι → F))) + (f : {a : F // a ∈ G} → (ι → F)) + (hfRS : ∀ a, f a ∈ (RS : Set (ι → F))) + (hfclose : ∀ a, Δ₀(u + a.1 • v, f a) ≤ e) : + ∃ (cstar dstar : ι → F), cstar ∈ (RS : Set (ι → F)) ∧ dstar ∈ (RS : Set (ι → F)) ∧ + (∀ a, f a = cstar + a.1 • dstar) := by + classical + -- Anchor codewords in RS + set z0 : ι → F := f ⟨a0, ha0⟩ + set z1 : ι → F := f ⟨a1, ha1⟩ + -- Inverse of (a1 - a0) + set inv01 : F := (a1 - a0)⁻¹ + have h01_ne : a1 - a0 ≠ 0 := sub_ne_zero.mpr (by exact hneq.symm) + -- Define d* and c* + let dstar : ι → F := inv01 • (z1 - z0) + let cstar : ι → F := z0 - a0 • dstar + -- Membership in RS + have hz0 : z0 ∈ (RS : Submodule F (ι → F)) := by simpa [z0] using hfRS ⟨a0, ha0⟩ + have hz1 : z1 ∈ (RS : Submodule F (ι → F)) := by simpa [z1] using hfRS ⟨a1, ha1⟩ + have h_d_in : dstar ∈ (RS : Set (ι → F)) := by + have hsub : z1 - z0 ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.sub_mem RS hz1 hz0 + have : inv01 • (z1 - z0) ∈ (RS : Submodule F (ι → F)) := + Submodule.smul_mem RS inv01 hsub + simpa [dstar] using this + have h_c_in : cstar ∈ (RS : Set (ι → F)) := by + have : z0 - a0 • dstar ∈ (RS : Submodule F (ι → F)) := by + have hsm : a0 • dstar ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS a0 (by simpa using h_d_in) + simpa using Submodule.sub_mem RS hz0 hsm + simpa [cstar] using this + -- For any a ∈ G, solve f a = c* + a•d* using the triple-combo identity + have hfa_affine : ∀ a : {a : F // a ∈ G}, f a = cstar + a.1 • dstar := by + intro a + -- Using three-close-points combo = 0 + have htriple := + three_close_points_combo_is_zero (RS := RS) (e := e) (u := u) (v := v) (he := he3) + (a := a.1) (b := a0) (c := a1) + (fa := f a) (fb := z0) (fc := z1) + (hfa := by simpa using hfRS a) + (hfb := by simpa [z0] using hfRS ⟨a0, ha0⟩) + (hfc := by simpa [z1] using hfRS ⟨a1, ha1⟩) + (hwa := hfclose a) + (hwb := by simpa [z0] using hfclose ⟨a0, ha0⟩) + (hwc := by simpa [z1] using hfclose ⟨a1, ha1⟩) + -- Let X + Y + Z = 0 with Y = (a0 - a1)•f a + set X : ι → F := (a.1 - a0) • z1 + set Y : ι → F := (a0 - a1) • f a + set Z : ι → F := (a1 - a.1) • z0 + have hXYZ : X + Y + Z = 0 := by + simpa [X, Y, Z, add_comm, add_left_comm, add_assoc] + using htriple + -- Rearrange and cancel (a0 - a1) + have hY : Y = -(X + Z) := by + have : Y + (X + Z) = 0 := by simpa [add_comm, add_left_comm, add_assoc] using hXYZ + exact eq_neg_of_add_eq_zero_left this + -- Use inv10 = (a0 - a1)⁻¹ = -inv01 + have hsub : a0 - a1 = -(a1 - a0) := by + simpa [sub_eq_add_neg] using (neg_sub a1 a0).symm + set inv10 : F := -inv01 + have hmul_inv10 : (a0 - a1) * inv10 = (1 : F) := by + calc + (a0 - a1) * inv10 + = (-(a1 - a0)) * (-inv01) := by + -- Expand inv10 first to avoid deep simp recursion, then rewrite with hsub + dsimp [inv10] + rw [hsub] + _ = (a1 - a0) * inv01 := by simpa using (neg_mul_neg (a1 - a0) inv01) + _ = 1 := by simpa [inv01, h01_ne] + have hfa_eq_sum' : f a = inv10 • (-(X + Z)) := by + -- Multiply Y = (a0 - a1)•f a = -(X + Z) by inv10 on the left and cancel + have h1 := congrArg (fun t => inv10 • t) hY + have h2 : ((a0 - a1) * inv10) • f a = inv10 • (-(X + Z)) := by + simpa [Y, smul_smul, mul_comm] using h1 + have hcoef : ((a0 - a1) * inv10) = (1 : F) := hmul_inv10 + simpa [hcoef, one_smul] using h2 + have hfa_eq_sum : f a = inv01 • X + inv01 • Z := by + -- inv10 = -inv01; distribute over addition, then cancel the negatives + simpa [inv10, smul_neg, neg_smul, smul_add, add_comm, add_left_comm, add_assoc] + using hfa_eq_sum' + -- Distribute and simplify scalars + have hfa_eq' : f a = ((a.1 - a0) * inv01) • z1 + ((a1 - a.1) * inv01) • z0 := by + have hX' : inv01 • X = ((a.1 - a0) * inv01) • z1 := by + simpa [X, smul_smul, mul_comm, mul_left_comm, mul_assoc] + have hZ' : inv01 • Z = ((a1 - a.1) * inv01) • z0 := by + simpa [Z, smul_smul, mul_comm, mul_left_comm, mul_assoc] + calc + f a = inv01 • X + inv01 • Z := hfa_eq_sum + _ = ((a.1 - a0) * inv01) • z1 + ((a1 - a.1) * inv01) • z0 := by + simpa [add_comm, add_left_comm, add_assoc, hX', hZ'] + have hRHS' : cstar + a.1 • dstar + = ((a1 - a.1) * inv01) • z0 + ((a.1 - a0) * inv01) • z1 := by + -- Expand cstar and dstar and collect coefficients of z0 and z1 + have hstep1 : cstar + a.1 • dstar + = (z0 - a0 • dstar) + a.1 • dstar := rfl + have hstep2 : (z0 - a0 • dstar) + a.1 • dstar + = z0 + (a.1 • dstar - a0 • dstar) := by + simp [sub_eq_add_neg, add_comm, add_left_comm] + have hstep3 : a.1 • dstar - a0 • dstar = (a.1 - a0) • dstar := by + -- Use (a - b) • x = a•x - b•x + have h := (sub_smul (a.1) a0 dstar) + simpa [sub_eq_add_neg] using h.symm + have hstep4 : z0 + (a.1 - a0) • dstar + = z0 + ((a.1 - a0) * inv01) • (z1 - z0) := by + simp [dstar, smul_smul] + have hstep : cstar + a.1 • dstar + = z0 + ((a.1 - a0) * inv01) • (z1 - z0) := by + simpa [hstep1, hstep2, hstep3, hstep4] + have hcollect : cstar + a.1 • dstar + = (1 - ((a.1 - a0) * inv01)) • z0 + ((a.1 - a0) * inv01) • z1 := by + -- Distribute over the difference (z1 - z0) + have : z0 + ((a.1 - a0) * inv01) • (z1 - z0) + = (1 - ((a.1 - a0) * inv01)) • z0 + ((a.1 - a0) * inv01) • z1 := by + -- Rearrange: z0 + t•(z1 - z0) = (1 - t)•z0 + t•z1 + have : z0 + ((a.1 - a0) * inv01) • z1 + -(((a.1 - a0) * inv01) • z0) + = (1 - ((a.1 - a0) * inv01)) • z0 + ((a.1 - a0) * inv01) • z1 := by + simp [one_smul, sub_eq_add_neg, add_smul, add_comm, add_left_comm, add_assoc] + simpa [smul_sub, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this + simpa [hstep] + have hcoeff : 1 - ((a.1 - a0) * inv01) = ((a1 - a.1) * inv01) := by + have h1eq : (a1 - a0) * inv01 = (1 : F) := by simpa [inv01, h01_ne] + calc + 1 - ((a.1 - a0) * inv01) + = ((a1 - a0) * inv01) - ((a.1 - a0) * inv01) := by simpa [h1eq] + _ = ((a1 - a0) - (a.1 - a0)) * inv01 := by + simp [sub_mul] + _ = (a1 - a.1) * inv01 := by + have : (a1 - a0) - (a.1 - a0) = a1 - a.1 := by ring + simpa [this] + simpa [hcollect, hcoeff] + -- Reorder and finish + have hfa_comm : f a + = ((a1 - a.1) * inv01) • z0 + ((a.1 - a0) * inv01) • z1 := by + simpa [add_comm, add_left_comm, add_assoc] using hfa_eq' + have hfinal : f a = cstar + a.1 • dstar := by + simpa [hRHS', add_comm, add_left_comm, add_assoc] using hfa_comm + simp [hfinal] + exact ⟨cstar, dstar, h_c_in, h_d_in, hfa_affine⟩ + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/CardScalarsSmallWeightBound.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/CardScalarsSmallWeightBound.lean new file mode 100644 index 000000000..5f260cd05 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/CardScalarsSmallWeightBound.lean @@ -0,0 +1,267 @@ +/- +Bound on the number of scalars with small weight along an affine line. +-/ + +import ArkLib.Data.CodingTheory.Basic +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +/-- Case 2 (ii) (Appendix A): bound the number of scalars `a` for which +`wt(u + a•v) ≤ e`. We record a slightly looser but sufficient bound `≤ e` +(Appendix A gives `≤ |supp(u) ∩ supp(v)|`). -/ +lemma card_scalars_with_small_weight_bound + (u v : ι → F) {e : ℕ} + (hv : Code.wt v ≤ e) + (h_union_ge : ((Finset.univ.filter fun i : ι => u i ≠ 0) ∪ + (Finset.univ.filter fun i : ι => v i ≠ 0)).card ≥ e + 1) : + Nat.card {a : F // Code.wt (u + a • v) ≤ e} ≤ e := by + classical + -- Notation + let Su : Finset ι := Finset.univ.filter fun i : ι => u i ≠ 0 + let Sv : Finset ι := Finset.univ.filter fun i : ι => v i ≠ 0 + let T : Finset ι := Su ∪ Sv + have h_T_large : e < T.card := Nat.lt_of_succ_le h_union_ge + + -- Domain of scalars with small weight + let G := {a : F // Code.wt (u + a • v) ≤ e} + + -- For each a ∈ G, find an index i ∈ T such that (u + a•v) i = 0 and v i ≠ 0 + have exists_zero_in_T : ∀ x : G, ∃ i : ι, i ∈ T ∧ (u + x.1 • v) i = 0 ∧ v i ≠ 0 := by + intro x + -- support of (u + a•v) is contained in T + let Ssum : Finset ι := Finset.univ.filter (fun i : ι => (u i + x.1 * v i) ≠ 0) + have hsubset : Ssum ⊆ T := by + intro i hi + have hne : u i + x.1 * v i ≠ 0 := (Finset.mem_filter.mp hi).2 + by_cases hu0 : u i = 0 + · have hv0 : v i ≠ 0 := by + intro hv_eq + have : u i + x.1 * v i = 0 := by simp [hu0, hv_eq] + exact hne this + have : i ∈ Sv := by simp [Sv, hv0] + exact Finset.mem_union.mpr (Or.inr this) + · have : i ∈ Su := by simp [Su, hu0] + exact Finset.mem_union.mpr (Or.inl this) + -- Weight bound implies |Ssum| ≤ e + have hSsum_le_e : Ssum.card ≤ e := by + have hwt_eq : Code.wt (u + x.1 • v) = Ssum.card := by + simp [Code.wt, Ssum, Pi.smul_apply, smul_eq_mul] + simpa [hwt_eq] using x.2 + -- Since T.card ≥ e+1, Ssum ⊂ T, hence T \ Ssum is nonempty + have hlt : Ssum.card < T.card := lt_of_le_of_lt hSsum_le_e h_T_large + have hneq : Ssum ≠ T := by + intro hEq + -- contradiction: card Ssum < card T but Ssum = T + simpa [hEq] using hlt + have hss : Ssum ⊂ T := Finset.ssubset_iff_subset_ne.mpr ⟨hsubset, hneq⟩ + rcases Finset.exists_of_ssubset hss with ⟨i, hiT, hin⟩ + have hwi0 : (u + x.1 • v) i = 0 := by + -- i ∉ Ssum ⇒ (u + a•v) i = 0 + have : (u i + x.1 * v i) = 0 := by + have : i ∉ Ssum := hin + have : ¬ (u i + x.1 * v i ≠ 0) := by simpa [Ssum] using this + simpa [not_ne_iff] using this + simpa [Pi.smul_apply, smul_eq_mul, add_comm, add_left_comm, add_assoc] using this + -- i ∈ T and w i = 0 force v i ≠ 0 + have hvi_ne0 : v i ≠ 0 := by + by_cases hv0 : v i = 0 + · have : i ∈ Su ∨ i ∈ Sv := (Finset.mem_union.mp hiT) + cases this with + | inl hiSu => + have hui_ne0 : u i ≠ 0 := by simpa [Su] using hiSu + have : (u + x.1 • v) i ≠ 0 := by simp [Pi.smul_apply, smul_eq_mul, hv0, hui_ne0] + exact (this (by simpa using hwi0)).elim + | inr hiSv => + have : v i ≠ 0 := by simpa [Sv] using hiSv + exact (this hv0).elim + · exact hv0 + exact ⟨i, hiT, hwi0, hvi_ne0⟩ + + -- Define an injection φ : G → Idx by choosing an index i with v i ≠ 0 and (u + a•v) i = 0 + let Idx := {i : ι // v i ≠ 0} + have exists_zero_at : ∀ x : G, ∃ i : ι, v i ≠ 0 ∧ (u + x.1 • v) i = 0 := by + intro x + obtain ⟨i, hiT, hw0, hvi0⟩ := exists_zero_in_T x + exact ⟨i, hvi0, hw0⟩ + let pickIdx : G → ι := fun x => Classical.choose (exists_zero_at x) + have pickIdx_ne0 : ∀ x : G, v (pickIdx x) ≠ 0 := by + intro x; exact (Classical.choose_spec (exists_zero_at x)).1 + have pickIdx_eq0 : ∀ x : G, (u + x.1 • v) (pickIdx x) = 0 := by + intro x; exact (Classical.choose_spec (exists_zero_at x)).2 + let φ : G → Idx := fun x => ⟨pickIdx x, pickIdx_ne0 x⟩ + -- Uniqueness of the scalar at a fixed index with v i ≠ 0 + have uniq_scalar_at_index : ∀ i : ι, v i ≠ 0 → ∀ {a b : F}, + u i + a * v i = 0 → u i + b * v i = 0 → a = b := by + intro i hvi a b ha hb + have ha' : a * v i = -u i := by + have := congrArg (fun t => t - u i) ha + simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this + have hb' : b * v i = -u i := by + have := congrArg (fun t => t - u i) hb + simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this + have : a = b := by + have hmul : a = (-u i) * (v i)⁻¹ := by + have := congrArg (fun t => t * (v i)⁻¹) ha' + simpa [mul_assoc, hvi] using this + have hmul' : b = (-u i) * (v i)⁻¹ := by + have := congrArg (fun t => t * (v i)⁻¹) hb' + simpa [mul_assoc, hvi] using this + simpa [hmul, hmul'] + simpa using this + -- φ is injective because for a fixed index i there is at most one scalar + have inj_φ : Function.Injective φ := by + intro x y hxy + apply Subtype.ext + have hi : pickIdx x = pickIdx y := by simpa using congrArg Subtype.val hxy + -- Use uniqueness at index hi + have hx : + u (pickIdx x) + x.1 * v (pickIdx x) = 0 := by + simpa [Pi.smul_apply, smul_eq_mul] using pickIdx_eq0 x + have hy : + u (pickIdx y) + y.1 * v (pickIdx y) = 0 := by + simpa [Pi.smul_apply, smul_eq_mul] using pickIdx_eq0 y + have := uniq_scalar_at_index (pickIdx x) (pickIdx_ne0 x) (a := x.1) (b := y.1) + (by simpa using hx) (by simpa [hi] using hy) + exact this + -- Hence card G ≤ card Idx + have hG_le_Idx : Nat.card G ≤ Nat.card Idx := + Finite.card_le_of_injective φ inj_φ + -- Combine with bound card Idx by wt(v) ≤ e + have hIdx_le_e : Nat.card Idx ≤ e := by + -- Fintype.card Idx = card Sv = Code.wt v ≤ e + have hcard_idx : Nat.card Idx = (Finset.univ.filter fun i : ι => v i ≠ 0).card := by + classical + simpa [Idx] using Fintype.card_subtype (fun i : ι => v i ≠ 0) + have : (Finset.univ.filter fun i : ι => v i ≠ 0).card = Code.wt v := by + simp [Code.wt] + rwa [hcard_idx, this] + exact le_trans hG_le_Idx hIdx_le_e + +/- + A slightly more general bound: if we only know a bound `R` on the weight of `v`, + then the number of scalars producing small weight (≤ `e`) is at most `R`. + This is the same proof as above, ending with `Fintype.card Idx = Code.wt v ≤ R`. +-/ +lemma card_scalars_with_small_weight_bound_by_wt + (u v : ι → F) {e R : ℕ} + (hv : Code.wt v ≤ R) + (h_union_ge : + ((Finset.univ.filter fun i : ι => u i ≠ 0) ∪ + (Finset.univ.filter fun i : ι => v i ≠ 0)).card ≥ e + 1) : + Nat.card {a : F // Code.wt (u + a • v) ≤ e} ≤ R := by + classical + -- We can reuse the entire construction from the previous lemma, but finish with `≤ R`. + -- Domain of scalars with small weight + let G := {a : F // Code.wt (u + a • v) ≤ e} + -- As before, produce an index with `v i ≠ 0` and `(u + a•v) i = 0` for each `a ∈ G`. + -- We reuse the proof blocks from `card_scalars_with_small_weight_bound` verbatim. + let Su : Finset ι := Finset.univ.filter fun i : ι => u i ≠ 0 + let Sv : Finset ι := Finset.univ.filter fun i : ι => v i ≠ 0 + let T : Finset ι := Su ∪ Sv + have h_T_large : e < T.card := Nat.lt_of_succ_le h_union_ge + have exists_zero_in_T : ∀ x : G, ∃ i : ι, i ∈ T ∧ (u + x.1 • v) i = 0 ∧ v i ≠ 0 := by + intro x + let Ssum : Finset ι := Finset.univ.filter (fun i : ι => (u i + x.1 * v i) ≠ 0) + have hsubset : Ssum ⊆ T := by + intro i hi + have hne : u i + x.1 * v i ≠ 0 := (Finset.mem_filter.mp hi).2 + by_cases hu0 : u i = 0 + · have hv0 : v i ≠ 0 := by + intro hv_eq + have : u i + x.1 * v i = 0 := by simp [hu0, hv_eq] + exact hne this + have : i ∈ Sv := by simp [Sv, hv0] + exact Finset.mem_union.mpr (Or.inr this) + · have : i ∈ Su := by simp [Su, hu0] + exact Finset.mem_union.mpr (Or.inl this) + have hSsum_le_e : Ssum.card ≤ e := by + have hwt_eq : Code.wt (u + x.1 • v) = Ssum.card := by + simp [Code.wt, Ssum, Pi.smul_apply, smul_eq_mul] + simpa [hwt_eq] using x.2 + have hlt : Ssum.card < T.card := lt_of_le_of_lt hSsum_le_e h_T_large + have hneq : Ssum ≠ T := by + intro hEq; simpa [hEq] using hlt + have hss : Ssum ⊂ T := Finset.ssubset_iff_subset_ne.mpr ⟨hsubset, hneq⟩ + rcases Finset.exists_of_ssubset hss with ⟨i, hiT, hin⟩ + have hwi0 : (u + x.1 • v) i = 0 := by + have : (u i + x.1 * v i) = 0 := by + have : i ∉ Ssum := hin + have : ¬ (u i + x.1 * v i ≠ 0) := by simpa [Ssum] using this + simpa [not_ne_iff] using this + simpa [Pi.smul_apply, smul_eq_mul, add_comm, add_left_comm, add_assoc] using this + have hvi_ne0 : v i ≠ 0 := by + by_cases hv0 : v i = 0 + · have : i ∈ Su ∨ i ∈ Sv := (Finset.mem_union.mp hiT) + cases this with + | inl hiSu => + have hui_ne0 : u i ≠ 0 := by simpa [Su] using hiSu + have : (u + x.1 • v) i ≠ 0 := by simp [Pi.smul_apply, smul_eq_mul, hv0, hui_ne0] + exact (this (by simpa using hwi0)).elim + | inr hiSv => + have : v i ≠ 0 := by simpa [Sv] using hiSv + exact (this hv0).elim + · exact hv0 + exact ⟨i, hiT, hwi0, hvi_ne0⟩ + let Idx := {i : ι // v i ≠ 0} + have exists_zero_at : ∀ x : G, ∃ i : ι, v i ≠ 0 ∧ (u + x.1 • v) i = 0 := by + intro x + obtain ⟨i, hiT, hw0, hvi0⟩ := exists_zero_in_T x + exact ⟨i, hvi0, hw0⟩ + let pickIdx : G → ι := fun x => Classical.choose (exists_zero_at x) + have pickIdx_ne0 : ∀ x : G, v (pickIdx x) ≠ 0 := by + intro x; exact (Classical.choose_spec (exists_zero_at x)).1 + have pickIdx_eq0 : ∀ x : G, (u + x.1 • v) (pickIdx x) = 0 := by + intro x; exact (Classical.choose_spec (exists_zero_at x)).2 + let φ : G → Idx := fun x => ⟨pickIdx x, pickIdx_ne0 x⟩ + -- Injectivity as before + have uniq_scalar_at_index : ∀ i : ι, v i ≠ 0 → ∀ {a b : F}, + u i + a * v i = 0 → u i + b * v i = 0 → a = b := by + intro i hvi a b ha hb + have ha' : a * v i = -u i := by + have := congrArg (fun t => t - u i) ha + simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this + have hb' : b * v i = -u i := by + have := congrArg (fun t => t - u i) hb + simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this + have : a = b := by + have hmul : a = (-u i) * (v i)⁻¹ := by + have := congrArg (fun t => t * (v i)⁻¹) ha' + simpa [mul_assoc, hvi] using this + have hmul' : b = (-u i) * (v i)⁻¹ := by + have := congrArg (fun t => t * (v i)⁻¹) hb' + simpa [mul_assoc, hvi] using this + simpa [hmul, hmul'] + simpa using this + have inj_φ : Function.Injective φ := by + intro x y hxy + apply Subtype.ext + have hi : pickIdx x = pickIdx y := by + simpa using congrArg Subtype.val hxy + have hx : u (pickIdx x) + x.1 * v (pickIdx x) = 0 := by + simpa [Pi.smul_apply, smul_eq_mul] using pickIdx_eq0 x + have hy : u (pickIdx y) + y.1 * v (pickIdx y) = 0 := by + simpa [Pi.smul_apply, smul_eq_mul] using pickIdx_eq0 y + have := uniq_scalar_at_index (pickIdx x) (pickIdx_ne0 x) (a := x.1) (b := y.1) + (by simpa using hx) (by simpa [hi] using hy) + exact this + have hG_le_Idx : Nat.card G ≤ Nat.card Idx := + Finite.card_le_of_injective φ inj_φ + -- Finish with the bound `card Idx = wt v ≤ R`. + have hIdx_le_R : Nat.card Idx ≤ R := by + have hcard_idx : Nat.card Idx = (Finset.univ.filter fun i : ι => v i ≠ 0).card := by + classical + simpa [Idx] using Fintype.card_subtype (fun i : ι => v i ≠ 0) + have : (Finset.univ.filter fun i : ι => v i ≠ 0).card = Code.wt v := by + simp [Code.wt] + rwa [hcard_idx, this] + exact le_trans hG_le_Idx hIdx_le_R + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/DichotomyCardGood.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/DichotomyCardGood.lean new file mode 100644 index 000000000..931aff0b2 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/DichotomyCardGood.lean @@ -0,0 +1,318 @@ +/- +Dichotomy (cardinality form) for RS proximity along an affine line. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44.AffineParamOnG +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44.CardScalarsSmallWeightBound +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] +variable {deg : ℕ} {α : ι ↪ F} {e : ℕ} + +-- Algebraic helper: distribute subtraction over an affine combination. +omit [DecidableEq F] [Fintype F] [Fintype ι] [DecidableEq ι] in +lemma sub_affine_distrib + (u v c d : ι → F) (a : F) : + (u + a • v) - (c + a • d) = (u - c) + a • (v - d) := by + funext i + simp [Pi.smul_apply, smul_eq_mul, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] + +omit [Fintype F] in +/-- Case 1 (Appendix A): if `|supp(u) ∪ supp(v)| ≤ e`, then every point on the line is within +distance ≤ e from the code (since 0 ∈ L). -/ +lemma all_points_close_when_union_support_le_e + (L : LinearCode ι F) (u v : ι → F) {e : ℕ} + (h_union : ((Finset.univ.filter fun i : ι => u i ≠ 0) ∪ + (Finset.univ.filter fun i : ι => v i ≠ 0)).card ≤ e) : + ∀ a : F, distFromCode (u + a • v) (L : Set (ι → F)) ≤ e := by + classical + intro a + let Su : Finset ι := Finset.univ.filter (fun i : ι => u i ≠ 0) + let Sv : Finset ι := Finset.univ.filter (fun i : ι => v i ≠ 0) + let Ssum : Finset ι := Finset.univ.filter (fun i : ι => u i + a * v i ≠ 0) + have hsubset : Ssum ⊆ Su ∪ Sv := by + intro i hi + have hne : u i + a * v i ≠ 0 := (Finset.mem_filter.mp hi).2 + by_cases hu0 : u i = 0 + · have hv0 : v i ≠ 0 := by + intro hv_eq; have : u i + a * v i = 0 := by simp [hu0, hv_eq] + exact hne this + have : i ∈ Sv := by simp [Sv, hv0] + exact Finset.mem_union.mpr (Or.inr this) + · have : i ∈ Su := by simp [Su, hu0] + exact Finset.mem_union.mpr (Or.inl this) + have hwt_le : Code.wt (u + a • v) ≤ (Su ∪ Sv).card := by + have : Code.wt (u + a • v) = Ssum.card := by + simp [Code.wt, Ssum, smul_eq_mul, Pi.smul_apply] + have : Ssum.card ≤ (Su ∪ Sv).card := Finset.card_mono hsubset + simp [Ssum] at this + simpa [Code.wt, Ssum, smul_eq_mul, Pi.smul_apply] using this + have hwt_le_e : Code.wt (u + a • v) ≤ e := le_trans hwt_le h_union + have h0mem : (0 : ι → F) ∈ (L : Set (ι → F)) := by exact (Submodule.zero_mem L) + have hham_le_nat : hammingDist (u + a • v) (0 : ι → F) ≤ e := by + simpa [LinearCode.hammingDist_eq_wt_sub] using hwt_le_e + have hmem : (e : ℕ∞) ∈ {d : ℕ∞ | ∃ z ∈ (L : Set (ι → F)), hammingDist (u + a • v) z ≤ d} := by + refine ⟨0, h0mem, ?_⟩ + simpa using (by exact_mod_cast hham_le_nat : (hammingDist (u + a • v) (0 : ι → F) : ℕ∞) ≤ e) + have hsInf_le := sInf_le hmem + simpa [Code.distFromCode] using hsInf_le + +/-- Far branch core (Appendix A): under `3*e < minDist(RS)`, along the line `u + a•v`, +either all scalars are good (every point is within `e` of `RS`) or the good scalars are +bounded by `minDist(RS)`. This is the RS‑specific “either all or ≤ d” statement. + +Blueprint proof: unique witnesses within `e`, triple‑scalar identity forcing affine centers, +double counting to bound the bad coordinate set by `≤ e`, then globalize to all scalars. -/ +private lemma far_branch_either_all_or_bound + (RS : LinearCode ι F) {e : ℕ} + (he : 3 * e < Code.minDist (RS : Set (ι → F))) + (u v : ι → F) : + (∀ a : F, distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e) + ∨ (Nat.card {a : F // distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e} + ≤ Code.minDist (RS : Set (ι → F))) := by + classical + -- Let G be the set of good scalars: those with distance ≤ e to RS. + let fFintype : Fintype F := Fintype.ofFinite F + let G : Finset F := + Finset.univ.filter (fun a : F => distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e) + -- If all scalars are good, we are done. + by_cases hall : (∀ a : F, distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e) + · exact Or.inl hall + -- Otherwise, we will bound the number of good scalars by minDist(RS), + -- unless we can still conclude that all scalars are good after re-centering. + -- If |G| ≤ 1, the bound is trivial since minDist ≥ 1 (from 3e < minDist). + by_cases hLe1 : G.card ≤ 1 + · have hminpos : 1 ≤ Code.minDist (RS : Set (ι → F)) := by + have : 0 < Code.minDist (RS : Set (ι → F)) := lt_of_le_of_lt (Nat.zero_le _) he + exact Nat.succ_le_of_lt this + -- Convert between the subtype cardinality and the filtered finset cardinality + have hcard_eq : + Nat.card {a : F // distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e} = G.card := by + classical + -- standard equivalence between subtype over a decidable predicate and a filtered finset + simpa [G] using Fintype.card_subtype + (fun a : F => distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e) + have : Nat.card {a : F // distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e} ≤ 1 := by + rwa [hcard_eq] + exact Or.inr (le_trans this hminpos) + -- Now assume |G| ≥ 2. Pick two distinct good scalars a0, a1 in G. + · -- There exist two distinct good scalars in G since ¬ (G.card ≤ 1). + classical + have h1lt : 1 < G.card := Nat.lt_of_not_ge hLe1 + -- Pick any element a0 ∈ G (nonempty since card > 0) + have hpos : 0 < G.card := lt_trans (by decide) h1lt + obtain ⟨a0, ha0G⟩ := Finset.card_pos.mp hpos + -- From 1 < card, there exists a1 ∈ G with a1 ≠ a0 + have hex := Finset.exists_ne_of_one_lt_card (s := G) h1lt + rcases hex a0 with ⟨a1, ha1G, hneq⟩ + -- For each a ∈ G, pick a witness codeword within distance ≤ e + have hGdef : ∀ {a : F}, a ∈ G → distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e := by + intro a ha + have : a ∈ Finset.univ.filter + (fun a : F => distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e) := ha + simpa [G] using (Finset.mem_filter.mp this).2 + -- Package G as a subtype and choose witnesses + let Gsub := {a : F // a ∈ G} + -- For each a ∈ G, pick f a ∈ RS with Δ(u + a•v, f a) ≤ e + choose f hf_mem hf_close using + (fun (a : Gsub) => + ProximityToRS.exists_codeword_close_of_dist_le + (u := u + a.1 • v) (C := (RS : Set (ι → F))) (e := e) (h := hGdef a.property)) + -- Apply the affine parametrization on G using the triple-combo zero identity + have he3 : 3 * e < Code.minDist (RS : Set (ι → F)) := he + -- Build the finset structure for G and provide two distinct anchors + have ha0G' : a0 ∈ G := ha0G + have ha1G' : a1 ∈ G := ha1G + -- Prepare inputs for `affine_param_on_G` + have hfRS : ∀ a : Gsub, f a ∈ (RS : Set (ι → F)) := fun a => (hf_mem a) + have hfclose : ∀ a : Gsub, Δ₀(u + a.1 • v, f a) ≤ e := fun a => (hf_close a) + -- Convert a0, a1 to subtype elements of G + have ha0_sub : Gsub := ⟨a0, ha0G⟩ + have ha1_sub : Gsub := ⟨a1, ha1G⟩ + -- Run the affine parametrization + obtain ⟨cstar, dstar, hc_in, hd_in, hfa_affine⟩ := + ProximityToRS.affine_param_on_G (RS := RS) (u := u) (v := v) + (G := G) (a0 := a0) (a1 := a1) (ha0 := ha0G) (ha1 := ha1G) (hneq := hneq.symm) + (he3 := he3) (f := f) (hfRS := hfRS) (hfclose := hfclose) + -- Define shifted parameters u' and v' + let u' : ι → F := u - cstar + let v' : ι → F := v - dstar + -- If the union support of u' and v' is small, then all scalars are good. + let Su' : Finset ι := Finset.univ.filter fun i : ι => u' i ≠ 0 + let Sv' : Finset ι := Finset.univ.filter fun i : ι => v' i ≠ 0 + by_cases h_small : (Su' ∪ Sv').card ≤ e + · -- Conclude all scalars are good using the general case-1 lemma on u', v', then translate. + have hall' : ∀ a : F, distFromCode (u' + a • v') (RS : Set (ι → F)) ≤ e := + all_points_close_when_union_support_le_e (L := RS) (u := u') (v := v') h_small + -- Show c* + a•d* ∈ RS for every a + have hcode : ∀ a : F, (cstar + a • dstar) ∈ (RS : Set (ι → F)) := by + intro a + have hc' : cstar ∈ (RS : Submodule F (ι → F)) := by simpa using hc_in + have hd' : dstar ∈ (RS : Submodule F (ι → F)) := by simpa using hd_in + have : cstar + a • dstar ∈ (RS : Submodule F (ι → F)) := + Submodule.add_mem RS hc' (Submodule.smul_mem RS a hd') + simpa using this + -- Use translation invariance: Δ₀((u' + a•v') + (c* + a•d*), RS) = Δ₀(u' + a•v', RS) + have hall_all : ∀ a : F, distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e := by + intro a + have hdist_eq := + Code.distFromCode_add_codeword_eq (LC := RS) (w := u' + a • v') + (c := cstar + a • dstar) (hc := hcode a) + have hsum : (u' + a • v') + (cstar + a • dstar) = u + a • v := by + simp [u', v', sub_eq_add_neg, add_comm, add_left_comm, add_assoc, smul_add] + have hEq : distFromCode (u + a • v) (RS : Set (ι → F)) + = distFromCode (u' + a • v') (RS : Set (ι → F)) := by + -- Prefer `simp` rewriting over `simpa` for lint + have := hdist_eq + simp [hsum] at this + exact this + have hbound : distFromCode (u' + a • v') (RS : Set (ι → F)) ≤ e := hall' a + simpa [hEq] using hbound + exact Or.inl hall_all + -- Large union support for u', v'. Use the affine witnesses to bound |G|. + -- First, bound wt(v') by the sum of residual weights at two good scalars. + have ha0_good : distFromCode (u + a0 • v) (RS : Set (ι → F)) ≤ e := hGdef ha0G + have ha1_good : distFromCode (u + a1 • v) (RS : Set (ι → F)) ≤ e := hGdef ha1G + have ha0_sub' : Gsub := ⟨a0, ha0G⟩ + have ha1_sub' : Gsub := ⟨a1, ha1G⟩ + have rwt_a0 : Code.wt (u' + a0 • v') ≤ e := by + -- residual r(a0) equals u' + a0•v' + have hdist : hammingDist (u + a0 • v) (f ⟨a0, ha0G⟩) ≤ e := by + simpa using hfclose ⟨a0, ha0G⟩ + have hdist' : Code.wt ((u + a0 • v) - (f ⟨a0, ha0G⟩)) ≤ e := by + simpa [LinearCode.hammingDist_eq_wt_sub] using hdist + have hres : (u + a0 • v) - (cstar + a0 • dstar) = u' + a0 • v' := by + simpa [u', v'] using ProximityToRS.sub_affine_distrib (u) (v) (cstar) (dstar) a0 + simpa [hfa_affine ⟨a0, ha0G⟩, hres] using hdist' + have rwt_a1 : Code.wt (u' + a1 • v') ≤ e := by + have hdist : hammingDist (u + a1 • v) (f ⟨a1, ha1G⟩) ≤ e := by + simpa using hfclose ⟨a1, ha1G⟩ + have hdist' : Code.wt ((u + a1 • v) - (f ⟨a1, ha1G⟩)) ≤ e := by + simpa [LinearCode.hammingDist_eq_wt_sub] using hdist + have hres : (u + a1 • v) - (cstar + a1 • dstar) = u' + a1 • v' := by + simpa [u', v'] using ProximityToRS.sub_affine_distrib (u) (v) (cstar) (dstar) a1 + simpa [hfa_affine ⟨a1, ha1G⟩, hres] using hdist' + -- Deduce wt(v') ≤ 2e from the difference of residuals at a1 and a0. + have h_v'_wt_le_2e : Code.wt v' ≤ 2 * e := by + -- (u' + a1•v') - (u' + a0•v') = (a1 - a0) • v' + have hdiff_eq' : (u' + a1 • v') - (u' + a0 • v') = a1 • v' - a0 • v' := by + simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using + (add_sub_add_comm u' (a1 • v') u' (a0 • v')) + -- wt((a1 - a0)•v') = wt(v') since (a1 - a0) ≠ 0 + have hcoeff_ne : (a1 - a0) ≠ 0 := sub_ne_zero.mpr hneq + have hwt_smul : Code.wt ((a1 - a0) • v') = Code.wt v' := + ProximityToRS.wt_smul_eq_of_ne_zero (ι := ι) (a := (a1 - a0)) (x := v') hcoeff_ne + -- wt((a1 - a0)•v') = wt((u' + a1•v') - (u' + a0•v')) ≤ wt(u' + a1•v') + wt(u' + a0•v') ≤ 2e + have base : Code.wt ((u' + a1 • v') - (u' + a0 • v')) + ≤ Code.wt (u' + a1 • v') + Code.wt (-(u' + a0 • v')) := by + simpa [sub_eq_add_neg] using + (ProximityToRS.wt_add_le (x := (u' + a1 • v')) (y := -(u' + a0 • v'))) + have hneg : Code.wt (-u' + -(a0 • v')) = Code.wt (u' + a0 • v') := by + have hne : (- (1 : F)) ≠ 0 := by exact (neg_ne_zero.mpr (one_ne_zero : (1 : F) ≠ 0)) + have := + (ProximityToRS.wt_smul_eq_of_ne_zero (ι := ι) (a := (-1 : F)) (x := (u' + a0 • v')) hne) + simpa [one_smul, Pi.smul_apply, smul_eq_mul, sub_eq_add_neg, add_comm] using this + have hstep : + Code.wt (a1 • v' - a0 • v') + ≤ Code.wt (u' + a1 • v') + Code.wt (u' + a0 • v') := by + simpa [hdiff_eq', hneg, add_comm, add_assoc] using base + have : Code.wt ((a1 - a0) • v') ≤ e + e := by + -- rewrite the left side using sub_smul + have : + Code.wt ((a1 - a0) • v') + ≤ Code.wt (u' + a1 • v') + Code.wt (u' + a0 • v') := by + simpa [sub_smul] using hstep + refine le_trans this ?_ + have : Code.wt (u' + a1 • v') + Code.wt (u' + a0 • v') ≤ e + e := by + simpa [add_comm, add_left_comm, add_assoc] using (add_le_add rwt_a1 rwt_a0) + exact this + -- Conclude wt(v') ≤ 2e + -- First rewrite wt v' using hwt_smul, then apply the bound + simpa [hwt_smul, two_mul] using this + -- Use the counting lemma on the residuals r(a) = u' + a•v' to bound |G|. + have hcard_le : + Nat.card {a : F // Code.wt (u' + a • v') ≤ e} ≤ 2 * e := by + -- Large union support for u', v' (negation of the small case) + have h_union_large : (Su' ∪ Sv').card ≥ e + 1 := by + exact Nat.succ_le_of_lt (lt_of_not_ge h_small) + -- Apply the generalized counting bound with R = 2e + have hv' : Code.wt v' ≤ 2 * e := h_v'_wt_le_2e + exact ProximityToRS.card_scalars_with_small_weight_bound_by_wt (u := u') (v := v') + (e := e) (R := 2 * e) hv' (h_union_ge := h_union_large) + -- Map each good scalar a ∈ G to the fact that `wt(u' + a•v') ≤ e` using the affine witnesses. + -- Define an injective map from good scalars to small-weight scalars + let g : {a : F // distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e} → + {a : F // Code.wt (u' + a • v') ≤ e} := + fun a => + by + -- Show `wt(u' + a•v') ≤ e` using the affine witnesses + have haG : a.1 ∈ G := by + have hmem : a.1 ∈ Finset.univ ∧ distFromCode (u + a.1 • v) (RS : Set (ι → F)) ≤ e := by + exact ⟨by simp, a.2⟩ + have : a.1 ∈ Finset.univ.filter + (fun a : F => distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e) := + Finset.mem_filter.mpr hmem + simpa [G] using this + have hdist : hammingDist (u + a.1 • v) (f ⟨a.1, haG⟩) ≤ e := by + simpa using hfclose ⟨a.1, haG⟩ + have hdist' : Code.wt ((u + a.1 • v) - (f ⟨a.1, haG⟩)) ≤ e := by + simpa [LinearCode.hammingDist_eq_wt_sub] using hdist + have hres : (u + a.1 • v) - (cstar + a.1 • dstar) = u' + a.1 • v' := by + simpa [u', v'] using ProximityToRS.sub_affine_distrib (u) (v) (cstar) (dstar) a.1 + have hwt : Code.wt (u' + a.1 • v') ≤ e := by + simpa [hfa_affine ⟨a.1, haG⟩, hres] using hdist' + exact ⟨a.1, hwt⟩ + have ginj : Function.Injective g := by + intro x y h + cases x; cases y; cases h; rfl + -- Therefore |G| ≤ |{a | wt(u' + a•v') ≤ e}| ≤ 2e < minDist(RS). + -- Convert cardinalities via `card_subtype`. + have hcard_good_le : + Nat.card {a : F // distFromCode (u + a • v) (RS : Set (ι → F)) ≤ e} + ≤ Nat.card {a : F // Code.wt (u' + a • v') ≤ e} := + Finite.card_le_of_injective g ginj + have hcard_le' := le_trans hcard_good_le hcard_le + -- Finally, compare 2e with minDist via `he`. + have h2e_lt : 2 * e < Code.minDist (RS : Set (ι → F)) := by + have : 2 * e ≤ 3 * e := by nlinarith + exact lt_of_le_of_lt this he + -- from card ≤ 2e and 2e < d, deduce card ≤ d + have hlt := lt_of_le_of_lt hcard_le' h2e_lt + exact Or.inr (le_of_lt hlt) + +/-- Lemma 4.4 (dichotomy form, counting good scalars), specialized to RS. -/ +lemma line_dichotomy_card_good + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (u v : ι → F) : + (∀ a : F, distFromCode (u + a • v) (ReedSolomon.code α deg) ≤ e) + ∨ (Nat.card {a : F // distFromCode (u + a • v) (ReedSolomon.code α deg) ≤ e} + ≤ Code.minDist (ReedSolomon.code α deg : Set (ι → F))) := by + classical + -- Abbreviation + set RS := (ReedSolomon.code α deg) with hRS + -- Case 1: small union support ⇒ all scalars are good + let Su : Finset ι := Finset.univ.filter fun i : ι => u i ≠ 0 + let Sv : Finset ι := Finset.univ.filter fun i : ι => v i ≠ 0 + by_cases hSmall : (Su ∪ Sv).card ≤ e + · left + intro a + simpa [hRS] using + (all_points_close_when_union_support_le_e (L := ReedSolomon.code α deg) + (u := u) (v := v) hSmall a) + · -- Large union support: invoke the far‑branch disjunction + have hfar := far_branch_either_all_or_bound (RS := ReedSolomon.code α deg) (e := e) + (he := by simpa [hRS] using he) (u := u) (v := v) + rcases hfar with hall | hbound + · left; intro a; simpa [hRS] using hall a + · right; simpa [hRS] using hbound +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/MinDistHelpers.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/MinDistHelpers.lean new file mode 100644 index 000000000..0a622a340 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/MinDistHelpers.lean @@ -0,0 +1,43 @@ +/- +Helpers about minimum distance for linear codes and Reed–Solomon. +-/ + +import ArkLib.Data.CodingTheory.Basic +import ArkLib.Data.CodingTheory.ReedSolomon +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] +variable {ι : Type*} [Fintype ι] + +/-- General helper: in any linear code, a nonzero codeword has weight at least the minimum distance. +Contraposition form: if a codeword has weight strictly less than `minDist`, it must be zero. -/ +lemma zero_of_wt_lt_minDist + (L : LinearCode ι F) {c : ι → F} + (hc : c ∈ (L : Set (ι → F))) + (hwt : Code.wt c < Code.minDist (L : Set (ι → F))) : + c = 0 := by + classical + by_contra hcz + -- From the definition of `minDist`, nonzero `c ∈ L` witnesses `minDist ≤ wt c`. + have hmin : Code.minDist (L : Set (ι → F)) ≤ Code.wt c := by + unfold Code.minDist + refine Nat.sInf_le ?_ + exact ⟨c, hc, 0, by simp, hcz, by simp [LinearCode.hammingDist_eq_wt_sub]⟩ + -- Contradiction with `wt c < minDist` + exact (not_lt_of_ge hmin hwt).elim + +/-- RS helper: same as `zero_of_wt_lt_minDist` specialized to Reed–Solomon codes. -/ +lemma rs_zero_of_wt_lt_minDist + {α : ι ↪ F} {deg : ℕ} {c : ι → F} + (hc : c ∈ (ReedSolomon.code α deg : Set (ι → F))) + (hwt : Code.wt c < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) : + c = 0 := + zero_of_wt_lt_minDist (L := ReedSolomon.code α deg) hc hwt + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/TripleComboZero.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/TripleComboZero.lean new file mode 100644 index 000000000..ead8e8893 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma44/TripleComboZero.lean @@ -0,0 +1,90 @@ +/- +Triple-combination zero lemmas used by affine parametrization. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44.MinDistHelpers +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.ThreeClosePoints +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] + +omit [Fintype F] [DecidableEq ι] in +/-- Appendix A: Under `3*e < minDist(RS)`, the triple combination must be zero. -/ +lemma triple_combo_is_zero + (RS : LinearCode ι F) {e : ℕ} + (he : 3 * e < Code.minDist (RS : Set (ι → F))) + {a b c : F} {fa fb fc : ι → F} + (hfa : fa ∈ (RS : Set (ι → F))) (hfb : fb ∈ (RS : Set (ι → F))) (hfc : fc ∈ (RS : Set (ι → F))) + (hwt : Code.wt ((a - b) • fc + (b - c) • fa + (c - a) • fb) ≤ 3 * e) : + (a - b) • fc + (b - c) • fa + (c - a) • fb = 0 := by + classical + -- The triple linear combination is a codeword in RS by closure under add and smul. + have hfa' : fa ∈ (RS : Submodule F (ι → F)) := by simpa using hfa + have hfb' : fb ∈ (RS : Submodule F (ι → F)) := by simpa using hfb + have hfc' : fc ∈ (RS : Submodule F (ι → F)) := by simpa using hfc + have hmem_RS : + (a - b) • fc + (b - c) • fa + (c - a) • fb ∈ (RS : Set (ι → F)) := by + -- Use Submodule closure operations + have h1 : (a - b) • fc ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS (a - b) hfc' + have h2 : (b - c) • fa ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS (b - c) hfa' + have h3 : (c - a) • fb ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS (c - a) hfb' + have h12 : (a - b) • fc + (b - c) • fa ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.add_mem RS h1 h2 + have h123 : (a - b) • fc + (b - c) • fa + (c - a) • fb ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.add_mem RS h12 h3 + simpa using h123 + -- Turn the ≤ and < into a strict inequality via transitivity: wt < minDist + have hlt : Code.wt ((a - b) • fc + (b - c) • fa + (c - a) • fb) + < Code.minDist (RS : Set (ι → F)) := lt_of_le_of_lt hwt he + -- Apply the general helper specialized to RS + exact zero_of_wt_lt_minDist (L := RS) hmem_RS hlt + +/-- Using `three_close_points_weight_bound`, the triple combination of +three `e`-close RS codewords along the line is the zero codeword when `3*e < minDist(RS)`. -/ +lemma three_close_points_combo_is_zero + (RS : LinearCode ι F) {e : ℕ} (u v : ι → F) + (he : 3 * e < Code.minDist (RS : Set (ι → F))) + {a b c : F} {fa fb fc : ι → F} + (hfa : fa ∈ (RS : Set (ι → F))) (hfb : fb ∈ (RS : Set (ι → F))) (hfc : fc ∈ (RS : Set (ι → F))) + (hwa : Δ₀(u + a • v, fa) ≤ e) (hwb : Δ₀(u + b • v, fb) ≤ e) (hwc : Δ₀(u + c • v, fc) ≤ e) : + (a - b) • fc + (b - c) • fa + (c - a) • fb = 0 := by + classical + -- Use the shared weight bound and then apply the zero lemma. + have hwt : Code.wt ((b - c) • fa + (c - a) • fb + (a - b) • fc) ≤ 3 * e := by + -- Import from ThreeClosePoints; note the order of terms matches by commutativity. + simpa [add_comm, add_left_comm, add_assoc] + using (three_close_points_weight_bound (a := a) (b := b) (c := c) + (u := u) (v := v) (wₐ := fa) (w_b := fb) (w_c := fc) hwa hwb hwc) + -- The combination is a codeword in RS by closure (smul, add) + have hfa' : fa ∈ (RS : Submodule F (ι → F)) := by simpa using hfa + have hfb' : fb ∈ (RS : Submodule F (ι → F)) := by simpa using hfb + have hfc' : fc ∈ (RS : Submodule F (ι → F)) := by simpa using hfc + have hmem_RS : (a - b) • fc + (b - c) • fa + (c - a) • fb ∈ (RS : Set (ι → F)) := by + have h1 : (a - b) • fc ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS (a - b) hfc' + have h2 : (b - c) • fa ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS (b - c) hfa' + have h3 : (c - a) • fb ∈ (RS : Submodule F (ι → F)) := by + simpa using Submodule.smul_mem RS (c - a) hfb' + have h12 := Submodule.add_mem RS h1 h2 + have h123 := Submodule.add_mem RS h12 h3 + simpa using h123 + -- Reorder hwt to the expected sum and conclude + have hwt' : Code.wt ((a - b) • fc + (b - c) • fa + (c - a) • fb) ≤ 3 * e := by + simpa [add_comm, add_left_comm, add_assoc] using hwt + have hlt : Code.wt ((a - b) • fc + (b - c) • fa + (c - a) • fb) + < Code.minDist (RS : Set (ι → F)) := lt_of_le_of_lt hwt' he + exact zero_of_wt_lt_minDist (L := RS) hmem_RS hlt + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45.lean new file mode 100644 index 000000000..3c86950a6 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45.lean @@ -0,0 +1,40 @@ +/- +Lemma 4.5 (Ligero): probability of bad points on the row span. +This file hosts the statement; proof to be added. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.ClosePoints +import Mathlib.Probability.Distributions.Uniform +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma45.Assemble +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {κ ι : Type*} [Fintype κ] [Fintype ι] [DecidableEq ι] [Nonempty ι] + +noncomputable instance fintype_rowSpan + (U : Matrix κ ι F) : + Fintype ↥(Matrix.rowSpan U : Submodule F (ι → F)) := + Fintype.ofFinite _ + +/-- +Lemma 4.5 Ligero +-/ +lemma probOfBadPts {deg : ℕ} {α : ι ↪ F} {e : ℕ} {U : Matrix κ ι F} [NeZero deg] + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (hU : e < Δ(U,InterleavedCode.matrixSubmoduleOfLinearCode κ (ReedSolomon.code α deg))) : + (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure + { w | distFromCode (n := ι) (R := F) w (ReedSolomon.code α deg) ≤ e } + ≤ (Fintype.card ι - deg + 1)/(Fintype.card F) := by + -- Delegate to the assembly lemma combining direction existence, line counting, and averaging + simpa using + (ProximityToRS.probOfBadPts_assemble (deg := deg) (α := α) (e := e) (U := U) he hU) + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/00_Blueprint.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/00_Blueprint.lean new file mode 100644 index 000000000..57495d40b --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/00_Blueprint.lean @@ -0,0 +1,54 @@ +/- +Lemma 4.5 (Ligero): Probability of bad points on the row span. + +This file is a blueprint for the proof of Lemma 4.5. It outlines the +structure and the intermediate lemmas to be proved in the sibling files +of this directory. No statements are proved here; this is a roadmap. + +High‑level statement (informal): +Let `L = RS_{F,n,k,η}` have distance `d = n - k + 1` and let `e < d/3`. +If `Δ(U, L^m) > e` for an `m×n` matrix `U`, then for a uniformly random +`w` in the row span `L* = rowSpan U`, + + Pr[ distFromCode(w, L) ≤ e ] ≤ d / |F|. + +We implement this with a counting argument on cosets of the 1‑dimensional +subspace spanned by a particular direction `v* ∈ rowSpan U` that is +farther than `e` from `L` (via Lemma 4.3). + +Proof plan: +- Step A (Direction existence): From `Δ(U, L^m) > e` and `3e < d`, obtain + a vector `v* ∈ rowSpan U` with `distFromCode(v*, L) > e`. + Source: Lemma 4.3 (file: InterleavedCode/Lemma43.lean). + +- Step B (Per‑line counting): For any `x : F^n`, consider the affine line + `ℓ_x := { x + α • v* | α ∈ F }`. By Lemma 4.4 (line dichotomy), for each + `x` the number of `α` with `distFromCode(x + α•v*, L) ≤ e` is ≤ `d`. + The alternative case that all points on the line are within distance `≤ e` + is ruled out by `distFromCode(v*, L) > e` (take `x = 0, α = 1`). + +- Step C (Coset averaging): Partition `rowSpan U` into cosets of the + 1‑dimensional subspace `⟪v*⟫`. Each coset has size `|F|` and, by Step B, + contains at most `d` “good” elements (≤ e close to `L`). Therefore the + total number of good elements in `rowSpan U` is ≤ `(#cosets) * d`. + Since `#rowSpan U = (#cosets) * |F|`, the uniform probability is ≤ `d/|F|`. + +Files and responsibilities: +- 01_CosetAveraging.lean — finite coset partition and the probability bound +- 02_LineCounting.lean — apply Lemma 4.4 to show ≤ d good points per line +- 03_ExistDirection.lean — import Lemma 4.3 to get a far direction in row span +- 04_Assemble.lean — combine A+B+C to derive Lemma 4.5 + +Integration notes: +- The main theorem lives in `ProximityToRS/Lemma45.lean` as `probOfBadPts`. + Once helper lemmas are implemented, it can import the above files and + replace the placeholder proof. + +Dependencies: +- Lemma 4.3: `InterleavedCode/Lemma43.lean` (exists far direction in row span) +- Lemma 4.4: `ProximityToRS/Lemma44.lean` (line dichotomy bound ≤ d) + +-/ + +-- This file intentionally contains no executable code. + diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/Assemble.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/Assemble.lean new file mode 100644 index 000000000..45da5427e --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/Assemble.lean @@ -0,0 +1,103 @@ +/- +Assembling Lemma 4.5 from the components: lemma stub. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma45.CosetAveraging +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma45.LineCounting +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma45.ExistDirection +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {κ ι : Type*} [Fintype κ] [Fintype ι] [DecidableEq ι] [Nonempty ι] + +-- Stub: assemble the probability bound using the three components. +lemma probOfBadPts_assemble {deg : ℕ} [NeZero deg] {α : ι ↪ F} {e : ℕ} {U : Matrix κ ι F} + [Fintype (Matrix.rowSpan U)] + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (hU : e < Δ(U,InterleavedCode.matrixSubmoduleOfLinearCode κ (ReedSolomon.code α deg))) : + (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure + { w | distFromCode (n := ι) (R := F) w (ReedSolomon.code α deg) ≤ e } + ≤ (Fintype.card ι - deg + 1)/(Fintype.card F) := by + classical + -- Notation for the RS code + let RS : Set (ι → F) := (ReedSolomon.code α deg : Set (ι → F)) + -- Field size lower bound needed by Lemma 4.3 + have hmin' : Code.minDist (ReedSolomon.code α deg : Set (ι → F)) + = Fintype.card ι - deg + 1 := by + simpa using (ProximityToRS.minDist_RS_general (α := α) (deg := deg) (F := F) (ι := ι)) + have he' : 3 * e < Fintype.card ι - deg + 1 := by + simpa [hmin'] using he + have h_le : Fintype.card ι - deg + 1 ≤ Fintype.card ι + 1 := + Nat.succ_le_succ (Nat.sub_le _ _) + have h3e_le_n : 3 * e ≤ Fintype.card ι := by + have := lt_of_lt_of_le he' h_le + exact (Nat.lt_succ_iff.mp this) + have hι_leF : Fintype.card ι ≤ Fintype.card F := + Fintype.card_le_of_injective (fun i => (α i)) (by intro _ _ h; simpa using (α.injective h)) + have h3e_le_F : 3 * e ≤ Fintype.card F := le_trans h3e_le_n hι_leF + have hF : Nat.card F ≥ e.succ.succ := by + cases e with + | zero => + -- Show 2 ≤ |F| using 0 ≠ 1 in a field. + have h2le : 2 ≤ Fintype.card F := by + classical + -- Inject `Fin 2` into `F` via 0 ↦ 0, 1 ↦ 1 + let f : Fin 2 → F := fun i => (if (i : ℕ) = 0 then (0 : F) else 1) + have hf_inj : Function.Injective f := by + intro i j hij + fin_cases i <;> fin_cases j <;> simp [f] at hij ⊢ + have := Fintype.card_le_of_injective f hf_inj + simpa using this + simpa using h2le + | succ e' => + -- From 3(e+1) ≤ |F| and e+3 ≤ 3(e+1), deduce e+3 ≤ |F|. + have h_e3_le_3e : e'.succ.succ.succ ≤ 3 * e'.succ := by + -- nlinarith handles simple linear arithmetic over ℕ + nlinarith + have : e'.succ.succ.succ ≤ Fintype.card F := + le_trans h_e3_le_3e (by simpa using h3e_le_F) + -- e.succ.succ = (e'+1).succ.succ = e'+3 + simpa using this + -- Far direction in the row span from Lemma 4.3 + rcases ProximityToRS.exists_far_dir_in_rowSpan (α := α) (e := e) (U := U) + (hF := hF) (he := he) (hU := hU) with ⟨v, hv_span, hv_far⟩ + -- Per-line counting bound (≤ d = n - deg + 1 good scalars per line parallel to v) + have hline : ∀ x : ι → F, + Fintype.card {a : F // Code.distFromCode (x + a • v) RS ≤ e} + ≤ (Fintype.card ι - deg + 1) := + per_line_close_count_le_d (deg := deg) (α := α) (e := e) (v := v) + (he := he) (hv_far := hv_far) + -- A Fintype instance on the row span is available from the `Finite` hypothesis + -- Apply the uniform fraction bound with predicate P(w) := distFromCode(w, RS) ≤ e + let P : (ι → F) → Prop := fun w => Code.distFromCode w RS ≤ e + have hcoset : ∀ x ∈ Matrix.rowSpan U, + Nat.card {a : F // P (fun j => x j + a * v j)} ≤ (Fintype.card ι - deg + 1) := by + intro x _hx + simpa [P, Pi.add_apply, Pi.smul_apply, smul_eq_mul] using (hline x) + have hbound0 := + ProximityToRS.uniform_fraction_bound (U := U) (v := v) + (M := Fintype.card ι - deg + 1) P hv_span hcoset + -- Convert Nat.card to Fintype.card in the denominator. + have hbound : + (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure {w | P (w : ι → F)} + ≤ ((Fintype.card ι - deg + 1 : ENNReal) / (Fintype.card F : ENNReal)) := by + simpa [Nat.card_eq_fintype_card] using hbound0 + -- Rewrite to the desired form + -- Final rewrite to the goal statement: unfold the LHS definitionally + change + (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure + {w | P (w : ι → F)} + ≤ ((Fintype.card ι - deg + 1 : ENNReal) / (Fintype.card F : ENNReal)) + simpa [P, RS] using hbound + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/CosetAveraging.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/CosetAveraging.lean new file mode 100644 index 000000000..e9320647b --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/CosetAveraging.lean @@ -0,0 +1,212 @@ +/- +Coset averaging over a 1‑dimensional direction in a finite vector space. +This file provides lemma stubs used to bound the fraction of “good” points +in `rowSpan U` by averaging over cosets of a 1D subspace spanned by `v`. +-/ + +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Tactic + +noncomputable section + +open Code +open scoped BigOperators + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {κ ι : Type*} [Fintype κ] [Fintype ι] [DecidableEq ι] + +-- Injectivity: α ↦ x + α•v along a nonzero direction. +omit [Fintype F] [DecidableEq ι] in +lemma coset_injective {v x : ι → F} + (hv_ne : v ≠ 0) : + Function.Injective (fun a : F => (fun j => x j + a * v j)) := by + classical + intro a b h + -- Evaluate equality at a coordinate where v is nonzero. + have hex : ∃ j : ι, v j ≠ 0 := by + by_contra hnone + push_neg at hnone + apply hv_ne + funext j; simp [hnone j] + rcases hex with ⟨j₀, hvj₀⟩ + have hcoord := congrArg (fun (f : ι → F) => f j₀) h + have hmul : a * v j₀ = b * v j₀ := by + -- From x j₀ + a * v j₀ = x j₀ + b * v j₀ + have := hcoord + -- cancel x j₀ on the left + exact add_left_cancel this + -- From equality, deduce (a - b) * v j₀ = 0, and use v j₀ ≠ 0. + have h0 : (a - b) * v j₀ = 0 := by + have : a * v j₀ - b * v j₀ = 0 := sub_eq_zero.mpr hmul + simpa [sub_mul] using this + have : a - b = 0 := (mul_eq_zero.mp h0).resolve_right hvj₀ + exact sub_eq_zero.mp this + +-- Combinatorial core: double counting over cosets parallel to `v` inside `rowSpan U`. +-- It yields a cardinality inequality that underlies the uniform probability bound. +omit [DecidableEq F] [Fintype κ] [Fintype ι] [DecidableEq ι] in +lemma coset_averaging_card_bound + {U : Matrix κ ι F} {v : ι → F} {M : ℕ} + (P : (ι → F) → Prop) [DecidablePred P] + (hv_span : v ∈ Matrix.rowSpan U) + (hcoset : ∀ x ∈ Matrix.rowSpan U, + Nat.card {a : F // P (fun j => x j + a * v j)} ≤ M) + [Fintype (Matrix.rowSpan U)] : + Nat.card {w : Matrix.rowSpan U // P ((w : ι → F))} * Nat.card F + ≤ M * Nat.card (Matrix.rowSpan U) := by + classical + -- Regard v as an element of the row span and denote it by w. + let w : Matrix.rowSpan U := ⟨v, hv_span⟩ + -- Define the set of pairs (x, a) with x ∈ rowSpan U and P(x + a•v). + let Pairs := Σ x : Matrix.rowSpan U, {a : F // P ((x : ι → F) + a • v)} + have hPairs_le_F : Fintype.card Pairs ≤ Fintype.card (Matrix.rowSpan U) * M := by + -- card Σ x, {a // P(x + a•v)} = ∑_x card {a // ...} ≤ ∑_x M = |S| * M + classical + have hSigma_card : + Fintype.card Pairs + = ∑ x : Matrix.rowSpan U, Fintype.card {a : F // P ((x : ι → F) + a • v)} := by + -- standard cardinality of sigma over a finite index type + simp [Pairs] + have hSum_le : + (∑ x : Matrix.rowSpan U, Fintype.card {a : F // P ((x : ι → F) + a • v)}) + ≤ ∑ _x : Matrix.rowSpan U, M := by + refine Finset.sum_le_sum ?_ + intro x hx + -- Apply the coset hypothesis at x ∈ S + have hxS : (x : ι → F) ∈ Matrix.rowSpan U := x.property + have hx' := (hcoset (x := (x : ι → F)) hxS) + -- normalize pointwise description of (x + a•v) + simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using hx' + have hPairs_le_sum : Fintype.card Pairs ≤ ∑ _x : Matrix.rowSpan U, M := by + simpa [hSigma_card] using hSum_le + -- ∑_x M = |rowSpan U| * M + simpa [Finset.card_univ, Finset.sum_const_nat] using hPairs_le_sum + -- Build an injection from Good × F into Pairs, where Good := {y ∈ S | P y}. + let Good := {y : Matrix.rowSpan U // P ((y : ι → F))} + let ψ : Good × F → Pairs := + fun p => + let y : Matrix.rowSpan U := p.1.val + let a : F := p.2 + -- Show that P holds at ((y - a•w) + a•v) = y + have hP : P (((y - a • w : Matrix.rowSpan U) : ι → F) + a • v) := by + -- coe (y - a•w) = (y : _) - a•v, so the sum simplifies to y + have hsum : ((y - a • w : Matrix.rowSpan U) : ι → F) + a • v = (y : ι → F) := by + -- Use linearity of coercion and sub_add_cancel + -- In S: (y - a•w) + a•w = y + have hS : (y - a • w : Matrix.rowSpan U) + a • w = y := sub_add_cancel y (a • w) + -- Coerce to the ambient function space + have hcoe := congrArg (fun (z : Matrix.rowSpan U) => (z : ι → F)) hS + simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul, w, Subtype.coe_mk] using hcoe + -- use the fact that y is good under P + have hyP : P ((y : ι → F)) := p.1.property + -- Transport `hyP : P y` along the equality `hsum : ((y - a•w) + a•v) = y`. + have hEq : P (((y - a • w : Matrix.rowSpan U) : ι → F) + a • v) + = P ((y : ι → F)) := congrArg P hsum + exact (Eq.mp hEq.symm hyP) + -- Pack into the sigma type + ⟨y - a • w, ⟨a, hP⟩⟩ + have hψ_inj : Function.Injective ψ := by + intro p q h + -- Unpack components + rcases p with ⟨⟨y, hy⟩, a⟩; rcases q with ⟨⟨y', hy'⟩, a'⟩ + -- Extract second component equality to get a = a' + have haeq : a = a' := by + -- Compare the second component value (the scalar) of ψ p and ψ q + have h2 := congrArg (fun t : Pairs => t.2.1) h + -- By definition, (ψ ⟨⟨y,hy⟩, a⟩).2.1 = a + simpa [ψ] using h2 + -- With a = a', deduce y = y' from equality of first components + have hy_eq : y = y' := by + have hfirst := congrArg (fun t : Pairs => t.1) h + have hfirst' : (y - a • w : Matrix.rowSpan U) = (y' - a' • w : Matrix.rowSpan U) := by + simpa [ψ] using hfirst + -- rewrite a' by a and cancel + have hfirst'' : (y - a • w : Matrix.rowSpan U) = (y' - a • w : Matrix.rowSpan U) := by + simpa [haeq] + using hfirst' + -- add a•w to both sides and cancel + simpa using congrArg (fun z : Matrix.rowSpan U => z + a • w) hfirst'' + -- Conclude p = q + cases haeq; cases hy_eq; rfl + -- |Good| * |F| ≤ |Pairs| + have hGood_mul_le_F : Fintype.card Good * Fintype.card F ≤ Fintype.card Pairs := by + have hprod : Fintype.card (Good × F) = Fintype.card Good * Fintype.card F := by + classical + simpa using (Fintype.card_prod (α := Good) (β := F)) + simpa [hprod] using Fintype.card_le_of_injective (f := ψ) hψ_inj + -- Chain inequalities + have hPairs_le_nat : Nat.card Pairs ≤ M * Nat.card (Matrix.rowSpan U) := by + simpa [mul_comm] using hPairs_le_F + have hGood_mul_le_nat : + Nat.card {w : Matrix.rowSpan U // P ((w : ι → F))} * Nat.card F + ≤ Nat.card Pairs := by + simpa using hGood_mul_le_F + exact (hGood_mul_le_nat).trans (by simpa [mul_comm] using hPairs_le_nat) + +-- Uniform fraction bound stub: if each coset contributes at most M good points, +-- then the uniform probability over rowSpan U of being good is ≤ M/|F|. +lemma uniform_fraction_bound + {U : Matrix κ ι F} {v : ι → F} {M : ℕ} + (P : (ι → F) → Prop) [DecidablePred P] + (hv_span : v ∈ Matrix.rowSpan U) + (hcoset : ∀ x ∈ Matrix.rowSpan U, + Nat.card {a : F // P (fun j => x j + a * v j)} ≤ M) + [Fintype (Matrix.rowSpan U)] : + (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure { w | P (w : ι → F) } + ≤ (M : ENNReal) / (Nat.card F) := by + classical + -- Compute the LHS as a simple cardinality ratio via mathlib + let E' : Set (Matrix.rowSpan U) := { w | P (w : ι → F) } + -- Cardinality double counting bound on Good × F versus pairs (x,a) + have hcard := + coset_averaging_card_bound (U := U) (v := v) (M := M) P hv_span hcoset + -- Rewrite the RHS bound in terms of ENNReal arithmetic + have hF_ne : (Nat.card F : ENNReal) ≠ 0 := by simp + have hS_ne : (Nat.card (Matrix.rowSpan U) : ENNReal) ≠ 0 := by simp + have hcast : + ((Nat.card {w : Matrix.rowSpan U // P ((w : ι → F))} : ℕ) : ENNReal) + * (Nat.card F : ENNReal) + ≤ (M : ENNReal) * (Nat.card (Matrix.rowSpan U) : ENNReal) := by + exact_mod_cast hcard + have hratio₀ : ((Nat.card {w : Matrix.rowSpan U // P ((w : ι → F))} : ENNReal) + / (Nat.card (Matrix.rowSpan U) : ENNReal)) + ≤ (M : ENNReal) / (Nat.card F : ENNReal) := by + -- Clear denominator on the RHS + refine (ENNReal.le_div_iff_mul_le (h0 := Or.inl hF_ne) (ht := Or.inl (by simp))).2 ?_ + -- First, rewrite (a/#S) * #F as (a*#F)/#S in terms of Fintype.card + have hmul_div_rewrite' : + ((Fintype.card {w : Matrix.rowSpan U // P ((w : ι → F))} : ENNReal) + / (Fintype.card (Matrix.rowSpan U) : ENNReal)) * (Fintype.card F : ENNReal) + = (((Fintype.card {w : Matrix.rowSpan U // P ((w : ι → F))} : ENNReal) + * (Fintype.card F : ENNReal)) + / (Fintype.card (Matrix.rowSpan U) : ENNReal)) := by + simp [ENNReal.div_eq_inv_mul, mul_comm, mul_left_comm] + -- Now absorb the denominator (#S) using the casted cardinal inequality + have hdiv_le_nat : + (((Nat.card {w : Matrix.rowSpan U // P ((w : ι → F))} : ENNReal) + * (Nat.card F : ENNReal)) + / (Nat.card (Matrix.rowSpan U) : ENNReal)) ≤ (M : ENNReal) := by + exact (ENNReal.div_le_iff_le_mul (hb0 := Or.inl hS_ne) (hbt := Or.inl (by simp))).2 hcast + have hdiv_le : + (((Fintype.card {w : Matrix.rowSpan U // P ((w : ι → F))} : ENNReal) + * (Fintype.card F : ENNReal)) + / (Fintype.card (Matrix.rowSpan U) : ENNReal)) ≤ (M : ENNReal) := by + simpa using hdiv_le_nat + simpa [hmul_div_rewrite'] + -- Convert to a statement phrased using `Nat.card ↑E'` + have hratio : ((Nat.card (↑E') : ENNReal) + / (Nat.card (Matrix.rowSpan U) : ENNReal)) + ≤ (M : ENNReal) / (Nat.card F : ENNReal) := by + simpa [E'] using hratio₀ + -- Conclude via the uniform cardinality formula + calc + (PMF.uniformOfFintype (Matrix.rowSpan U)).toOuterMeasure E' + = (Nat.card (↑E') : ENNReal) / (Nat.card (Matrix.rowSpan U) : ENNReal) := by + simpa using (PMF.toOuterMeasure_uniformOfFintype_apply + (α := Matrix.rowSpan U) (s := E')) + _ ≤ (M : ENNReal) / (Nat.card F : ENNReal) := hratio + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/ExistDirection.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/ExistDirection.lean new file mode 100644 index 000000000..a66eae4c1 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/ExistDirection.lean @@ -0,0 +1,40 @@ +/- +Existence of a far direction in the row span (delegates to Lemma 4.3). +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.Defs +import ArkLib.Data.CodingTheory.InterleavedCode.Lemma43 +import Mathlib.Tactic + +noncomputable section + +open Code +open InterleavedCode + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {κ ι : Type*} [Fintype κ] [Fintype ι] [DecidableEq ι] + +-- Thin wrapper: obtain a far direction v* ∈ rowSpan U under the 3e and Δ(U, L^m) bounds. +lemma exists_far_dir_in_rowSpan + {deg : ℕ} {α : ι ↪ F} {e : ℕ} {U : Matrix κ ι F} + (hF : Nat.card F ≥ e.succ.succ) + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (hU : e < Δ(U,InterleavedCode.matrixSubmoduleOfLinearCode κ (ReedSolomon.code α deg))) : + ∃ v ∈ Matrix.rowSpan U, e < Code.distFromCode v (ReedSolomon.code α deg) := by + -- Instantiates Lemma 4.3 (InterleavedCode/Lemma43.lean) with the RS code. + classical + -- Package the RS code as a lawful interleaved code + let IC := InterleavedCode.lawfulInterleavedCodeOfLinearCode (κ := κ) + (LC := (ReedSolomon.code α deg : LinearCode ι F)) + -- Apply the main lemma + have := InterleavedCode.Lemma43.distInterleavedCodeToCodeLB + (IC := IC) (U := U) (e := e) + (hF := hF) (he := by simpa using he) (hU := by simpa using hU) + (hMF := rfl) + -- Unpack and conclude + simpa using this + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/LineCounting.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/LineCounting.lean new file mode 100644 index 000000000..89f04fca1 --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/Lemma45/LineCounting.lean @@ -0,0 +1,448 @@ +/- +Per‑line counting via Lemma 4.4 (Roth–Zémor): finished proofs. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Lemma44 +import Mathlib.Tactic + +open scoped BigOperators + +set_option linter.unnecessarySimpa false + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι] + +omit [Fintype F] [DecidableEq ι] [Nonempty ι] in +private lemma v_in_RS_of_all_close_e0 + {deg : ℕ} {α : ι ↪ F} {v x : ι → F} + (hall0 : ∀ a : F, Code.distFromCode (x + a • v) (ReedSolomon.code α deg) ≤ 0) : + v ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) := by + classical + have hx_mem : x ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) := by + have hx0 := hall0 0 + have : Code.distFromCode x (ReedSolomon.code α deg) = 0 := + le_antisymm (by simpa using hx0) bot_le + simpa using + (Code.distFromCode_eq_zero_iff_mem + ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) x).1 this + have hx1_mem : (x + (1 : F) • v) + ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) := by + have hx1 := hall0 1 + have : Code.distFromCode (x + (1 : F) • v) (ReedSolomon.code α deg) = 0 := + le_antisymm (by simpa using hx1) bot_le + simpa using + (Code.distFromCode_eq_zero_iff_mem + ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) + (x + (1 : F) • v)).1 this + have hsmul_mem : (1 : F) • v + ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) := by + have hsub := + Submodule.sub_mem (ReedSolomon.code α deg) + (by simpa using hx1_mem) (by simpa using hx_mem) + have hdiff : (x + (1 : F) • v) - x = (1 : F) • v := by simp + simpa [hdiff] using hsub + have : (1 : F)⁻¹ • ((1 : F) • v) + ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) := by + simpa using + Submodule.smul_mem (ReedSolomon.code α deg) ((1 : F)⁻¹) (by simpa using hsmul_mem) + simpa using this + +-- Existence of a far point on each parallel line through x. +lemma exists_far_on_line_through_x + {deg : ℕ} [NeZero deg] {α : ι ↪ F} {e : ℕ} {v x : ι → F} + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (hv_far : e < Code.distFromCode v (ReedSolomon.code α deg)) : + ∃ a : F, e < Code.distFromCode (x + a • v) (ReedSolomon.code α deg) := by + classical + -- Suppose, towards a contradiction, that every point on the line is within distance ≤ e. + by_contra hforall + have hall : ∀ a : F, + Code.distFromCode (x + a • v) (ReedSolomon.code α deg) ≤ e := by + intro a; exact not_lt.mp ((not_exists.mp hforall) a) + -- Split on whether e = 0 or e ≥ 1. + cases e with + | zero => + have hv_mem : v ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) := + v_in_RS_of_all_close_e0 (deg := deg) (α := α) (v := v) (x := x) + (by intro a; simpa using hall a) + have : Code.distFromCode v (ReedSolomon.code α deg) = 0 := by + simpa using + (Code.distFromCode_eq_zero_iff_mem + ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)) v).2 hv_mem + exact (lt_irrefl (0 : ℕ∞)) (by simpa [this] using hv_far) + | succ e' => + -- Build affine witnesses on all scalars and recenter to residuals r(a) = u' + a•v'. + let G : Finset F := Finset.univ + -- Helper: sum over the field of an indicator equals 1 + have sum_eq_one : ∀ x : F, + (Finset.univ : Finset F).sum (fun a => (if a = x then (1 : ℕ) else 0)) = 1 := by + classical + intro x + have hsum_card : + (Finset.univ : Finset F).sum (fun a => (if a = x then (1 : ℕ) else 0)) + = (Finset.univ.filter (fun a : F => a = x)).card := by + simpa [Finset.card_filter] + have hfilter : + (Finset.univ.filter (fun a : F => a = x)) = ({x} : Finset F) := by + classical + ext a; by_cases h : a = x + · simp [h] + · simp [h] + calc + (Finset.univ : Finset F).sum (fun a => (if a = x then (1 : ℕ) else 0)) + = (Finset.univ.filter (fun a : F => a = x)).card := hsum_card + _ = ({x} : Finset F).card := by simpa [hfilter] + _ = 1 := by simp + have hf_ex : ∀ a : {a : F // a ∈ G}, + ∃ w ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)), + Δ₀(x + a.1 • v, w) ≤ e'.succ := by + intro a + exact + ProximityToRS.exists_codeword_close_of_dist_le + (u := x + a.1 • v) (C := (ReedSolomon.code α deg)) (e := e'.succ) + (by simpa using hall a.1) + choose f hfRS hfclose using hf_ex + have h0 : (0 : F) ∈ G := by simp [G] + have h1 : (1 : F) ∈ G := by simp [G] + obtain ⟨cstar, dstar, hc_in, hd_in, hfa_affine⟩ := + ProximityToRS.affine_param_on_G (RS := ReedSolomon.code α deg) + (u := x) (v := v) (G := G) (a0 := 0) (a1 := 1) + (ha0 := h0) (ha1 := h1) (hneq := by simpa using (zero_ne_one : (0 : F) ≠ 1)) + (he3 := he) (f := f) + (hfRS := by intro a; simpa using hfRS a) + (hfclose := by intro a; simpa using hfclose a) + set u' : ι → F := x - cstar + set v' : ι → F := v - dstar + have hres_le : ∀ a : F, Code.wt (u' + a • v') ≤ e'.succ := by + intro a + have hfa := congrArg (fun (g : ι → F) => (x + a • v) - g) (hfa_affine ⟨a, by simp [G]⟩) + have hdist_le : Code.wt ((x + a • v) - f ⟨a, by simp [G]⟩) ≤ e'.succ := by + simpa [LinearCode.hammingDist_eq_wt_sub] using (hfclose ⟨a, by simp [G]⟩) + have hdist_le' : Code.wt ((x + a • v) - (cstar + a • dstar)) ≤ e'.succ := by + simpa [hfa] using hdist_le + have : (x + a • v) - (cstar + a • dstar) = u' + a • v' := by + simp [u', v', sub_eq_add_neg, add_comm, add_left_comm, add_assoc, smul_add] + simpa [this, sub_eq_add_neg] using hdist_le' + -- New double-counting lower bound on the total sum of weights across all scalars + let S : Finset ι := Finset.univ.filter (fun i : ι => v' i ≠ 0) + have hsum_lb : (∑ a : F, Code.wt (u' + a • v')) + ≥ (Fintype.card F - 1) * S.card := by + classical + let a0 : ι → F := fun i => if h : v' i = 0 then 0 else -u' i * (v' i)⁻¹ + have hsubset_for_a : ∀ a : F, + (S.filter (fun i : ι => a ≠ a0 i)) + ⊆ (Finset.univ.filter + (fun i : ι => (u' + a • v') i ≠ 0)) := by + intro a i hi + have hvi : v' i ≠ 0 := by simpa [S] using (Finset.mem_filter.mp hi).1 + have ha_ne : a ≠ a0 i := (Finset.mem_filter.mp hi).2 + have hneq : u' i + a * v' i ≠ 0 := by + have ha0_def : a0 i = -u' i * (v' i)⁻¹ := by simpa [a0, hvi] + intro hzero + -- Multiply by (v' i)⁻¹ and solve for a; use v' i ≠ 0 + have hmul := congrArg (fun t => t * (v' i)⁻¹) hzero + have hvne : v' i ≠ 0 := hvi + have hsum : u' i * (v' i)⁻¹ + a = 0 := by + -- (u' + a * v') * (v')⁻¹ = u' * (v')⁻¹ + a * (v' * (v')⁻¹) = u' * (v')⁻¹ + a + simpa [mul_add, add_mul, mul_left_comm, mul_comm, mul_assoc, + CommGroupWithZero.mul_inv_cancel (v' i) hvne, mul_one] using hmul + have a_eq : a = -u' i * (v' i)⁻¹ := by + have : a = -(u' i * (v' i)⁻¹) := by + have := eq_neg_of_add_eq_zero_right hsum + simpa [mul_comm] using this + simpa [mul_comm] using this + have : a = a0 i := by simpa [ha0_def] using a_eq + exact ha_ne this + have : (u' + a • v') i ≠ 0 := by + -- pointwise evaluation of addition and scalar multiplication on functions + simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using hneq + have : i ∈ (Finset.univ.filter fun i : ι => (u' + a • v') i ≠ 0) := by + apply Finset.mem_filter.mpr; apply And.intro; simp; exact this + exact this + have hwt_ge : ∀ a : F, + Code.wt (u' + a • v') ≥ (S.filter (fun i : ι => a ≠ a0 i)).card := by + intro a; simpa [Code.wt] using Finset.card_mono (hsubset_for_a a) + have hsum_ge : (∑ a : F, Code.wt (u' + a • v')) + ≥ ∑ a : F, (S.filter (fun i : ι => a ≠ a0 i)).card := + by exact Finset.sum_le_sum (fun a _ => hwt_ge a) + -- Direct double counting via swapping sums and counting nonzeros for each coordinate + -- First, evaluate the inner sum for each fixed coordinate i ∈ S. + have hinner : ∀ i ∈ S, + ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) + = Fintype.card F - 1 := by + classical + intro i hi + have hvne : v' i ≠ 0 := by + have : i ∈ Finset.univ.filter (fun j : ι => v' j ≠ 0) := by simpa [S] using hi + simpa [Finset.mem_filter] using this + -- Unique zero at a0 i + have hzero_iff : ∀ a : F, (u' i + a * v' i) = 0 ↔ a = a0 i := by + intro a; constructor + · intro h0 + -- Multiply by (v' i)⁻¹ on the right and solve for a + have hmul := congrArg (fun t => t * (v' i)⁻¹) h0 + have hsum : u' i * (v' i)⁻¹ + a = 0 := by + -- (u' + a * v') * (v')⁻¹ = u' * (v')⁻¹ + a * (v' * (v')⁻¹) = u' * (v')⁻¹ + a + simpa [mul_add, add_mul, mul_left_comm, mul_comm, mul_assoc, + CommGroupWithZero.mul_inv_cancel (v' i) hvne, mul_one] using hmul + have hsum' : a + u' i * (v' i)⁻¹ = 0 := by simpa [add_comm] using hsum + have : a = -(u' i * (v' i)⁻¹) := eq_neg_of_add_eq_zero_left hsum' + simpa [a0, hvne, mul_comm, mul_left_comm, mul_assoc] using this + · intro ha + -- Substitute a = a0 i and compute + subst ha + have hmul' : a0 i * v' i = -u' i := by + simp [a0, hvne] + simpa [hmul'] + -- sum of (≠ 0) equals |F| - sum of (=0) + -- Evaluate the inner sum via counting: {a | u' i + a*v' i ≠ 0} = univ.erase (a0 i) + have hzero_iff' : ∀ a : F, (u' i + a * v' i = 0) ↔ a = a0 i := hzero_iff + have hfilter_eq : + (Finset.univ.filter fun a : F => (u' i + a * v' i) ≠ 0) + = (Finset.univ.erase (a0 i)) := by + classical + ext a; constructor + · intro ha + have haU : a ∈ (Finset.univ : Finset F) := by simpa using (Finset.mem_filter.mp ha).1 + have hane : a ≠ a0 i := by + have : (u' i + a * v' i) ≠ 0 := (Finset.mem_filter.mp ha).2 + exact by + intro hEq; apply this; have := (hzero_iff' a).mpr hEq; simpa using this + simpa [Finset.mem_erase, haU, hane, and_comm] -- reorder to match simp normal form + · intro ha + have haU : a ∈ (Finset.univ : Finset F) := by + exact (Finset.mem_erase.mp ha).2 + have hane : a ≠ a0 i := (Finset.mem_erase.mp ha).1 + have hne0 : (u' i + a * v' i) ≠ 0 := by + intro h0; exact hane ((hzero_iff' a).mp h0) + exact by + apply Finset.mem_filter.mpr; exact And.intro (by simpa using haU) hne0 + -- Now evaluate the sum as a cardinality + have hzsum : + ∑ a : F, (if (u' i + a * v' i) = 0 then 1 else 0) = 1 := by + classical + have : (fun a : F => (if (u' i + a * v' i) = 0 then 1 else 0)) + = (fun a : F => (if a = a0 i then 1 else 0)) := by + funext a; by_cases h : (u' i + a * v' i) = 0 + · have : a = a0 i := (hzero_iff' a).mp h; simp [←this, h] + · have : a ≠ a0 i := by + intro contra; apply h; have := (hzero_iff' a).mpr contra; simpa using this + simp [h, this] + simpa [this] using (sum_eq_one (a0 i)) + have htot : ∑ a : F, (1 : ℕ) = Fintype.card F := by + classical + have h₁ : ∀ a ∈ (Finset.univ : Finset F), (1 : ℕ) = 1 := by intro a ha; rfl + simpa using (Finset.sum_const_nat (s := (Finset.univ : Finset F)) (f := fun _ : F => (1 : ℕ)) (m := 1) h₁) + calc + ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) + = (Finset.univ.filter fun a : F => (u' i + a * v' i) ≠ 0).card := by + classical + simpa [Finset.card_filter] + _ = (Finset.univ.erase (a0 i)).card := by simpa [hfilter_eq] + _ = Fintype.card F - 1 := by + classical + simpa using (Finset.card_erase (s := (Finset.univ : Finset F)) (a := a0 i)) + -- Then swap sums and use the inner evaluation to compute the total. + have hsum_eq_S : + ∑ a : F, (S.filter (fun i : ι => (u' + a • v') i ≠ 0)).card + = (Fintype.card F - 1) * S.card := by + classical + have h1 : ∀ a : F, + (S.filter (fun i : ι => (u' + a • v') i ≠ 0)).card + = ∑ i ∈ S, (if (u' i + a * v' i) ≠ 0 then 1 else 0) := by + intro a; simp [Pi.smul_apply, smul_eq_mul, Finset.card_filter] + have h2 : + ∑ a : F, (S.filter (fun i : ι => (u' + a • v') i ≠ 0)).card + = ∑ a : F, ∑ i ∈ S, (if (u' i + a * v' i) ≠ 0 then 1 else 0) := by + refine Finset.sum_congr rfl ?_; + intro a ha; simpa using h1 a + have h3 : + ∑ a : F, ∑ i ∈ S, (if (u' i + a * v' i) ≠ 0 then 1 else 0) + = ∑ i ∈ S, ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) := by + classical + -- Swap the order of summation explicitly to avoid heavy simp search + exact Finset.sum_comm + have h4 : + ∑ i ∈ S, ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) + = (Fintype.card F - 1) * S.card := by + -- Evaluate each inner sum using hinner and then sum constants over S + have h4a : + ∑ i ∈ S, ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) + = ∑ i ∈ S, (Fintype.card F - 1) := + Finset.sum_congr rfl (fun i hi => by simpa using hinner i hi) + have h4b : ∑ i ∈ S, (Fintype.card F - 1) = S.card * (Fintype.card F - 1) := by + classical + -- Sum of a constant over a finite set equals cardinality times the constant + simpa [Finset.sum_const, nsmul_eq_mul] + -- Chain the equalities and orient the product at the end + calc + ∑ i ∈ S, ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) + = ∑ i ∈ S, (Fintype.card F - 1) := by simpa using h4a + _ = S.card * (Fintype.card F - 1) := h4b + _ = (Fintype.card F - 1) * S.card := by simpa [Nat.mul_comm] + -- Rewrite the left-hand side via h2, then swap sums (h3), and apply h4 + calc + ∑ a : F, (S.filter (fun i : ι => (u' + a • v') i ≠ 0)).card + = ∑ a : F, ∑ i ∈ S, (if (u' i + a * v' i) ≠ 0 then 1 else 0) := by simpa using h2 + _ = ∑ i ∈ S, ∑ a : F, (if (u' i + a * v' i) ≠ 0 then 1 else 0) := by simpa using h3 + _ = (Fintype.card F - 1) * S.card := h4 + -- Final lower bound: wt dominates filtered-card sum + have hsum_ge' : + (∑ a : F, Code.wt (u' + a • v')) + ≥ ∑ a : F, (S.filter (fun i : ι => (u' + a • v') i ≠ 0)).card := by + classical + refine Finset.sum_le_sum ?_ + intro a ha + -- S.filter ⊆ univ.filter ⇒ card ≤ card; but wt = card of univ.filter + have hsubset : (S.filter (fun i : ι => (u' + a • v') i ≠ 0)) + ⊆ (Finset.univ.filter (fun i : ι => (u' + a • v') i ≠ 0)) := by + intro i hi + have hiU : i ∈ Finset.univ := by simp + have hcond : (u' + a • v') i ≠ 0 := (Finset.mem_filter.mp hi).2 + simpa [Finset.mem_filter] using And.intro hiU hcond + have hcard_le := Finset.card_mono hsubset + simpa [Code.wt, Pi.smul_apply, smul_eq_mul] using hcard_le + -- Combine the two steps to get the target bound + have : (∑ a : F, Code.wt (u' + a • v')) ≥ (Fintype.card F - 1) * S.card := by + classical + calc + ∑ a : F, Code.wt (u' + a • v') + ≥ ∑ a : F, (S.filter (fun i : ι => (u' + a • v') i ≠ 0)).card := hsum_ge' + _ = (Fintype.card F - 1) * S.card := hsum_eq_S + exact this + -- Upper bound via the per-scalar residual guarantee. + have hsum_ub : + (∑ a : F, Code.wt (u' + a • v')) ≤ (Fintype.card F) * e'.succ := by + classical + have hpt : ∀ a : F, Code.wt (u' + a • v') ≤ e'.succ := hres_le + have hsum_le : + (∑ a : F, Code.wt (u' + a • v')) ≤ ∑ a : F, e'.succ := + Finset.sum_le_sum (by intro a _; exact hpt a) + -- Evaluate the RHS as a constant sum over univ + simpa [Finset.card_univ, Finset.sum_const, nsmul_eq_mul, Nat.mul_comm] + using hsum_le + -- From 3*e < d ≤ |ι| + 1 ≤ |F| + 1, deduce |F| ≥ e + 2 + have hminRS : Code.minDist (ReedSolomon.code α deg : Set (ι → F)) + = Fintype.card ι - deg + 1 := by + simpa using (ProximityToRS.minDist_RS_general (α := α) (deg := deg) (F := F) (ι := ι)) + have h3e_lt : 3 * e'.succ < Fintype.card ι - deg + 1 := by simpa [hminRS] using he + have h3e_le_ι : 3 * e'.succ ≤ Fintype.card ι := by + have : Fintype.card ι - deg + 1 ≤ Fintype.card ι + 1 := Nat.succ_le_succ (Nat.sub_le _ _) + exact Nat.lt_succ_iff.mp (lt_of_lt_of_le h3e_lt this) + have hι_leF : Fintype.card ι ≤ Fintype.card F := + Fintype.card_le_of_injective (fun i => (α i)) (by intro i j hij; simpa using (α.injective hij)) + have hF_large : e'.succ.succ.succ ≤ Fintype.card F := by + have h3e_leF : 3 * e'.succ ≤ Fintype.card F := le_trans h3e_le_ι hι_leF + -- Since e'.succ ≥ 1, we have e'.succ + 2 ≤ 3 * e'.succ + have h1 : e'.succ.succ.succ ≤ 3 * e'.succ := by nlinarith + exact le_trans h1 h3e_leF + -- If wt(v') ≥ e+1, then (|F|-1)*(e+1) ≤ sum ≤ |F|*e, impossible when |F| ≥ e+2. + have hv'_le : Code.wt v' ≤ e'.succ := by + classical + by_contra hk + have hk' : e'.succ.succ ≤ Code.wt v' := Nat.succ_le_of_lt (lt_of_not_ge hk) + have hsum_lb' : + (Fintype.card F - 1) * (e'.succ + 1) + ≤ (∑ a : F, Code.wt (u' + a • v')) := by + have : (Fintype.card F - 1) * (e'.succ + 1) + ≤ (Fintype.card F - 1) * (Code.wt v') := + Nat.mul_le_mul_left _ hk' + exact le_trans this hsum_lb + have hle : + (Fintype.card F - 1) * (e'.succ + 1) + ≤ Fintype.card F * e'.succ := + le_trans hsum_lb' hsum_ub + -- But for |F| ≥ e+2 this inequality is false. + have : False := by + -- Rewrite (|F|-1)*(e+1) as |F|*e + (|F| - (e+1)) and cancel. + -- From e + 2 ≤ |F| we also get e + 1 < |F| + have hltF' : e'.succ.succ < Fintype.card F := (Nat.succ_le_iff.mp hF_large) + have hrewrite : + (Fintype.card F - 1) * (e'.succ + 1) + = Fintype.card F * e'.succ + + (Fintype.card F - (e'.succ + 1)) := by + -- (m - 1) * k = m*k - 1*k + have h₁ : + (Fintype.card F - 1) * (e'.succ + 1) + = Fintype.card F * (e'.succ + 1) - (e'.succ + 1) := by + simpa using Nat.sub_mul (Fintype.card F) 1 (e'.succ + 1) + -- m * (n + 1) = m*n + m + have h₂ : Fintype.card F * (e'.succ + 1) + = Fintype.card F * e'.succ + Fintype.card F := by + simpa [Nat.mul_add, Nat.mul_one, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] + -- (a + b) - c = a + (b - c) when c ≤ b + have hleF : e'.succ + 1 ≤ Fintype.card F := le_of_lt hltF' + have h₃ : (Fintype.card F * e'.succ + Fintype.card F) + - (e'.succ + 1) + = Fintype.card F * e'.succ + + (Fintype.card F - (e'.succ + 1)) := by + -- (a + b) - c = a + (b - c) when c ≤ b + have hgen := Nat.add_sub_assoc hleF + simpa using (hgen (Fintype.card F * e'.succ)) + -- Chain the equalities + calc + (Fintype.card F - 1) * (e'.succ + 1) + = Fintype.card F * (e'.succ + 1) - (e'.succ + 1) := h₁ + _ = (Fintype.card F * e'.succ + Fintype.card F) + - (e'.succ + 1) := by simpa [h₂] + _ = Fintype.card F * e'.succ + + (Fintype.card F - (e'.succ + 1)) := h₃ + -- Cancel the common left summand to get (|F| - (e+1)) ≤ 0 + have hcancel : Fintype.card F - (e'.succ + 1) ≤ 0 := by + -- From hle and the rewrite, cancel the left term using add_le_add_iff_left + have : Fintype.card F * e'.succ + + (Fintype.card F - (e'.succ + 1)) + ≤ Fintype.card F * e'.succ := by + simpa [hrewrite] using hle + exact Nat.le_of_add_le_add_left this + -- But |F| ≥ e+2 ⇒ |F| - (e+1) ≥ 1, contradiction + have hpos : 0 < Fintype.card F - (e'.succ + 1) := Nat.sub_pos_of_lt hltF' + have hone_le : 1 ≤ Fintype.card F - (e'.succ + 1) := Nat.succ_le_of_lt hpos + exact (not_le_of_gt hone_le hcancel).elim + exact this.elim + -- Conclude dist(v, RS) ≤ e using d* ∈ RS and wt(v - d*) ≤ e. + have hv_le : Code.distFromCode v (ReedSolomon.code α deg) ≤ e'.succ := by + have hvd_nat : (Code.wt v' : ℕ∞) ≤ (e'.succ : ℕ∞) := by exact_mod_cast hv'_le + have hvd_le : (hammingDist v dstar : ℕ∞) ≤ e'.succ := by + simpa [LinearCode.hammingDist_eq_wt_sub, v', sub_eq_add_neg] using hvd_nat + have hmem : (e'.succ : ℕ∞) + ∈ {d : ℕ∞ | ∃ z ∈ ((ReedSolomon.code α deg : Submodule F (ι → F)) : Set (ι → F)), hammingDist v z ≤ d} := by + exact ⟨dstar, hd_in, hvd_le⟩ + have hsInf_le := sInf_le hmem + simpa [Code.distFromCode] using hsInf_le + -- Combine dist ≤ e and e < dist to get a contradiction + have hlt := lt_of_le_of_lt hv_le hv_far + exact lt_irrefl _ hlt + +-- Bound the count of close points per line by d. +lemma per_line_close_count_le_d + {deg : ℕ} [NeZero deg] {α : ι ↪ F} {e : ℕ} {v : ι → F} + (he : 3 * e < Code.minDist (ReedSolomon.code α deg : Set (ι → F))) + (hv_far : e < Code.distFromCode v (ReedSolomon.code α deg)) : + ∀ x : ι → F, + Fintype.card {a : F // Code.distFromCode (x + a • v) (ReedSolomon.code α deg) ≤ e} + ≤ (Fintype.card ι - deg + 1) := by + classical + intro x + have h := ProximityToRS.line_dichotomy_card_good (deg := deg) (α := α) (e := e) he x v + rcases h with hall | hfew + · -- Contradiction with existence of a far point on the line + have ⟨a, ha⟩ := exists_far_on_line_through_x (deg := deg) (α := α) (e := e) + (he := he) (hv_far := hv_far) (x := x) + have : Code.distFromCode (x + a • v) (ReedSolomon.code α deg) ≤ e := hall a + exact (lt_of_le_of_lt this ha).false.elim + · -- Bound the number of good scalars by the RS minimum distance, then rewrite to d = n - deg + 1. + have hmin : + Code.minDist (ReedSolomon.code α deg : Set (ι → F)) = Fintype.card ι - deg + 1 := by + simpa using (ProximityToRS.minDist_RS_general (α := α) (deg := deg) (F := F) (ι := ι)) + simpa [hmin] using hfew + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/ThreeClosePoints.lean b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/ThreeClosePoints.lean new file mode 100644 index 000000000..f0e28facf --- /dev/null +++ b/ArkLib/Data/CodingTheory/InterleavedCode/ProximityToRS/ThreeClosePoints.lean @@ -0,0 +1,119 @@ +/- +Three close points on an affine line and consequences. +This file isolates the long weight bound lemma so it can compile separately. +-/ + +import ArkLib.Data.CodingTheory.ReedSolomon +import ArkLib.Data.CodingTheory.InterleavedCode.ProximityToRS.Aux +import Mathlib.Tactic + +noncomputable section + +open Code + +namespace ProximityToRS + +variable {F : Type*} [Field F] [DecidableEq F] [Fintype F] +variable {ι : Type*} [Fintype ι] [DecidableEq ι] +variable {deg : ℕ} {α : ι ↪ F} + +/-- If three points on the affine line are each within `e` of the RS code, then the standard +linear combination has weight at most `3*e`. + +Let `wₐ, w_b, w_c` be corresponding close codewords to `u + a•v`, `u + b•v`, `u + c•v`. +Then `(b-c)•wₐ + (c-a)•w_b + (a-b)•w_c` has weight ≤ `3*e`. +-/ +lemma three_close_points_weight_bound + (a b c : F) {e : ℕ} {u v : ι → F} + {wₐ w_b w_c : ι → F} + (dₐ : Δ₀(u + a • v, wₐ) ≤ e) + (d_b : Δ₀(u + b • v, w_b) ≤ e) + (d_c : Δ₀(u + c • v, w_c) ≤ e) : + Code.wt ((b - c) • wₐ + (c - a) • w_b + (a - b) • w_c) ≤ 3 * e := by + classical + -- Define residuals rₐ, r_b, r_c capturing the e-closeness witnesses + set rₐ : ι → F := (u + a • v) - wₐ + set r_b : ι → F := (u + b • v) - w_b + set r_c : ι → F := (u + c • v) - w_c + have hrₐ : Code.wt rₐ ≤ e := by + -- Δ₀(u + a•v, wₐ) = wt((u + a•v) - wₐ) + simpa [rₐ, LinearCode.hammingDist_eq_wt_sub, sub_eq_add_neg] using dₐ + have hr_b : Code.wt r_b ≤ e := by + simpa [r_b, LinearCode.hammingDist_eq_wt_sub, sub_eq_add_neg] using d_b + have hr_c : Code.wt r_c ≤ e := by + simpa [r_c, LinearCode.hammingDist_eq_wt_sub, sub_eq_add_neg] using d_c + + -- Consider the standard linear combination of residuals and codewords + let R : ι → F := (b - c) • rₐ + (c - a) • r_b + (a - b) • r_c + let W : ι → F := (b - c) • wₐ + (c - a) • w_b + (a - b) • w_c + let S : ι → F := + (b - c) • (u + a • v) + (c - a) • (u + b • v) + (a - b) • (u + c • v) + + -- Coefficient identity used for cancellation on the affine line + have hcoeff_v : (b - c) * a + (c - a) * b + (a - b) * c = (0 : F) := by ring + + -- Regroup S into u- and v-terms, both vanish + have hS_zero : S = 0 := by + -- Prove pointwise using cancellation of coefficients + ext i + have : + S i = ((b - c) + (c - a) + (a - b)) * (u i) + + ((b - c) * a + (c - a) * b + (a - b) * c) * (v i) := by + simp [S] + ring + simp [this, hcoeff_v] + + -- R = S - W, hence R = -W since S = 0 + have hRS : R = S - W := by + unfold R W S rₐ r_b r_c + simp [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] + have hR_eq_negW : R = -W := by + simpa [hS_zero] using hRS + + -- wt(W) = wt(-R) = wt(R) + have hwt_eq : Code.wt W = Code.wt R := by + -- From R = -W, deduce W = (-1)•R and use weight invariance under nonzero smul + have hneg : (-1 : F) ≠ 0 := by simpa using (neg_ne_zero.mpr (one_ne_zero : (1 : F) ≠ 0)) + have hW_eq : (-1 : F) • R = W := by + -- Apply smul to both sides of R = -W + have := congrArg (fun x => (-1 : F) • x) hR_eq_negW + simpa [smul_neg, one_smul] using this + -- thus wt W = wt ((-1)•R) = wt R + simpa [hW_eq] using (wt_smul_eq_of_ne_zero (ι := ι) (a := (-1 : F)) (x := R) hneg) + + -- Triangle inequality and scaling bound give wt(R) ≤ wt((b-c)•rₐ) + wt((c-a)•r_b) + wt((a-b)•r_c) + have hsmul_le : ∀ (s : F) (x : ι → F), Code.wt (s • x) ≤ Code.wt x := by + intro s x; by_cases hs : s = 0 + · simp [hs, Code.wt] + · simp [wt_smul_eq_of_ne_zero hs] + have hR_le : Code.wt R ≤ Code.wt ((b - c) • rₐ) + Code.wt ((c - a) • r_b + (a - b) • r_c) := by + simpa [R, add_assoc] using + (wt_add_le (x := (b - c) • rₐ) (y := (c - a) • r_b + (a - b) • r_c)) + have h_tail : Code.wt ((c - a) • r_b + (a - b) • r_c) + ≤ Code.wt ((c - a) • r_b) + Code.wt ((a - b) • r_c) := by + simpa using (wt_add_le (x := (c - a) • r_b) (y := (a - b) • r_c)) + have hR_le' : Code.wt R ≤ Code.wt ((b - c) • rₐ) + + (Code.wt ((c - a) • r_b) + Code.wt ((a - b) • r_c)) := by + exact le_trans hR_le (add_le_add_left h_tail _) + -- Bound each scaled residual by the residual's weight + have hb1 : Code.wt ((b - c) • rₐ) ≤ Code.wt rₐ := hsmul_le (b - c) rₐ + have hb2 : Code.wt ((c - a) • r_b) ≤ Code.wt r_b := hsmul_le (c - a) r_b + have hb3 : Code.wt ((a - b) • r_c) ≤ Code.wt r_c := hsmul_le (a - b) r_c + -- Chain the inequalities and use hrₐ, hr_b, hr_c ≤ e + have : Code.wt R ≤ e + (e + e) := by + refine le_trans hR_le' ?_ + have hsumle' : Code.wt ((b - c) • rₐ) + + (Code.wt ((c - a) • r_b) + Code.wt ((a - b) • r_c)) + ≤ Code.wt rₐ + (Code.wt r_b + Code.wt r_c) := by + simpa [add_assoc] using (add_le_add (add_le_add hb1 hb2) hb3) + have hsumle : Code.wt rₐ + (Code.wt r_b + Code.wt r_c) ≤ e + (e + e) := by + simpa [add_assoc] using (add_le_add (add_le_add hrₐ hr_b) hr_c) + exact le_trans hsumle' hsumle + -- Convert to 3*e by arithmetic + have hsum : e + (e + e) = 3 * e := by linarith + -- Conclude for W using wt(W) = wt(R) + have hR_le_3e : Code.wt R ≤ 3 * e := by simpa [hsum] using this + simp [←hwt_eq, W] at hR_le_3e + exact hR_le_3e + +end ProximityToRS diff --git a/ArkLib/Data/CodingTheory/Prelims.lean b/ArkLib/Data/CodingTheory/Prelims.lean index c09231d79..cb3274c79 100644 --- a/ArkLib/Data/CodingTheory/Prelims.lean +++ b/ArkLib/Data/CodingTheory/Prelims.lean @@ -68,10 +68,12 @@ end Matrix end -/-- Affine line between two vectors with coefficients in a semiring. +/-- Affine line through `u` in direction `v`: the set `{u + a • v | a : F}`. +Note: we intentionally return a `Set` (not a submodule), since an affine line is generally +not closed under addition unless `u = 0`. This matches the intended usage “x ∈ Affine.line u v”. -/ -def Affine.line {F : Type*} {ι : Type*} [Ring F] (u v : ι → F) : Submodule F (ι → F) := - vectorSpan _ {u, v} +def Affine.line {F : Type*} {ι : Type*} [Semiring F] (u v : ι → F) : Set (ι → F) := + {x | ∃ a : F, x = u + a • v} namespace sInf