fix: add nolint unusedArguments to incomplete definitions

Add @[nolint unusedArguments] to three definitions with incomplete proofs:
- DirectSumDecomposition.refinement
- Dual.DirectSumDecomposition.refinement
- limit_elt_mk

These arguments are likely needed when the proofs are completed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

Author: kim-em

PersistentDecomp/DirectSumDecomposition.lean

@@ -211,6 +211,7 @@ variable {D : DirectSumDecomposition M}
 /-- If `D` is a direct sum decomposition of `M` and for each `N` appearing in `D` we are given a
 direct sum decomposition of `N`, we can construct a refinement of `D` whose underlying set is the
 union of all decompositions of the `N`'s appearing in `D`. -/
+@[nolint unusedArguments]
 def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) : DirectSumDecomposition M where

PersistentDecomp/DirectSumDecompositionDual.lean

@@ -294,6 +294,7 @@ variable {D : DirectSumDecomposition M}
 
 /--If `D` is a direct sum decomposition of `M` and for each `N` appearing in `S` we are given a
 direct sum decomposition of `N`, we can construct a refinement of `D`.-/
+@[nolint unusedArguments]
 def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) : DirectSumDecomposition M where

PersistentDecomp/MaximalDecompExists.lean

@@ -59,6 +59,7 @@ notation3:max "M["l"]_[" c "]" => chainBound l c
 
 lemma chainBound_le : M[l] ≤ (Λ I l).val := iInf_le ..
 
+@[nolint unusedArguments]
 noncomputable def limit_elt_mk (hT : IsChain LE.le T) (f : T → PersistenceSubmodule M)
   (h_le : ∀ (I J : T), I ≤ J → f J ≤ f I) (h_mem : ∀ I : T, (f I) ∈ I.val) : (L T) := by
   let f' : (I : T) → (Pone T).obj I := by