Resolving issue #217

[DimitriosMitsios]

This PR completes issue #217.

The definition of checkMatrix follows the instructions of issue #217 along with:

1. An additional typeclass assumption Field F due to the existence of an inverse in the formula of the matrix element.
2. The modifier noncomputable dealing with the definition of the polynomial.
3. The addition of the typeclass assumption Semiring F in genMatrix

[github-actions]

🤖 Gemini PR Summary

This PR implements the parity-check matrix functionality for Reed-Solomon codes as specified in issue #217. The changes focus on mathematical correctness and typeclass alignment within the ArkLib coding theory module.

Features

• Reed-Solomon Check Matrix: Implemented the checkMatrix definition, providing the standard parity-check matrix representation for Reed-Solomon codes.

Refactoring

• Typeclass Constraints Optimization:
  • Updated genMatrix to require the Semiring F typeclass assumption, ensuring broader compatibility and mathematical rigor.
  • Added a Field F constraint to checkMatrix to support the inverse operations required by the matrix element formulas.
• Computability Management: Marked polynomial-related definitions as noncomputable where necessary to align with Lean's handling of specific algebraic operations.

Documentation

• Issue Tracking: Formally linked and resolved issue Proof obligation for checkMatrix in ArkLib/Data/CodingTheory/ReedSolomon.lean #217.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	5
❌ Lines Removed	5

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• def checkMatrix (deg : ℕ) [Fintype ι] : Matrix (Fin (Fintype.card ι - deg)) ι F in ArkLib/Data/CodingTheory/ReedSolomon.lean

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• Lines 61 and 62 (within checkMatrix):

  +  let P := Finset.univ.prod fun j => (X - C (domain j))
  +  .of fun i j => domain j ^ (i : ℕ) * (P.derivative.eval (domain j))⁻¹

  Violation: These lines use => for anonymous functions. The style guide requires following the mathlib Style Guide, which states: "Use ↦ instead of => for anonymous functions."

(Note: While line 53 also uses =>, it is part of the existing context and not a new code change.)

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ReedSolomon.lean: Implement the checkMatrix for Reed-Solomon codes and update the typeclass arguments for genMatrix.

---

Last updated: 2026-01-10 13:57 UTC.

[DimitriosMitsios]

done!

[alexanderlhicks]

Thank you! lgtm!