[{"type":"thinking","thinking":"Now §16 (3d): the main finset + unit_family_le + bucket counts. Plan:\n\n1. `mainFinset (t : ℝ) : Finset {ρ : ℂ // IsNontrivialZero ρ} := (finite_subtype_norm_lt (2*t+1)).toFinset.filter (fun ρ => 1 ≤ |ρ.1.im − t| ∧ |ρ.1.im − t| < (Nat.floor t : ℝ) + 1)`\n   Hmm — wait. Let me reconsider the main definition. Buckets k = ⌊x⌋₊ ≤ ⌊t⌋₊ ⟺ x < ⌊t⌋₊+1. The finset: zeros with x ≥ 1 and x < ⌊t⌋₊+1. Ball: x < ⌊t⌋₊+1 ≤ t+1 ⟹ |γ| ≤ t+x < 2t+1 ✓.\n   Membership lemma: ρ ∈ mainFinset t ↔ 1 ≤ x ∧ x < ⌊t⌋₊+1 (given ‖ρ‖ < 2t+1, which follows — need to prove in the mem lemma: from x < ⌊t⌋₊+1 ≤ t+1: |γ| ≤ t+x < 2t+1, ‖ρ‖ ≤ |re|+|im| ≤ 1 + (2t+1) = 2t+2... wait — finite_subtype_norm_lt (2t+1) needs ‖ρ‖ < 2t+1: ‖ρ‖ ≤ |re|+|im| ≤ 1+(t+x) with x < t+1: < 1+t+t+1 = 2t+2 — NOT < 2t+1!! Tighten: |im| = |γ| ≤ t+x (for t ≥ 0: |γ| ≤ |t|+x = t+x ✓), so ‖ρ‖ ≤ 1 + t + x < 1 + t + (t+1) = 2t+2 — need the ball bound 2t+2: use finite_subtype_norm_lt (2t+2). ✓\n\n2. `mem_mainFinset : ρ ∈ mainFinset t ↔ 1 ≤ |ρ.1.im − t| ∧ |ρ.1.im − t| < (Nat.floor t : ℝ) + 1` — needs t ≥ 0 for the ball argument.\n\n3. `unit_family_le` (the generalized dyadic_family_le clone):\n```\nlemma unit_family_le (FS : Finset {ρ : ℂ // IsNontrivialZero ρ})\n    (j : {ρ : ℂ // IsNontrivialZero ρ} → ℕ) (K : ℕ)\n    (g : {ρ : ℂ // IsNontrivialZero ρ} → ℝ) (W : ℕ → ℝ) (cnt : ℕ → ℝ)\n    (hW : ∀ k : ℕ, 0 ≤ W k)\n    (hj : ∀ ρ ∈ FS, 1 ≤ j ρ ∧ j ρ ≤ K)\n    (hterm : ∀ ρ ∈ FS, g ρ ≤ W (j ρ) * (zeroMult (ρ : ℂ) : ℝ))\n    (hcount : ∀ k : ℕ,\n      ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), (zeroMult (ρ : ℂ) : ℝ) ≤ cnt k) :\n    ∑ ρ ∈ FS, g ρ ≤ ∑ k ∈ Finset.Ico 1 (K + 1), W k * cnt k\n```\n— direct clone of dyadic_family_le's proof.\n\n4. `farG_le_farW_mul (ρ, x ≥ 1)`: farG t ρ ≤ 4.5·farW (⌊x⌋₊)·m: x ≥ k = ⌊x⌋₊ ⟹ x√(1+x²) ≥ k√(1+k²) (monotone: mul_le_mul: x ≥ k ≥ 0 and √(1+x²) ≥ √(1+k²) via sqrt_le_sqrt + pow) ⟹ 4.5·m/(x√(1+x²)) ≤ 4.5·m/(k√(1+k²)) = 4.5·m·farW k: div_le_div_iff₀ + mul_le_mul... form: farG = 4.5·m/(x√) vs 4.5·(m·farW k) = 4.5·m/(k√): \n```\nlemma farG_le_farW_mul {t : ℝ} (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hx : 1 ≤ |ρ.1.im - t|) :\n    farG t ρ ≤ 4.5 * (farW (Nat.floor |ρ.1.im - t|) * (zeroMult ρ.1 : ℝ))\n```\n— via the monotone chain. Note farG has the if — ρ with x ≥ 1 is far ✓ if_neg.\n\n5. `main_bucket_count (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t} (ht : 10 ≤ t) (k : ℕ) (hk1 : 1 ≤ k) (hk2 : k ≤ Nat.floor t) : ∑ ρ ∈ (mainFinset t).filter (fun ρ => Nat.floor |ρ.1.im − t| = k), (zeroMult ρ.1 : ℝ) ≤ 2 * C0hat (t+1) + 0.55`:\n   The bucket's zeros: x ∈ [k, k+1): γ ∈ [t+k, t+k+1) ∪ (t−k−1, t−k].\n   - Map to (zeroWindow (t+k)).toFinset ∪ (zeroWindow (t−k−1)).toFinset via val-image (like near_sum_refPoint_le's hsub).\n   - Right count: hZC (t+k) (t+k ≥ 2 ✓) ≤ C0hat(t+k+1) ≤ C0hat(2t+1) (C0hat_mono: 1 ≤ t+k+1 ≤ 2t+1 ✓) ≤ C0hat(t+1)+0.55 (C0hat_two_t_add_one_le ht).\n   - Left count: cases on k ≤ t−3: hZC (t−k−1) (t−k−1 ≥ 2) ≤ C0hat(t−k) ≤ C0hat(t+1) (mono: t−k ≥ 3 ≥ 1); else (k > t−3): the window [t−k−1, t−k] ⊆ (−14, 14) — empty by NoLowZeros: the toFinset sum = 0: prove: every element of (zeroWindow_finite (t−k−1)).toFinset has |im| < 14, contradicting NoLowZeros ⟹ the finset is empty ⟹ sum = 0. Formalize: \n     ```\n     have hempty : (zeroWindow_finite (t−k−1)).toFinset = ∅ := by\n       rw [Finset.eq_empty_iff_forall_notMem]\n       intro ρ hρ\n       rw [Set.Finite.mem_toFinset] at hρ\n       obtain ⟨hz, h1, h2⟩ := hρ  -- hz : IsNontrivialZero ρ, h1 : t−k−1 ≤ ρ.im, h2 : ρ.im ≤ t−k\n       have h3 : 14 ≤ |ρ.im| := hNLZ ρ hz\n       -- |ρ.im| < 14: ρ.im ∈ [t−k−1, t−k] with t−k < 5, t−k−1 > −14+... hmm: k > t−3 ⟹ t−k < 3... wait: k > t−3 ⟺ t−k < 3. And k ≤ ⌊t⌋₊ ≤ t ⟹ t−k ≥ 0. So ρ.im ∈ [t−k−1, t−k] ⊆ [−1, 3]: |ρ.im| ≤ 3 < 14 contradiction.\n       -- Actually: t−k−1 ≥ t−t−1 = −1 (k ≤ t) and t−k < 3: ρ.im ∈ [−1, 3) hmm t−k−1 ≥ −1 (from k ≤ t): so ρ.im ≥ −1 ≥ −14 and ρ.im ≤ t−k < 3 < 14: |ρ.im| ≤ 3 < 14 ⟹ contradiction with h3.\n     ```\n     Hmm wait — k ≤ Nat.floor t ≤ t: t−k ≥ 0 ✓; k > t−3 ⟹ t−k < 3 ✓; t−k−1 ∈ [−1, 2): ρ.im ≥ t−k−1 ≥ −1; ρ.im ≤ t−k < 3. So ρ.im ∈ [−1, 3): |ρ.im| ≤ 3 < 14 ⟹ NoLowZeros (14 ≤ |ρ.im|) fails ⟹ no such ρ ✓.\n   - Then the filter-sum ≤ right-count + left-count ≤ (C0hat(t+1)+0.55) + C0hat(t+1) = 2C0hat(t+1)+0.55 ✓.\n   The image bridge: FS.filter(j ρ = k) — the mult-sum over the image (Subtype.val): Finset.sum_image (Subtype.val injective) ✓ (near_sum_refPoint_le pattern); subset: image ⊆ union of the two window toFinsets: for ρ in the bucket: x = |ρ.im − t| ∈ [k, k+1): cases γ ≥ t: γ ∈ [t+k, t+k+1): zeroWindow (t+k) = [t+k, t+k+1] (closed) ✓; γ < t: γ ∈ (t−k−1, t−k] ⊆ zeroWindow (t−k−1) (closed) ✓.\n   Then: sum over filter = sum over image ≤ sum over union = right + left (Finset.sum_le_sum_of_subset_of_nonneg + Finset.sum_union (disjoint: γ ≥ t+k ≥ t vs γ ≤ t−k ≤ t−1 ✓)).\n\n6. The main assembly:\n```\nlemma farG_main_le {t : ℝ} (ht : 10 ≤ t) (hZC : ZeroCountProp) (hNLZ : NoLowZeros) :\n    ∑ ρ ∈ mainFinset t, farG t ρ ≤ 4.5 * (2 * C0hat (t + 1) + 0.55) * 1.3476 := by\n  apply (unit_family_le (mainFinset t) (fun ρ => Nat.floor |ρ.1.im − t|) (Nat.floor t)\n    (farG t) (fun k => 4.5 * farW k) (fun _ => 2 * C0hat (t + 1) + 0.55)\n    (fun k => by positivity-ish farW_nonneg...) _ _ _ _).trans ?_\n  · -- Σ (4.5·farW k)·cnt = (4.5·cnt)·Σ farW k ≤ (4.5·cnt)·1.3476\n    rw [← Finset.mul_sum]\n    exact mul_le_mul_of_nonneg_left (farW_Ico_le _) (by positivity)\n  · intro ρ hρ\n    have hx := (mem_mainFinset ...).mp hρ\n    -- 1 ≤ ⌊x⌋₊: Nat.one_le_floor_iff? : 1 ≤ ⌊x⌋₊ ⟺ 1 ≤ x — `Nat.one_le_floor_iff (hx : 0 ≤ x)?` or prove: ⌊x⌋₊ ≥ 1 from x ≥ 1: Nat.succ_le_floor? `Nat.one_le_floor_iff : 1 ≤ ⌊r⌋₊ ↔ 1 ≤ r` for r ≥ 0? — there's Nat.one_le_floor_iff (hr : 0 ≤ r)?? Let me guess: `Nat.one_le_floor_iff : 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a` might need 0 ≤ a. floor of abs ≥ 0 always. Try Nat.succ_le_floor : 0 < a → n < a → n+1 ≤ ⌊a⌋₊?? For 1 ≤ x: Nat.one_le_iff_pos? Hmm — simplest: Nat.floor_mono (hx : 1 ≤ x) : ⌊1⌋₊ ≤ ⌊x⌋₊ with ⌊1⌋₊ = 1: `Nat.floor_mono : a ≤ b → ⌊a⌋₊ ≤ ⌊b⌋₊` ✓ and Nat.floor_one : ⌊(1:ℝ)⌋₊ = 1 ✓.\n    -- ⌊x⌋₊ ≤ ⌊t⌋₊: Nat.floor_mono (x ≤ ... hmm x < ⌊t⌋₊+1 ⟹ ⌊x⌋₊ ≤ ⌊t⌋₊: Nat.floor_le_floor? — x < ⌊t⌋₊+1 ⟹ ⌊x⌋₊ < ⌊t⌋₊+1 ⟹ ⌊x⌋₊ ≤ ⌊t⌋₊: Nat.floor_lt : x < n+1... `Nat.floor_lt' (hn : n ≠ 0)?` or: ⌊x⌋₊ ≤ ⌊t⌋₊ ⟺ x < ⌊t⌋₊+1 (Nat.floor_le_iff? or Nat.lt_floor_add_one): `Nat.lt_floor_add_one (x) : x < ⌊x⌋₊ + 1` — I have x < ⌊t⌋₊+1: suppose ⌊x⌋₊ > ⌊t⌋₊: ⌊x⌋₊ ≥ ⌊t⌋₊+1 ⟹ x ≥ ⌊x⌋₊ ≥ ⌊t⌋₊+1 (Nat.floor_le) contradiction ✓ — prove by contradiction or use `Nat.floor_le_floor`? Let me use: have h := Nat.floor_le_floor (x) (Nat.floor t)?? — `Nat.floor_le_floor : x ≤ y → ⌊x⌋₊ ≤ ⌊y⌋₊`?? that's floor_mono. The bound: x < ⌊t⌋₊+1 doesn't give x ≤ t. Direct: Nat.floor_le_iff : ⌊x⌋₊ ≤ n ↔ x < n+1 (for n : ℕ): `Nat.floor_le_iff (hx : 0 ≤ x)?` — hmm. There's `Nat.floor_le' ?`. I'll find: Nat.floor_le_floor?? Let me use the contradiction approach in proof.\n  · intro ρ hρ; exact farG_le_farW_mul ρ ((mem_mainFinset.mp hρ).1)\n  · intro k; exact main_bucket_count hZC hNLZ ht k ? ?  -- needs the k range... but hcount quantifies over ALL k!\n```\nPROBLEM: unit_family_le's hcount is ∀ k — but main_bucket_count needs 1 ≤ k ≤ ⌊t⌋₊. For k OUTSIDE the bucket range, the filter is EMPTY (no ρ with j ρ = k since j ρ ∈ [1, K]) ⟹ sum = 0 ≤ cnt k ✓. So hcount: for k ∉ [1, ⌊t⌋₊]: empty-filter proof; else main_bucket_count. Write:\n```\n  · intro k\n    by_cases hk : 1 ≤ k ∧ k ≤ Nat.floor t\n    · exact main_bucket_count hZC hNLZ ht k hk.1 hk.2\n    · -- the filter is empty\n      have hempty : (mainFinset t).filter (fun ρ => Nat.floor |ρ.1.im − t| = k) = ∅ := by\n        rw [Finset.eq_empty_iff_forall_notMem]\n        intro ρ hρ\n        rw [Finset.mem_filter] at hρ\n        obtain ⟨hmem, heq⟩ := hρ\n        have hj := (mem_mainFinset_range ...).mp hmem  -- 1 ≤ ⌊x⌋₊ ∧ ⌊x⌋₊ ≤ ⌊t⌋₊\n        exact hk ⟨heq ▸ hj.1, heq ▸ hj.2⟩\n      rw [hempty, Finset.sum_empty]\n      positivity\n```\n— needs the bucket-range factoring (mem of mainFinset ⟹ 1 ≤ ⌊x⌋₊ ≤ ⌊t⌋₊).\n\nHmm — main_bucket_count's cnt needs C0hat(t+1) — note ZeroCountProp is the hypothesis hZC. The main assembly's final form: 4.5·(2C₀+0.55)·1.3476 — matches my planned main bound ✓ (12.1284·C₀+3.33531 when expanded later).\n\nFor the bucket index: use `Nat.floor |ρ.1.im − t|` — written `⌊|ρ.1.im − t|⌋₊` in notation: Nat.floor (·) — in Lean: `⌊x⌋₊` is notation for Nat.floor x. Let me use the notation.\n\nLet me now also check `finite_subtype_norm_lt` exists (used in nearZerosSub ✓) and `Nat.floor` API names: Nat.floor_mono ✓ (probably), Nat.floor_one, Nat.floor_le (⌊x⌋₊ ≤ x for x ≥ 0: `Nat.floor_le (hx : 0 ≤ x) : ⌊x⌋₊ ≤ x` ✓), Nat.lt_floor_add_one ✓ (probably: `Nat.lt_floor_add_one (x : ℝ) : x < ⌊x⌋₊ + 1` ✓ — was used in LiCircleBound: `Nat.lt_floor_add_one _` ✓).\nFor ⌊x⌋₊ ≥ 1 from x ≥ 1: `Nat.one_le_floor_iff : 1 ≤ ⌊x⌋₊ ↔ 1 ≤ x`? — or Nat.floor_mono with Nat.floor_one. I'll use: have := Nat.floor_mono hx1 : Nat.floor 1 ≤ ⌊x⌋₊; rw [Nat.floor_one] at this ✓ — Nat.floor_one : ⌊(1:ℝ)⌋₊ = 1 ✓ probably exists; Nat.floor_mono : a ≤ b → ⌊a⌋₊ ≤ ⌊b⌋₊ ✓ exists (maybe `Nat.floor_mono`).\nFor ⌊x⌋₊ ≤ ⌊t⌋₊ from x < ⌊t⌋₊+1: `Nat.floor_lt' ?` or: by_contra: ⌊x⌋₊ > ⌊t⌋₊ ⟹ ⌊x⌋₊ ≥ ⌊t⌋₊+1 ⟹ (⌊t⌋₊+1 : ℝ) ≤ (⌊x⌋₊ : ℝ) ≤ x (Nat.floor_le (abs_nonneg _)) ⟹ ⌊t⌋₊+1 ≤ x contradicts x < ⌊t⌋₊+1 ✓ omega/nlinarith.\n\nOK let me write §16. Also the filter-emptiness: `Finset.eq_empty_iff_forall_notMem` — banked from journal-032 ✓ exists.\n\nOne more check: `mem_mainFinset` needs t ≥ 0 (for |t| = t and the ball): prove with (ht : 0 ≤ t). The ball: ‖ρ.1‖ ≤ |re| + |im| (Complex.norm_le_abs_re_add_abs_im ✓ used in nearZerosSub); |re| ≤ 1 ✓; |im| = |γ| ≤ t + x (t ≥ 0): |γ| = |γ − t + t| ≤ x + t ✓; x < ⌊t⌋₊+1 ≤ t+1 (Nat.floor_le ht) ⟹ ‖ρ‖ < 1 + t + t + 1 = 2t+2 ✓ ball finite_subtype_norm_lt (2t+2) ✓.","signature":""},{"type":"text","text":"Now §16 (3d: main bucket machine). Writing unit_family_le + mainFinset + bucket counts + main assembly."},{"type":"tool_use","id":"Edit_165","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"  have h1 := norm_tsum_le_tsum_norm hnorm_summ\n  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      ‖if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖)\n      ≤ ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farG t ρ :=\n    Summable.tsum_le_tsum (fun ρ => seriesDiffTerm_norm_le_farG ht hσlo hσhi him hζ ρ)\n      hnorm_summ (farG_summable (by linarith : (0 : ℝ) ≤ t))\n  exact h1.trans h2\n\nend NguyenRH1\n\nend","new_string":"  have h1 := norm_tsum_le_tsum_norm hnorm_summ\n  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      ‖if ρ ∈ nearZerosSub t then (0 : ℂ) else seriesDiffTerm s (2 + t * Complex.I) ρ‖)\n      ≤ ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farG t ρ :=\n    Summable.tsum_le_tsum (fun ρ => seriesDiffTerm_norm_le_farG ht hσlo hσhi him hζ ρ)\n      hnorm_summ (farG_summable (by linarith : (0 : ℝ) ≤ t))\n  exact h1.trans h2\n\n/-! ## 16. Piece 3h: the main bucket machine -/\n\n/-- **The generic bucket-family bound** (the unit-interval analog of\nLiCircleBound's `dyadic_family_le`): with bucket index j(ρ) ∈ Ico 1 (K+1),\nper-element bound g ρ ≤ W(j(ρ))·m, and per-bucket mult count ≤ cnt k,\nthe FS-sum of g is at most Σ_{k ∈ Ico 1 (K+1)} W k · cnt k. -/\nlemma unit_family_le (FS : Finset {ρ : ℂ // IsNontrivialZero ρ})\n    (j : {ρ : ℂ // IsNontrivialZero ρ} → ℕ) (K : ℕ)\n    (g : {ρ : ℂ // IsNontrivialZero ρ} → ℝ) (W : ℕ → ℝ) (cnt : ℕ → ℝ)\n    (hW : ∀ k : ℕ, 0 ≤ W k)\n    (hj : ∀ ρ ∈ FS, 1 ≤ j ρ ∧ j ρ ≤ K)\n    (hterm : ∀ ρ ∈ FS, g ρ ≤ W (j ρ) * (zeroMult (ρ : ℂ) : ℝ))\n    (hcount : ∀ k : ℕ,\n      ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), (zeroMult (ρ : ℂ) : ℝ) ≤ cnt k) :\n    ∑ ρ ∈ FS, g ρ ≤ ∑ k ∈ Finset.Ico 1 (K + 1), W k * cnt k := by\n  classical\n  have h1 : ∑ ρ ∈ FS, g ρ\n      ≤ ∑ ρ ∈ FS, W (j ρ) * (zeroMult (ρ : ℂ) : ℝ) :=\n    Finset.sum_le_sum (fun ρ hρ => hterm ρ hρ)\n  have hmaps : ∀ ρ ∈ FS, j ρ ∈ Finset.Ico 1 (K + 1) := by\n    intro ρ hρ\n    rw [Finset.mem_Ico]\n    have h1' := (hj ρ hρ).1\n    have h2' := (hj ρ hρ).2\n    exact ⟨h1', by omega⟩\n  have h2 : ∑ ρ ∈ FS, W (j ρ) * (zeroMult (ρ : ℂ) : ℝ)\n      = ∑ k ∈ Finset.Ico 1 (K + 1),\n        ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), W (j ρ) * (zeroMult (ρ : ℂ) : ℝ) :=\n    (Finset.sum_fiberwise_of_maps_to hmaps\n      (fun ρ => W (j ρ) * (zeroMult (ρ : ℂ) : ℝ))).symm\n  have h3 : ∀ k ∈ Finset.Ico 1 (K + 1),\n      ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), W (j ρ) * (zeroMult (ρ : ℂ) : ℝ)\n      = W k * ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), (zeroMult (ρ : ℂ) : ℝ) := by\n    intro k hk\n    have hterm' : ∀ ρ ∈ FS.filter (fun ρ => j ρ = k),\n        W (j ρ) * (zeroMult (ρ : ℂ) : ℝ) = W k * (zeroMult (ρ : ℂ) : ℝ) := by\n      intro ρ hρ\n      rw [Finset.mem_filter] at hρ\n      rw [hρ.2]\n    rw [Finset.sum_congr rfl hterm', Finset.mul_sum]\n  have h4 : ∀ k ∈ Finset.Ico 1 (K + 1),\n      W k * ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), (zeroMult (ρ : ℂ) : ℝ)\n        ≤ W k * cnt k :=\n    fun k hk => mul_le_mul_of_nonneg_left (hcount k) (hW k)\n  calc ∑ ρ ∈ FS, g ρ\n      ≤ ∑ ρ ∈ FS, W (j ρ) * (zeroMult (ρ : ℂ) : ℝ) := h1\n    _ = ∑ k ∈ Finset.Ico 1 (K + 1),\n          ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), W (j ρ) * (zeroMult (ρ : ℂ) : ℝ) := h2\n    _ = ∑ k ∈ Finset.Ico 1 (K + 1),\n          W k * ∑ ρ ∈ FS.filter (fun ρ => j ρ = k), (zeroMult (ρ : ℂ) : ℝ) :=\n        Finset.sum_congr rfl h3\n    _ ≤ ∑ k ∈ Finset.Ico 1 (K + 1), W k * cnt k :=\n        Finset.sum_le_sum h4\n\n/-- The main finset: far zeros with bucket k = ⌊x⌋₊ ≤ ⌊t⌋₊ (x = |γ−t|,\nequivalently x < ⌊t⌋₊+1; contained in the ball ‖ρ‖ < 2t+2). -/\ndef mainFinset (t : ℝ) : Finset {ρ : ℂ // IsNontrivialZero ρ} :=\n  (finite_subtype_norm_lt (2 * t + 2)).toFinset.filter fun ρ =>\n    1 ≤ |ρ.1.im - t| ∧ |ρ.1.im - t| < (Nat.floor t : ℝ) + 1\n\nlemma mem_mainFinset {t : ℝ} (ht : 0 ≤ t) {ρ : {ρ : ℂ // IsNontrivialZero ρ}} :\n    ρ ∈ mainFinset t ↔\n      1 ≤ |ρ.1.im - t| ∧ |ρ.1.im - t| < (Nat.floor t : ℝ) + 1 := by\n  rw [mainFinset, Finset.mem_filter]\n  refine ⟨fun h => h.2, fun h => ⟨?_, h⟩⟩\n  rw [Set.Finite.mem_toFinset]\n  show ‖ρ.1‖ < 2 * t + 2\n  have hle : ‖ρ.1‖ ≤ |ρ.1.re| + |ρ.1.im| := Complex.norm_le_abs_re_add_abs_im _\n  have hre : |ρ.1.re| ≤ 1 := by\n    have h1 : 0 < ρ.1.re := ρ.2.2.1\n    have h2 : ρ.1.re < 1 := ρ.2.2.2\n    rw [abs_le]\n    constructor <;> linarith\n  have him : |ρ.1.im| ≤ t + |ρ.1.im - t| := by\n    calc |ρ.1.im| = |ρ.1.im - t + t| := by rw [sub_add_cancel]\n      _ ≤ |ρ.1.im - t| + |t| := abs_add_le _ _\n      _ = |ρ.1.im - t| + t := by rw [abs_of_nonneg ht]\n      _ = t + |ρ.1.im - t| := by ring\n  have hft : (Nat.floor t : ℝ) ≤ t := Nat.floor_le ht\n  have hx := h.2\n  have htr : (Nat.floor t : ℝ) + 1 ≤ t + 1 := by linarith [hft]\n  have hx2 : |ρ.1.im - t| < t + 1 := lt_of_lt_of_le hx htr\n  linarith [hle, hre, him, hx2]\n\n/-- The bucket index of a main-finset element lies in [1, ⌊t⌋₊]. -/\nlemma mainFinset_bucket_range {t : ℝ} (ht : 0 ≤ t)\n    {ρ : {ρ : ℂ // IsNontrivialZero ρ}} (hρ : ρ ∈ mainFinset t) :\n    1 ≤ Nat.floor |ρ.1.im - t| ∧ Nat.floor |ρ.1.im - t| ≤ Nat.floor t := by\n  have hx := (mem_mainFinset ht).mp hρ\n  constructor\n  · have h1 := Nat.floor_mono hx.1\n    rwa [Nat.floor_one] at h1\n  · by_contra hbad\n    push_neg at hbad\n    have h2 : Nat.floor t + 1 ≤ Nat.floor |ρ.1.im - t| := hbad\n    have h3 : ((Nat.floor t + 1 : ℕ) : ℝ) ≤ (Nat.floor |ρ.1.im - t| : ℝ) := by\n      exact_mod_cast h2\n    have h4 : (Nat.floor |ρ.1.im - t| : ℝ) ≤ |ρ.1.im - t| :=\n      Nat.floor_le (abs_nonneg _)\n    have h5 : ((Nat.floor t : ℕ) : ℝ) + 1 ≤ |ρ.1.im - t| := by\n      have h6 : ((Nat.floor t + 1 : ℕ) : ℝ) = (Nat.floor t : ℝ) + 1 := by\n        push_cast; ring\n      rw [h6] at h3\n      linarith [h3, h4]\n    linarith [hx.2, h5]\n\n/-- farG is bounded by 4.5·farW(⌊x⌋₊)·m (the monotone weight chain). -/\nlemma farG_le_farW_mul {t : ℝ} (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hx : 1 ≤ |ρ.1.im - t|) :\n    farG t ρ ≤ 4.5 * (farW (Nat.floor |ρ.1.im - t|) * (zeroMult ρ.1 : ℝ)) := by\n  classical\n  have hfar : ρ ∉ nearZerosSub t := fun h => (not_lt).mp (by\n    have h' := mem_nearZerosSub.mp h\n    linarith [h', hx]) hx\n  rw [farG, if_neg hfar, farW]\n  set k : ℕ := Nat.floor |ρ.1.im - t|\n  set x : ℝ := |ρ.1.im - t|\n  have hk1 : (1 : ℝ) ≤ (k : ℝ) := by\n    have h1 := Nat.floor_mono hx\n    rw [Nat.floor_one] at h1\n    exact_mod_cast h1\n  have hkx : (k : ℝ) ≤ x := Nat.floor_le (abs_nonneg _)\n  have hmono : (k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2)\n      ≤ x * Real.sqrt (1 + x ^ 2) := by\n    apply mul_le_mul hkx _ (Real.sqrt_nonneg _) (by positivity)\n    apply Real.sqrt_le_sqrt\n    nlinarith [hkx, abs_nonneg x, hkx]\n  have hm : (0 : ℝ) ≤ (zeroMult ρ.1 : ℝ) := Nat.cast_nonneg _\n  have hpos : (0 : ℝ) < (k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2) := by\n    have h1 : (0 : ℝ) < (k : ℝ) := by linarith [hk1]\n    positivity\n  rw [show (4.5 : ℝ) * (1 / ((k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2)) * (zeroMult ρ.1 : ℝ))\n      = (4.5 * (zeroMult ρ.1 : ℝ)) * (1 / ((k : ℝ) * Real.sqrt (1 + (k : ℝ) ^ 2))) from by ring]\n  rw [show (4.5 : ℝ) * (zeroMult ρ.1 : ℝ) / (x * Real.sqrt (1 + x ^ 2))\n      = (4.5 * (zeroMult ρ.1 : ℝ)) * (1 / (x * Real.sqrt (1 + x ^ 2))) from by\n        rw [div_eq_mul_inv]]\n  apply mul_le_mul_of_nonneg_left _ (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4.5) hm)\n  exact one_div_le_one_div_of_le hpos hmono\n\n/-- **The main bucket count**: the mult-weighted count of main-finset\nzeros with bucket k (1 ≤ k ≤ ⌊t⌋₊) is at most 2·C0hat(t+1) + 0.55\n(the two-window perimeter bound + NoLowZeros emptiness for low windows). -/\nlemma main_bucket_count (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t)\n    {k : ℕ} (hk1 : 1 ≤ k) (hk2 : k ≤ Nat.floor t) :\n    ∑ ρ ∈ (mainFinset t).filter (fun ρ => Nat.floor |ρ.1.im - t| = k), (zeroMult ρ.1 : ℝ)\n      ≤ 2 * C0hat (t + 1) + 0.55 := by\n  classical\n  set FS := (mainFinset t).filter (fun ρ => Nat.floor |ρ.1.im - t| = k) with hFS\n  have hk2R : (k : ℝ) ≤ t := (Nat.floor_le (by linarith : (0 : ℝ) ≤ t)).trans\n    (by exact_mod_cast hk2)\n  -- the right window count\n  have htk2 : (2 : ℝ) ≤ t + (k : ℝ) := by\n    have h1 : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk1\n    linarith [ht, h1]\n  have hright : ((zeroWindow_finite (t + (k : ℝ))).toFinset.sum fun ρ => zeroMult ρ : ℝ)\n      ≤ C0hat (t + (k : ℝ) + 1) := hZC (t + (k : ℝ)) htk2\n  have hright2 : C0hat (t + (k : ℝ) + 1) ≤ C0hat (t + 1) + 0.55 := by\n    have h1 : C0hat (t + (k : ℝ) + 1) ≤ C0hat (2 * t + 1) := by\n      apply C0hat_mono (by linarith [ht, hk1] : (1 : ℝ) ≤ t + (k : ℝ) + 1)\n      linarith [hk2R]\n    exact h1.trans (C0hat_two_t_add_one_le ht)\n  -- the left window count (case split on k ≤ t−3)\n  have hleft : ((zeroWindow_finite (t - (k : ℝ) - 1)).toFinset.sum fun ρ => zeroMult ρ : ℝ)\n      ≤ C0hat (t + 1) := by\n    by_cases hcase : (3 : ℝ) ≤ t - (k : ℝ)\n    · have h1 : (2 : ℝ) ≤ t - (k : ℝ) - 1 := by linarith [hcase]\n      have h2 := hZC (t - (k : ℝ) - 1) h1\n      have h3 : C0hat (t - (k : ℝ) - 1 + 1) ≤ C0hat (t + 1) := by\n        apply C0hat_mono (by linarith [hcase] : (1 : ℝ) ≤ t - (k : ℝ))\n        linarith [ht]\n      have h4 : t - (k : ℝ) - 1 + 1 = t - (k : ℝ) := by ring\n      rw [h4] at h2\n      exact h2.trans h3\n    · push_neg at hcase\n      have hempty : (zeroWindow_finite (t - (k : ℝ) - 1)).toFinset = ∅ := by\n        rw [Finset.eq_empty_iff_forall_notMem]\n        intro ρ hρ\n        rw [Set.Finite.mem_toFinset] at hρ\n        obtain ⟨hz, h1, h2⟩ := hρ\n        have h3 : 14 ≤ |ρ.im| := hNLZ ρ hz\n        have h4 : ρ.im ≤ t - (k : ℝ) := h2\n        have h5 : t - (k : ℝ) < 3 := hcase\n        have h6 : t - (k : ℝ) - 1 ≥ -1 := by linarith [hk2R]\n        have h7 : ρ.im ≥ -1 := by linarith [h1, h6]\n        have h8 : |ρ.im| < 14 := by\n          rw [abs_lt]\n          constructor <;> linarith [h4, h5, h7]\n        linarith [h3, h8]\n      rw [hempty, Finset.sum_empty]\n      have h9 : (0 : ℝ) ≤ C0hat (t + 1) := by\n        have h10 := two_le_C0hat (by linarith [ht] : (1 : ℝ) ≤ t + 1)\n        linarith\n      exact h9\n  -- the image bridge: bucket ⊆ right ∪ left windows\n  have hbridge : ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n      = ∑ ρ ∈ FS.image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by\n    rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n  have hsub : FS.image (fun ρ => ρ.1)\n      ⊆ (zeroWindow_finite (t + (k : ℝ))).toFinset ∪\n        (zeroWindow_finite (t - (k : ℝ) - 1)).toFinset := by\n    intro z hz\n    obtain ⟨ρ, hρ, rfl⟩ := Finset.mem_image.mp hz\n    rw [hFS, Finset.mem_filter] at hρ\n    obtain ⟨hmem, heq⟩ := hρ\n    have hx := (mem_mainFinset (by linarith : (0 : ℝ) ≤ t)).mp hmem\n    have hk : Nat.floor |ρ.1.im - t| = k := heq\n    have hxk : (k : ℝ) ≤ |ρ.1.im - t| := Nat.floor_le (abs_nonneg _)\n    rw [← hk] at hxk\n    have hxk1 : |ρ.1.im - t| < (k : ℝ) + 1 := by\n      have h1 := Nat.lt_floor_add_one |ρ.1.im - t|\n      rw [hk] at h1\n      have h2 : ((k + 1 : ℕ) : ℝ) = (k : ℝ) + 1 := by push_cast; ring\n      rwa [h2] at h1\n    rcases le_or_gt t ρ.1.im with him | him\n    · -- γ ≥ t: x = γ − t ∈ [k, k+1): γ ∈ [t+k, t+k+1) ⊆ zeroWindow (t+k)\n      apply Finset.mem_union_left\n      rw [Set.Finite.mem_toFinset]\n      refine ⟨ρ.2, ?_, ?_⟩\n      · have h1 : |ρ.1.im - t| = ρ.1.im - t := abs_of_nonneg (by linarith [him])\n        rw [h1] at hxk\n        linarith [hxk]\n      · have h1 : |ρ.1.im - t| = ρ.1.im - t := abs_of_nonneg (by linarith [him])\n        rw [h1] at hxk1\n        linarith [hxk1]\n    · -- γ < t: x = t − γ ∈ [k, k+1): γ ∈ (t−k−1, t−k] ⊆ zeroWindow (t−k−1)\n      apply Finset.mem_union_right\n      rw [Set.Finite.mem_toFinset]\n      refine ⟨ρ.2, ?_, ?_⟩\n      · have h1 : |ρ.1.im - t| = t - ρ.1.im := abs_of_neg (by linarith [him])\n        rw [h1] at hxk1\n        linarith [hxk1]\n      · have h1 : |ρ.1.im - t| = t - ρ.1.im := abs_of_neg (by linarith [him])\n        rw [h1] at hxk\n        linarith [hxk]\n  have hdisj : Disjoint (zeroWindow_finite (t + (k : ℝ))).toFinset\n      (zeroWindow_finite (t - (k : ℝ) - 1)).toFinset := by\n    rw [Finset.disjoint_left]\n    intro z hz1 hz2\n    rw [Set.Finite.mem_toFinset] at hz1 hz2\n    have h1 : t + (k : ℝ) ≤ z.im := hz1.2.1\n    have h2 : z.im ≤ t - (k : ℝ) := hz2.2.2\n    have h3 : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk1\n    linarith [h1, h2, h3]\n  have hW1 := (zeroWindow_finite (t + (k : ℝ)))\n  have hW2 := (zeroWindow_finite (t - (k : ℝ) - 1))\n  calc ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n      = ∑ z ∈ FS.image (fun ρ => ρ.1), (zeroMult z : ℝ) := hbridge\n    _ ≤ ∑ z ∈ hW1.toFinset ∪ hW2.toFinset, (zeroMult z : ℝ) :=\n        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n    _ = ∑ z ∈ hW1.toFinset, (zeroMult z : ℝ) + ∑ z ∈ hW2.toFinset, (zeroMult z : ℝ) :=\n        Finset.sum_union hdisj\n    _ ≤ (C0hat (t + 1) + 0.55) + C0hat (t + 1) := by\n        have h1 : (((hW1).toFinset.sum fun ρ => zeroMult ρ) : ℝ)\n            ≤ C0hat (t + 1) + 0.55 := hright.trans hright2\n        have h2 : (((hW2).toFinset.sum fun ρ => zeroMult ρ) : ℝ)\n            ≤ C0hat (t + 1) := hleft\n        linarith [h1, h2]\n    _ = 2 * C0hat (t + 1) + 0.55 := by ring\n\n/-- **The main bound**: the main-finset farG sum is at most\n4.5·(2·C0hat(t+1) + 0.55)·1.3476. -/\nlemma farG_main_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t) :\n    ∑ ρ ∈ mainFinset t, farG t ρ\n      ≤ 4.5 * (2 * C0hat (t + 1) + 0.55) * 1.3476 := by\n  classical\n  have hU := unit_family_le (mainFinset t) (fun ρ => Nat.floor |ρ.1.im - t|)\n    (Nat.floor t) (farG t) (fun k => 4.5 * farW k)\n    (fun _ => 2 * C0hat (t + 1) + 0.55)\n    (fun k => mul_nonneg (by norm_num : (0 : ℝ) ≤ 4.5) (farW_nonneg k))\n    (fun ρ hρ => mainFinset_bucket_range (by linarith : (0 : ℝ) ≤ t) hρ)\n    (fun ρ hρ => farG_le_farW_mul ρ\n      ((mem_mainFinset (by linarith : (0 : ℝ) ≤ t)).mp hρ).1)\n    (fun k => by\n      by_cases hk : 1 ≤ k ∧ k ≤ Nat.floor t\n      · exact main_bucket_count hZC hNLZ ht hk.1 hk.2\n      · push_neg at hk\n        have hempty : (mainFinset t).filter (fun ρ => Nat.floor |ρ.1.im - t| = k) = ∅ := by\n          rw [Finset.eq_empty_iff_forall_notMem]\n          intro ρ hρ\n          rw [Finset.mem_filter] at hρ\n          obtain ⟨hmem, heq⟩ := hρ\n          have hj := mainFinset_bucket_range (by linarith : (0 : ℝ) ≤ t) hmem\n          rw [heq] at hj\n          exact hk ⟨hj.1, hj.2⟩\n        rw [hempty, Finset.sum_empty]\n        positivity)\n  have hsum : ∑ k ∈ Finset.Ico 1 (Nat.floor t + 1), (4.5 * farW k) * (2 * C0hat (t + 1) + 0.55)\n      = (4.5 * (2 * C0hat (t + 1) + 0.55)) * ∑ k ∈ Finset.Ico 1 (Nat.floor t + 1), farW k := by\n    rw [Finset.mul_sum]\n    apply Finset.sum_congr rfl\n    intro k _\n    ring\n  calc ∑ ρ ∈ mainFinset t, farG t ρ\n      ≤ ∑ k ∈ Finset.Ico 1 (Nat.floor t + 1), (4.5 * farW k) * (2 * C0hat (t + 1) + 0.55) := hU\n    _ = (4.5 * (2 * C0hat (t + 1) + 0.55)) * ∑ k ∈ Finset.Ico 1 (Nat.floor t + 1), farW k := hsum\n    _ ≤ (4.5 * (2 * C0hat (t + 1) + 0.55)) * 1.3476 :=\n        mul_le_mul_of_nonneg_left (farW_Ico_le _) (by positivity)\n\nend NguyenRH1\n\nend"},"extra_content":null}]