Prove argmin_unique in the Lean formalization (D-805)

Replace the `sorry` with a complete proof: from the two min-bounds the selected
costs are equal (Int.le_antisymm), then trichotomy on the indices — either side's
smallest-index tie-break contradicts equality (Int.lt_irrefl). No Mathlib.

`lean lean/ProvableWorldModel/Freivalds.lean` now compiles with zero warnings.
The verify_argmin soundness contract is fully formalized; the Freivalds
probability bound (Mathlib finite-field counting) remains the open target.

Author: AbdelStark

lean/ProvableWorldModel/Freivalds.lean

@@ -24,9 +24,22 @@ def IsArgmin (costs : List Int) (sel : Nat) (c : Int) : Prop :=
 
 /-- Soundness: the argmin is unique. If two indices both satisfy the contract they
 are equal — so a verifier that accepts the contract pins down exactly one
-selection (a wrong selection cannot also satisfy it). Proof pending (D-805). -/
+selection (a wrong selection cannot also satisfy it). -/
 theorem argmin_unique {costs : List Int} {i j : Nat} {ci cj : Int}
-    (_hi : IsArgmin costs i ci) (_hj : IsArgmin costs j cj) : i = j := by
-  sorry
+    (hi : IsArgmin costs i ci) (hj : IsArgmin costs j cj) : i = j := by
+  obtain ⟨hi_get, hi_min, hi_tie⟩ := hi
+  obtain ⟨hj_get, hj_min, hj_tie⟩ := hj
+  -- Costs at i and j are equal (each ≤ the other).
+  have hcc : ci = cj := Int.le_antisymm (hi_min j cj hj_get) (hj_min i ci hi_get)
+  rcases Nat.lt_trichotomy i j with hlt | heq | hgt
+  · -- i < j: tie-break at j forces cj < ci = cj, impossible.
+    have h : cj < ci := hj_tie i ci hlt hi_get
+    rw [hcc] at h
+    exact absurd h (Int.lt_irrefl cj)
+  · exact heq
+  · -- j < i: tie-break at i forces ci < cj = ci, impossible.
+    have h : ci < cj := hi_tie j cj hgt hj_get
+    rw [hcc] at h
+    exact absurd h (Int.lt_irrefl cj)
 
 end ProvableWorldModel

lean/README.md

@@ -5,16 +5,15 @@ intent of CommitLLM's `lean/` tree for the parts this project relies on.
 
 | File | Status |
 |---|---|
-| `ProvableWorldModel/Freivalds.lean` | **Compiles** (self-contained, no Mathlib). States the `verify_argmin` soundness contract (`IsArgmin`) and the argmin-uniqueness theorem (proof pending, `sorry`); documents the Freivalds probability-bound theorem to be proved next. |
+| `ProvableWorldModel/Freivalds.lean` | **Compiles, no `sorry`** (self-contained, no Mathlib). States the `verify_argmin` soundness contract (`IsArgmin`) and **proves** `argmin_unique` (the accepted selection is unique); documents the Freivalds probability-bound theorem to be proved next. |
 
 Build (Lean toolchain pinned by `lean-toolchain`):
 
 ```bash
-lean lean/ProvableWorldModel/Freivalds.lean   # warns on `sorry`, no errors
+lean lean/ProvableWorldModel/Freivalds.lean   # compiles cleanly, no warnings
 ```
 
 Remaining formalization work:
-- Prove `argmin_unique` (elementary; core Lean).
 - The **Freivalds soundness bound** (`#{r | r·z = r·(W·x)} ≤ |F|^(m-1)` when
   `z ≠ W·x`) needs a finite-field counting development — `ZMod p`, `Fintype.card`,
   nonzero-linear-functional kernel size — i.e. a Mathlib dependency (a `lakefile`