Joint Agreement iff joint Proximity

@[simp]theorem jointAgreement_iff_jointProximity    {F : Type*} {κ ι : Type*} [Fintype κ] [Fintype ι] [Nonempty ι] [DecidableEq F]    (C : Set (ι → F)) (u : WordStack F κ ι) (δ : ℝ≥0) :    jointAgreement (C := C) (δ := δ) (W := u)  ↔ jointProximity (C := C) (u := u) (δ := δ) := by  classical  let e : ℕ := Nat.floor (δ * Fintype.card ι)  constructor  · -- Forward direction: jointAgreement → jointProximity    intro h_words    rcases h_words with ⟨S, hS_card, v, hv⟩    -- We have: |S| ≥ (1-δ)*|ι| and ∀ i, v i ∈ MC and S ⊆ {j | v i j = u i j}    -- Need to show: δᵣ(u_interleaved, MC.interleavedCode) ≤ δ    -- Define interleaved word from u    let u_interleaved : InterleavedWord F κ ι := ⋈|u    -- Construct interleaved codeword from v    let v_interleaved : InterleavedWord F κ ι := interleaveWordStack v    have hv_interleaved_mem : v_interleaved ∈ interleavedCodeSet C := by      rw [mem_interleavedCode_iff]      intro k      exact (hv k).1    -- Now show that u_interleaved and v_interleaved agree on S    -- This gives us the distance bound    have h_agree_on_S : ∀ j ∈ S, u_interleaved j = getSymbol v_interleaved j := by      intro j hj      ext k      -- u_interleaved j k = u k j, v_interleaved j k = v k j; Need: u k j = v k j      have h_agree := (hv k).2      have hj_in_filter : j ∈ Finset.filter (fun j => v k j = u k j) Finset.univ := by        rw [Finset.mem_filter]        constructor        · exact Finset.mem_univ j        · -- v k j = u k j          have h_subset := Finset.subset_iff.mp h_agree          have hj_mem : j ∈ S := hj          let res := h_subset (x := j) hj_mem          simp only [Finset.mem_filter, Finset.mem_univ, true_and] at res          exact res      simp only [Finset.mem_filter] at hj_in_filter      exact hj_in_filter.2.symm    -- From agreement on S, we get distance bound    have h_dist : δᵣ(u_interleaved, v_interleaved) ≤ δ := by      rw [relCloseToWord_iff_exists_agreementCols]      use S      rw [relDist_floor_bound_iff_complement_bound]      constructor      · exact hS_card      · intro j        constructor        · intro hj_in_S          have h_agree := h_agree_on_S j hj_in_S          exact h_agree        · intro hj_not_in_S          by_contra hj_in_S          exact hj_not_in_S (h_agree_on_S j hj_in_S)    rw [←ENNReal.coe_le_coe] at h_dist    -- Since v_interleaved ∈ MC.interleavedCode, we have δᵣ(u_interleaved, MC.interleavedCode) ≤ δ    unfold jointProximity    have h_min_dist :        δᵣ(u_interleaved, interleavedCodeSet C) ≤ δᵣ(u_interleaved, v_interleaved)      := by      apply relDistFromCode_le_relDist_to_mem (u := u_interleaved) (C := interleavedCodeSet C)        (v := v_interleaved) (hv := hv_interleaved_mem)    exact le_trans h_min_dist h_dist  · -- Backward direction: jointProximity → jointAgreement    intro h_joint    unfold jointProximity at h_joint    let u_interleaved : InterleavedWord F κ ι := ⋈|u    -- h_joint says: δᵣ(u_interleaved, MC.interleavedCode) ≤ δ    -- This means there exists v in the interleaved code with δᵣ(u_interleaved, v) ≤ δ    have h_close := Code.closeToCode_iff_closeToCodeword_of_minDist      (C := (interleavedCodeSet C)) (u := u_interleaved)    -- Convert relative distance to natural distance    -- Key: if δᵣ(u, C) ≤ δ, there exists a codeword v with δᵣ(u, v) ≤ δ    have h_rel_to_nat : δᵣ(u_interleaved, interleavedCodeSet C) ≤ δ →        ∃ v ∈ (interleavedCodeSet C), δᵣ(u_interleaved, v) ≤ δ := by      intro h_rel      rw [relCloseToCode_iff_relCloseToCodeword_of_minDist] at h_rel      exact h_rel    have h_exists_v := h_rel_to_nat h_joint    rcases h_exists_v with ⟨v, hv_mem, hv_dist⟩    -- Now convert relative distance to agreement set    -- We need: δᵣ(u_interleaved, v) ≤ δ → ∃ S, |S| ≥ (1-δ)*|ι| and agreement    -- Convert relative distance δ to natural distance e    have h_nat_dist : Δ₀(u_interleaved, v) ≤ e := by      rw [pairRelDist_le_iff_pairDist_le (δ := δ)] at hv_dist      exact hv_dist    have h_agree := Code.closeToWord_iff_exists_agreementCols      (u := u_interleaved) (v := v) (e := e)    have h_agree_nat := h_agree.mp h_nat_dist    rcases h_agree_nat with ⟨S, hS_card, h_agree_S⟩    -- Now extract rows from v to get v : κ → ι → F    let v_rows : κ → ι → F := fun k => getRow v k    use S    constructor    · -- Prove |S| ≥ (1-δ)*|ι|      rw [ge_iff_le]      rw [relDist_floor_bound_iff_complement_bound] at hS_card      exact hS_card    · -- Prove agreement      use v_rows      intro i      constructor      · -- v_rows i ∈ MC        simp only [interleavedCodeSet, Set.mem_setOf_eq] at hv_mem        exact hv_mem i      · -- S ⊆ {j | v_rows i j = u i j}        simp only [Finset.subset_iff]        intro j hj_mem        simp only [Finset.mem_filter, Finset.mem_univ, true_and] -- ⊢ v_rows i j = u i j        have h_agree := h_agree_S (colIdx := j).1 hj_mem        apply congrArg (fun x => x i) at h_agree        exact id (Eq.symm h_agree)