Fiberwise dist lt imp dist lt unique decoding radius

theorem fiberwise_dist_lt_imp_dist_lt_unique_decoding_radius (i : Fin ℓ) (steps : ℕ)    [NeZero steps] (h_i_add_steps : i.val + steps ≤ ℓ)    (f : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i, by omega⟩)  (h_fw_dist_lt : fiberwiseClose 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)    (i := i) (steps := steps) (h_i_add_steps := h_i_add_steps) (f := f)) :  hammingClose 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i, by omega⟩ f := by  unfold fiberwiseClose at h_fw_dist_lt  unfold hammingClose  -- 2 * Δ₀(f, ↑(BBF_Code 𝔽q β ⟨↑i, ⋯⟩)) < ↑(BBF_CodeDistance ℓ 𝓡 ⟨↑i, ⋯⟩)  let d_fw := fiberwiseDistance 𝔽q β (i := i) steps h_i_add_steps f  let C_i := (BBF_Code 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i, by omega⟩)  let d_H := Code.distFromCode f C_i  let d_i := BBF_CodeDistance ℓ 𝓡 (⟨i, by omega⟩)  let d_i_plus_steps := BBF_CodeDistance ℓ 𝓡 ⟨i.val + steps, by omega⟩   have h_d_i_gt_0 : d_i > 0 := by    dsimp [d_i, BBF_CodeDistance] -- ⊢ 2 ^ (ℓ + 𝓡 - ↑i) - 2 ^ (ℓ - ↑i) + 1 > 0    have h_exp_lt : ℓ - i.val < ℓ + 𝓡 - i.val := by      exact Nat.sub_lt_sub_right (a := ℓ) (b := ℓ + 𝓡) (c := i.val) (by omega) (by        apply Nat.lt_add_of_pos_right; exact pos_of_neZero 𝓡)    have h_pow_lt : 2 ^ (ℓ - i.val) < 2 ^ (ℓ + 𝓡 - i.val) := by      exact Nat.pow_lt_pow_right (by norm_num) h_exp_lt    omega   have h_C_i_nonempty : Nonempty C_i := by    simp only [nonempty_subtype, C_i]    exact Submodule.nonempty (BBF_Code 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i.val, by omega⟩)   -- 1. Relate Hamming distance `d_H` to fiber-wise distance `d_fw`.  obtain ⟨g', h_g'_mem, h_g'_min_card⟩ : ∃ g' ∈ C_i, d_fw    = (fiberwiseDisagreementSet 𝔽q β i steps h_i_add_steps f g').ncard := by    -- Let `S` be the set of all possible fiber-wise disagreement sizes.    let S := (fun (g : C_i) => (fiberwiseDisagreementSet 𝔽q β i steps h_i_add_steps      f g).ncard) '' Set.univ    -- The code `C_i` (a submodule) is non-empty, so `S` is also non-empty.    have hS_nonempty : S.Nonempty := by      refine Set.image_nonempty.mpr ?_       exact Set.univ_nonempty    -- For a non-empty set of natural numbers, `sInf` is an element of the set.    have h_sInf_mem : sInf S ∈ S := Nat.sInf_mem hS_nonempty    -- By definition, `d_fw = sInf S`.    unfold d_fw at h_sInf_mem    -- Since `sInf S` is in the image set `S`, there must be an element `g_subtype` in the domain    -- (`C_i`) that maps to it. This `g_subtype` is the codeword we're looking for.    rw [Set.mem_image] at h_sInf_mem    rcases h_sInf_mem with ⟨g_subtype, _, h_eq⟩    -- Extract the codeword and its membership proof.    exact ⟨g_subtype.val, g_subtype.property, by exact id (Eq.symm h_eq)⟩   -- The Hamming distance to any codeword `g'` is bounded by `d_fw * 2 ^ steps`.  have h_dist_le_fw_dist_times_fiber_size : (hammingDist f g' : ℕ∞) ≤ d_fw * 2 ^ steps := by    -- This proves `dist f g' ≤ (fiberwiseDisagreementSet ... f g').ncard * 2 ^ steps`    -- and lifts to ℕ∞. We prove the `Nat` version `hammingDist f g' ≤ ...`,    -- which is equivalent.    change (Δ₀(f, g') : ℕ∞) ≤ ↑d_fw * ((2 ^ steps : ℕ) : ℕ∞)    rw [←ENat.coe_mul, ENat.coe_le_coe, h_g'_min_card]    -- Let ΔH be the finset of actually bad x points where f and g' disagree.    set ΔH := Finset.filter (fun x => f x ≠ g' x) Finset.univ    have h_dist_eq_card : hammingDist f g' = ΔH.card := by      simp only [hammingDist, ne_eq, ΔH]    rw [h_dist_eq_card]    -- Y_bad is the set of quotient points y that THERE EXISTS a bad fiber point x    set Y_bad := fiberwiseDisagreementSet 𝔽q β i steps h_i_add_steps f g'    simp only at * -- simplify domain indices everywhere     -- ⊢ #ΔH ≤ Y_bad.ncard * 2 ^ steps     have hFinType_Y_bad : Fintype Y_bad := by exact Fintype.ofFinite ↑Y_bad    -- Every point of disagreement `x` must belong to a fiber over some `y` in `Y_bad`,    -- BY DEFINITION of `Y_bad`. Therefore, `ΔH` is a subset of the union of the fibers    -- of `Y_bad`    have h_ΔH_subset_bad_fiber_points : ΔH ⊆ Finset.biUnion Y_bad.toFinset        (t := fun y => ((qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)          (h_i_add_steps := by apply Nat.lt_add_of_pos_right_of_le; omega) (y := y)) ''          (Finset.univ : Finset (Fin ((2:ℕ)^steps)))).toFinset) := by      -- ⊢ If any x ∈ ΔH, then x ∈ Union(qMap_total_fiber(y), ∀ y ∈ Y_bad)      intro x hx_in_ΔH; -- ⊢ x ∈ Union(qMap_total_fiber(y), ∀ y ∈ Y_bad)      simp only [ΔH, Finset.mem_filter] at hx_in_ΔH      -- Now we actually apply iterated qMap into x to get y_of_x,      -- then x ∈ qMap_total_fiber(y_of_x) by definition      let y_of_x := iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i steps h_i_add_steps x      apply Finset.mem_biUnion.mpr; use y_of_x      -- ⊢ y_of_x ∈ Y_bad.toFinset ∧ x ∈ qMap_total_fiber(y_of_x)      have h_elemenet_Y_bad : y_of_x ∈ Y_bad.toFinset := by        -- ⊢ y ∈ Y_bad.toFinset        simp only [fiberwiseDisagreementSet, iteratedQuotientMap, ne_eq, Subtype.exists,          Set.toFinset_setOf, mem_filter, mem_univ, true_and, Y_bad]        -- one bad fiber point of y_of_x is x itself        let X := x.val        have h_X_in_source : X ∈ sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩) := by          exact Submodule.coe_mem x        use X        use h_X_in_source        -- ⊢ Ŵ_steps⁽ⁱ⁾(X) = y (iterated quotient map) ∧ ¬f ⟨X, ⋯⟩ = g' ⟨X, ⋯⟩        have h_forward_iterated_qmap : Polynomial.eval X            (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i, by omega⟩              ⟨steps, by simp only; omega⟩) = y_of_x := by          simp only [iteratedQuotientMap, X, y_of_x];        have h_eval_diff : f ⟨X, by omega⟩ ≠ g' ⟨X, by omega⟩ := by          unfold X          simp only [Subtype.coe_eta, ne_eq, hx_in_ΔH, not_false_eq_true]        simp only [h_forward_iterated_qmap, Subtype.coe_eta, h_eval_diff,          not_false_eq_true, and_self]      simp only [h_elemenet_Y_bad, true_and]       set qMapFiber := qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)        (h_i_add_steps := by apply Nat.lt_add_of_pos_right_of_le; omega) (y := y_of_x)      simp only [coe_univ, Set.image_univ, Set.toFinset_range, mem_image, mem_univ, true_and]      use (pointToIterateQuotientIndex (i := ⟨i, by omega⟩) (steps := steps)        (h_i_add_steps := by omega) (x := x))      have h_res := is_fiber_iff_generates_quotient_point 𝔽q β i steps (by omega)        (x := x) (y := y_of_x).mp (by rfl)      exact h_res    -- ⊢ #ΔH ≤ Y_bad.ncard * 2 ^ steps    -- The cardinality of a subset is at most the cardinality of the superset.    apply (Finset.card_le_card h_ΔH_subset_bad_fiber_points).trans    -- The cardinality of a disjoint union is the sum of cardinalities.    rw [Finset.card_biUnion]    · -- The size of the sum is the number of bad fibers (`Y_bad.ncard`) times      -- the size of each fiber (`2 ^ steps`).      simp only [Set.toFinset_card]      have h_card_fiber_per_quotient_point := card_qMap_total_fiber 𝔽q β        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i steps h_i_add_steps      simp only [Set.image_univ, Fintype.card_ofFinset,        Subtype.forall] at h_card_fiber_per_quotient_point      have h_card_fiber_of_each_y : ∀ y ∈ Y_bad.toFinset,          Fintype.card ((qMap_total_fiber 𝔽q β (i := ⟨↑i, by omega⟩) (steps := steps)            (h_i_add_steps := by apply Nat.lt_add_of_pos_right_of_le; omega) (y := y)) ''            ↑(Finset.univ : Finset (Fin ((2:ℕ)^steps)))) = 2 ^ steps := by        intro y hy_in_Y_bad        have hy_card_fiber_of_y := h_card_fiber_per_quotient_point (a := y) (b := by          exact Submodule.coe_mem y)        simp only [coe_univ, Set.image_univ, Fintype.card_ofFinset, hy_card_fiber_of_y]      rw [Finset.sum_congr rfl h_card_fiber_of_each_y]      -- ⊢ ∑ x ∈ Y_bad.toFinset, 2 ^ steps ≤ Y_bad.encard.toNat * 2 ^ steps      simp only [sum_const, Set.toFinset_card, smul_eq_mul, ofNat_pos, pow_pos,        _root_.mul_le_mul_right, ge_iff_le]      conv_rhs => rw [←_root_.Nat.card_coe_set_eq] -- convert .ncard back to .card      -- ⊢ Fintype.card ↑Y_bad ≤ Nat.card ↑Y_bad      simp only [card_eq_fintype_card, le_refl]    · -- Prove that the fibers for distinct quotient points y₁, y₂ are disjoint.      intro y₁ hy₁ y₂ hy₂ hy_ne      have h_disjoint := qMap_total_fiber_disjoint (i := ⟨↑i, by omega⟩) (steps := steps)        (h_i_add_steps := by omega) (y₁ := y₁) (y₂ := y₂) (hy_ne := hy_ne)      simp only [Function.onFun, coe_univ]      exact h_disjoint   -- The minimum distance `d_H` is bounded by the distance to this specific `g'`.  have h_dist_bridge : d_H ≤ d_fw * 2 ^ steps := by    -- exact h_dist_le_fw_dist_times_fiber_size    apply le_trans (a := d_H) (c := d_fw * 2 ^ steps) (b := hammingDist f g')    · -- ⊢ d_H ≤ ↑Δ₀(f, g')      simp only [distFromCode, SetLike.mem_coe, hammingDist, ne_eq, d_H];      -- ⊢ Δ₀(f, C_i) ≤ ↑Δ₀(f, g')      -- ⊢ sInf {d | ∃ v ∈ C_i, ↑(#{i | f i ≠ v i}) ≤ d} ≤ ↑(#{i | f i ≠ g' i})      apply sInf_le      use g'    · exact h_dist_le_fw_dist_times_fiber_size   -- 2. Use the premise : `2 * d_fw < d_{i+steps}`.  -- As a `Nat` inequality, this is equivalent to `2 * d_fw ≤ d_{i+steps} - 1`.  have h_fw_bound : 2 * d_fw ≤ d_i_plus_steps - 1 := by    -- Convert the ENat inequality to a Nat inequality using `a < b ↔ a + 1 ≤ b`.    exact Nat.le_of_lt_succ (WithTop.coe_lt_coe.1 h_fw_dist_lt)   -- 3. The Algebraic Identity.  -- The core of the proof is the identity : `(d_{i+steps} - 1) * 2 ^ steps = d_i - 1`.  have h_algebraic_identity : (d_i_plus_steps - 1) * 2 ^ steps = d_i - 1 := by    dsimp [d_i, d_i_plus_steps, BBF_CodeDistance]    rw [Nat.sub_mul, ←Nat.pow_add, ←Nat.pow_add];    have h1 : ℓ + 𝓡 - (↑i + steps) + steps = ℓ + 𝓡 - i := by      rw [Nat.sub_add_eq_sub_sub_rev (h1 := by omega) (h2 := by omega),        Nat.add_sub_cancel (n := i) (m := steps)]    have h2 : (ℓ - (↑i + steps) + steps) = ℓ - i := by      rw [Nat.sub_add_eq_sub_sub_rev (h1 := by omega) (h2 := by omega),        Nat.add_sub_cancel (n := i) (m := steps)]    rw [h1, h2]   -- 4. Conclusion : Chain the inequalities to prove `2 * d_H < d_i`.  -- We know `d_H` is finite, since `C_i` is nonempty.  have h_dH_ne_top : d_H ≠ ⊤ := by    simp only [ne_eq, d_H]    rw [Code.distFromCode_eq_top_iff_empty f C_i]    exact Set.nonempty_iff_ne_empty'.mp h_C_i_nonempty   -- We can now work with the `Nat` value of `d_H`.  let d_H_nat := ENat.toNat d_H  have h_dH_eq : d_H = d_H_nat := (ENat.coe_toNat h_dH_ne_top).symm   -- The calculation is now done entirely in `Nat`.  have h_final_inequality : 2 * d_H_nat ≤ d_i - 1 := by    have h_bridge_nat : d_H_nat ≤ d_fw * 2 ^ steps := by        rw [←ENat.coe_le_coe]        exact le_of_eq_of_le (id (Eq.symm h_dH_eq)) h_dist_bridge    calc 2 * d_H_nat      _ ≤ 2 * (d_fw * 2 ^ steps) := by gcongr      _ = (2 * d_fw) * 2 ^ steps := by rw [mul_assoc]      _ ≤ (d_i_plus_steps - 1) * 2 ^ steps := by gcongr;      _ = d_i - 1 := h_algebraic_identity   simp only [d_H, d_H_nat] at h_dH_eq  -- This final line is equivalent to the goal statement.  rw [h_dH_eq]  -- ⊢ 2 * ↑Δ₀(f, C_i).toNat < ↑(BBF_CodeDistance ℓ 𝓡 ⟨↑i, ⋯⟩)  change ((2 : ℕ) : ℕ∞) * ↑Δ₀(f, C_i).toNat < ↑(BBF_CodeDistance ℓ 𝓡 ⟨↑i, by omega⟩)  rw [←ENat.coe_mul, ENat.coe_lt_coe]  apply Nat.lt_of_le_pred (n := 2 * Δ₀(f, C_i).toNat) (m := d_i) (h := h_d_i_gt_0)    (h_final_inequality)