fix(issue-211): prove linsolve_some

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

linsolve A b = some x → A.mulVec x = b (linsolve_some).

• touched file: ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean
• linsolve is kept noncomputable with witness extraction via Classical.choose
• linsolve_none is left for PR fix(issue-214): prove linsolve_none #379

Resolves #211.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

Proves the linsolve_some theorem: linsolve A b = some x → A.mulVec x = b. This establishes that any solution returned by the solver correctly satisfies the linear system $Ax = b$ within the Berlekamp-Welch implementation.

Technical Implementation

• Axiom Removal: Replaces the opaque placeholder in ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean with a verified definition.
• Witness Extraction: Employs Classical.choose to extract solution vectors, maintaining linsolve as a noncomputable function.
• Scope: Addresses correctness for successful lookups (linsolve_some) to resolve Proof obligation for linsolve_some in ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean #211. Completeness proofs (linsolve_none) are deferred to PR fix(issue-214): prove linsolve_none #379.

Metadata

• Resolves: Proof obligation for linsolve_some in ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean #211
• Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	18
❌ Lines Removed	8

---

Lean Declarations

✏️ **Removed:** 1 declaration(s)

• opaque linsolve (A : Matrix (Fin n) (Fin m) F) (b : Fin n → F) : Option (Fin m → F) in ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean

---

sorry Tracking

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

• theorem linsolve_some {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F} {x : Fin m → F} in ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean
• opaque linsolve (A : Matrix (Fin n) (Fin m) F) (b : Fin n → F) : Option (Fin m → F) in ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean

---

🎨 **Style Guide Adherence**

The following lines violate the ArkLib style guide:

• Line 53: Option (Fin m → F) := violates "Use 2 spaces for indentation." (indented 4 spaces instead of 2).
• Line 54: by violates "Tactic Mode: Place by at the end of the line preceding the tactic block." (placed on its own line instead of at the end of line 53).
• Line 55: classical violates "Use 2 spaces for indentation." (indented 4 spaces instead of 2).
• Line 56: exact if h : ∃ x, A.mulVec x = b then some (Classical.choose h) else none violates "Use 2 spaces for indentation." (indented 4 spaces instead of 2).
• Line 56: exact if h : ∃ x, A.mulVec x = b then some (Classical.choose h) else none violates "Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting." (use some <| Classical.choose h instead).
• Line 66: : A.mulVec x = b := by violates "Operators: ... Place them [:] before a line break rather than at the start of the next line." (the colon should be placed at the end of line 65).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean: Replaces the opaque placeholder for the linsolve linear system solver with a formal noncomputable definition and provides the proof for its basic correctness theorem.

---

Last updated: 2026-03-02 10:48 UTC.