[{"type":"thinking","thinking":"I have the full picture of the ii′-4c pattern. Now write the general version. Note the structure differences for general n:\n\n- HfunT n s := 2 * (π:ℂ)^(−s/2) * Γ(s/2 + n + 1) / Q n s where Q n s := ∏ j ∈ Finset.range n, (s/2 + ↑j).\n- At n = 1: Q 1 s = (s/2 + 0) = s/2; HfunT 1 s = 2π^{−s/2}Γ(s/2+2)/(s/2) = 4π^{−s/2}Γ(s/2+2)/s = Hfun s ✓ consistent (good sanity check).\n\nPlan the file `NguyenRH1/LiTrivialZeros.lean`:\n\n```\n/-\nNguyenRH1/LiTrivialZeros.lean — ii′-5e prep: zeroMult(−2n) = 1 for ALL n ≥ 1\n...\n-/\nimport Mathlib\nimport Zeta23.RvM.CountByIntegral\nimport NguyenRH1.LiContour   -- for consistency of environment (zeroMult used in LiSides etc.)\n```\nHmm — actually importing LiContour pulls LiSides + LiSkeleton — heavy but built. Do I need anything from them? zeroMult is Zeta23.Statement (via LiContour's import). Let me just import Mathlib + Zeta23.Statement + Zeta23.RvM.CountByIntegral. Check: does Zeta23.RvM.CountByIntegral import Zeta23.Statement? It uses IsNontrivialZero — yes surely. So imports: Mathlib + Zeta23.RvM.CountByIntegral suffices; add Zeta23.Statement for safety (cheap).\n\nWait — do I want this in a separate file or in LiReflect.lean? A separate file is cleaner (thematic: trivial zeros). But the root import list must add it. Since LiReflect builds on LiDisc (heavy), and this file doesn't need LiDisc, a separate file keeps it light. But — hmm, actually for ii′-5e I'll eventually have a LiIdentity.lean that imports everything. Fine: new file LiTrivialZeros.lean.\n\nNow write the code:\n\n§1 Gamma_mul_prod:\n```\n/-- The product-form Γ recurrence: Γ(z)·∏_{j≤n}(z+j) = Γ(z+n+1),\nvalid when z avoids {0, −1, …, −n} (the poles crossed by the iteration). -/\ntheorem Complex.Gamma_mul_prod (z : ℂ) (n : ℕ) (hz : ∀ k : ℕ, k ≤ n → z ≠ -(k : ℂ)) :\n    Complex.Gamma z * ∏ j ∈ Finset.range (n + 1), (z + (j : ℂ))\n      = Complex.Gamma (z + n + 1) := by\n  induction n with\n  | zero =>\n    have h0 : z ≠ 0 := by\n      have := hz 0 (le_refl 0)\n      simpa using this\n    rw [Finset.range_one, Finset.prod_singleton]\n    -- Γ z * (z + 0) = Γ (z + 0 + 1): hmm cast: ((0:ℕ):ℂ): z + ↑0 = z + 0 = z; and z + ↑0 + 1 vs z + 1\n    simp [Complex.Gamma_add_one z h0]  -- Gamma (z+1) = z * Gamma z: goal Γ z * (z + ↑0) = Γ (z + ↑0 + 1): normalize casts: ↑0 = 0: simp; then Γ z * z = Γ (z + 1): rw [Complex.Gamma_add_one z h0]; ring (mul_comm)\n  | succ m ih =>\n    have hz' : ∀ k : ℕ, k ≤ m → z ≠ -(k : ℂ) := fun k hk => hz k (hk.trans (Nat.le_succ m))\n    have hlast : z + (m : ℂ) + 1 ≠ 0 := by\n      have h := hz (m + 1) (le_refl _)\n      -- h : z ≠ -↑(m+1): need z + ↑m + 1 ≠ 0: z + ↑m + 1 = z + ↑(m+1): push_cast\n      intro hzero\n      apply h\n      -- from z + ↑m + 1 = 0: z = -(↑m + 1) = -↑(m+1)\n      have h2 : z = -(z + (m:ℂ) + 1) + (z + (m:ℂ) + 1) + z?? -- overcomplicating: z + ↑m + 1 = 0 ⟹ z = -(↑m+1): by linear? complex: z = (z + ↑m + 1) - (↑m + 1) = -(↑m+1):\n      have h3 : z = -((m : ℂ) + 1) := by\n        have := hzero\n        -- z + ↑m + 1 = 0 ⟹ z = -(↑m) - 1 = -(↑m + 1)\n        field_simp? no: just: eq_neg_of_add_eq_zero_left? h2 : (z + ↑m) + 1 = 0: eq_neg_of_add_eq_zero_left h2 : z + ↑m = -1: then z = -1 - ↑m = -(↑m + 1): \n      ...\n```\nLet me redo hlast cleanly: goal z + ↑m + 1 ≠ 0. Suppose hzero : z + ↑m + 1 = 0. Then z = −(↑m + 1): `eq_neg_of_add_eq_zero_left : a + b = 0 → a = −b` — hmm hzero : (z + ↑m) + 1 = 0 — as (z + ↑m) + 1: eq_neg_of_add_eq_zero_left hzero : z + ↑m = −1. Then z = −1 − ↑m: eq_sub_of... z = (z + ↑m) − ↑m = −1 − ↑m = −(↑m + 1): \n```\n      have h4 : z = -((m : ℂ) + 1) := by\n        have h5 : z + (m : ℂ) = -1 := eq_neg_of_add_eq_zero_left hzero  -- wait hzero : z + ↑m + 1 = 0 parses as (z + ↑m) + 1 = 0 ✓\n        -- z = -1 - ↑m\n        have h6 : z = -1 - (m : ℂ) := by\n          have := congrArg (· - (m : ℂ)) h5\n          rwa [add_sub_cancel_right] at this  -- this : z = -1 - ↑m\n        rw [h6]; ring\n      -- target: z = -↑(m+1): -((m:ℂ)+1) = -↑(m+1): push_cast\n      rw [h4]  -- goal -((m:ℂ)+1) = -↑(m+1)?? no — I need to contradict h : z ≠ -↑(m+1): apply h; rw [h4]; push_cast; ring\n```\nCleaner: apply h; then goal z = −↑(m+1); rw [h4]: goal −(↑m+1) = −↑(m+1): push_cast; ring — ↑(m+1) = ↑m + 1 ✓. So:\n```\n    have hlast : z + (m : ℂ) + 1 ≠ 0 := by\n      intro hzero\n      have h5 : z + (m : ℂ) = -1 := eq_neg_of_add_eq_zero_left hzero\n      have h6 : z = -1 - (m : ℂ) := by\n        have h7 := congrArg (· - (m : ℂ)) h5\n        rwa [add_sub_cancel_right] at h7\n      exact hz (m + 1) (le_refl _) (by rw [h6]; push_cast; ring)\n```\nThen the step:\n```\n    rw [Finset.prod_range_succ]\n    -- goal: Γ z * (∏ j ∈ range (m+1), (z+↑j)) * (z + ↑(m+1))?? — prod_range_succ : ∏ j ∈ range (m+2), f j = (∏ j ∈ range (m+1), f j) * f (m+1): with succ m: range (m+1+1): f (m+1) = z + ↑(m+1).\n    -- Γ z * ((∏_{j≤m}) * (z + ↑(m+1))) = [Γ z * ∏_{j≤m}] * (z + ↑(m+1)) = Γ(z+m+1) * (z+↑(m+1)) [ih hz'] \n    -- = Γ(z+↑m+1) * (z + ↑m + 1) [cast: ↑(m+1) = ↑m+1] = Γ((z+↑m+1)+1) [Gamma_add_one _ hlast] = Γ(z+↑(m+1)+1)?? target: Γ(z + ↑(m+1) + 1) — succ m's target: Gamma (z + ↑(m+1) + 1) with ↑(m+1) = Nat.cast: normalize: z + ↑(m+1) + 1 = z + ↑m + 2?? wait target of succ-case: Gamma (z + ↑(Nat.succ m) + 1) = Gamma (z + ↑(m+1) + 1). And my chain ends at Gamma (z + ↑m + 1 + 1) = Gamma (z + ↑m + 2)... hmm: Gamma_add_one (z+↑m+1) hlast : Gamma ((z+↑m+1) + 1) = (z+↑m+1) * Gamma (z+↑m+1). (z+↑m+1)+1 = z + ↑m + 2. Target: Gamma (z + ↑(m+1) + 1) = Gamma (z + (↑m+1) + 1) = Gamma (z + ↑m + 2) ✓ same after push_cast/ring. So:\n    calc Complex.Gamma z * ((∏ j ∈ Finset.range (m + 1), (z + (j : ℂ))) * (z + ((m + 1 : ℕ) : ℂ)))\n        = (Complex.Gamma z * ∏ j ∈ Finset.range (m + 1), (z + (j : ℂ))) * (z + ((m + 1 : ℕ) : ℂ)) := by ring\n      _ = Complex.Gamma (z + (m : ℂ) + 1) * (z + ((m + 1 : ℕ) : ℂ)) := by rw [ih hz']\n      _ = Complex.Gamma (z + (m : ℂ) + 1) * (z + (m : ℂ) + 1) := by push_cast; ring_nf  -- ↑(m+1) = ↑m + 1: congr 1... let me: have : ((m+1:ℕ):ℂ) = (m:ℂ)+1 := by push_cast; ring; rw [this] — direction issues; use: rw [show ((m+1:ℕ):ℂ) = (m:ℂ) + 1 by push_cast; ring]\n      _ = Complex.Gamma (z + ((m + 1 : ℕ) : ℂ) + 1) := by\n          rw [← Complex.Gamma_add_one _ hlast]  -- Gamma ((z+↑m+1)+1) = (z+↑m+1) * Gamma(z+↑m+1): ← direction rewrites (z+↑m+1)*Γ(z+↑m+1) → Γ(z+↑m+1+1): then show the args equal: z+↑m+1+1 = z+↑(m+1)+1: congr 1; push_cast; ring\n```\nHmm getting fiddly with the cast/ring bridges. Alternative formulation avoiding +1's: state as Gamma z * ∏ j ∈ range (n+1), (z + j) = Gamma (z + (n+1 : ℕ))?? The +1's are unavoidable (Gamma_add_one). Let me define the target with (n : ℝ)-style: Gamma (z + (n:ℂ) + 1). OK.\n\nActually cleaner: state as `Complex.Gamma z * ∏ j ∈ Finset.range n, (z + (j:ℂ)) = Complex.Gamma (z + (n:ℂ))` — with product over range n (j = 0..n−1) and target z + n: n=0: Γ z * ∏ j ∈ range 0 = Γ z = Γ (z + 0) ✓ trivially (empty product, no side conditions!). Step to n+1: Γ z * ∏_{j<n+1} = Γ z * ∏_{j<n} * (z+n) = Γ(z+n)*(z+n) [IH needs ∀ k < n... wait side conditions: for the step Gamma_add_one (z+n) needs z+n ≠ 0: side condition z ≠ −n i.e. k = n: so hypotheses ∀ k : ℕ, k < n → z ≠ −k... for the LAST step need k = n... Let me re-derive: with product over range n (j ≤ n−1) targeting Γ(z+n): induction on n: base n=0: Γ z * 1 = Γ z ✓ no conditions. Step n → n+1: Γ z * ∏_{j<n+1}(z+j) = Γ z * ∏_{j<n}(z+j) * (z+n) = Γ(z+n)·(z+n) [IH with hypotheses ∀ k < n] = Γ(z+n+1) [Gamma_add_one (z+n) (h : z+n ≠ 0)] — needs z ≠ −n = the k = n hypothesis. So hypotheses: ∀ k : ℕ, k < n + 1 → ... — with < n+1 i.e. k ≤ n: for the full statement `∀ k : ℕ, k < n → z ≠ -(k:ℂ)` hmm at step we need k < n+1 ⟹ the last k = n. So: statement: ∀ k < n, z ≠ −k ⟹ Γ z * ∏_{j ∈ range n} (z+j) = Γ (z + n). At the induction step (n → n+1) with hypothesis ∀ k < n+1: IH applies with ∀ k < n (⊂); the final mult needs z ≠ −n = hypothesis k = n < n+1 ✓. \n\nThis formulation is cleaner (empty-product base, no +1 targets). The application: ∏ j ∈ range (n+1), (s/2 + j) = Q_n(s)·(s/2+n) with Q_n := ∏ j ∈ range n (s/2+j) ✓ prod_range_succ. And Γ(s/2)·[Q_n·(s/2+n)] = Γ(s/2 + (n+1))... wait: with the product over range (n+1) and target Γ(s/2 + (n+1)): apply the lemma with n := n+1: Γ(s/2)·∏_{j<n+1}(s/2+j) = Γ(s/2 + ↑(n+1)) — and ↑(n+1) = ↑n + 1 ✓. Side conditions ∀ k < n+1, s/2 ≠ −↑k ✓ (ball argument).\n\nGood:\n```\ntheorem Complex.Gamma_mul_prod (z : ℂ) (n : ℕ) (hz : ∀ k : ℕ, k < n → z ≠ -(k : ℂ)) :\n    Complex.Gamma z * ∏ j ∈ Finset.range n, (z + (j : ℂ)) = Complex.Gamma (z + (n : ℂ)) := by\n  induction n with\n  | zero => simp\n  | succ m ih =>\n    have hz' : ∀ k : ℕ, k < m → z ≠ -(k : ℂ) := fun k hk => hz k (hk.trans (Nat.lt_succ_self m))\n    have hlast : z + (m : ℂ) ≠ 0 := by\n      intro hzero\n      exact hz m (Nat.lt_succ_self m) (by rw [hzero]; simp)  -- z = -↑m: from z + ↑m = 0: eq_neg_of_add_eq_zero_left hzero : z = -↑m ✓ direct\n    rw [Finset.prod_range_succ]\n    calc Complex.Gamma z * (∏ j ∈ Finset.range m, (z + (j : ℂ))) * (z + (m : ℂ))\n        = (Complex.Gamma z * ∏ j ∈ Finset.range m, (z + (j : ℂ))) * (z + (m : ℂ)) := by ring\n      _ = Complex.Gamma (z + (m : ℂ)) * (z + (m : ℂ)) := by rw [ih hz']\n      _ = Complex.Gamma (z + ((m + 1 : ℕ) : ℂ)) := by\n          rw [show z + ((m + 1 : ℕ) : ℂ) = (z + (m : ℂ)) + 1 by push_cast; ring,\n            Complex.Gamma_add_one _ hlast]\n    -- hmm the calc's first LHS: after rw [prod_range_succ] the goal is Γ z * (∏_{range m} * (z+↑m)) = Γ(z+↑(m+1)): my calc starts with (Γ z * ∏) * (z+↑m) — need Γ z * (∏ * (z+↑m)) = (Γ z * ∏) * (z+↑m): mul_assoc ✓ ring.\n```\nWait — after rw [Finset.prod_range_succ], the goal is `Complex.Gamma z * (∏ j ∈ Finset.range m, (z + ↑j) * (z + ↑m)) = Complex.Gamma (z + ↑(m+1))`. My calc's first line LHS `Complex.Gamma z * (∏ ...) * (z + ↑m)` — parses as (Γ z * ∏) * (z+↑m) (left-assoc *) — and the goal is Γ z * (∏ * (z+↑m)) — these differ by assoc: so start the calc from the goal's exact form: `Complex.Gamma z * ((∏ j ∈ Finset.range m, (z + (j:ℂ))) * (z + (m:ℂ)))` = step to `(Complex.Gamma z * ∏ ...) * (z + ↑m)` by ring... but wait — is the GOAL after rw the starting point of calc? The calc rewrites the goal: calc A = B := proof needs the goal to be A = target. After rw [prod_range_succ], goal: Γ z * ((∏_{range m}) * (z + ↑m)) = Γ (z + ↑(m+1)). So:\n```\n    rw [Finset.prod_range_succ]\n    calc Complex.Gamma z * ((∏ j ∈ Finset.range m, (z + (j : ℂ))) * (z + (m : ℂ)))\n        = (Complex.Gamma z * ∏ j ∈ Finset.range m, (z + (j : ℂ))) * (z + (m : ℂ)) := by ring\n      _ = Complex.Gamma (z + (m : ℂ)) * (z + (m : ℂ)) := by rw [ih hz']\n      _ = Complex.Gamma (z + ((m + 1 : ℕ) : ℂ)) := by\n          rw [show z + ((m + 1 : ℕ) : ℂ) = (z + (m : ℂ)) + 1 by push_cast; ring,\n            Complex.Gamma_add_one _ hlast]\n          ring  -- hmm after the rws: goal Γ(z+↑m+1) * (z+↑m) = (z+↑m+1) * Γ(z+↑m+1): mul_comm — wait: Gamma_add_one (z+↑m) hlast : Gamma (z+↑m + 1) = (z+↑m) * Gamma (z+↑m): the rw [← ...]?? Let me redo: goal at the last calc step: Γ(z+↑m) * (z+↑m) = Γ(z + ↑(m+1)). rw [show z + ↑(m+1) = (z+↑m)+1 ...] : RHS becomes Γ((z+↑m)+1); rw [Complex.Gamma_add_one _ hlast]: rewrites Γ((z+↑m)+1) → (z+↑m)*Γ(z+↑m): goal Γ(z+↑m)*(z+↑m) = (z+↑m)*Γ(z+↑m): mul_comm ✓ ring closes.\n```\nSo the last step: `rw [show ..., Complex.Gamma_add_one _ hlast]; ring`. Careful — after both rws the goal might be closed by ring (mul_comm) ✓; or if syntactically equal after rw, the rw auto-closes and ring errors. Use `... ; ring` and adjust if \"no goals\". Actually — after rw [Gamma_add_one], RHS = (z+↑m)*Γ(z+↑m), LHS = Γ(z+↑m)*(z+↑m): not syntactically equal ⟹ ring needed ✓.\n\nAlso hlast's closing: `exact hz m (Nat.lt_succ_self m) (by rw [hzero]; simp)` — hmm: hz m _ : z ≠ −↑m; to derive False: apply hz m (Nat.lt_succ_self m); goal z = −↑m; from hzero : z + ↑m = 0: eq_neg_of_add_eq_zero_left hzero : z = −↑m ✓ direct:\n```\n    have hlast : z + (m : ℂ) ≠ 0 := by\n      intro hzero\n      exact hz m (Nat.lt_succ_self m) (eq_neg_of_add_eq_zero_left hzero)\n```\n✓ clean. (hzero : z + ↑m = 0 — the hypothesis after intro on z + ↑m ≠ 0 ✓.)\n\nAnd the zero case: `simp` — goal: Gamma z * ∏ j ∈ range 0, (z + ↑j) = Gamma (z + ↑(0:ℕ)): prod_range_zero: ∏ = 1: Γ z * 1 = Γ z; RHS Gamma (z + ↑0): ↑0 = 0: Gamma (z + 0) = Gamma z: simp should close via prod_range_zero? simp knows Finset.prod_range_zero? `Finset.prod_range_zero : ∏ j ∈ range 0, f j = 1` ✓ simp; Nat.cast_zero, add_zero ✓. So `simp` ✓ — if not fully, `simp [Complex.Gamma_add_one]`... zero case needs no Gamma_add_one. Fine, adjust at build.\n\nNamespace: should I put it in `namespace Complex`? The theorem is about Complex.Gamma — putting `theorem Complex.Gamma_mul_prod` inside namespace NguyenRH1 gives NguyenRH1.Complex.Gamma_mul_prod — hmm, dot-notation access Complex.Gamma_mul_prod works if it's in the Complex namespace. But polluting Complex namespace from our package — the Zeta23 style: they declare in Zeta23 namespace. I'll keep it in NguyenRH1 namespace with name `Complex.Gamma_mul_prod`? That requires `namespace Complex` block. Simpler: name it `gamma_mul_prod` in NguyenRH1. OK.\n\n§2 Q and HfunT:\n```\n/-- The partial denominator product Q_n(s) = ∏_{j<n} (s/2 + j). -/\ndef trivQ (n : ℕ) (s : ℂ) : ℂ := ∏ j ∈ Finset.range n, (s / 2 + (j : ℂ))\n\ntheorem trivQ_ne_zero (n : ℕ) (hn : 1 ≤ n) {s : ℂ}\n    (hs : s ∈ Metric.ball (-2 * (n : ℂ)) 1) (hsn : s ≠ -2 * (n : ℂ)) :\n    trivQ n s ≠ 0 := by\n  unfold trivQ\n  rw [Finset.prod_ne_zero_iff]\n  intro j hj\n  rw [Finset.mem_range] at hj  -- j < n\n  -- s/2 + j ≠ 0: else s = −2j with |−2j − (−2n)| < 1, j < n ⟹ 2(n−j) ≥ 2\n  intro h\n  have h2 : s = -2 * (j : ℂ) := by\n    have h1 : s / 2 = -(j : ℂ) := by\n      have := h  -- s/2 + ↑j = 0\n      ... eq_neg_of_add_eq_zero_left h : s/2 = −↑j ✓\n    have h3 := congrArg (· * (2 : ℂ)) h1\n    rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at h3\n    rw [h3]; ring\n  rw [h2, Metric.mem_ball, dist_eq_norm] at hs\n  -- ‖−2j + 2n‖ = 2(n−j) ≥ 2 (j < n)\n  have h4 : (-2 : ℂ) * (j : ℂ) - -2 * (n : ℂ) = ((2 * (n - j : ℕ) : ℝ) : ℂ) := by\n    have hjn : j ≤ n := hj.le\n    push_cast [Nat.cast_sub hjn]?? -- −2j + 2n = 2(n−j): with Nat.cast_sub (hjn : j ≤ n): ↑(n−j) = ↑n − ↑j\n    ... \n```\nLet me write h4's proof: goal (−2:ℂ)*↑j − (−2)*↑n = ↑(2*(n−j : ℕ)... hmm let me use ℝ-intermediate: (−2)*↑j + 2*↑n = 2(↑n − ↑j) = 2·↑(n−j) [Nat.cast_sub hjn] = ↑(2(n−j)): \n```\n  have h4 : (-2 : ℂ) * (j : ℂ) - -2 * (n : ℂ) = (((2 * (n - j) : ℕ)) : ℂ) := by\n    rw [Nat.cast_sub hj.le]  -- hmm: ↑(n − j) appears only after massaging; do:\n    push_cast [Nat.cast_sub hj.le]\n    ring\n```\npush_cast with the extra lemma: `push_cast [Nat.cast_sub hj.le]` should handle: ↑(n−j) → ↑n − ↑j, then ring: −2↑j + 2↑n = 2(↑n − ↑j) ✓. But the cast chain ((2*(n−j) : ℕ):ℂ) — push_cast splits 2*(n−j): ↑2 * (↑n − ↑j) ✓ ring ✓.\nThen:\n```\n  rw [h4] at hs  -- hmm: hs : ‖(-2)*↑j − (−2)*↑n‖ < 1: rw [h4] at hs : ‖↑(2*(n−j))‖ < 1: Complex.norm_real? ((x:ℝ):ℂ) norm = |x|: but my h4 RHS is ((2*(n−j) : ℕ):ℂ) — a ℕ cast: Complex.norm_natCast? (RCLike.norm_natCast banked journal-024: norm_natCast is RCLike.norm_natCast) : ‖↑k‖ = ↑k for k : ℕ ✓\n  rw [RCLike.norm_natCast] at hs  -- hs : (↑(2*(n−j)) : ℝ) < 1\n  have h5 : (2 : ℝ) ≤ (2 * (n - j) : ℕ) := by\n    have h6 : 1 ≤ n - j := Nat.sub_pos_of_lt hj  -- hmm Nat.sub_pos_of_lt : j < n → 0 < n − j ✓\n    -- 2*(n−j) ≥ 2\n    have : 2 ≤ 2 * (n - j) := by\n      have := Nat.mul_le_mul_left 2 h6?? 2*1 ≤ 2*(n−j): Nat.mul_le_mul_left — form: 2 * 1 ≤ 2 * (n-j) via Nat.mul_le_mul_left (2) h6 : 2*1 ≤ 2*(n−j) ✓ then 2*1 = 2: rw at... \n      calc (2:ℕ) = 2 * 1 := by norm_num\n        _ ≤ 2 * (n - j) := Nat.mul_le_mul_left 2 h6\n    exact_mod_cast this\n  linarith [hs, h5]  -- 2 ≤ ↑(2(n−j)) < 1 contradiction\n```\nHmm — exact_mod_cast on (2:ℕ) ≤ 2*(n−j) to (2:ℝ) ≤ ↑(2*(n−j)) ✓.\n\nCareful with h2's derivation: from h : s/2 + ↑j = 0 (the prod factor = 0): the factor is (s/2 + (j:ℂ)): h : s/2 + ↑j = 0 ✓ (Finset.prod_ne_zero_iff gives f j ≠ 0 with f j = s/2 + ↑j — after intro h : s/2 + ↑j = 0). eq_neg_of_add_eq_zero_left h : s/2 = −↑j ✓.\n\nThen the recurrence side conditions at z = s/2: ∀ k < n+1, s/2 ≠ −↑k: same ball argument with k ≤ n (k < n+1 ⟺ k ≤ n): if s/2 = −↑k: s = −2↑k: ‖(−2↑k) − (−2↑n)‖ = 2|n−k| < 1: k ≤ n: 2(n−k) < 1: n−k ≥ 1 (k ≠ n) ⟹ ≥ 2 contra; k = n ⟹ s = −2n excluded by hsn ✓:\n```\ntheorem trivRecurrence_side (n : ℕ) {s : ℂ}\n    (hs : s ∈ Metric.ball (-2 * (n : ℂ)) 1) (hsn : s ≠ -2 * (n : ℂ)) :\n    ∀ k : ℕ, k < n + 1 → s / 2 ≠ -(k : ℂ) := by\n  intro k hk h\n  -- h : s/2 = −↑k\n  have h2 : s = -2 * (k : ℂ) := by\n    have h3 := congrArg (· * (2 : ℂ)) h\n    rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at h3\n    rw [h3]; ring\n  rw [h2, Metric.mem_ball, dist_eq_norm] at hs\n  rw [Nat.lt_succ_iff] at hk  -- k ≤ n\n  rcases eq_or_ne k n with hkn | hkn\n  · subst hkn  -- k = n: s = −2↑n = the excluded point\n    exact hsn (by rw [h2]; ring)  -- hmm: s = −2↑k with k=n substituted: −2*↑n: h2 : s = −2*↑n ✓ directly hsn h2 — after subst, h2 : s = -2 * (n:ℂ): exact hsn h2 ✓\n  · -- k < n: 2(n−k) ≥ 2\n    have hlt : k < n := lt_of_le_of_ne hk hkn\n    have h4 : (-2 : ℂ) * (k : ℂ) - -2 * (n : ℂ) = (((2 * (n - k) : ℕ)) : ℂ) := by\n      push_cast [Nat.cast_sub hk]\n      ring\n    rw [h4, RCLike.norm_natCast] at hs\n    have h5 : (2 : ℝ) ≤ ((2 * (n - k) : ℕ) : ℝ) := by\n      have h6 : 1 ≤ n - k := Nat.sub_pos_of_lt hlt\n      have h7 : (2 : ℕ) ≤ 2 * (n - k) := by\n        calc (2:ℕ) = 2 * 1 := by norm_num\n          _ ≤ 2 * (n - k) := Nat.mul_le_mul_left 2 h6\n      exact_mod_cast h7\n    linarith [hs, h5]\n```\nHmm wait — Nat.mul_le_mul_left in recent Mathlib: `Nat.mul_le_mul_left (k : ℕ) (h : m ≤ n) : k * m ≤ k * n`? or {k} implicit? The signature changed across versions: currently `Nat.mul_le_mul_left {m n : ℕ} (k : ℕ) (h : m ≤ n) : k * m ≤ k * n`? I'll adapt at build; fallback: `by have := h6; nlinarith? no — naturals: omega: 2*(n−k) ≥ 2*1 = 2: `by omega`? with h6 : 1 ≤ n − k: omega proves 2 ≤ 2*(n−k) ✓ (omega handles linear nat arithmetic with multiplication by constants ✓). Use omega — robust:\n```\n    have h7 : (2 : ℕ) ≤ 2 * (n - k) := by omega\n```\nwith h6 in context ✓.\n\nHmm wait — but is `2 * (n - k)` linear for omega? n−k is a variable-ish term; 2*(n−k) = 2·X with X ≥ 1 ⟹ ≥ 2 ✓ omega handles constant multiplication ✓.\n\nSimilarly in trivQ_ne_zero use omega.\n\nAlso the geometry in these: hs after rw [h2, Metric.mem_ball, dist_eq_norm]: ‖(−2*↑j) − (−2*↑n)‖ < 1. Note dist a b = ‖a − b‖: mem_ball: dist s (−2*↑n) < 1: dist_eq_norm : dist s c = ‖s − c‖ ✓.\n\n§2b HfunT:\n```\n/-- The cofactor at −2n: HfunT n s = 2·π^{−s/2}·Γ(s/2+n+1)/Q_n(s).\nEquals (s+2n)·ΓR(s) off the recurrence's bad set; analytic and nonzero\nat −2n (its value is 2πⁿ·1/((−1)ⁿn!) up to sign — all factors nonzero). -/\nnoncomputable def HfunT (n : ℕ) (s : ℂ) : ℂ :=\n  2 * (Real.pi : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2 + (n : ℂ) + 1) / trivQ n s\n```\nWait — the target form of the recurrence lemma: Gamma (z + (n:ℂ)) with product over range n. So Γ(s/2)·∏_{j<n+1}(s/2+j) = Γ(s/2 + ↑(n+1)). With ∏_{j<n+1} = Q_{n+1}... hold on — let me recompute the cofactor with THIS formulation: Γ(s/2)·Q_{n+1}(s) = Γ(s/2 + (n+1)) where Q_{n+1} = ∏_{j<n+1}(s/2+j) = Q_n(s)·(s/2+n). So Γ(s/2) = Γ(s/2+n+1)/(Q_n(s)·(s/2+n)) — hmm the target has z + ↑(n+1) = s/2 + (n+1) = s/2 + n + 1 ✓ same thing.\n\n(s+2n)·ΓR(s) = (s+2n)·π^{−s/2}·Γ(s/2) = (s+2n)·π^{−s/2}·Γ(s/2+n+1)/(Q_n(s)·(s/2+n)). And (s+2n)/(s/2+n) = 2. So = 2·π^{−s/2}·Γ(s/2+n+1)/Q_n(s) ✓ HfunT as defined. \n\nAnalyticity at −2n:\n```\ntheorem HfunT_analyticAt (n : ℕ) (hn : 1 ≤ n) :\n    AnalyticAt ℂ (HfunT n) (-2 * (n : ℂ)) := by\n  have hcpi : AnalyticAt ℂ (fun s : ℂ => (Real.pi : ℂ) ^ (-s / 2)) (-2 * (n : ℂ)) := by\n    -- copy ii′-4c's hcpi (exp form congr)\n    have hexp : AnalyticAt ℂ\n        (fun s : ℂ => Complex.exp ((Complex.log (Real.pi : ℂ) * (-1 / 2)) * s)) (-2 * (n : ℂ)) :=\n      (analyticAt_const.mul analyticAt_id).cexp\n    apply hexp.congr\n    filter_upwards with s\n    rw [Complex.cpow_def_of_ne_zero (by norm_num : (Real.pi : ℂ) ≠ 0)]\n    ring_nf\n  have hGamma : AnalyticAt ℂ (fun s : ℂ => Complex.Gamma (s / 2 + (n : ℂ) + 1)) (-2 * (n : ℂ)) := by\n    have hd : DifferentiableOn ℂ (fun s : ℂ => Complex.Gamma (s / 2 + (n : ℂ) + 1))\n        (Metric.ball (-2 * (n : ℂ)) (1 : ℝ)) := by\n      intro s hs\n      have hg : DifferentiableAt ℂ Complex.Gamma (s / 2 + (n : ℂ) + 1) := by\n        apply Complex.differentiableAt_Gamma\n        intro m hm\n        -- s/2 + n + 1 = −m ⟹ s = −2(n+1+m): distance ≥ 2 from −2n\n        have hs_eq : s = -2 * ((n : ℂ) + 1 + (m : ℂ)) := by linear_combination 2 * hm\n        rw [hs_eq, Metric.mem_ball, dist_eq_norm] at hs\n        have h1 : (-2 : ℂ) * ((n : ℂ) + 1 + (m : ℂ)) - -2 * (n : ℂ)\n            = -(((2 : ℝ) * (1 + m) : ℝ) : ℂ) := by push_cast; ring\n        rw [h1, norm_neg, Complex.norm_real, Real.norm_eq_abs] at hs\n        rw [abs_of_nonneg (by positivity : (0:ℝ) ≤ 2 * (1 + (m:ℝ)))] at hs\n        have hm0 : (0:ℝ) ≤ (m : ℝ) := by positivity\n        linarith\n      exact (hg.comp s (by fun_prop : DifferentiableAt ℂ (fun s : ℂ => s / 2 + (n : ℂ) + 1) s)).differentiableWithinAt\n    exact (hd.analyticOnNhd Metric.isOpen_ball) _\n      (Metric.mem_ball_self (zero_lt_one : (0:ℝ) < 1))\n  have hQ : AnalyticAt ℂ (fun s : ℂ => trivQ n s) (-2 * (n : ℂ)) := by\n    apply Finset.analyticAt_fun_prod\n    intro j _\n    exact ((differentiableAt_id.div_const 2).add_const _).analyticAt\n  have hQne : trivQ n (-2 * (n : ℂ)) ≠ 0 := by\n    unfold trivQ\n    rw [Finset.prod_ne_zero_iff]\n    intro j hj\n    rw [Finset.mem_range] at hj\n    -- at s = −2n: s/2 + j = −n + j ≠ 0 (j < n)\n    have h1 : (-2 * (n : ℂ)) / 2 + (j : ℂ) = -((n : ℂ) - (j : ℂ)) := by push_cast; ring\n    rw [h1]\n    -- −(↑n − ↑j) ≠ 0 ⟺ ↑n ≠ ↑j: n ≠ j ✓ (j < n)\n    rw [ne_eq, neg_eq_zero, sub_eq_zero]  -- ↑n = ↑j\n    -- n ≠ j since j < n\n    have h2 : (n : ℂ) ≠ (j : ℂ) := by\n      intro h3\n      have : n = j := by exact_mod_cast h3  -- hmm direction: (↑n = ↑j) → n = j: Nat.cast_injective — exact_mod_cast handles\n      omega\n    exact h2\n  exact ((analyticAt_const.mul hcpi).mul hGamma).div hQ hQne\n```\nHmm — `Finset.analyticAt_fun_prod` signature: (from line 1196) `theorem Finset.analyticAt_fun_prod {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] ... (h : ∀ i ∈ s, AnalyticAt 𝕜 (f i) x) : AnalyticAt 𝕜 (fun x => ∏ i ∈ s, f i x) x`? — I'll trust and adapt. Note the factor fun s => s/2 + ↑j differentiable: differentiableAt_id.div_const 2 : DifferentiableAt ℂ (fun s => s/2) s? `DifferentiableAt.div_const (hf : DifferentiableAt 𝕜 f x) (c : 𝕜') : DifferentiableAt 𝕜 (fun x => f x / c) x`? hmm — div_const for 𝕜'-valued division — for ℂ → ℂ: DifferentiableAt.div_const (hf : DifferentiableAt ℂ f x) (c : ℂ) ✓ I think exists. Then .add_const (↑j) ✓ `DifferentiableAt.add_const (hf) (c)` ✓.\n\nWait — the h1 computation in hQne: (−2↑n)/2 + ↑j = −↑n + ↑j = −(↑n − ↑j): push_cast; ring ✓. Then rw [h1]: goal −(↑n − ↑j) ≠ 0. rw [ne_eq, neg_eq_zero, sub_eq_zero]: goal becomes ↑n = ↑j → False... careful: ne_eq : a ≠ b ↔ ¬(a = b); neg_eq_zero : −a = 0 ↔ a = 0; sub_eq_zero : a − b = 0 ↔ a = b. After the three rews: goal ¬ (↑n = ↑j)?? no — goal was −(↑n−↑j) ≠ 0: ne_eq unfolds ≠ to ¬ =; neg_eq_zero: −X = 0 ↔ X = 0 rewrites the inner: ¬(↑n − ↑j = 0); sub_eq_zero: ¬(↑n = ↑j). Then intro h3; exact_mod_cast... h3 : (↑n:ℂ) = ↑j: n = j by exact_mod_cast (Nat.cast_injective) — hmm exact_mod_cast h3 : n = j works ✓ then omega with hj : j < n... wait hj is in context ✓. Actually simpler: `exact_mod_cast (ne_of_gt hj)` : (n:ℂ) ≠ ↑j — hmm: n ≠ j from j < n: ne_of_gt hj : n ≠ j ✓ then cast: (h : n ≠ j) : (n:ℂ) ≠ (j:ℂ) by exact_mod_cast h ✓:\n```\n    exact_mod_cast (ne_of_gt hj)  -- goal (n:ℂ) ≠ (j:ℂ)? after the rews the goal is ¬(↑n = ↑j) = (↑n ≠ ↑j) ✓\n```\nHmm — but after rw [ne_eq, ...] the goal is ¬(↑n = ↑j); exact_mod_cast (ne_of_gt hj) : the term has type n ≠ j — needed (↑n:ℂ) ≠ ↑j: exact_mod_cast normalizes casts — should work: `exact_mod_cast (ne_of_gt hj)` where the goal ¬(↑n = ↑j) — ne_of_gt hj : n ≠ j = ¬(n = j): exact_mod_cast bridges the cast equality ✓.\n\nHmm wait — actually the rewrite chain: `rw [ne_eq, neg_eq_zero, sub_eq_zero]` — rw with iff-rewrites works on Prop goals ✓. But `neg_eq_zero : -a = 0 ↔ a = 0` — rw in a ¬ goal: the ¬(−X = 0): rw [neg_eq_zero] rewrites the equation −X = 0 inside: ¬(X = 0) ✓ works under ¬.\n\n§3 HfunT value nonzero:\n```\ntheorem HfunT_ne_zero (n : ℕ) (hn : 1 ≤ n) : HfunT n (-2 * (n : ℂ)) ≠ 0 := by\n  unfold HfunT\n  apply div_ne_zero\n  · -- numerator: 2 * π^(−(−2n)/2) * Γ(−n + n + 1) = 2 * π^n * Γ(1) = 2πⁿ ≠ 0\n    have h1 : (-(-2 * (n : ℂ)) / 2) = (n : ℂ) := by ring  -- −(−2n)/2 = n: ring? −(−2*↑n)/2 = 2↑n/2 = ↑n: field... `ring` handles division by literal 2 ✓ probably; else field_simp\n    rw [h1]  -- rewrites the exponent −s/2 at s = −2n... the term is (π:ℂ)^(−(−2*↑n)/2): h1's LHS must match the displayed term — the function 2 * π^(−s/2) * Γ(s/2+↑n+1) at s = −2↑n: components: −(−2↑n)/2 and (−2↑n)/2 + ↑n + 1. h1 handles the first. For the Gamma arg: (−2↑n)/2 + ↑n + 1 = 1: \n    have h2 : (-2 * (n : ℂ)) / 2 + (n : ℂ) + 1 = 1 := by ring\n    rw [h2, Complex.Gamma_one, mul_one]\n    -- now: 2 * (π:ℂ)^(↑n) ≠ 0\n    apply mul_ne_zero (by norm_num : (2 : ℂ) ≠ 0)\n    -- (π:ℂ)^(↑n) with ↑n : ℂ nat-cast — cpow with a nat-cast exponent = π^n: `Complex.cpow_natCast`? : x ^ (↑n : ℂ) = x ^ n ✓ exists I believe\n    rw [Complex.cpow_natCast]  -- (π:ℂ)^n\n    exact pow_ne_zero n (by exact_mod_cast Real.pi_ne_zero)\n  · exact trivQ_ne_zero_at_center...  -- the Q value at −2n ≠ 0: that's hQne from the analyticity proof — factor it out as its own theorem trivQ_center_ne_zero\n```\nLet me factor `trivQ_center_ne_zero (n : ℕ) (hn : 1 ≤ n)? : trivQ n (−2*↑n) ≠ 0` — actually hn not needed for that (j < n ⟹ −n+j ≠ 0 ✓ any n ≥ 1... for n = 0 the product is empty = 1 ≠ 0 ✓ actually any n works). Keep hn for consistency but drop if unused — actually just don't require it: trivQ_center_ne_zero (n : ℕ) : trivQ n (−2*↑n) ≠ 0. Wait for n=0: trivQ 0 s = 1 ≠ 0 ✓ (empty prod) — the proof via prod_ne_zero_iff handles: no j ∈ range 0 ✓. OK no hn needed.\n\nAnd h1/h2: the terms inside HfunT's unfold: `2 * (Real.pi:ℂ)^(-(-2*↑n)/2) * Complex.Gamma ((-2*↑n)/2 + ↑n + 1)` — hmm the exponent is `-(−2*↑n)/2`: parses as (−(−2*↑n))/2 = −(−2↑n)/2... note `-s / 2` with s = −2↑n: -(−2↑n)/2 — unary minus then divide: (−(−2↑n))/2 = (2↑n)/2 = ↑n ✓ `ring` should do (division by numeral is ring-normalizable ✓).\nh2: (−2↑n)/2 + ↑n + 1 = 1: −↑n + ↑n + 1 = 1 ✓ ring.\nBUT the rw [h1] needs the pattern `-(−2*↑n)/2` to appear — after `unfold HfunT`, the goal is `2 * (π:ℂ)^(-(−2*↑n)/2) * Γ((−2*↑n)/2 + ↑n + 1) / trivQ n (−2*↑n) ≠ 0`. My h1's LHS: -(-2 * (n:ℂ)) / 2 — should match syntactically (both `Neg.neg (HMul.hMul (-2) ↑n) / 2`?) — the unfolded term: (-s / 2) with s := -2 * ↑n: substitution gives -(-2 * ↑n) / 2 ✓. I wrote h1 as `(-(-2 * (n : ℂ)) / 2) = (n : ℂ)` ✓. And `Complex.cpow_natCast : x ^ (↑n : ℂ) = x ^ n`? — check name: `Complex.cpow_natCast (x : ℂ) (n : ℕ) : x ^ (↑n : ℂ) = x ^ n`? I think `Complex.cpow_natCast` exists ✓ (maybe `cpow_natCast` root). Build will tell.\n\nHmm wait — one subtlety: after `apply div_ne_zero`, two goals: numerator ≠ 0 and trivQ ≠ 0 — the order: div_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a/b ≠ 0 — apply div_ne_zero leaves goals a ≠ 0 and b ≠ 0 in order ✓.\n\n§4 the punctured identity:\n```\ntheorem HfunT_eq (n : ℕ) (hn : 1 ≤ n) {s : ℂ}\n    (hs : s ∈ Metric.ball (-2 * (n : ℂ)) 1) (hsn : s ≠ -2 * (n : ℂ)) :\n    (s + 2 * (n : ℂ)) * Complex.Gammaℝ s = HfunT n s := by\n  -- side conditions for the recurrence at z = s/2\n  have hside : ∀ k : ℕ, k < n + 1 → s / 2 ≠ -(k : ℂ) := trivRecurrence_side n hs hsn\n  have hQne : trivQ n s ≠ 0 := trivQ_ne_zero n hn hs hsn\n  have hrec := Complex.Gamma_mul_prod (s / 2) (n + 1) hside  -- Γ(s/2) * ∏_{j<n+1}(s/2+j) = Γ(s/2 + ↑(n+1))\n  rw [Finset.prod_range_succ] at hrec  -- Γ(s/2) * (Q_n * (s/2 + ↑n)) = Γ(s/2 + ↑(n+1))\n  -- Γ(s/2) = Γ(s/2+n+1) / (Q_n * (s/2+n))\n  have hsn2 : s / 2 + (n : ℂ) ≠ 0 := by\n    intro h\n    exact hside n (Nat.lt_succ_self n) (eq_neg_of_add_eq_zero_left h)\n  have hGamma : Complex.Gamma (s / 2)\n      = Complex.Gamma (s / 2 + (n : ℂ) + 1) / (trivQ n s * (s / 2 + (n : ℂ))) := by\n    -- from hrec: Γ(s/2) * (Q * (s/2+n)) = Γ(s/2 + ↑(n+1)): divide by (Q*(s/2+n)) ≠ 0\n    have hne : trivQ n s * (s / 2 + (n : ℂ)) ≠ 0 := mul_ne_zero hQne hsn2\n    -- Γ(s/2+↑(n+1)) = Γ(s/2+↑n+1): cast\n    have hcast : s / 2 + ((n + 1 : ℕ) : ℂ) = s / 2 + (n : ℂ) + 1 := by push_cast; ring\n    rw [hcast] at hrec\n    exact (eq_div_iff hne).mpr hrec  -- hmm: eq_div_iff (hc : c ≠ 0) : a = b/c ↔ a * c = b: hrec : Γ(s/2) * (Q*(..)) = Γ(..): so a := Γ(s/2), c := Q*(s/2+n), b := Γ(s/2+n+1): (eq_div_iff hne).mpr hrec : Γ(s/2) = Γ(..)/(Q*(..)) ✓ — but hrec's product form: Γ(s/2) * (Q_n * (s/2+↑n)): my hrec after prod_range_succ: Γ(s/2) * (∏_{range n} * (s/2+↑n)) — and trivQ n s = ∏_{range n}: the forms match? trivQ is a def — unfold: hrec has ∏ j ∈ Finset.range n, (s/2 + ↑j) — trivQ n s unfolds to exactly that ✓ but syntactically hrec shows the product un-unfolded. For the rw/eq_div_iff matching I need them syntactically equal: `show` or `rw [trivQ]`-unfold in hrec... Let me insert: have hrec' : ... with trivQ — via `show`: \n    Actually: unfold trivQ at * or change. Use: have hQu : trivQ n s = ∏ j ∈ Finset.range n, (s / 2 + (j : ℂ)) := rfl (def unfolds by rfl ✓). Then rw [hQu] in the goal-with-trivQ... Manage at build.\n  -- assemble\n  rw [Complex.Gammaℝ_def, hGamma]  -- (s + 2n) * (π^(−s/2) * Γ(s/2)) — wait: (s+2n)*ΓR s = (s+2n)*π^{−s/2}*Γ(s/2): rw [Gammaℝ_def] : goal (s+2↑n) * (π^(−s/2) * Γ(s/2)) = HfunT n s: then rw [hGamma]: substitutes Γ(s/2): \n  unfold HfunT\n  -- goal: (s+2↑n) * (π^(−s/2) * (Γ(s/2+n+1)/(Q*(s/2+↑n)))) = 2 * π^(−s/2) * Γ(s/2+↑n+1) / Q\n  field_simp [hQne, hsn2, cpow_ne_zero...]  -- needs (π:ℂ)^(−s/2) ≠ 0 for field_simp? only if it appears in denominators — it doesn't. field_simp [hQne, hsn2]\n  ring\n```\nCheck the algebra: LHS = (s+2n)·π^{−s/2}·Γrec/(Q·(s/2+n)); RHS = 2π^{−s/2}Γrec/Q. Ratio: (s+2n)/(s/2+n) = 2 ✓ and Q/(Q·(s/2+n)) ... LHS = π^{−s/2}Γrec/Q · (s+2n)/(s/2+n) = π^{−s/2}Γrec/Q · 2 ✓. field_simp [hQne, hsn2] then ring — the remaining identity after clearing denominators: (s+2n)·(π·Γ)·Q·... hmm field_simp clears: LHS·(Q·(s/2+n))·Q vs RHS·... it should reduce to (s+2n)·X = 2·(s/2+n)·X-ish: ring needs the π^{−s/2} and Γ factors to cancel — they will (common factors). Risk: field_simp might need (π:ℂ)^(−s/2) ≠ 0 if it ends up in a denominator — it's not. OK.\n\n§5 the main theorem:\n```\ntheorem zeroMult_neg_two_mul (n : ℕ) (hn : 1 ≤ n) :\n    zeroMult (-2 * (n : ℂ)) = 1 := by\n  have hH_an : AnalyticAt ℂ (HfunT n) (-2 * (n : ℂ)) := HfunT_analyticAt n hn\n  have hH_ne : HfunT n (-2 * (n : ℂ)) ≠ 0 := HfunT_ne_zero n hn\n  have hΛ_an : AnalyticAt ℂ completedRiemannZeta (-2 * (n : ℂ)) := by\n    have hd : DifferentiableOn ℂ completedRiemannZeta (Metric.ball (-2 * (n : ℂ)) 1) := by\n      intro s hs\n      have hs0 : s ≠ 0 := by\n        rintro h\n        rw [h, Metric.mem_ball, dist_eq_norm] at hs\n        -- ‖0 − (−2n)‖ = 2n ≥ 2 > 1\n        have h1 : ((0 : ℂ) - -2 * (n : ℂ)) = ((2 * n : ℕ) : ℂ) := by push_cast; ring\n        rw [h1, RCLike.norm_natCast] at hs\n        have h2 : (2:ℝ) ≤ ((2 * n : ℕ) : ℝ) := by\n          have h3 : (2:ℕ) ≤ 2 * n := by omega\n          exact_mod_cast h3\n        linarith [hs, h2]\n      have hs1 : s ≠ 1 := by\n        rintro h\n        rw [h, Metric.mem_ball, dist_eq_norm] at hs\n        -- ‖1 + 2n‖ = 2n+1 ≥ 3 > 1\n        have h1 : ((1 : ℂ) - -2 * (n : ℂ)) = (((2 * n + 1 : ℕ)) : ℂ) := by push_cast; ring\n        rw [h1, RCLike.norm_natCast] at hs\n        have h2 : (3:ℝ) ≤ ((2 * n + 1 : ℕ) : ℝ) := by\n          have h3 : (3:ℕ) ≤ 2 * n + 1 := by omega\n          exact_mod_cast h3\n        linarith [hs, h2]\n      exact (differentiableAt_completedZeta hs0 hs1).differentiableWithinAt\n    exact (hd.analyticOnNhd Metric.isOpen_ball) _ (Metric.mem_ball_self (zero_lt_one : (0:ℝ) < 1))\n  have hΛ_ne : completedRiemannZeta (-2 * (n : ℂ)) ≠ 0 := by\n    have hΓR : Complex.Gammaℝ (1 + 2 * (n : ℂ)) ≠ 0 :=\n      Complex.Gammaℝ_ne_zero_of_re_pos (by\n        have : (1 + 2 * (n : ℂ)).re = 1 + 2 * (n : ℝ) := by\n          simp [Complex.add_re, Complex.mul_re, Complex.one_re]  -- needs natCast re: push_cast? simp [Complex.add_re, Complex.one_re, Complex.natCast_re, Complex.mul_re, Complex.ofNat_re...]\n        rw [this]; positivity)  -- 1 + 2n > 0 ✓ positivity handles with n cast nonneg? positivity proves 0 < 1 + 2*↑n ✓\n    have hζ : riemannZeta (1 + 2 * (n : ℂ)) ≠ 0 :=\n      riemannZeta_ne_zero_of_one_lt_re (by\n        have : (1 + 2 * (n : ℂ)).re = 1 + 2 * (n : ℝ) := by simp [...]\n        rw [this]\n        have : (1:ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n        linarith)\n    have hΛ1 : completedRiemannZeta (1 + 2 * (n : ℂ)) ≠ 0 := by\n      rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul (by\n        intro h\n        have := congrArg Complex.re h\n        simp [Complex.add_re, ...] at this  -- re(1+2n) = 0 contra\n        ...)] hmm — 1+2↑n ≠ 0: re = 1+2n ≥ 3 > 0: \n        ...\n      exact mul_ne_zero hΓR hζ\n    have hfe : completedRiemannZeta (-2 * (n : ℂ)) = completedRiemannZeta (1 + 2 * (n : ℂ)) := by\n      have h := completedRiemannZeta_one_sub (-2 * (n : ℂ))\n      -- h : Λ (1 − (−2n)) = Λ (−2n): 1 − (−2n) = 1 + 2n\n      rw [show (1 : ℂ) - -2 * (n : ℂ) = 1 + 2 * (n : ℂ) by ring] at h\n      exact h.symm\n    rw [hfe]\n    exact hΛ1\n  -- G := Λ / HfunT n\n  have hG_an : AnalyticAt ℂ (fun s => completedRiemannZeta s / HfunT n s) (-2 * (n : ℂ)) :=\n    hΛ_an.div hH_an hH_ne\n  have hG_ne : completedRiemannZeta (-2 * (n : ℂ)) / HfunT n (-2 * (n : ℂ)) ≠ 0 :=\n    div_ne_zero hΛ_ne hH_ne\n  have hEv : ∀ᶠ s in 𝓝 (-2 * (n : ℂ)),\n      riemannZeta s = (s - -2 * (n : ℂ)) ^ 1 • (completedRiemannZeta s / HfunT n s) := by\n    have hHne_ev : ∀ᶠ s in 𝓝 (-2 * (n : ℂ)), HfunT n s ≠ 0 :=\n      hH_an.continuousAt.eventually_ne hH_ne\n    filter_upwards [Metric.ball_mem_nhds _ (zero_lt_one : (0:ℝ) < 1), hHne_ev] with s hs1 hHne\n    by_cases hs : s = -2 * (n : ℂ)\n    · subst hs\n      have hz0 : riemannZeta (-2 * (n : ℂ)) = 0 := by\n        have h := riemannZeta_neg_two_mul_nat_add_one (n - 1)\n        -- h : ζ(−2 * ((n−1)+1)) = 0: (n−1)+1 = n\n        rw [Nat.sub_add_cancel hn] at h  -- h : ζ(−2 * ↑n) = 0 — careful the cast: −2 * (↑(n−1)+1 : ℂ): after Nat.sub_add_cancel: ↑(n−1)+1 → ↑n: the cast: riemannZeta_neg_two_mul_nat_add_one's arg: -2 * ((n - 1 : ℕ) + 1 : ℂ)?? the lemma: riemannZeta (-2 * (n + 1)) with (n+1 : ℕ) cast to ℂ: so h : riemannZeta (-2 * (((n−1 : ℕ) + 1 : ℕ) : ℂ)) = 0: rw [Nat.sub_add_cancel hn] at h rewrites ((n−1)+1 : ℕ) → n inside ✓ then h : ζ(−2 * (↑n : ℂ)) = 0 ✓ exact h.\n        exact h\n      rw [hz0]\n      simp\n    · -- s ≠ −2n in the ball\n      have hs0 : s ≠ 0 := by\n        rintro h\n        rw [h, Metric.mem_ball, dist_eq_norm] at hs1\n        have h1 : ((0 : ℂ) - -2 * (n : ℂ)) = ((2 * n : ℕ) : ℂ) := by push_cast; ring\n        rw [h1, RCLike.norm_natCast] at hs1\n        have h2 : (2:ℝ) ≤ ((2 * n : ℕ) : ℝ) := by have h3 : (2:ℕ) ≤ 2*n := by omega; exact_mod_cast h3\n        linarith [hs1, h2]\n      have hΓR : Complex.Gammaℝ s ≠ 0 := by\n        rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]\n        rintro ⟨m, hm⟩\n        -- s = −2m in the ball ⟹ m = n (geometry) ⟹ s = −2n contra hs\n        rw [hm, Metric.mem_ball, dist_eq_norm] at hs1\n        -- ‖−2m + 2n‖ = 2|n − m| < 1 ⟹ m = n\n        by_cases hmn : m ≤ n\n        · have h4 : (-2 : ℂ) * (m : ℂ) - -2 * (n : ℂ) = (((2 * (n - m) : ℕ)) : ℂ) := by\n            push_cast [Nat.cast_sub hmn]\n            ring\n          rw [h4, RCLike.norm_natCast] at hs1\n          by_cases hmn' : m = n\n          · subst hmn'\n            exact hs hm  -- hm : s = −2*↑n — wait after subst m = n: hm : s = −2*↑n: exact hs hm ✓\n          · have hlt : m < n := lt_of_le_of_ne hmn hmn'\n            have h5 : (2:ℝ) ≤ ((2 * (n - m) : ℕ) : ℝ) := by\n              have h6 : (1:ℕ) ≤ n - m := Nat.sub_pos_of_lt hlt\n              have h7 : (2:ℕ) ≤ 2 * (n - m) := by omega\n              exact_mod_cast h7\n            linarith [hs1, h5]\n        · -- m > n: ‖·‖ = 2(m−n) ≥ 2\n          push Not at hmn  -- n < m\n          have h4 : (-2 : ℂ) * (m : ℂ) - -2 * (n : ℂ) = -(((2 * (m - n) : ℕ)) : ℂ) := by\n            push_cast [Nat.cast_sub hmn.le]\n            ring\n          rw [h4, norm_neg, RCLike.norm_natCast] at hs1\n          have h5 : (2:ℝ) ≤ ((2 * (m - n) : ℕ) : ℝ) := by\n            have h6 : (1:ℕ) ≤ m - n := Nat.sub_pos_of_lt hmn\n            have h7 : (2:ℕ) ≤ 2 * (m - n) := by omega\n            exact_mod_cast h7\n          linarith [hs1, h5]\n      have hΛ := RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hΓR\n      have hH : (s + 2 * (n : ℂ)) * Complex.Gammaℝ s = HfunT n s := HfunT_eq n hn hs1 hs\n      have hsn2n : s - -2 * (n : ℂ) = s + 2 * (n : ℂ) := by ring\n      rw [pow_one, smul_eq_mul, hsn2n]\n      have hz : riemannZeta s = completedRiemannZeta s / Complex.Gammaℝ s := by\n        rw [hΛ, mul_div_cancel_left₀ _ hΓR]\n      rw [hz, ← mul_div_assoc, div_eq_div_iff hΓR hHne, ← hH]\n      ring\n  have hRHS_an : AnalyticAt ℂ\n      (fun s => (s - -2 * (n : ℂ)) ^ 1 • (completedRiemannZeta s / HfunT n s)) (-2 * (n : ℂ)) :=\n    ((analyticAt_id.sub analyticAt_const).pow 1).smul hG_an\n  have hzeta_an : AnalyticAt ℂ riemannZeta (-2 * (n : ℂ)) := hRHS_an.congr (EventuallyEq.symm hEv)\n  have horder : analyticOrderAt riemannZeta (-2 * (n : ℂ)) = 1 :=\n    (hzeta_an.analyticOrderAt_eq_natCast).mpr\n      ⟨fun s => completedRiemannZeta s / HfunT n s, hG_an, hG_ne, hEv⟩\n  rw [zeroMult, horder]\n  exact ENat.toNat_one\n```\nWait — one thing in hEv: at the by_cases subst point: `rw [hz0]; simp` — goal after subst: riemannZeta (−2↑n) = ((−2↑n) − −(−2↑n))^1 • (Λ/HfunT)(−2↑n): LHS = 0 (hz0); RHS = 0^1 • ... = 0: rw [hz0]: goal 0 = ((−2↑n) − −(−2↑n))^1 • G: simp should close: (−2↑n) − −(−2↑n) = 0: sub_self... the term s − −2↑n with s := −2↑n: (−2↑n) − (−(−2↑n))?? careful: the expression is `(s - -2 * (n:ℂ))` = s − (−2↑n): at s = −2↑n: (−2↑n) − (−2↑n) = 0 ✓ sub_self: then 0^1 = 0 (zero_pow one_ne_zero), 0 • x = 0 ✓ simp closes ✓ (mirrors ii′-4c which did exactly `rw [hz0]; simp`).\n\nAlso — in ii′-4c's hEv they wrote `rw [pow_one, smul_eq_mul, show s - -2 = s + 2 by ring]` then the div chain — mirror ✓ (my hsn2n handles the show).\n\nOne more check — the `div_eq_div_iff` at the end: goal after rw [hz, ← mul_div_assoc]: (s+2↑n) * Λ s / ΓR s = (s+2↑n) * (Λ s / HfunT n s). Let me redo: goal is ζ s = (s+2↑n) * (Λ s / HfunT n s). rw [hz]: Λ s / ΓR s = (s+2↑n) * (Λ s / HfunT n s). ← mul_div_assoc: mul_div_assoc : a * b / c = a * (b / c): ← direction rewrites a * (b/c) → a*b/c: RHS becomes (s+2↑n) * Λ s / HfunT n s. Then div_eq_div_iff hΓR hHne : a/b = c/d ↔ a*d = c*b: goal: Λ s * HfunT n s = (s+2↑n) * Λ s * ΓR s. ← hH: hH : (s+2↑n) * ΓR s = HfunT n s: rw [← hH] rewrites HfunT n s → (s+2↑n)*ΓR s: goal: Λ s * ((s+2↑n)*ΓR s) = (s+2↑n)*Λ s*ΓR s: ring ✓. (This mirrors ii′-4c exactly ✓.)\n\n`analyticOrderAt_eq_natCast` — used in ii′-4c as `hzeta_an.analyticOrderAt_eq_natCast` with ⟨g, hg_an, hg_ne, hEv⟩ — same signature ✓.\n\n`ENat.toNat_one : (1 : ℕ∞).toNat = 1`? — used in ii′-4c ✓.\n\nThe h2 re statements: (1 + 2↑n).re = 1 + 2n: simp [Complex.add_re, Complex.one_re, Complex.mul_re, ...] — (2*↑n : ℂ).re: mul_re: 2.re*↑n.re − 2.im*↑n.im = 2*↑n.re... hmm ↑n.re = n (natCast_re ✓ simp). So simp [Complex.add_re, Complex.mul_re, Complex.natCast_re, Complex.one_re, ...] should give 1 + 2*↑n. Let me use a robust form: \n```\n        have hre : (1 + 2 * (n : ℂ)).re = 1 + 2 * (n : ℝ) := by\n          simp [Complex.add_re, Complex.mul_re, Complex.one_re, Complex.natCast_re]\n```\nhmm — mul_re : (a*b).re = a.re*b.re − a.im*b.im: with a = 2 (ofNat): ofNat_re/ofNat_im simp lemmas (Complex.ofNat_re : (ofNat n).re = ...)? The numeral 2:ℂ's re: via the earlier-established fact that simp computes numeral re/im (from LiDisc's working simp calls with `2 + t*I`) ✓. So simp [Complex.add_re, Complex.mul_re] with the default numeral simp lemmas + natCast_re ✓ should close to 1 + 2*↑n. Then positivity / linarith.\n\nAlso note hΓR : Gammaℝ (1+2↑n) ≠ 0 via Gammaℝ_ne_zero_of_re_pos — needs 0 < (1+2↑n).re ✓ positivity after hre rw (1 + 2*↑n > 0: positivity with Nat.cast_nonneg — positivity knows ↑n ≥ 0 ✓).\n\nNow, where does `zeroMult` come from — Zeta23.Statement: `def zeroMult (ρ : ℂ) : ℕ := (analyticOrderAt riemannZeta ρ).toNat` — the final `rw [zeroMult, horder]`: zeroMult is a def — `rw [zeroMult]`?? in ii′-4c they did `rw [zeroMult, horder]` — rw with a def name works if there's an equation lemma (zeroMult ρ = (analyticOrderAt riemannZeta ρ).toNat — auto-generated eq lemma? For a plain def, `rw [zeroMult]` uses the definitional unfolding via the equational lemma zeroMult.eq_def? or fails... they did it successfully so fine — mirror. It's `rw [zeroMult]` probably via `Zeta23.zeroMult` def unfold lemma — it worked in LiContour (same namespace context: LiContour has `open Zeta23`).\n\nSo my file needs `open Zeta23 Complex` + noncomputable section + namespace NguyenRH1 — mirror LiContour's header. Let me check LiContour's header opens... earlier: import Mathlib / Zeta23.Statement / Zeta23.RvM.CountByIntegral / NguyenRH1.LiSides / NguyenRH1.LiSkeleton. Let me check its open line.","signature":""},{"type":"text","text":"I have the full pattern. Checking LiContour's opens, then writing the new file."},{"type":"tool_use","id":"Bash_176","name":"Bash","input":{"command":"sed -n '29,45p' /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiContour.lean && grep -n \"open\\|^namespace\\|noncomputable\" /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiContour.lean | head -8","description":"Check LiContour header opens"},"extra_content":null}]