RS-membership lemmas for evalOnPoints (☺️ very cute ☺️)

[ElijahVlasov]

To prove that evalOnPoints α p belongs to a code α n it is enough to prove that p has an appropriate degree bound.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: RS-membership lemmas for evalOnPoints (☺️ very cute ☺️)

Mathematical Formalization

This PR adds two new membership lemmas for Reed–Solomon codes, making it more convenient to prove that a codeword produced by evalOnPoints α p belongs to the code code α n.

• evalOnPoints_mem_code_of_degree_lt: If p.degree < n then evalOnPoints α p ∈ code α n.
• evalOnPoints_mem_code_of_natDegree_lt: If p.natDegree < n then evalOnPoints α p ∈ code α n.

These provide shortened, purpose-built criteria compared to the existing general lemma mem_code_iff_exists_polynomial. The core addition is concentrated in ArkLib/Data/CodingTheory/ReedSolomon.lean; the unit of analysis is the polynomial p and these lemmas directly connect degree bounds on p to code membership of the evaluated vector. No sorry or admit placeholders are introduced.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	12
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 2 declaration(s)

ArkLib/Data/CodingTheory/ReedSolomon.lean (2)

• lemma evalOnPoints_mem_code_of_degree_lt {α : ι ↪ F} {p : F[X]} (h_deg : p.degree < n) :
• lemma evalOnPoints_mem_code_of_natDegree_lt {α : ι ↪ F} {p : F[X]} (h_deg : p.natDegree < n) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The code changes in the diff are consistent with the ArkLib contribution guidelines. No violations of the provided style, naming, documentation, or formatting rules were detected in the code diff itself. (The PR title and description were not available for review, so the title format guidelines could not be checked.)

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ReedSolomon.lean: Added two new lemmas, evalOnPoints_mem_code_of_degree_lt and evalOnPoints_mem_code_of_natDegree_lt, which provide shortened membership criteria for the Reed–Solomon code code α n: they state that evalOnPoints α p is in the code whenever p.degree < n or p.natDegree < n respectively. The existing lemma mem_code_iff_exists_polynomial is left unchanged. No sorry or admit is introduced.

---

Last updated: 2026-07-21 19:31 UTC.