[{"type":"thinking","thinking":"The file compiles clean (no errors). The core lemmas are green:\n- `liSummand`, `summand_conj`, `liSummand_eq`\n- `pow_one_add_inv_two_mul_le`\n- `re_li_summand_le` (the key estimate)\n\nNow I need the final summability assembly: `liSummable`. Let me append it to the file. Components:\n1. Comparison: 1 + normSq (gammaOf z) ≤ (9/4)·‖z‖² for z with re ∈ [0,1] and ‖z‖ ≥ 2n (n ≥ 1).\n2. The dominator D and its summability via zero_sum_inv_sq + finite support modification.\n3. Final: Summable (liSummand n) via Summable.of_norm_bounded.\n\nFor the comparison lemma:\n```\nlemma normSq_gammaOf_le_mul_norm_sq {n : ℕ} (hn : 1 ≤ n) {z : ℂ}\n    (hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :\n    1 + Complex.normSq (gammaOf z) ≤ 9 / 4 * ‖z‖ ^ 2 := by\n  have hzn : ... \n  have hgam : Complex.normSq (gammaOf z) = z.im ^ 2 + (1 / 2 - z.re) ^ 2 := by\n    rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]  -- wait, namespaces: gammaOf_re/gammaOf_im are in Zeta23.WeilEF namespace\n    ring\n  rw [hgam, Complex.normSq_eq_norm_sq z, Complex.normSq_apply]\n  have him : 1 ≤ z.im ^ 2 := by\n    have : z.re ^ 2 ≤ 1 := by nlinarith [hzre0, hzre1]\n    have hz2 : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2 := by rw [← hnsq?...]\n    nlinarith [hz, hzre0, hzre1, ...]\n  nlinarith [hzre0, hzre1, him]\n```\nHmm — ‖z‖² = re² + im²: from Complex.normSq_eq_norm_sq z : normSq z = ‖z‖² and normSq_apply : normSq z = re*re + im*im — so ‖z‖² = re²+im² (with squares: re*re = re^2 via sq). Then:\n1 + normSq γ_ρ = 1 + im² + (1/2−re)². (1/2−re)² ≤ 1/4 since re ∈ [0,1] (|1/2−re| ≤ 1/2). So LHS ≤ 5/4 + im². RHS = 9/4·(re²+im²) ≥ 9/4·im². Need 5/4 + im² ≤ 9/4·im² ⟺ 5/4 ≤ 5/4·im² ⟺ 1 ≤ im². And im² = ‖z‖² − re² ≥ (2n)² − 1 ≥ 3 ≥ 1 ✓ (n ≥ 1: 4n² ≥ 4, −1: ≥ 3).\nnlinarith should close: given hzre0, hzre1, hz : 2n ≤ ‖z‖ (need ‖z‖² ≥ 4n²: from hz and nonneg: `sq_le_sq`... (2n)² ≤ ‖z‖² via pow_le_pow_left₀ (by positivity) hz 2), ‖z‖² = re²+im², re² ≤ 1 (from re ∈ [0,1]: nlinarith).\nLet me structure with explicit haves and one nlinarith at the end.\n\nFor the final summability:\n\n```\ntheorem liSummable (n : ℕ) : Summable (liSummand n) := by\n  cases Nat.eq_zero_or_pos n with\n  | inl h0 =>\n      subst h0\n      have : liSummand 0 = fun _ => 0 := by\n        funext ρ\n        simp [liSummand]\n      rw [this]\n      exact summable_zero\n  | inr hn =>\n    -- dominator\n    let D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n      if (2 * n : ℝ) ≤ ‖(ρ : ℂ)‖ then\n        (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))\n      else ‖liSummand n ρ‖\n    have hD : Summable D := by\n      have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n          (9 / 2) * n ^ 2 * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by\n        have h := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9 / 2) * (n : ℝ) ^ 2)\n        -- h : Summable ((9/2)n² • (mult/(1+normSq))) — show forms match\n        convert h using 2\n        · ext ρ; ring\n      ...\n```\n\nHmm wait — careful with forms: zero_sum_inv_sq zetaSeam : Summable (fun ρ : (zetaZeros zetaSeam).carrier => (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))). The subtype (zetaZeros zetaSeam).carrier — defeq to {ρ // IsNontrivialZero ρ}. `.mul_left c` : Summable (fun ρ => c * (zeroMult ρ / (1+...))) — `Summable.mul_left : Summable f → Summable (fun i => c * f i)`. So h : Summable (fun ρ => ((9/2)*n²) * ((zeroMult ρ:ℝ)/(1+normSq (gammaOf ρ)))). And I want Summable (fun ρ => (9/2)n²·mult/(1+normSq)): same up to assoc/division form: (9/2)*n² * (mult/(1+..)) vs (9/2)*n²*mult/(1+..) — equal by ring (div). And the subtype mismatch: h is over (zetaZeros zetaSeam).carrier, I claim it over {ρ // IsNontrivialZero ρ} — `show` conversion (defeq via zetaZeroConfig_carrier rfl). Actually zero_sum_inv_sq's statement: `Summable (fun ρ : (zetaZeros hs).carrier => (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))`. Is `(zetaZeros zetaSeam).carrier` defeq `{ρ | IsNontrivialZero ρ}`? zetaZeroConfig_carrier : zetaZeroConfig.carrier = {ρ | IsNontrivialZero ρ} := rfl — and zetaZeroConfig := zetaZeros zetaSeam — so (zetaZeros zetaSeam).carrier is DEFEQ {ρ | IsNontrivialZero ρ} ✓. The subtype {x // x ∈ {ρ | IsNontrivialZero ρ}} vs {ρ // IsNontrivialZero ρ}: defeq (Set.mem_setOf) ✓.\n\nSo: have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => (9/2)*(n:ℝ)^2 * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by\n  have h := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9 / 2) * (n : ℝ) ^ 2)\n  exact h  -- if defeq works; else convert\n\nThen D = (fun ρ => if 2n ≤ ‖ρ‖ then hbase-family else ‖liSummand n ρ‖):\nD = hbase-family + (D − hbase-family), where the difference is supported in the ball {‖ρ‖ < 2n} — finite.\n\nCleaner: define E := D − hbasefam (pointwise); E ρ = if 2n ≤ ‖ρ‖ then 0 else ‖liSummand n ρ‖ − hbasefam ρ. supp E ⊆ {ρ : ‖ρ‖ < 2n} finite.\nD = hbasefam + E: `Summable.add`.\n\nThe finite support set: {ρ : {ρ // IsNontrivialZero ρ} | ¬ (2n ≤ ‖(ρ:ℂ)‖)}:\nhave hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) * n ≤ ‖(ρ : ℂ)‖)}.Finite := by\n  have hcomp : IsCompact (Metric.closedBall (0 : ℂ) (2 * n)) := isCompact_closedBall _ _\n  have hsub : (Metric.closedBall (0 : ℂ) (2 * n)) ∩ riemannZetaZeros := hcomp.inter_riemannZetaZeros_finite\n  -- wait: `IsCompact.inter_riemannZetaZeros_finite (hS : IsCompact S) : (S ∩ riemannZetaZeros).Finite`\n  have hzeros : (Metric.closedBall (0 : ℂ) (2 * n)) ∩ {ρ | IsNontrivialZero ρ} ⊆ \n      Metric.closedBall (0:ℂ) (2*n) ∩ riemannZetaZeros := by\n    apply Set.inter_subset_inter_left\n    intro ρ hρ\n    exact hρ.1  -- IsNontrivialZero ρ → riemannZeta ρ = 0 → ρ ∈ riemannZetaZeros\n  have hfin2 : (Metric.closedBall (0 : ℂ) (2 * n)) ∩ {ρ | IsNontrivialZero ρ} := \n    (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n  -- transfer to the subtype-set via coe injection\n  ...\n  \nHmm — riemannZetaZeros : Set ℂ := riemannZeta ⁻¹' {0}. ρ ∈ riemannZetaZeros ⟺ riemannZeta ρ = 0 ✓ (mem_preimage, mem_singleton). IsNontrivialZero ρ := riemannZeta ρ = 0 ∧ 0 < ρ.re ∧ ρ.re < 1 ✓ so .1 gives membership ✓.\n\nThen the set {ρ : subtype | ‖ρ‖ < 2n} = Subtype.val ⁻¹' (ball ∩ {IsNontrivialZero})-ish: the subtype set S' = {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ:ℂ)‖ < 2n}: its image under Subtype.val is {z : ℂ | IsNontrivialZero z ∧ ‖z‖ < 2n} ⊆ ball ∩ IsNontrivialZero-set — finite. And Subtype.val injective: Set.Finite.of_finite_image:\n`Set.Finite.of_finite_image (hf : (f '' s).Finite) (hinj : Set.InjOn f s) : s.Finite` ✓.\n\nSo:\nhave hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) * n ≤ ‖(ρ : ℂ)‖)}.Finite := by\n  have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2:ℝ)*n ≤ ‖(ρ:ℂ)‖)}).Finite := by\n    apply Set.Finite.subset hfin2\n    rintro z ⟨ρ, hρ, rfl⟩\n    -- show z ∈ closedBall ∩ {IsNontrivialZero}\n    constructor\n    · -- z ∈ closedBall 0 (2n): ‖z‖ ≤ 2n\n      simp only [Metric.mem_closedBall, dist_zero_right]\n      -- dist z 0 = ‖z‖: mem_closedBall: dist z 0 ≤ 2n\n      have : ‖z‖ < 2 * n := lt_of_not_ge hρ\n      -- need dist z 0 ≤ 2n: dist = norm\n      ...\n    · exact ρ.2\n  exact Set.Finite.of_finite_image himg (fun _ _ _ _ h => Subtype.ext h)\n  \nHmm — Set.InjOn of Subtype.val: Subtype.val_injective.injOn — `Subtype.val_injective : Function.Injective Subtype.val` ✓ .injOn.\n\ndist_zero_right : dist z 0 = ‖z‖ ✓ (dist_zero_right (z) : dist z 0 = ‖z‖).\n\nSupport: Function.support E ⊆ that set: E ρ ≠ 0 ⟹ ¬(2n ≤ ‖ρ‖): by construction E ρ = if 2n ≤ ‖ρ‖ then (fam − fam) else (‖liSummand‖ − fam): define E directly as D − fam: supp(D − fam) ⊆ {¬(2n ≤ ‖ρ‖)}: for ρ with 2n ≤ ‖ρ‖: D ρ = fam ρ ⟹ (D − fam) ρ = 0 ✓.\n\nThen:\nhave hE : Summable E := summable_of_finite_support hsuppfin\nhave hD : Summable D := by\n  have : D = fun ρ => hbasefam ρ + E ρ := by funext ρ; simp [E, D]; split <;> ring\n  rw [this]\n  exact hbase.add hE\n\nHmm — cleaner: hD via `hbase.add hE` and show D ρ = hbasefam ρ + E ρ by funext + split + ring.\n\nAnd finally:\nrefine Summable.of_norm_bounded hD (fun ρ => ?_)\n-- ‖liSummand n ρ‖ ≤ D ρ\nby_cases hρ : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖\n· -- main bound\n  rw [liSummand_eq n ρ]\n  have hbound : ‖liSummand n ρ‖ ≤ (9/2)*n^2*(zeroMult ρ : ℝ)/(1 + normSq (gammaOf ρ)) := ...\n  simp only [D, hρ, if_pos hρ]  -- D ρ = the if-true branch\n  ...\n· simp [D, hρ]  -- else branch: D ρ = ‖liSummand n ρ‖, le_refl\n\nThe main bound: ‖(zeroMult : ℂ)·((f.re : ℂ))‖ = (zeroMult : ℝ)·|f.re| (mult ≥ 0: norm_num cast: ‖(m : ℂ)‖ = m for m : ℕ — `Complex.norm_natCast`? ‖(n : ℂ)‖ = n — exists as `Complex.norm_natCast (n : ℕ) : ‖(n : ℂ)‖ = n` or `norm_natCast` generic (RCLike.norm_natCast). Then:\n≤ (zeroMult : ℝ) · (2n²/‖ρ‖²)  [re_li_summand_le with hzre from IsNontrivialZero: 0 < re, re < 1 — need 0 ≤ re and re ≤ 1: from hρ2 : ρ.2 : IsNontrivialZero ρ: hρ2.2.1.le and hρ2.2.2.le]\n≤ (zeroMult : ℝ) · (2n² · (9/4)/(1+‖γ‖²))  [normSq_gammaOf_le: mult/‖ρ‖² ≤ mult·(9/4)/(1+‖γ‖²) ⟺ mult·(1+‖γ‖²)·... careful: mult/‖ρ‖² ≤ (9/4)·mult/(1+‖γ‖²) ⟺ mult·(1+‖γ‖²) ≤ (9/4)·mult·‖ρ‖² ⟸ (1+‖γ‖²) ≤ (9/4)‖ρ‖² ✓ (mult ≥ 0)]\n= (9/2)·n²·mult/(1+‖γ‖²) ✓.\n\nLet me write these steps as an explicit calc with the div manipulations via div_le_iff₀ and friends. To keep it manageable, I'll write a helper lemma:\n\nlemma liSummand_norm_le {n : ℕ} (hn : 1 ≤ n) (ρ : {ρ // IsNontrivialZero ρ})\n    (hρ : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖) :\n    ‖liSummand n ρ‖ ≤ (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)) := by\n  rw [liSummand_eq n ρ]\n  have hz := ρ.2  -- IsNontrivialZero (ρ:ℂ)\n  have hre0 : 0 ≤ (ρ : ℂ).re := hz.2.1.le\n  have hre1 : (ρ : ℂ).re ≤ 1 := hz.2.2.le\n  have hcore := re_li_summand_le hn hre0 hre1 hρ  -- |(f).re| ≤ 2n²/‖ρ‖²\n  have hcomp := normSq_gammaOf_le_mul_norm_sq hn hre0 hre1 hρ  -- 1+‖γ‖² ≤ (9/4)‖ρ‖²\n  -- norm of the complex product\n  have hnorm : ‖(zeroMult ρ : ℂ) * (((1 - (1 - 1 / (ρ:ℂ)) ^ n).re) : ℂ)‖\n      = (zeroMult ρ : ℝ) * |(1 - (1 - 1 / (ρ:ℂ)) ^ n).re| := by\n    rw [norm_mul]\n    congr 1\n    · exact RCLike.norm_natCast (K := ℂ) (zeroMult ρ) -- hmm name; check: RCLike.norm_natCast?\n    · exact RCLike.norm_ofReal ((1 - (1 - 1 / (ρ:ℂ)) ^ n).re)  -- RCLike.norm_ofReal? or Complex.norm_ofReal\n  rw [hnorm]\n  -- chain: mult·|re| ≤ mult·2n²/‖ρ‖² ≤ (9/2)n²·mult/(1+‖γ‖²)\n  ...\n```\n\nNorm names: `RCLike.norm_natCast (n : ℕ) : ‖(n : K)‖ = n` — exists? There's `Complex.norm_natCast`? In Mathlib: `RCLike.norm_natCast (n : ℕ) : ‖(n : 𝕜)‖ = n` ✓ I believe. And ofReal: `RCLike.norm_ofReal (r : ℝ) : ‖(r : 𝕜)‖ = |r|` ✓ exists. Also `Complex.norm_ofReal`? RCLike version should work for ℂ.\n\nThe chain mult·|re| ≤ (9/2)n²·mult/(1+‖γ‖²):\nmult·|re| ≤ mult·(2n²/‖ρ‖²) (mul_le_mul_of_nonneg_left hcore (Nat.cast_nonneg _))\nand 2n²·mult/‖ρ‖² ≤ (9/2)n²·mult/(1+‖γ‖²):\n  ⟺ 2·mult/‖ρ‖² ≤ (9/2)·mult/(1+‖γ‖²) (divide n²>0)\n  ⟸ 2·mult·(1+‖γ‖²) ≤ (9/2)·mult·‖ρ‖² (cross-multiply, both sides pos)\n  ⟸ 2·(1+‖γ‖²) ≤ (9/2)·‖ρ‖² (divide mult ≥ 0 — careful mult could be... zeroMult ≥ 1 for zeros! (ZetaSeam.one_le_mult_holds : 1 ≤ zeroMult ρ for IsNontrivialZero) ✓ but we just need ≥ 0 for the mul, and if mult = 0 everything is 0 ✓ — so just nlinarith with mult ≥ 0)\n  follows from hcomp : 1+‖γ‖² ≤ (9/4)‖ρ‖²: 2·(1+‖γ‖²) ≤ 2·(9/4)‖ρ‖² = (9/2)‖ρ‖² ✓.\nWrite via div_le_iff₀ + nlinarith, or explicit cross-multiplication. I'll do:\n```\nhave hn2 : (0 : ℝ) < n ^ 2 := by positivity\nhave hz0' : (0 : ℝ) < ‖(ρ : ℂ)‖ ^ 2 := by positivity  -- needs ‖ρ‖ ≠ 0: from 2n ≤ ‖ρ‖ and n ≥ 1: ‖ρ‖ ≥ 2 > 0\nhave hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n  have : 0 ≤ Complex.normSq (gammaOf (ρ : ℂ)) := Complex.normSq_nonneg _\n  linarith\nhave key : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2)\n    ≤ (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n  rw [div_le_iff₀ hz0'']  -- hmm direction: A ≤ B/C... let me use le_div_iff₀\n  ...\n```\nLet me set it up as: goal2 : (zeroMult:ℝ) * (2*n²/‖ρ‖²) ≤ (9/2)*n²*mult/(1+‖γ‖²). \nUse le_div_iff₀ : a ≤ b / c ↔ a * c ≤ b (hc : 0 < c): with a = mult·(2n²/‖ρ‖²), c = 1+‖γ‖², b = (9/2)n²·mult:\ngoal: mult·(2n²/‖ρ‖²)·(1+‖γ‖²) ≤ (9/2)n²·mult.\nThen: mult·(2n²/‖ρ‖²)·(1+‖γ‖²) ≤ mult·(2n²/‖ρ‖²)·(9/4‖ρ‖²) = (9/2)n²·mult: via mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left ... ) — nlinarith might handle given hcomp and nonneg facts. I'll write:\n```\n  rw [le_div_iff₀ hg0]\n  have hbound : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * (1 + Complex.normSq (gammaOf (ρ : ℂ)))\n      ≤ (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2) := by\n    apply mul_le_mul_of_nonneg_left hcomp (by positivity)\n  calc (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * (1 + Complex.normSq (gammaOf (ρ : ℂ)))\n      ≤ (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2) := hbound\n    _ = (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) := by field_simp; ring\n```\nle_div_iff₀ signature check: `le_div_iff₀ (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b` ✓ (dual of div_le_iff₀). Let me grep to confirm both names. Actually from the earlier grep: `div_le_iff₀ (hc : 0 < c) : b / c ≤ a ↔ b ≤ a * c` at GroupWithZero/Basic.lean:1138 ✓. le_div_iff₀ should be nearby — likely exists.\n\nWait — hcomp : 1 + normSq ≤ (9/4)·‖ρ‖² but mul_le_mul_of_nonneg_left expects b ≤ c: hcomp's LHS 1+normSq, RHS (9/4)‖ρ‖² ✓ b := 1+normSq, c := (9/4)‖ρ‖², a := mult·(2n²/‖ρ‖²) ✓.\n\nAnd the final calc target after le_div_iff₀: a*c ≤ b: a = mult·(2n²/‖ρ‖²), c = 1+‖γ‖², b = (9/2)n²·mult ✓ matches.\n\n`Complex.normSq_nonneg` — check: normSq_nonneg (z) : 0 ≤ normSq z ✓ exists I believe.\n\nAlso `hz0''` for field_simp at the end — field_simp handles ‖ρ‖² ≠ 0 — need ‖ρ‖ ≠ 0: (‖ρ‖ ≥ 2n ≥ 2 > 0): have hz0' : ‖(ρ:ℂ)‖ ≠ 0 := ne_of_gt (by ... : 0 < ‖ρ‖): have hpos : 0 < ‖(ρ:ℂ)‖ := by have := hρ; ... : 0 < 2n ≤ ‖ρ‖: exact lt_of_lt_of_le (by positivity : (0:ℝ) < 2*n) hρ. positivity proves 0 < 2*(n:ℝ)? 2*n with n : ℕ cast, hn : 1 ≤ n — positivity needs to know n > 0 — from hn in context: `by positivity` might not find it; use `by have : (0:ℝ) < n := by exact_mod_cast hn; positivity`. OK.\n\nThen the last assembly:\n```\n  calc (zeroMult ρ : ℝ) * |(1 - (1 - 1 / (ρ:ℂ)) ^ n).re|\n      ≤ (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) :=\n        mul_le_mul_of_nonneg_left hcore (Nat.cast_nonneg _)\n    _ ≤ (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := key\n```\n\nNow — normSq_gammaOf_le_mul_norm_sq: need WeilEF.gammaOf_re / gammaOf_im — they're in namespace Zeta23.WeilEF: `WeilEF.gammaOf_re (ρ : ℂ) : (gammaOf ρ).re = ρ.im` ✓ (from ZeroSummability.lean, public lemmas in Zeta23.WeilEF namespace). With open Zeta23, use WeilEF.gammaOf_re.\n\nComplex.normSq_apply : normSq z = z.re * z.re + z.im * z.im ✓.\n\nFor the comparison lemma, final nlinarith:\n```\nlemma normSq_gammaOf_le_mul_norm_sq {n : ℕ} (hn : 1 ≤ n) {z : ℂ}\n    (hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :\n    1 + Complex.normSq (gammaOf z) ≤ 9 / 4 * ‖z‖ ^ 2 := by\n  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn\n  have hz2 : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2 := by\n    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    ring\n  have hz4 : 4 * n ^ 2 ≤ ‖z‖ ^ 2 := by\n    have h := pow_le_pow_left₀ (by positivity : (0:ℝ) ≤ 2 * n) hz 2\n    ring_nf at h ⊢\n    exact h\n  have hre2 : z.re ^ 2 ≤ 1 := by nlinarith [hzre0, hzre1]\n  have him : 1 ≤ z.im ^ 2 := by nlinarith [hz2, hz4, hre2, hn0]\n  have hgam : Complex.normSq (gammaOf z) = z.im ^ 2 + (1 / 2 - z.re) ^ 2 := by\n    rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n    ring\n  rw [hgam, hz2]\n  nlinarith [hzre0, hzre1, him, hre2]\n```\nWait — the goal after rw [hgam, hz2]: 1 + (im² + (1/2−re)²) ≤ 9/4·(re²+im²): with (1/2−re)² ≤ 1/4 (from re ∈ [0,1] via nlinarith) and 1 ≤ im²: nlinarith [hzre0, hzre1, him, hre2] — need it to derive: LHS = 1+im²+(1/2−re)² and RHS = (9/4)(re²+im²): since re² ≥ 0: RHS ≥ (9/4)im²; LHS ≤ 1 + im² + 1/4 = 5/4 + im²; 5/4+im² ≤ (9/4)im² ⟺ 5/4 ≤ 5/4 im² ⟺ 1 ≤ im² ✓. nlinarith should manage with him and the square nonneg + (1/2−re)² ≤ 1/4 derived from hzre0/hzre1 (nlinarith can do: (1/2−re)² ≤ 1/4 needs expansion — nlinarith with hints [sq_nonneg (1/2 − z.re), hzre0, hzre1] ✓). Let me give nlinarith more hints: nlinarith [hzre0, hzre1, him, hre2, sq_nonneg (1 / 2 - z.re), sq_nonneg z.re].\n\nhz4 : 4n² ≤ ‖z‖²: pow_le_pow_left₀ (0 ≤ 2n) hz 2 gives (2n)² ≤ ‖z‖²: (2n)² = 4n²: ring_nf at h ⊢ — h : (2n)² ≤ ‖z‖² — ring_nf converts (2*n)^2 → 4*n^2 ✓.\n\nHmm, wait: `pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a^n ≤ b^n` — hz : 2*n ≤ ‖z‖ with 2*n as ℝ: 2*(n:ℝ) or (2*n : ℝ)? The hypothesis hz : 2 * n ≤ ‖z‖ — with n : ℕ, this elaborates as ↑(2*n)? or 2*↑n? In my statements I've been writing `2 * n ≤ ‖z‖` and Lean elaborated `2 * ↑n ≤ ‖z‖` (from the error displays: hz : 2 * ↑n ≤ ‖z‖ ✓). Good.\n\nOne more piece — the main summability theorem. Let me also double check `Summable.of_norm_bounded` exists with that exact name. And `summable_of_finite_support`, `Set.Finite.of_finite_image`, `isCompact_closedBall`, `IsCompact.inter_riemannZetaZeros_finite` (from agent: exists in ZetaZeros.lean ✓), `dist_zero_right`, `Subtype.val_injective`.\n\n`Summable.of_norm_bounded`: grep it. Let me write the code and check names as I go. Actually — one more check on names before the big write: Summable.of_norm_bounded, summable_of_finite_support, Set.Finite.of_finite_image.","signature":""},{"type":"text","text":"Core estimates compile. Let me verify the remaining API names for the summability assembly."},{"type":"tool_use","id":"Bash_134","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem Summable.of_norm_bounded\\|lemma Summable.of_norm_bounded\" Mathlib/ --include=*.lean | head -2; grep -rn \"theorem summable_of_finite_support\\|lemma summable_of_finite_support\" Mathlib/ --include=*.lean | head -2; grep -rn \"theorem Set.Finite.of_finite_image\\|lemma Set.Finite.of_finite_image\" Mathlib/ --include=*.lean | head -2; grep -rn \"norm_natCast\\|norm_ofReal\" Mathlib/Analysis/RCLike/Basic.lean | head -4","description":"Verify summability assembly API names"},"extra_content":null}]