UDR close iff exists unique close codeword

theorem UDR_close_iff_exists_unique_close_codeword {ι : Type*} [Fintype ι] {F : Type*}    [DecidableEq F] (C : Set (ι → F)) [Nonempty C] (u : ι → F) :    Δ₀(u, C) ≤ Code.uniqueDecodingRadius C ↔ ∃! v ∈ C, Δ₀(u, v) ≤ Code.uniqueDecodingRadius C := by  -- 1. Define t (radius) and d (distance) for brevity  set t := Code.uniqueDecodingRadius C  set d := ‖C‖₀  constructor  · -- (→) Direction 1: "Close" implies "Uniquely Close"    intro h_dist_le_t    -- 2. First, prove *existence*    let v := pickClosestCodeword_of_Nonempty_Code (C := C) (u := u)    have h_close_to_v : Δ₀(u, v) ≤ t := by      rw [distFromPickClosestCodeword_of_Nonempty_Code (C := C) (u := u)] at h_dist_le_t      simp only [Nat.cast_le] at h_dist_le_t      exact h_dist_le_t    have h_exists : ∃ v, v ∈ C ∧ Δ₀(u, v) ≤ t := by      use v      simp only [Subtype.coe_prop, true_and]      exact h_close_to_v    -- 3. Second, prove *uniqueness*    have h_uniq : ∀ (v₁ : ι → F) (v₂ : ι → F),      v₁ ∈ C → v₂ ∈ C → Δ₀(u, v₁) ≤ t → Δ₀(u, v₂) ≤ t → v₁ = v₂ := by      intro v₁ v₂ hv₁_mem hv₂_mem h_dist_v₁ h_dist_v₂      -- We will use the triangle inequality to bound the distance between v₁ and v₂      have h_dist_v1_v2 : Δ₀(v₁, v₂) ≤ Δ₀(v₁, u) + Δ₀(u, v₂) := by        exact hammingDist_triangle v₁ u v₂      -- The distance is symmetric      rw [hammingDist_comm v₁ u] at h_dist_v1_v2      -- Substitute the known bounds `≤ t`      have h_le_2t : Δ₀(v₁, v₂) ≤ t + t :=        h_dist_v1_v2.trans (Nat.add_le_add h_dist_v₁ h_dist_v₂)      rw [←Nat.two_mul] at h_le_2t      -- 4. Now, we show that `2 * t < d`      -- We handle the main case (d ≥ 2) and the trivial case (d < 2) separately      by_cases h_d_ge_2 : d ≥ 2      · -- Case 1: d ≥ 2 (the standard case)        -- We have t = ⌊(d-1)/2⌋. We know 2 * ⌊(d-1)/2⌋ ≤ d-1        have h_2t_le_d_minus_1 : 2 * t ≤ d - 1 := by          dsimp only [d, t, uniqueDecodingRadius]          rw [mul_comm]          exact Nat.div_mul_le_self (‖C‖₀ - 1) 2        -- Since d ≥ 2, we know d-1 < d        have h_d_minus_1_lt_d : d - 1 < d := by          apply Nat.sub_lt_of_pos_le          · linarith -- d > 0          · linarith -- 1 > 0        -- Chain the inequalities: Δ₀(v₁, v₂) ≤ 2*t ≤ d-1 < d        have h_dist_lt_d : Δ₀(v₁, v₂) < d := by omega        -- By `eq_of_lt_dist`, if two codewords have a distance less than        -- the minimum distance of the code, they must be equal.        exact eq_of_lt_dist hv₁_mem hv₂_mem h_dist_lt_d      · -- Case 2: d < 2 (i.e., d = 0 or d = 1)        -- This means the code is trivial or has min distance 1        have h_d_le_1 : d ≤ 1 := by omega        -- If d ≤ 1, then t = ⌊(1-1)/2⌋ = 0 or ⌊(0-1)/2⌋ = 0        have h_t_eq_0 : t = 0 := by          dsimp only [t, d, uniqueDecodingRadius]          apply Nat.le_zero.mp          omega        -- Our assumption `Δ₀(u, v₁) ≤ t` becomes `Δ₀(u, v₁) ≤ 0`        rw [h_t_eq_0] at h_dist_v₁ h_dist_v₂        rw [Nat.le_zero] at h_dist_v₁ h_dist_v₂        -- If the distance is 0, the words are equal        have h_u_eq_v1 : u = v₁ := by rw [←hammingDist_eq_zero]; exact h_dist_v₁        have h_u_eq_v2 : u = v₂ := by rw [←hammingDist_eq_zero]; exact h_dist_v₂        -- By transitivity, v₁ = u = v₂, so v₁ = v₂        rw [←h_u_eq_v1, h_u_eq_v2]    -- 5. Combine existence and uniqueness    -- apply ExistsUnique.intro h_exists    refine existsUnique_of_exists_of_unique h_exists ?_    intro v₁ v₂ ⟨hv₁_mem, h_dist_v₁⟩ ⟨hv₂_mem, h_dist_v₂⟩    exact h_uniq v₁ v₂ hv₁_mem hv₂_mem h_dist_v₁ h_dist_v₂  · -- (←) Direction 2: "Uniquely Close" implies "Close"    intro h_exists_unique    rcases h_exists_unique with ⟨v, hv_mem, h_dist_le⟩    rw [closeToCode_iff_closeToCodeword_of_minDist]    use v