fix(issue-214): prove linsolve_none

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

linsolve A b = none → ¬ ∃ x, A.mulVec x = b (linsolve_none).

• touched file: ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean
• proof is by case split on existence in linsolve, contradiction in the some branch
• linsolve_some is left for PR fix(issue-211): prove linsolve_some #378

Resolves #214.

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

[github-actions]

🤖 Gemini PR Summary

Formalizes the soundness of the linear system solver's failure case within the Berlekamp-Welch algorithm, resolving issue #214.

Mathematical Formalization

Provides a formal proof for the linsolve_none theorem:

• Theorem: linsolve A b = none → ¬ ∃ x, A.mulVec x = b
• Logic: Employs a case split on the existence of a solution in linsolve, utilizing a contradiction in the some branch to guarantee that a none result implies an inconsistent linear system.

Implementation Details

• File updated: ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean
• Refactoring: Replaces placeholder "sorries" with a proven implementation. The solver now uses noncomputable classical principles to facilitate formal reasoning within the library.

Project Context

• Roadmap: This PR specifically addresses the failure (none) case. The success (some) case, linsolve_some, is tracked for PR fix(issue-211): prove linsolve_some #378.
• Collaboration: Proofs were auto-formalized in collaboration with @Aristotle-Harmonic.

Resolves: #214

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	15
❌ 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_none {A : Matrix (Fin n) (Fin m) F} {b : Fin n → 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 violations of the style guide were identified:

• Line 49: "Use 2 spaces for indentation." (Indented 4 spaces instead of 2).
• Line 50: "Place by at the end of the line preceding the tactic block." (by is placed on its own line instead of at the end of the line containing :=).
• Line 51: "Use 2 spaces for indentation." (Indented 4 spaces instead of 2).
• Line 52: "Use 2 spaces for indentation." (Indented 4 spaces instead of 2).
• Line 52: "Put spaces on both sides of :, :=, and infix operators." (Missing space before : in h : ∃).
• Line 52: "Use a space after binders (e.g., ∀ x, not ∀x,)." (Missing space after ∃).
• Line 79: "When translating theorem statements into names, we use standard mappings for symbols" (The name linsolve_none fails to map = to eq, ¬ to not, ∃ to exists, or → to of).
• Line 81: "Put spaces on both sides of :, :=, and infix operators." (Missing space before : at the start of the line).
• Line 81: "Use a space after binders (e.g., ∀ x, not ∀x,)." (Missing space after ∃).
• Line 83: "h, h₁, ... : Assumptions/Hypotheses" (Uses the identifier hex instead of the mandated convention).
• Line 83: "Put spaces on both sides of :, :=, and infix operators." (Missing space before : in hex : ∃).
• Line 83: "Use a space after binders (e.g., ∀ x, not ∀x,)." (Missing space after ∃).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/BerlekampWelch/Sorries.lean: This change replaces the opaque placeholder for the Berlekamp-Welch linear system solver with a noncomputable classical implementation and provides a formal proof for its corresponding correctness theorem.

---

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