[{"type":"thinking","thinking":"`Finset.Ico_succ_right_eq_Icc (a b : α) : Ico a (succ b) = Icc a b` (SuccPred.lean:98, for SuccOrder) — for ℕ: `Finset.Ico_succ_right_eq_Icc 1 n : Ico 1 (n+1) = Icc 1 n` — wait succ b = b + 1? In ℕ, succ b = b+1 defeq ✓. So `Finset.Icc 1 n = Finset.Ico 1 (n + 1)` via .symm — but the succ vs +1 syntactic form: succ n vs n + 1 — for ℕ these are defeq but rw needs syntactic match — `Nat.succ_eq_add_one` simp can bridge. There's also possibly a direct `Finset.Nat.Icc_eq_Ico_succ_right`? Let me just use: \n\n```lean\nhave hIcc : Finset.Icc 1 n = Finset.Ico 1 (n + 1) := by\n  rw [← Finset.Ico_succ_right_eq_Icc, Nat.succ_eq_add_one]\n```\n`Finset.Ico_succ_right_eq_Icc 1 n : Ico 1 (succ n) = Icc 1 n` — ← direction: rewrites Icc 1 n → Ico 1 (succ n) — wait my goal: Icc 1 n = Ico 1 (n+1). rw [← Finset.Ico_succ_right_eq_Icc] rewrites Icc 1 n → Ico 1 (Nat.succ n): goal becomes Ico 1 (succ n) = Ico 1 (n+1) — then Nat.succ_eq_add_one : succ n = n + 1 — rw → Ico 1 (n+1) = Ico 1 (n+1) rfl ✓. Hmm — rw [← ...] on the goal `Icc 1 n = Ico 1 (n+1)`: pattern Icc 1 n matches LHS ✓.\n\nHmm, is Ico_succ_right_eq_Icc in Finset namespace? The file SuccPred.lean line 98 — inside `namespace Finset`? The SuccPred file — likely `namespace Finset` — the lemma name would be `Finset.Ico_succ_right_eq_Icc` ✓. If not namespaced, bare `Ico_succ_right_eq_Icc`. I'll try Finset.-prefixed; fallback bare.\n\nActually — simpler alternative avoiding Ico entirely: the Icc 1 n ↔ range n conversion via sum_bij (i ↦ i − 1) like session 016's ResW1_eq_sum did (Finset.sum_bij with i ↦ n − i). One bespoke lemma:\n\n```lean\nlemma sum_Icc_one_eq_sum_range {M : Type*} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) :\n    ∑ j ∈ Finset.Icc 1 n, f j = ∑ k ∈ Finset.range n, f (k + 1) := by\n  apply Finset.sum_bij (fun j _ => j - 1)\n  · intro j hj; rw [Finset.mem_Icc] at hj; rw [Finset.mem_range]; omega\n  · intro a ha b hb h; rw [Finset.mem_Icc] at ha hb; omega\n  · intro k hk; rw [Finset.mem_range] at hk\n    exact ⟨k + 1, by rw [Finset.mem_Icc]; omega, by omega⟩\n  · intro j hj; rw [Finset.mem_Icc] at hj\n    congr 1; omega\n```\nsum_bij arg order (session-016 note): (i, hi, i_inj, i_surj, h) ✓. This is bulletproof (no name hunting). Use this.\n\nSimilarly for Icc 2 n ↔ range (n−1) (k+2):\n```lean\nlemma sum_Icc_two_eq_sum_range {M : Type*} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) :\n    ∑ j ∈ Finset.Icc 2 n, f j = ∑ k ∈ Finset.range (n - 1), f (k + 2) := by\n  apply Finset.sum_bij (fun j _ => j - 2)\n  · intro j hj; rw [Finset.mem_Icc] at hj; rw [Finset.mem_range]; omega\n  · intro a ha b hb h; rw [Finset.mem_Icc] at ha hb; omega\n  · intro k hk; rw [Finset.mem_range] at hk\n    exact ⟨k + 2, by rw [Finset.mem_Icc]; omega, by omega⟩\n  · intro j hj; rw [Finset.mem_Icc] at hj\n    congr 1; omega\n```\n✓ (surj: k ∈ range(n−1) ⟹ k+2 ∈ Icc 2 n: k < n−1 ⟹ k+2 < n+1 ⟹ k+2 ≤ n ✓ omega; j−2 = k: j = k+2 ✓.)\n\nHmm — the sum_bij signature: does it take the function as `fun j _ => j - 1` (with the membership arg) — session 016 used `Finset.sum_bij (fun i _ => n - i)` then 4 goals: mem/inj/surj/term ✓ copy that exactly.\n\nNow — with these two conversion lemmas, everything else stays in Icc form and I convert to range only where sum_range_succ' is convenient... Actually wait — do I even need sum_range_succ'? Let me re-plan with what I have:\n\n**(i) binomial expansion** `one_sub_one_sub_pow` (polymorphic CommRing R):\n1 − (1−x)^n = Σ_{j∈Icc 1 n} (−1)^{j+1}C(n,j)x^j.\nProof: (1−x)^n = ((−x)+1)^n = Σ_{k∈range(n+1)} (−x)^k·1^{n−k}·C(n,k) [add_pow (−x) 1 n] = Σ_{k∈range(n+1)} (−x)^k·C(n,k) [simp one_pow, mul_one].\nNow: 1 − that = 1 − Σ_{range(n+1)} g k. Split off k = 0: sum_range_succ' gives Σ_{range(n+1)} g = Σ_{range n} g(k+1) + g 0 with g 0 = (−x)^0·C(n,0) = 1 ✓. So 1 − (Σ_{range n} g(k+1) + 1) = −Σ_{range n} g(k+1) = Σ_{range n} (−g(k+1)) [Finset.sum_neg_distrib... : ∑ (−f) = −∑ f — `Finset.sum_neg_distrib` ✓ exists I believe].\nPer-term: −g(k+1) = −((−x)^{k+1}·C(n,k+1)) = −(−1)^{k+1}x^{k+1}C(n,k+1) [neg_pow] = (−1)^{k+2}... — target form (−1)^{j+1}C(n,j)x^j with j = k+1: (−1)^{k+2} = (−1)^{(k+1)+1} ✓ EXACT match — no parity manipulation needed! −(−x)^{k+1}·C = −(−1)^{k+1}·x^{k+1}·C and I want (−1)^{k+2}·C·x^{k+1}: −(−1)^{k+1} = (−1)^{k+2}? (−1)^{k+2} = (−1)^{k+1}·(−1) = −(−1)^{k+1} ✓ — via pow_succ: (−1)^{k+2} = (−1)^{k+1}·(−1) ✓ = −(−1)^{k+1} by mul_neg_one ✓. So per-term: −(−1)^{k+1}·x^{k+1}·C = (−1)^{k+1}·(−1)·C·x^{k+1} — ring after rewriting with pow_succ in the right direction. \n\nStructure:\n```lean\nlemma one_sub_one_sub_pow {R : Type*} [CommRing R] (n : ℕ) (x : R) :\n    1 - (1 - x) ^ n = ∑ j ∈ Finset.Icc 1 n, (-1 : R) ^ (j + 1) * (n.choose j : R) * x ^ j := by\n  have hexp : (1 - x) ^ n = 1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R) := by\n    rw [show (1 : R) - x = -x + 1 from by ring, add_pow, Finset.sum_range_succ']\n    simp  -- goal: Σ(−x)^k·1^{n−k}·C = Σ_{range n}(−x)^{k+1}·C(k+1) + 1... \n  sorry-shaped\n```\nHmm wait — after rw [show 1−x = −x+1, add_pow, Finset.sum_range_succ']: goal (not hexp yet — let me set hexp's RHS carefully). add_pow (−x) 1 n : (−x + 1)^n = ∑ m ∈ range(n+1), (−x)^m * 1^(n−m) * n.choose m. Then Finset.sum_range_succ' : ∑_{range(n+1)} f m = (∑_{range n} f (m+1)) + f 0. f 0 = (−x)^0·1^n·C(n,0) = 1·1·1 = 1 (simp: pow_zero, one_pow, Nat.choose_zero_self, cast, mul_one...). f(m+1) = (−x)^{m+1}·1^{n−(m+1)}·C(n,m+1) — simp [one_pow, mul_one] → (−x)^{m+1}·C(n,m+1) ✓.\n\nSo after rw [...]: goal 1 − (1−x)^n = ... becomes with the expansion: the goal is hexp's: (−x+1)^n = 1 + Σ_{range n} (−x)^{k+1}·C(k+1) — wait I need to formulate hexp as `(1 - x) ^ n = 1 + ∑ k ∈ Finset.range n, (-x)^(k+1) * (n.choose (k+1) : R)`:\n```lean\n  have hexp : (1 - x) ^ n = 1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R) := by\n    rw [show (1 : R) - x = -x + 1 from by ring, add_pow, Finset.sum_range_succ']\n    rw [add_comm]  -- goal: (Σ_{range n} f(k+1)) + f 0 = 1 + Σ ... — reorder\n    congr 1\n    · simp  -- f 0 = 1\n    · apply Finset.sum_congr rfl; intro k hk; simp  -- f(k+1) = (−x)^{k+1}·C(k+1)\n  rw [hexp, add_comm 1 _]  -- 1 − (1 + S) with add_comm → 1 − (S + 1) = −S? sub_add_eq... (1 − (S+1)) = −S: `sub_add_eq_sub_sub`? then sub_self... messy. Use: have : (1:R) − (1 + S) = −S := by ring — with S free variable — ring handles (1 − (1+S) = −S) ✓ (S is an atom to ring) ✓.\n```\nHmm wait, after rw [add_comm] on hexp's goal — the goal after the first rw-chain: ∑_{range(n+1)}-expanded... hold on. hexp goal: (1−x)^n = 1 + Σ_{range n} (−x)^{k+1}C(k+1). rw [show 1−x = −x+1] : LHS → (−x+1)^n. rw [add_pow]: LHS → Σ_{m∈range(n+1)} (−x)^m·1^{n−m}·C(n,m). rw [Finset.sum_range_succ']: LHS → (∑_{k∈range n} (−x)^{k+1}·1^{n−(k+1)}·C(n,k+1)) + (−x)^0·1^n·C(n,0). Goal: that = 1 + Σ_{range n} (−x)^{k+1}·C(n,k+1). rw [add_comm]: rewrites FIRST a+b — LHS's (Σ + f0) → (f0 + Σ)?? add_comm is dangerous (rewrites first match anywhere). Better: `rw [add_comm (∑ k ∈ Finset.range n, (-x)^(k+1) * 1^(n-(k+1)) * (n.choose (k+1) : R))]` — explicit args — long. Alternative: trans + module-style:\n\nsimplest: congr-style:\n```lean\n    rw [show (1 : R) - x = -x + 1 from by ring, add_pow, Finset.sum_range_succ']\n    have h0 : (-x) ^ 0 * 1 ^ (n - 0) * (n.choose 0 : R) = 1 := by simp\n    have hrest : ∀ k ∈ Finset.range n,\n        (-x) ^ (k + 1) * 1 ^ (n - (k + 1)) * (n.choose (k + 1) : R) =\n          (-x) ^ (k + 1) * (n.choose (k + 1) : R) := fun k _ => by simp\n    rw [Finset.sum_congr rfl hrest, h0]  -- hmm sum_congr produces an eq; rw with it?\n```\nrw with Finset.sum_congr rfl hrest : (∑_{range n} LHS-form) = (∑_{range n} RHS-form) — rewrites the LHS-form sum to the RHS-form ✓ (the sum appears in the goal ✓). Then the goal: (∑_{range n} (−x)^{k+1}·C) + 1 = 1 + Σ_{range n} (−x)^{k+1}·C — add_comm instance — `exact add_comm _ _` ✓.\n\nHmm wait — h0's rewrite: the f 0 term in the goal is (−x)^0 * 1^(n−0) * (n.choose 0 : R) — sum_range_succ' produces `f 0` where f m = (−x)^m * 1^(n−m) * n.choose m — so f 0 = (−x)^0 * 1^(n−0) * ↑(n.choose 0) — beta-reduced ✓. rw [h0] rewrites that exact term ✓ (up to the beta form — hopefully matches; else simp only [pow_zero, Nat.sub_zero, one_pow, Nat.choose_zero_self, Nat.cast_one, mul_one, one_mul] first). Risk-managed: replace `rw [Finset.sum_congr rfl hrest, h0]` with `simp [Finset.sum_congr rfl hrest]`... no. Let me structure more defensively:\n\n```lean\n  have hexp : (1 - x) ^ n = 1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R) := by\n    rw [show (1 : R) - x = -x + 1 from by ring, add_pow, Finset.sum_range_succ']\n    simp [one_pow, Nat.choose_zero_self]  -- normalizes 1^· and choose 0\n    ring_nf  -- ? risky\n```\nHmm — after simp [one_pow, ...]: LHS: (∑_{k∈range n} (−x)^{k+1}·C(n,k+1)) + 1 — wait simp would simplify 1^(n−(k+1)) → 1 INSIDE the sum (simp works under binders ✓) and (−x)^0 → 1, 1^(n−0) → 1, choose 0 → 1... then goal: (Σ_{range n} (−x)^{k+1}·↑(C(n,k+1))) + 1·1·↑1?? — messy normalization — simp normal forms might mangle differently on both sides. The remaining goal after simp should be (Σ ...) + 1 = 1 + (Σ ...) or already closed. If simp leaves `(∑ ...) + 1 = 1 + ∑ ...`, then `ring` closes? ring treats the sum as an atom ✓ a+1 = 1+a ✓ ring closes. But if simp closed it, ring errors. Use `simp [...]` then try `ring` — the \"no goals\" issue again. Use `<;>`? No — use `first | ring | done`? Hmm. \n\nCleanest deterministic: end with `rw [add_comm]` — but the first-match risk... After the simp, the goal is `X + 1 = 1 + X` (X the sum) — rw [add_comm] rewrites the FIRST _+_ found scanning the goal — the LHS X + 1's top-level + — becomes 1 + X = 1 + X — rfl closed ✓. But if simp fully closed the goal, rw errors — ugh. To be deterministic, do the simp as `simp only [...]` (controlled, won't close the add_comm goal):\n```lean\n    simp only [pow_zero, one_pow, Nat.choose_zero_self, Nat.cast_one, mul_one, one_mul, Nat.sub_zero]\n    rw [add_comm]\n```\nAfter simp only: LHS sum terms: (−x)^{k+1}·1·C → (−x)^{k+1}·C (mul_one) — wait the term is (−x)^{k+1} * 1^{n−(k+1)} * C — one_pow rewrites 1^{n−(k+1)} → 1, then mul_one: (−x)^{k+1}·1·C → (−x)^{k+1}·C ✓; f0: (−x)^0·1^{n−0}·C(n,0): pow_zero → 1·1^{n−0}·C, one_pow → 1·1·C, Nat.choose_zero_self → C(n,0) = 1 → casts, one_mul/mul_one → 1 ✓. Goal: (∑_{k∈range n} (−x)^{k+1}·↑C(n,k+1)) + 1 = 1 + ∑ k∈range n, (−x)^{k+1}·↑(n.choose(k+1)) — rw [add_comm] — first +: LHS's ✓ → 1 + Σ = 1 + Σ rfl ✓. Deterministic ✓. (One risk: simp only might also rewrite inside the RHS sum's (−x)^{k+1}·↑(n.choose (k+1)) — no applicable lemmas there except... none of the listed match ✓.)\n\nThen the main proof continues:\n```lean\n  rw [hexp]  -- goal: 1 − (1 + S) = ∑_{Icc 1 n} (−1)^{j+1}C(n,j)x^j  where S := ∑_{range n} (−x)^{k+1}C(k+1)\n  have hsub : (1 : R) - (1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R)) =\n      ∑ k ∈ Finset.range n, -((-x) ^ (k + 1) * (n.choose (k + 1) : R)) := by\n    rw [Finset.sum_neg_distrib]  -- wait direction: Finset.sum_neg_distrib : ∑ −f = −∑ f? then goal 1 − (1+S) = −S needs: have : 1 − (1+S) = −S by ring — ring with S atom ✓\n    ...\n```\nLet me restructure:\n```lean\n  rw [hexp]\n  have hsub : (1 : R) - (1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R)) =\n      ∑ k ∈ Finset.range n, -((-x) ^ (k + 1) * (n.choose (k + 1) : R)) := by\n    have h : (1 : R) - (1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R)) =\n        -(∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R)) := by ring\n    rw [h, Finset.sum_neg_distrib]  -- hmm Finset.sum_neg_distrib : ∑ i, −f i = −∑ i, f i — rewriting −∑ → ∑ −: ← direction: rw [← Finset.sum_neg_distrib]\n```\nh via ring: 1 − (1 + S) = −S ✓ ring (S atom) ✓. Then rw [h]: goal RHS-ish... the goal after rw [hexp] is 1 − (1 + S) = ∑_{Icc 1 n} ... — rw [h]: LHS → −S. Then rw [← Finset.sum_neg_distrib]: −S → ∑ −(term) ✓. Now goal: ∑_{k∈range n} −((−x)^{k+1}·C(n,k+1)) = ∑_{j∈Icc 1 n} (−1)^{j+1}·C(n,j)·x^j.\nConvert RHS to range: sum_Icc_one_eq_sum_range n f with f j := (−1)^{j+1}·C(n,j)·x^j: ∑_{Icc 1 n} f j = ∑_{k∈range n} f(k+1) — rw [sum_Icc_one_eq_sum_range]: goal's RHS → ∑_{k∈range n} (−1)^{(k+1)+1}·C(n,k+1)·x^{k+1} ✓. Then Finset.sum_congr rfl: per-term: −((−x)^{k+1}·C) = (−1)^{(k+1)+1}·C·x^{k+1}:\n```lean\n  apply Finset.sum_congr rfl\n  intro k hk\n  rw [neg_pow]  -- (−x)^{k+1} → (−1)^{k+1}·x^{k+1}\n  -- goal: −((−1)^{k+1}·x^{k+1}·C) = (−1)^{(k+1)+1}·C·x^{k+1}\n  rw [pow_succ]  -- (−1)^{(k+1)+1} → (−1)^{k+1}·(−1)^1?? pow_succ : a^{n+1} = a^n·a — (−1)^{k+1+1} → (−1)^{k+1}·(−1) ✓\n  ring\n```\nWait — pow_succ on (−1)^(k+1+1): gives (−1)^{k+1}·(−1)^1 — (−1)^1 = −1 needs pow_one... `pow_succ : a ^ (n + 1) = a ^ n * a` — with exponent (k+1)+1: rewrites to (−1)^{k+1}·(−1) ✓ (the trailing a^1 → a is automatic in the lemma form a^n * a ✓). Then ring: −((−1)^{k+1}·x^{k+1}·C) = (−1)^{k+1}·(−1)·C·x^{k+1} ✓ ring closes (treats (−1)^{k+1}, x^{k+1}, C as atoms) ✓.\n\nFinset.sum_neg_distrib — exact name: `Finset.sum_neg_distrib : ∑ i ∈ s, −f i = −(∑ i ∈ s, f i)` ✓ I'm confident (standard). So ← direction: −∑ → ∑ − ✓.\n\n**The h⁺ expansion lemma** (for ii):\n```lean\nlemma sInfty_summand_eq (n : ℕ) (hn : 1 ≤ n) (m : {m : ℕ // Odd m ∧ 3 ≤ m}) :\n    ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) =\n      ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j := by\n  have h1 := one_sub_one_sub_pow (R := ℝ) n (1 / (m : ℝ))\n  -- 1 − (1−1/m)^n = Σ_{Icc 1 n} (−1)^{j+1}C(n,j)(1/m)^j\n  -- so (1−1/m)^n − 1 + n/m = −Σ_{Icc 1 n} ... + n/m = Σ_{Icc 1 n} (−1)^j C (1/m)^j + n/m\n  -- peel j=1: term = (−1)^1 C(n,1)(1/m) = −n/m\n  ...\n```\nFrom one_sub_one_sub_pow: (1−1/m)^n − 1 = −Σ_{j∈Icc 1 n} (−1)^{j+1}C(n,j)(1/m)^j = Σ_{Icc 1 n} (−1)^j C(n,j)(1/m)^j. So LHS = Σ_{Icc 1 n} g j + n/m with g j := (−1)^j C(n,j)(1/m)^j; g 1 = (−1)·C(n,1)·(1/m) = −n·(1/m) = −n/m. Peel: Σ_{Icc 1 n} g = g 1 + Σ_{Icc 2 n} g (needs the peel lemma). Then LHS = −n/m + Σ_{Icc 2 n} g + n/m = Σ_{Icc 2 n} g ✓ ring.\n\nThe peel lemma:\n```lean\nlemma sum_Icc_one_eq_add_sum_Icc_two {M : Type*} [AddCommMonoid M] (n : ℕ) (hn : 1 ≤ n) (f : ℕ → M) :\n    ∑ j ∈ Finset.Icc 1 n, f j = f 1 + ∑ j ∈ Finset.Icc 2 n, f j\n```\nProof options: (a) via range conversions + sum_range_succ': \n∑_{Icc 1 n} f = ∑_{k∈range n} f(k+1) [sum_Icc_one_eq_sum_range] = (∑_{k∈range(n−1)} f(k+2)) + f 1 [sum_range_succ' with range n = range((n−1)+1) — n ≥ 1: n − 1 + 1 = n — need the rewrite: `Nat.sub_add_cancel hn : n − 1 + 1 = n` — sum_range_succ' (f∘·+1) (n−1): ∑_{k∈range((n−1)+1)} f(k+1) = (∑_{k∈range(n−1)} f(k+1+1)) + f(0+1) — then range((n−1)+1) = range n via Nat.sub_add_cancel hn rewrite] = ∑_{Icc 2 n} f + f 1 [sum_Icc_two_eq_sum_range] = f 1 + ∑ [add_comm].\n(b) via Icc/Ico erasure lemmas.\nOption (a) with my bespoke conversions — deterministic. Let me write it:\n```lean\nlemma sum_Icc_one_eq_add_sum_Icc_two {M : Type*} [AddCommMonoid M] (n : ℕ) (hn : 1 ≤ n)\n    (f : ℕ → M) :\n    ∑ j ∈ Finset.Icc 1 n, f j = f 1 + ∑ j ∈ Finset.Icc 2 n, f j := by\n  rw [sum_Icc_one_eq_sum_range n f, sum_Icc_two_eq_sum_range n f]\n  have hn' : n - 1 + 1 = n := Nat.sub_add_cancel hn\n  have h := Finset.sum_range_succ' (fun k => f (k + 1)) (n - 1)\n  rw [hn'] at h\n  -- h : ∑ k ∈ range n, f (k+1) = (∑ k ∈ range (n−1), f (k+1+1)) + f (0+1)\n  rw [h]\n  -- goal: (∑ k ∈ range (n−1), f (k+1+1)) + f (0+1) = f 1 + ∑ k ∈ range (n−1), f (k+2)\n  have h2 : ∀ k : ℕ, f (k + 1 + 1) = f (k + 2) := fun k => by ring_nf  -- k+1+1 = k+2: congr; omega\n  rw [Finset.sum_congr rfl (fun k _ => h2 k)]\n  -- f (0+1) = f 1\n  have : f (0 + 1) = f 1 := by norm_num  -- 0+1 = 1: congr... use congr 1; norm_num? or `show f 1 = f 1`... \n  rw [this]  -- hmm the term f (0+1) in goal — rewrite\n  exact add_comm _ _\n```\nHmm wait — after rw [sum_Icc_one_eq_sum_range n f, sum_Icc_two_eq_sum_range n f] the goal is: ∑_{k∈range n} f(k+1) = f 1 + ∑_{k∈range(n−1)} f(k+2). Then rw [h] (h : ∑_{range n} f(k+1) = (∑_{range(n−1)} f(k+1+1)) + f(0+1)) — LHS rewritten ✓. Then congr-normalizations: f(k+1+1) = f(k+2) — inside a sum, use sum_congr ✓; f(0+1) = f 1: `show f (0+1) = f 1`— just `norm_num`?? f is opaque — 0+1 = 1 by norm_num then congr — `congr 1` turns f (0+1) = f 1 into 0+1 = 1, closed by norm_num? `congr 1` might give f = f and 0+1 = 1: then `norm_num` on the second... Actually simplest: `have : (0 : ℕ) + 1 = 1 := rfl` — 0+1 = 1 is rfl in ℕ ✓ so f (0+1) is DEFEQ f 1 — no rewrite needed! Lean handles during exact add_comm _ _? The goal after sum_congr: f (0+1) + Σ... wait order: after rw [h]: goal ((∑_{range(n−1)} f(k+1+1)) + f (0+1)) = f 1 + ∑_{k∈range(n−1)} f(k+2). After sum_congr rfl h2-ish rewrite: (Σ f(k+2)) + f(0+1) = f 1 + Σ f(k+2). f(0+1) defeq f 1 — add_comm _ _ : a + b = b + a with a := Σ, b := f(0+1) — the RHS has f 1 — defeq f(0+1) — exact add_comm _ _ typechecks by defeq ✓.\n\nHmm — actually (k + 1 + 1 : ℕ) vs (k + 2): k+1+1 is HAdd (HAdd k 1) 1; k+2 is HAdd k 2 — defeq but not syntactic — the h2 congr fix handles ✓. Also (0+1) vs 1: defeq ✓ (Nat.reduceAdd... 0+1 = Nat.succ 0 = 1 ✓ rfl).\n\nActually — sum_range_succ' for ℕ addition: (fun k => f (k + 1)) (k+1)... the function in h is fun k => f (k+1), so the terms are f ((k+1)+1) = f (k+1+1) ✓ as I wrote.\n\n**The alternating binomial lemma:**\n```lean\nlemma sum_Icc_two_neg_one_choose (n : ℕ) (hn : 1 ≤ n) :\n    ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) = (n : ℝ) - 1 := by\n  have h0 : (0 : ℝ) = ∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * (n.choose k : ℝ) := by\n    have h := add_pow (-1 : ℝ) 1 n  -- (−1+1)^n = Σ (−1)^k·1^{n−k}·C\n    rw [neg_add_cancel...]  -- −1 + 1 = 0: `neg_add_cancel : -a + a = 0` — hmm −1+1: `add_neg_cancel`? (−1)+1 = 0: `neg_add_cancel : -a + a = 0` ✓ wait: -a + a — with a := 1: −1 + 1 = 0 ✓ neg_add_cancel? hmm: `neg_add_cancel : -a + a = 0` — yes.\n    hmm h : (-1 + 1)^n = Σ... rw [neg_add_cancel] at h — wait (−1:ℝ)+1 = 0 — `neg_add_cancel : -a + a = 0` has form −a + a — our term is (−1) + 1 ✓ matches with a := 1? −a := −1 means a := 1 ✓ then a = 1 ✓ so neg_add_cancel : (−1:ℝ) + 1 = 0 ✓.\n    rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h  -- h : 0 = Σ (−1)^k·1^{n−k}·C\n    rw [h]\n    apply Finset.sum_congr rfl; intro k hk; simp\n  -- peel 0 and 1\n  rw [Finset.sum_range_succ', ...] at h0 ...\n```\nLet me restructure: h0 : (0:ℝ) = Σ_{k∈range(n+1)} (−1)^k·C(n,k). Peel k=0: sum_range_succ': Σ_{range(n+1)} g = Σ_{range n} g(k+1) + g 0; g 0 = 1. Peel again on Σ_{range n} g(k+1) (n ≥ 1): sum_range_succ' (fun k => g(k+1)) (n−1) with range((n−1)+1) = range n: = Σ_{range(n−1)} g(k+2) + g 1; g 1 = −n. So 0 = Σ_{range(n−1)} g(k+2) + (−n) + 1. And Σ_{Icc 2 n} g = Σ_{range(n−1)} g(k+2) [sum_Icc_two_eq_sum_range — wait direction: ∑_{Icc 2 n} f j = ∑_{k∈range(n−1)} f(k+2) ✓]. So Σ_{Icc 2 n} = n − 1 ✓ (from 0 = X − n + 1 ⟹ X = n − 1 ✓ linarith/ring).\n\nCareful with g 1: g 1 = (−1)^1·C(n,1) = −1·n = −n ✓ (pow_one, Nat.choose_one_right : n.choose 1 = n ✓, cast).\n\nAssembly in Lean:\n```lean\nlemma sum_Icc_two_neg_one_choose (n : ℕ) (hn : 1 ≤ n) :\n    ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) = (n : ℝ) - 1 := by\n  have h0 : (0 : ℝ) = ∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * (n.choose k : ℝ) := by\n    have h := add_pow (-1 : ℝ) (1 : ℝ) n\n    rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h\n    rw [h]\n    apply Finset.sum_congr rfl\n    intro k hk\n    simp\n  -- h0 : 0 = Σ_{range(n+1)} (−1)^k·C\n  rw [Finset.sum_range_succ'] at h0\n  -- h0 : 0 = (∑_{range n} (−1)^{k+1}·C(k+1)) + (−1)^0·C(n,0)\n  have hn' : n - 1 + 1 = n := Nat.sub_add_cancel hn\n  have h1 := Finset.sum_range_succ' (fun k => (-1 : ℝ) ^ (k + 1) * (n.choose (k + 1) : ℝ)) (n - 1)\n  rw [hn'] at h1\n  rw [h1] at h0\n  -- h0 : 0 = ((∑_{range(n−1)} (−1)^{k+1+1}·C(k+2)) + (−1)^1·C(n,1)) + 1-ish\n  rw [sum_Icc_two_eq_sum_range n (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ))]\n  -- goal: ∑_{k∈range(n−1)} (−1)^{k+2}·C(k+2) = n − 1\n  ...\n```\nThis is getting intricate with the normalization of (−1)^0·C(n,0) → 1 and (−1)^1·C(n,1) → −n and the k+1+1 → k+2 congrs. Manageable — let me simplify by doing all normalization via simp at h0:\n\nAfter rw [Finset.sum_range_succ'] at h0 and rw [h1] at h0: h0 : 0 = ((∑_{k∈range(n−1)} (−1)^{k+1+1}·C(n,k+1+1)) + (−1)^{0+1}·C(n,0+1)) + (−1)^0·C(n,0).\nsimp at h0: (−1)^0 → 1, C(n,0) → 1 (Nat.choose_zero_right? — `Nat.choose_zero_right : n.choose 0 = 1` ✓), so the f0 term → 1. (−1)^{0+1}·C(n,0+1): 0+1 → 1 (norm_num inside? simp's arithmetic on Nat literals: (0+1) → 1 via... simp might not reduce 0+1 in ℕ exponents without help — `Nat.reduceAdd` simproc ✓ simp includes it). (−1)^1 → −1 (pow_one), C(n,1) → n (Nat.choose_one_right ✓ simp lemma?), casts... `simp at h0` with default simp set should reduce the f0/f1 terms to 1 and −↑n. The big sum: (−1)^{k+1+1} — hmm exponent k+1+1 — could simp to k+2 via Nat.reduceAdd? NO — k is a variable: k+1+1 → k+2 needs semiring normalization of the exponent — simp does have `Nat.reduceAdd` for LITERALS only. k+1+1 stays. My sum_congr congr-fix needed again:\n\nPlan: after the two peels and simp [Nat.choose_zero_right, Nat.choose_one_right, pow_one, pow_zero] at h0, h0 : 0 = ((∑_{k∈range(n−1)} (−1)^{k+1+1}·↑(n.choose (k+1+1))) + −↑n) + 1 or similar. Then:\n```lean\n  have h2 : ∀ k : ℕ, (-1 : ℝ) ^ (k + 1 + 1) * (n.choose (k + 1 + 1) : ℝ) =\n      (-1 : ℝ) ^ (k + 2) * (n.choose (k + 2) : ℝ) := fun k => by ring_nf  -- k+1+1 = k+2: ring_nf proves ℕ identities? ring_nf works on ℕ exponents? k+1+1 = k+2 as ℕ: `show (k+1+1:ℕ) = k+2 from rfl`?? k+1+1 vs k+2: both are Nat.succ (Nat.succ k)? k+2 = k + 2 = HAdd k 2 — reduces to succ(succ k)? and k+1+1 = succ (succ k) — defeq ✓ rfl ✓! So: by congr 2 <;> ... — simplest: `by have : k + 1 + 1 = k + 2 := rfl; rw [this]`\n```\nk+1+1 = k+2: is it rfl? k+1 = Nat.succ k; (k+1)+1 = Nat.succ (Nat.succ k)? HAdd.hAdd (Nat.succ k) 1 — Nat addition: Nat.add (succ k) 1 = succ (Nat.add k 1) = succ (succ k) ✓ and k+2 = Nat.add k 2 = Nat.add k (succ 1) = succ (Nat.add k 1) = succ (succ k) ✓ — rfl should hold (both compute to succ (succ k) by recursion on the LITERAL). ✓ So `have hcast : k + 1 + 1 = k + 2 := rfl`.\n\nThen rewrite h0's sum via sum_congr into the k+2 form, then rw [sum_Icc_two_eq_sum_range] on the goal and linarith:\n\nh0 : 0 = (X + (−↑n)) + 1 with X := ∑_{range(n−1)} (−1)^{k+2}C(k+2) — hmm sign: g 1 = (−1)^{0+1}·C(n,0+1) = (−1)^1·C(n,1) = −1·n = −n ✓. So 0 = X − n + 1 ⟹ X = n − 1 ✓.\nGoal: ∑_{Icc 2 n} (−1)^j C(n,j) = n − 1 — rw [sum_Icc_two_eq_sum_range]: ∑_{range(n−1)} (−1)^{k+2}C(k+2) = n − 1 — same X ✓. So linarith with h0: X = n − 1 from 0 = X + (−n) + 1 — `linarith` — but X contains a cast (n:ℝ) — linarith handles ✓.\n\nHmm — this is fiddly but doable. Alternatively — INDUCTION-free slicker: use the RANGE form throughout for the alternating sum:\nActually simplest: compute Σ_{Icc 2 n} = Σ_{range(n+1)} − f 0 − f 1 via:\nΣ_{Icc 2 n} g = Σ_{range(n−1)} g(k+2) [my conversion] and Σ_{range(n+1)} g = g 0 + g 1 + Σ_{range(n−1)} g(k+2) [two peels] = 1 − n + Σ — so Σ = (n+1)-sum − 1 + n = 0 − 1 + n. Same thing. OK.\n\n**One more piece for (ii)**: the slice summability over the odd subtype:\n```lean\nlemma oddSlice_summable (j : ℕ) (hj : 2 ≤ j) :\n    Summable (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) := by\n  have hbase : Summable (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ 2) := by\n    have h := summable_one_div_nat_pow.mpr (show 1 < 2 from by norm_num)\n    exact h.subtype _  -- Summable.subtype (hf) (p) — the predicate: fun m => Odd m ∧ 3 ≤ m — the subtype in my goal is {m // Odd m ∧ 3 ≤ m} ✓ defeq {m // p m}\n  apply summable_of_nonneg_of_le (g := fun m : {m // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ 2)\n  · intro m; positivity\n  · intro m\n    -- (1/m)^j ≤ (1/m)² for j ≥ 2, m ≥ 3 (1/m ≤ 1)\n    have hm3 : 3 ≤ (m : ℝ) := by exact_mod_cast m.2.2\n    have hpos : (0 : ℝ) ≤ 1 / (m : ℝ) := by positivity  -- m ≥ 3 > 0\n    have hle1 : 1 / (m : ℝ) ≤ 1 := by\n      rw [div_le_one (by positivity : (0:ℝ) < (m:ℝ))]  -- hmm: div_le_one (h : 0 < b) : a/b ≤ 1 ↔ a ≤ b\n      linarith\n    exact pow_le_pow_right_of_le_one hpos hle1 hj  -- a^m ≤ a^n when 0≤a≤1, n≤m? name: pow_le_pow_right_of_le_one : 0 ≤ a → a ≤ 1 → m ≤ n → a^n ≤ a^m? direction! I want (1/m)^j ≤ (1/m)^2 with 2 ≤ j: pow_le_pow_right_of_le_one (h0 : 0 ≤ a) (h1 : a ≤ 1) (h : n ≤ m) : a^m ≤ a^n ✓ probably — check: for 0≤a≤1, larger exponent = smaller: a^j ≤ a^2 with 2 ≤ j ✓ so the lemma gives a^m ≤ a^n for n ≤ m — with n := 2, m := j ✓.\n  · exact hbase\n```\n- `Summable.subtype` — from Group.lean:301 (Multipliable.subtype (hf) (p : β → Prop)) — to_additive name: `Summable.subtype (hf : Summable f) (p : β → Prop) : Summable (fun x : {x // p x} => f x)` ✓. Note my function is fun m : subtype => (1/(m:ℝ))^2 — that's (fun m : ℕ => 1/(m:ℝ)^2) restricted — defeq to (fun x : {x // p x} => f x) where f := fun m => 1/(m:ℝ)^2? The subtype val coercion: (m : ℝ) for m : {m // Odd m ∧ 3 ≤ m} — coe through subtype then ℕ→ℝ — (fun x : {x // p x} => f ↑x) — with f ↑x = 1/((x:ℕ):ℝ)^2 ✓ matches my lambda (m:ℝ)^... — the coercion (m : ℝ) where m : subtype: elaborates as ((m:ℕ):ℝ) ✓ defeq ✓.\n- `summable_one_div_nat_pow : Summable (fun n => 1/(n:ℝ)^p) ↔ 1 < p` ✓ (PSeries.lean:330).\n- `summable_of_nonneg_of_le` : (hf : ∀ b, 0 ≤ f b) (hgf : ∀ b, f b ≤ g b) (hg : Summable g) : Summable f ✓ standard.\n- `pow_le_pow_right_of_le_one` — check name: I recall `pow_le_pow_right_of_le_one (h₀ : 0 ≤ a) (h₁ : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n` ✓ (Mathlib.Algebra.Order.Ring... or pow_le_pow_left₀ etc.) — verify at compile; alternatives: pow_le_pow_of_le_one.\n\n- `div_le_one (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b` ✓ standard.\n\n**The swap (ii) main proof:**\n```lean\ntheorem sInfty_eq_sum (n : ℕ) (hn : 1 ≤ n) :\n    SInfty n = ∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j := by\n  -- unfold SInfty\n  rw [SInfty]  -- (1 − a₁)n − 1 + tsum h⁺\n  -- the tsum swap\n  have hswap : (∑' m : {m : ℕ // Odd m ∧ 3 ≤ m},\n        ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))) =\n      ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (lagariasA j - 1) := by\n    rw [tsum_congr (fun m => sInfty_summand_eq n hn m)]\n    rw [Summable.tsum_finsetSum (fun j hj => ?_)]\n    · apply Finset.sum_congr rfl\n      intro j hj\n      rw [Finset.mem_Icc] at hj\n      -- ∑' m, c_j·(1/m)^j = c_j·(lagariasA j − 1)\n      have hsumm := oddSlice_summable j hj.2\n      rw [show (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (-1:ℝ)^j * (n.choose j : ℝ) * (1/(m:ℝ))^j) =\n        (fun m => ((-1:ℝ)^j * (n.choose j : ℝ)) * (1/(m:ℝ))^j) from by funext m; ring]\n      rw [tsum_mul_left]  -- ∑' c·f = c·∑'f\n      congr 1\n      -- ∑' m, (1/m)^j = lagariasA j − 1\n      have hj1 : j ≠ 1 := by omega\n      rw [lagariasA, if_neg hj1]\n      ring  -- 1 + tsum − 1 = tsum: (1 + X) − 1 = X ✓ ring\n    · -- summability of the coefficient-multiplied slice\n      rw [Finset.mem_Icc] at hj\n      exact (oddSlice_summable j hj.2).mul_left _\n  rw [hswap]\n  -- now: (1−a₁)n − 1 + Σ_{Icc 2 n} (−1)^j C (a_j − 1) = Σ_{Icc 1 n} (−1)^j C a_j\n  rw [sum_Icc_one_eq_add_sum_Icc_two n hn (fun j => (-1:ℝ)^j * (n.choose j : ℝ) * lagariasA j)]\n  -- RHS: (−1)^1 C(n,1) a₁ + Σ_{Icc 2 n} ... = −n a₁ + Σ\n  ...\n  -- algebra finish with sum_Icc_two_neg_one_choose\n```\nThe final algebra:\nLHS = (1−a₁)n − 1 + Σ_{j∈Icc 2 n} (−1)^j C_j (a_j − 1)\nRHS = (−1)^1 C(n,1) a₁ + Σ_{j∈Icc 2 n} (−1)^j C_j a_j = −n a₁ + Σ_{Icc 2 n} (−1)^j C_j a_j.\nΣ_{Icc 2 n} (−1)^j C_j (a_j − 1) = Σ (−1)^j C_j a_j − Σ (−1)^j C_j [Finset.sum_sub_distrib ✓].\nSo LHS = n − n a₁ − 1 + Σ (−1)^j C_j a_j − Σ (−1)^j C_j = n − n a₁ − 1 + Σ... − (n−1) [sum_Icc_two_neg_one_choose] = Σ... − n a₁ = RHS ✓.\n\nThe g 1 term: (−1)^1·C(n,1)·lagariasA 1 = (−1)·n·a₁ = −n a₁: lagariasA 1 = lagariasA1 (if_pos rfl ✓); C(n,1) = n (Nat.choose_one_right ✓); (−1:ℝ)^1 = −1 (pow_one ✓).\n\nStructure the ending:\n```lean\n  rw [Finset.sum_sub_distrib]  -- hmm the LHS sum is over c_j·(a_j − 1) — need per-term split first:\n```\ncareful: Σ_{Icc 2 n} (−1)^j·C·(a_j − 1) — to split: per-term (−1)^j·C·(a_j−1) = (−1)^j·C·a_j − (−1)^j·C — ring per term via sum_congr then Finset.sum_sub_distrib ✓.\n\n```lean\n  have hsplit : ∑ j ∈ Finset.Icc 2 n, (-1:ℝ)^j * (n.choose j : ℝ) * (lagariasA j - 1) =\n      ∑ j ∈ Finset.Icc 2 n, (-1:ℝ)^j * (n.choose j : ℝ) * lagariasA j -\n        ∑ j ∈ Finset.Icc 2 n, (-1:ℝ)^j * (n.choose j : ℝ) := by\n    rw [← Finset.sum_sub_distrib]\n    apply Finset.sum_congr rfl\n    intro j hj; ring\n  rw [hsplit, sum_Icc_two_neg_one_choose n hn]\n  -- the j = 1 term of the RHS\n  have h1term : (-1:ℝ)^1 * (n.choose 1 : ℝ) * lagariasA 1 = -(n : ℝ) * lagariasA1 := by\n    rw [lagariasA, if_pos rfl, pow_one, Nat.choose_one_right]\n    push_cast; ring  -- (−1)·↑n·a₁ = −(↑n·a₁) ✓ — hmm push_cast on ↑(n.choose 1): after rw [Nat.choose_one_right]: (↑(n.choose 1):ℝ) — wait the term has (n.choose 1 : ℝ) — after rw [Nat.choose_one_right]: (↑n : ℝ)? Nat.choose_one_right : n.choose 1 = n — rewriting n.choose 1 → n — the cast (↑(n.choose 1)) becomes (↑n) ✓. Then goal: −1 * ↑n * lagariasA1 = −(↑n * lagariasA1) ✓ ring.\n  rw [h1term]\n  ring\n```\nFinal goal: (1 − lagariasA1)·↑n − 1 + (Σ_{Icc 2 n} c_j a_j − (↑n − 1)) = −(↑n·lagariasA1) + Σ_{Icc 2 n} c_j a_j — ring with the sum as atom ✓.\n\nHmm wait — where does the SInfty unfolding leave the tsum term? rw [SInfty]: SInfty n → (1 − lagariasA1)*↑n − 1 + tsum(...) — SInfty is a def: `rw [SInfty]` — equation lemma SInfty.eq_def? For a plain def `SInfty n := ...`, rw [SInfty] should work (auto equation lemma) — or `show`/`unfold`. LiSkeleton line 629-631: they used `show ... ≤ SInfty n` keeping SInfty folded, and line 648 `have h4 : SInfty n = ...` — how did they unfold? Let me check line 644-660 for the unfolding method. Actually simp only [SInfty] works for defs. I'll use `show` with the unfolded form (defeq) — safest:\n`show (1 - lagariasA1) * (n : ℝ) - 1 + (∑' m : {m : ℕ // Odd m ∧ 3 ≤ m}, ((1 - 1/(m:ℝ))^n − 1 + (n:ℝ)/(m:ℝ))) = ∑ j ∈ Finset.Icc 1 n, ...` — hmm the exact def: `tsum fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => ((1 - 1 \\ (m: ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))` — note the backslash: `1 \\ (m:ℝ)` — that's the JPG: that's `\\` = `\\\\`? In the grep output \"1 \\ (m: ℝ)\" — the file likely has `1 / (m : ℝ)` (the grep display escaped?). Probably just /. I'll match exactly when I read the actual def lines.\n\nAlso — hmm, wait: is SInfty's summand `(1 - 1/(m:ℝ))^n - 1 + n/(m:ℝ)` or with n cast `(n:ℝ)/(m:ℝ)` ✓ as grepped.\n\nOne subtlety — hswap's tsum_congr: the SInfty summand is (1 − 1/(m:ℝ))^n − 1 + (n:ℝ)/(m:ℝ) — my sInfty_summand_eq states exactly this equals the Icc 2 n sum ✓.\n\nAnd tsum_congr needs the two functions equal pointwise ✓ (sInfty_summand_eq gives it).\n\n`Summable.tsum_finsetSum (hf : ∀ i ∈ s, Summable (f i)) : ∑' a, ∑ i ∈ s, f i a = ∑ i ∈ s, ∑' a, f i a` — from the LSeries usage: `Summable.tsum_finsetSum hf` where hf : ∀ i ∈ s, Summable (...) ✓.\n\n`tsum_mul_left : ∑' b, a * f b = a * ∑' b, f b` ✓ standard.\n\n**For (i) — the ℂ side:**\n\nsigmaSlice summability — mirror liSummable. Let me write:\n```lean\n/-- The j-th power-sum slice of the zeros (paired): (mult/2)((1/ρ)^j + (1/ρ̄)^j). -/\ndef sigmaSlice (j : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ : ℂ) / 2 * ((1 / (ρ : ℂ)) ^ j + (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ j)\n\n/-- σ_j: the paired power sum over the zeros (absolutely summable for j ≥ 1). -/\ndef sigmaP (j : ℕ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, sigmaSlice j ρ\n```\n\nSummability bound lemma:\n```lean\nlemma sigmaSlice_norm_le {j : ℕ} (hj : 1 ≤ j) (ρ : {ρ : ℂ // IsNontrivialZero ρ})\n    (hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖) :\n    ‖sigmaSlice j ρ‖ ≤\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n  have hz := ρ.2\n  have hre0 : 0 ≤ (ρ : ℂ).re := hz.2.1.le\n  have hre1 : (ρ : ℂ).re ≤ 1 := hz.2.2.le\n  have hcomp := normSq_gammaOf_le_mul_norm_sq (show 1 ≤ 1 from le_rfl) hre0 hre1 (by simpa using hρ)\n  -- wait normSq_gammaOf_le_mul_norm_sq (hn : 1 ≤ n) ... (hz : 2*n ≤ ‖z‖) — with n := 1: 2*1 ≤ ‖ρ‖ — my hρ : 2 ≤ ‖ρ‖ — 2*1 = 2 defeq — `by simpa using hρ` or exact hρ (2*1 reduces to 2 ✓ defeq exact works? 2 * (1:ℝ) — needs norm_num1 — (2:ℝ)*1 = 2 by mul_one — defeq ✓ probably exact hρ works; use by simpa using hρ to be safe... simpa might over-normalize ‖ρ‖ — use `by exact_mod_cast hρ`? no casts involved. `by rw [mul_one]; exact hρ`? the hypothesis is (2:ℝ)*1 ≤ ‖ρ‖ — rw [mul_one] at * — hmm it's in the ARGUMENT: normSq_gammaOf_le_mul_norm_sq (n := 1) ... hρ' where hρ' : (2:ℝ)*1 ≤ ‖(ρ:ℂ)‖ — `by simpa using hρ` ✓.\n  -- the core: ‖sigmaSlice j ρ‖ ≤ mult/‖ρ‖²\n  have hcore : ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by\n    ...\n  -- combine like liSummand_norm_le's key\n  ...\n```\n\nhcore proof:\n```lean\n    have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ\n    have hρ0 : (ρ : ℂ) ≠ 0 := norm_pos_iff.mp hz0\n    have hnorm1 : ‖(1 / ((starRingEnd ℂ) (ρ : ℂ)))‖ = 1 / ‖(ρ : ℂ)‖ := by\n      rw [norm_div, norm_one, RCLike.norm_conj]  -- ‖star ρ‖ = ‖ρ‖: RCLike.norm_conj : ‖conj z‖ = ‖z‖ — with starRingEnd ℂ ρ = conj ρ: `Complex.starRingEnd_apply` rw first or RCLike.norm_conj handles starRingEnd application? There's `RCLike.norm_conj : ‖conj z‖ = ‖z‖` and starRingEnd ℂ z is defeq conj z — the term is (starRingEnd ℂ) (ρ:ℂ) — hmm — safer: rw [show ((starRingEnd ℂ) (ρ:ℂ)) = star (ρ:ℂ) from rfl]?? starRingEnd ℂ = star — `starRingEnd_apply : starRingEnd R x = star x` ✓ simp lemma. Then norm_star : ‖star z‖ = ‖z‖ ✓ (`norm_star`).\n      rw [starRingEnd_apply, norm_div, norm_one, norm_star]\n    by_cases hj1 : j = 1\n    · subst hj1\n      -- exact real form\n      have heq : sigmaSlice 1 ρ = (zeroMult ρ : ℂ) * (((1 / (ρ : ℂ)).re) : ℂ) := by\n        rw [sigmaSlice]\n        have hconj : (1 / ((starRingEnd ℂ) (ρ : ℂ))) = (starRingEnd ℂ) (1 / (ρ : ℂ)) := by\n          rw [map_div₀, map_one]  -- star (1/ρ) = star 1/star ρ = 1/star ρ — hmm map_div₀ (starRingEnd ℂ) : star (a/b) = star a/star b — so star(1/ρ) = 1/star ρ — I need 1/(star ρ) = star (1/ρ) — that's (map_div₀ ...).symm with map_one: star(1/ρ) = (star 1)/(star ρ) = 1/(star ρ) — so 1/(star ρ) = star(1/ρ): \n          -- rw [map_div₀] on goal LHS? goal: 1/(starRingEnd ℂ ρ) = starRingEnd ℂ (1/ρ). map_div₀ rewrites starRingEnd ℂ (1/ρ) → starRingEnd ℂ 1 / starRingEnd ℂ ρ — then map_one → 1/starRingEnd ℂ ρ ✓ goal becomes 1/star ρ = 1/star ρ rfl ✓. So: rw [map_div₀, map_one] — rewrites the RHS occurrence ✓.\n        rw [hconj, pow_one, pow_one, Complex.add_conj]\n        -- (mult/2)·(2·Re(1/ρ)) = mult·Re(1/ρ): add_conj : z + conj z = ((2·z.re : ℝ):ℂ)\n        push_cast\n        ring\n      rw [heq, norm_mul, RCLike.norm_natCast, RCLike.norm_ofReal]\n      -- |mult| = mult (natcast nonneg): RCLike.norm_natCast : ‖(n:ℂ)‖ = n ✓ hmm — ‖(zeroMult ρ : ℂ)‖ = zeroMult ρ — as ℝ equality: RCLike.norm_natCast gives ‖(n:ℂ‖ = ↑n? Then:\n      have hre : ((1 / (ρ : ℂ)).re) = (ρ : ℂ).re / Complex.normSq (ρ : ℂ) := by\n        rw [one_div, Complex.inv_re]\n      rw [hre]\n      have hnn : (0 : ℝ) < Complex.normSq (ρ : ℂ) := Complex.normSq_pos.mpr hρ0\n      have habs : |(ρ : ℂ).re / Complex.normSq (ρ : ℂ)| ≤ 1 / Complex.normSq (ρ : ℂ) := by\n        rw [abs_div]\n        apply div_le_div_of_nonneg_right? — hmm div_le_div_of_nonneg_right is a ≤ b → a/c ≤ b/c for 0 < c? name: `div_le_div_of_nonneg_right (h : a ≤ b) (hc : 0 < c)? : a / c ≤ b / c`? the current name might be div_le_div_right... In recent Mathlib: `div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b` ✓ — use (div_le_div_right hnn).mpr — with |re| ≤ 1:\n        have hre1' : |(ρ : ℂ).re| ≤ 1 := abs_le.mpr ⟨hz.2.1.le, hz.2.2.le⟩\n        exact (div_le_div_right hnn).mpr hre1'  -- hmm div_le_div_right (0 < c) : a/c ≤ b/c ↔ a ≤ b ✓\n      calc (zeroMult ρ : ℝ) * |(ρ:ℂ).re / Complex.normSq (ρ:ℂ)|\n          ≤ (zeroMult ρ : ℝ) * (1 / Complex.normSq (ρ:ℂ)) :=\n            mul_le_mul_of_nonneg_left habs (Nat.cast_nonneg _)\n        _ = (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖^2 := by\n            rw [Complex.normSq_eq_norm_sq]  -- normSq ρ = ‖ρ‖² — direction: normSq_eq_norm_sq : normSq z = ‖z‖^2 ✓\n            ring  -- mult·(1/‖ρ‖²) = mult/‖ρ‖² ✓\n      -- wait the LHS after rw [norm_mul, ...] is ‖(mult:ℂ)‖·|(1/ρ).re| = mult·|...| — RCLike.norm_natCast : ‖(n:ℂ)‖ = (n:ℝ)? there's `RCLike.norm_natCast : ‖(n : R)‖ = n`? For ℂ: ‖(n:ℂ)‖ = n as ℝ ✓ (used in liSummand_norm: rw [liSummand_eq, norm_mul, RCLike.norm_natCast] ✓ same).\n    · -- j ≥ 2\n      have hj2 : 2 ≤ j := by omega\n      have htr : ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ:ℂ)‖ ^ j + 1 / ‖(ρ:ℂ)‖ ^ j) := by\n        rw [sigmaSlice]\n        have h1 : ‖((zeroMult ρ : ℂ) / 2)‖ = (zeroMult ρ : ℝ) / 2 := by\n          rw [norm_div, RCLike.norm_natCast, norm_two]  -- ‖(2:ℂ)‖ = 2: norm_two ✓? `Complex.norm_two`? RCLike.norm_ofNat? — try norm_num\n        rw [norm_mul, h1]\n        apply mul_le_mul_of_nonneg_left _ (by positivity)\n        exact norm_add_le _ _  -- hmm ‖X + Y‖ ≤ ‖X‖+‖Y‖ — with the norms computed:\n        -- need ‖(1/ρ)^j‖ = 1/‖ρ‖^j and ‖(1/star ρ)^j‖ = 1/‖ρ‖^j\n      ...\n```\nLet me structure the j ≥ 2 branch more carefully:\n```lean\n    · have hj2 : 2 ≤ j := by omega\n      have hnormρ : ‖(1 / (ρ : ℂ)) ^ j‖ = 1 / ‖(ρ : ℂ)‖ ^ j := by\n        rw [norm_pow, norm_div, norm_one]\n      have hnormρ' : ‖(1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ j‖ = 1 / ‖(ρ : ℂ)‖ ^ j := by\n        rw [norm_pow, starRingEnd_apply, norm_div, norm_one, norm_star]\n      have hcast : ‖((zeroMult ρ : ℂ) / 2)‖ = (zeroMult ρ : ℝ) / 2 := by\n        rw [norm_div, RCLike.norm_natCast]\n        norm_num  -- ‖(2:ℂ)‖ = 2\n      have h1 : ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ:ℂ)‖ ^ j + 1 / ‖(ρ:ℂ)‖ ^ j) := by\n        rw [sigmaSlice, norm_mul, hcast]\n        apply mul_le_mul_of_nonneg_left _ (by positivity : (0:ℝ) ≤ (zeroMult ρ : ℝ)/2)\n        rw [hnormρ, hnormρ']\n      -- = mult/‖ρ‖^j\n      have h2 : (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ:ℂ)‖ ^ j + 1 / ‖(ρ:ℂ)‖ ^ j) =\n          (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖ ^ j := by ring\n      -- mult/‖ρ‖^j ≤ mult/‖ρ‖² since ‖ρ‖ ≥ 2, j ≥ 2\n      have h3 : (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖ ^ j ≤ (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖ ^ 2 := by\n        have hpow : ‖(ρ:ℂ)‖ ^ 2 ≤ ‖(ρ:ℂ)‖ ^ j :=\n          pow_le_pow_right₀ (by linarith : (1:ℝ) ≤ ‖(ρ:ℂ)‖) hj2\n        -- pow_le_pow_right₀ (ha : 1 ≤ a) : m ≤ n → a^m ≤ a^n ✓\n        have h4 : 1 / ‖(ρ:ℂ)‖ ^ j ≤ 1 / ‖(ρ:ℂ)‖ ^ 2 :=\n          one_div_le_one_div_of_le (by positivity) hpow\n        -- one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1/b ≤ 1/a ✓\n        exact div_le_div_of_nonneg_right?? — mult·(1/‖ρ‖^j) ≤ mult·(1/‖ρ‖²): the forms are div: mult/‖ρ‖^j vs mult/‖ρ‖² — write as div_le_div_of_nonneg_left? name... `div_le_div_of_nonneg_left (ha : 0 ≤ a)?`... In current Mathlib: `div_le_div_of_nonneg_left (ha : 0 < a) (hb : 0 < b) (h : b ≤ c) : a / c ≤ a / b`? — names shifted in the 2024-2025 refactor: div_le_div_of_nonneg_left (ha : 0 < a) (hb : 0 < b) (hbc : b ≤ c) : a / c ≤ a / b ✓ I think. Use that or one_div forms + mul_le_mul_of_nonneg_left:\n        calc (zeroMult ρ : ℝ) / ‖(ρ:ℂ)‖ ^ j = (zeroMult ρ : ℝ) * (1 / ‖(ρ:ℂ)‖ ^ j) := by rw [div_eq_mul_one_div]... \n        simpler: rw [div_eq_mul_one_div, div_eq_mul_one_div] then mul_le_mul_of_nonneg_left h4 (Nat.cast_nonneg _)\n      rw [h2] at h1  -- h1 : ‖sigmaSlice‖ ≤ mult/‖ρ‖^j\n      exact h1.trans h3\n```\nThen combine with hcomp (1+‖γ‖² ≤ (9/4)‖ρ‖²) as in liSummand_norm_le's key:\nmult/‖ρ‖² ≤ (9/4)·mult/(1+‖γ‖²) ⟺ (mult/‖ρ‖²)·(1+‖γ‖²) ≤ (9/4)mult ⟸ (mult/‖ρ‖²)·(9/4·‖ρ‖²) = (9/4)mult ✓ — mirror liSummand_norm_le lines 271-284 with 2n² → 1:\n```lean\n  have key : (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2)\n      ≤ (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n    rw [le_div_iff₀ hg0]  -- hg0 : 0 < 1 + normSq γ\n    have hbound : (zeroMult ρ : ℝ) * (1 / ‖(ρ:ℂ)‖ ^ 2) * (1 + Complex.normSq (gammaOf (ρ:ℂ)))\n        ≤ (zeroMult ρ : ℝ) * (1 / ‖(ρ:ℂ)‖ ^ 2) * ((9/4) * ‖(ρ:ℂ)‖ ^ 2) :=\n      mul_le_mul_of_nonneg_left hcomp (by positivity)\n    have heq : (zeroMult ρ : ℝ) * (1 / ‖(ρ:ℂ)‖ ^ 2) * ((9/4) * ‖(ρ:ℂ)‖ ^ 2)\n        = (9/4) * (zeroMult ρ : ℝ) := by field_simp; ring\n    exact hbound.trans (le_of_eq heq)\n  -- hcore : ‖sigmaSlice‖ ≤ mult/‖ρ‖² = mult * (1/‖ρ‖²)\n  exact (hcore.trans key')...\n```\nWait hcore's form: mult/‖ρ‖² vs mult*(1/‖ρ‖²) — unify: state hcore as ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ:ℝ) * (1/‖(ρ:ℂ)‖^2) — div_eq_mul_one_div bridge at the end. Fine — handle in assembly.\n\nHmm — also liSummand_norm_le's target form: (9/2)·n²·mult/(1+‖γ‖²) — mine: (9/4)·mult/(1+‖γ‖²) — then the dominator D uses (9/4)·mult/(1+‖γ‖²) — hbase := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9/4) — the base function form: fun ρ => (9/4)·((mult:ℝ)/(1+normSq γ)) ✓ matches liSummable's hbase with constant (9/2)n² → (9/4).\n\nThen:\n```lean\ntheorem sigmaSlice_summable (j : ℕ) (hj : 1 ≤ j) : Summable (sigmaSlice j) := by\n  -- clone of liSummable with the fixed radius 2 and constant 9/4\n```\nfollowing liSummable's structure exactly (hbase, D, hfin with closedBall 0 2, hE, hD, Summable.of_norm_bounded).\n\nNote: liSummable's hfin used 2*n with the ball of radius 2*n; mine uses radius 2 — same argument with n := 1-ish. Actually I can just copy the block with (2:ℝ) in place of 2*n:\n```lean\n    have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}.Finite := by\n      have hcomp : IsCompact (Metric.closedBall (0 : ℂ) 2) := isCompact_closedBall _ _\n      ... (same chain with 2*n → 2)\n```\n\nThen liSummand_eq_sum_slices + liCoeff_eq_sum_sigma as planned.\n\nliSummand_eq_sum_slices:\n```lean\nlemma liSummand_eq_sum_slices (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    liSummand n ρ = ∑ j ∈ Finset.Icc 1 n, (-1:ℂ)^(j+1) * (n.choose j : ℂ) * sigmaSlice j ρ := by\n  rw [liSummand, one_sub_one_sub_pow n (1 / (ρ : ℂ)),\n    one_sub_one_sub_pow n (1 / ((starRingEnd ℂ) (ρ : ℂ)))]\n  rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]\n  apply Finset.sum_congr rfl\n  intro j hj\n  rw [sigmaSlice]\n  ring\n```\nCheck: liSummand n ρ = (mult/2)·(A + B) where A = 1−(1−x)ⁿ, B = 1−(1−y)ⁿ. After the two rewrites: A = Σ c_j x^j, B = Σ c_j y^j. Goal: (mult/2)·(Σ c_j x^j + Σ c_j y^j) = Σ_j c_j·sigmaSlice j ρ. Finset.mul_sum : a·Σ f = Σ a·f — wait I have (mult/2)·(Σ + Σ) — first rewrite the outer: hmm the structure: (mult/2) * (S1 + S2): mul_add → (mult/2)*S1 + (mult/2)*S2; then Finset.mul_sum each: Σ (mult/2)*c_j x^j + Σ (mult/2)*c_j y^j; then ← Finset.sum_add_distrib : Σ f + Σ g = Σ (f+g) ✓; then per-term: (mult/2)*(c_j x^j) + (mult/2)*(c_j y^j) = c_j * sigmaSlice j ρ = c_j·(mult/2)(x^j + y^j) ✓ ring (after rw [sigmaSlice] unfolds the def ✓ — sigmaSlice j ρ := (mult/2)*((1/ρ)^j + (1/star ρ)^j) ✓ ring closes with x, y defeq to those ✓).\n\nWait — rw order: after rw [liSummand, one_sub_one_sub_pow n x, one_sub_one_sub_pow n y]: goal (mult/2) * (Σ c_j x^j + Σ c_j y^j) = Σ c_j·sigmaSlice j ρ. rw [Finset.mul_sum] — pattern a * Σ: the outer (mult/2)*(S1+S2) is a * (sum + sum) — Finset.mul_sum's pattern: b * ∑ i ∈ s, f i — the LHS (mult/2)*(S1 + S2) — S1+S2 is not syntactically a Finset.sum (it's a sum of two sums) — no match! First need mul_add: (mult/2)*(S1+S2) = (mult/2)*S1 + (mult/2)*S2 — rw [mul_add, Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib] ✓.\n\nFinset.mul_sum : ∑ i ∈ s, f i * b?? — direction check: `Finset.mul_sum : b * ∑ i ∈ s, f i = ∑ i ∈ s, b * f i` ✓ I believe ( Finset.mul_sum : (b : M) * ∑ i ∈ s, f i = ∑ i ∈ s, b * f i). ✓\n\nThen liCoeff_eq_sum_sigma:\n```lean\ntheorem liCoeff_eq_sum_sigma (n : ℕ) :\n    liCoeff n = ∑ j ∈ Finset.Icc 1 n, (-1:ℂ)^(j+1) * (n.choose j : ℂ) * sigmaP j := by\n  unfold liCoeff sigmaP\n  rw [tsum_congr (fun ρ => liSummand_eq_sum_slices n ρ)]\n  rw [Summable.tsum_finsetSum (fun j hj => ?_)]\n  · apply Finset.sum_congr rfl\n    intro j hj\n    rw [tsum_mul_left]  -- hmm the slice: c_j·sigmaSlice j ρ — the sum over ρ: ∑' ρ, c_j·sigmaSlice j ρ = c_j·∑' σ-slice — but after unfold sigmaP, the RHS's sigmaP j is already unfolded to the tsum ✓\n  · rw [Finset.mem_Icc] at hj\n    exact (sigmaSlice_summable j hj.1).const_mul _\n```\nHmm — the coefficient: the summand after liSummand_eq_sum_slices: (−1)^{j+1}·C(n,j)·sigmaSlice j ρ — as a function of ρ: fun ρ => (−1)^{j+1}·C(n,j)·sigmaSlice j ρ — for tsum_finsetSum, f j := fun ρ => (−1)^{j+1}·C·sigmaSlice j ρ ✓ Summable via (sigmaSlice_summable j hj.1).const_mul ((−1)^{j+1}·C(n,j)) — `Summable.const_mul : Summable f → Summable (fun b => c * f b)` — my lambda is fun ρ => c·(sigmaSlice j ρ) where c := (−1)^{j+1}·C — matches fun b => c * f b ✓.\n\nThen after tsum_finsetSum: ∑' ρ, Σ_j ... = Σ_j ∑' ρ, c_j·sigmaSlice j ρ. Then per-j: ∑' ρ, c_j·sigmaSlice j ρ = c_j·sigmaP j: tsum_mul_left : ∑' b, a * f b = a * ∑' b, f b — my function: fun ρ => c_j * sigmaSlice j ρ ✓ = c_j * ∑' ρ, sigmaSlice j ρ ✓ and sigmaP j unfolds to that ✓ — since I did `unfold liCoeff sigmaP` at the start, the goal's sigmaP j is already ∑' ρ, sigmaSlice j ρ ✓ so tsum_mul_left gives exactly the goal ✓. But wait — the lambda: after liSummand_eq_sum_slices, the summand is written (−1:ℂ)^(j+1) * (n.choose j : ℂ) * sigmaSlice j ρ — left-nested (a·b)·slice — tsum_mul_left's pattern a * f b — with a := (−1)^{j+1}·C(n,j), f b := sigmaSlice j ρ ✓ the lambda fun ρ => ((−1)^{j+1}·C) * sigmaSlice j ρ — is it syntactically fun ρ => a * f ρ? The term is ((−1:ℂ)^(j+1) * (n.choose j:ℂ)) * sigmaSlice j ρ — as a lambda in ρ ✓ — tsum_mul_left expects fun b => a * f b — match a := (−1)^{j+1}*C, f := sigmaSlice j ✓ — the parse ((−1)^(j+1) * C) * slice — first *'s args: ((−1)^(j+1)*C) and slice — so the outer HDiv... outer HMul.hMul ((−1)^{j+1}·C) (sigmaSlice j ρ) ✓ matches a * (f ρ) form ✓.\n\nCareful with `unfold liCoeff sigmaP` — unfold both: liCoeff n → ∑' ρ, liSummand n ρ ✓; sigmaP j → ∑' ρ, sigmaSlice j ρ (inside the sum ✓ unfold works under binders? unfold at the goal — the sum contains sigmaP j for VARIABLE j — unfold sigmaP rewrites all sigmaP ?j occurrences ✓ should work).\n\nHmm — but `unfold liCoeff` rewrites liCoeff n — the goal's LHS — ✓.\n\n**Now, one important design review**: Do I actually need R2(i) in the ℂ form or ℝ? Downstream: Sf n = SInfty n + 1 − (liCoeff n).re — real. The crux: SInfty n + 1 − (liCoeff n).re = (ResW1 n).re — both sides ℝ. ResW1 = Σ C(n,j)·lcoeff(j−1) — ℂ. The (4.10) bridge will relate lcoeff (ℂ, but real-valued) with a_j (ℝ) and σ_j (my sigmaP — ℂ but real-valued). To keep ii′-3/6 flexible, ℂ form for (i) is right (take .re when needed; the slices are manifestly real anyway — could ADD a lemma sigmaP_real : (sigmaP j).im = 0 or sigmaP j = ((sigmaP j).re : ℂ) — the paired form: each summand (mult/2)(x^j + conj(x^j))... wait (1/star ρ)^j = star((1/ρ)^j)? map_pow + map_div₀: star((1/ρ)^j) = (star(1/ρ))^j = (1/star ρ)^j ✓ so the pair is z + star z = 2Re — real ✓. sigmaP_im_eq_zero or similar — cheap via tsum of reals... `Complex.tsum_re`? For summable ℂ families, (∑' f).re = ∑' (f.re)? There's `Complex.re_tsum`? hmm — might need summability of the re family — I have norm bounds... Let me not bother now — downstream can add when needed. Actually wait — it might be cleaner for downstream to ALSO state the ℝ version of (i): (liCoeff n).re = Σ_j (−1)^{j+1}C(n,j)·(sigmaP j).re — trivial from the ℂ version by congrArg Complex.re + push_cast through the finite sum (Complex.map_sum? re of sum = sum of re: `Complex.re_sum`? there's `map_sum` for the ring hom... Complex.re is an ℝ-linear map — `Complex.reCLM`? — `map_sum (Complex.reCLM?)`... or `Complex.re_sum : (Σ s).re = Σ (re ∘ s)`? hmm `Complex.re_sum` might exist via `map_sum (f := Complex.reAddGroupHom)`? There's `Complex.reAddGroupHom`? I recall `Complex.reCLM` (continuous linear map) and re of tsum needs care, but for FINITE sums: `map_sum` with the add-group-hom `Complex.reAddMonoidHom`? — exists? There's `Complex.reAddGroupHom : ℂ →+ ℝ`? I believe yes. map_sum ✓. So the .re version is a 2-line corollary when needed. Skip for now.)\n\nOK — now also think: does R2(i) need n ≥ 1? At n = 0: liCoeff 0 = ∑' liSummand 0 = ∑' 0 = 0 (liSummand 0 = 0-fun — from liSummable's proof: liSummand 0 = fun _ => 0 ✓ — tsum_congr + tsum_zero). RHS: Icc 1 0 = ∅ → 0 ✓. So the theorem holds at n = 0 — my proof: liSummand_eq_sum_slices at n = 0: liSummand 0 ρ = (mult/2)((1−1)+(1−1)) = 0; RHS: Σ_{Icc 1 0} = ∅ = 0 — but the PROOF route: rw [liSummand, one_sub_one_sub_pow 0 x, one_sub_one_sub_pow 0 y]: one_sub_one_sub_pow at n = 0: 1 − (1−x)^0 = 0; RHS Σ_{Icc 1 0} = 0 — the proof: hexp at n=0: (1−x)^0 = 1 + Σ_{range 0} = 1 + 0 = 1 ✓ sum_range_succ' at n = 0: range(0+1) = {0}: ∑_{range 1} f = (∑_{range 0} f(k+1)) + f 0 = 0 + f 0 ✓ fine. So one_sub_one_sub_pow holds at n = 0 ✓ no hypothesis needed ✓. Then liSummand_eq_sum_slices at n = 0: (mult/2)·(0 + 0)... the rw chain: after rewrites goal (mult/2)·(Σ_{∅} + Σ_{∅}) = Σ_{∅}: 0 = 0 — but the tactic path: mul_add, Finset.mul_sum×2, ←sum_add_distrib, sum_congr — at n=0 the sums are empty; the per-term ring never fires (no members) — Finset.sum_congr rfl with intro j hj — hj : j ∈ ∅ — the goal after intros is the term eq — wait sum_congr rfl h : Σ f = Σ g needs h : ∀ j ∈ s, f j = g j — for s = ∅ the intro still produces j with hj : j ∈ Icc 1 0 = ∅ — the ring still proves the equation (it holds for all j regardless) ✓ no case issue. And liCoeff_eq_sum_sigma at n = 0: tsum_finsetSum over s = ∅: each slice summable ✓ (hj.1 : 1 ≤ j from j ∈ Icc 1 0 = ∅ — hj is absurd but the proof still works — wait: (sigmaSlice_summable j hj.1) — hj : j ∈ Finset.Icc 1 0 — Finset.mem_Icc at hj gives 1 ≤ j ∧ j ≤ 0 — hj.1 : 1 ≤ j ✓ fine (vacuously instantiated — but Lean doesn't care, the term is constructed for any j with the hypothesis proof ✓).\n\nEdge n = 0 ✓ all good.\n\n**Now (ii)'s edge n = 1**: sInfty_eq_sum needs 1 ≤ n ✓. Check n = 1: SInfty 1 = (1−a₁)·1 − 1 + Σ_m [(1−1/m) − 1 + 1/m] = (1−a₁) − 1 + Σ 0 = −a₁. RHS: Σ_{j∈Icc 1 1} = j=1: (−1)^1·C(1,1)·a₁ = −a₁ ✓. My proof: sInfty_summand_eq at n=1: (1−1/m) − 1 + 1/m = Σ_{Icc 2 1} = ∅ = 0 ✓ — the proof: from one_sub_one_sub_pow: (1−1/m)^1 − 1 = −Σ_{Icc 1 1} g = −g 1 = −(−1)^2·C(1,1)·(1/m) = −(1/m) — wait: (1−1/m) − 1 = −1/m ✓ and −Σ_{j∈Icc 1 1} (−1)^{j+1}C(1,j)(1/m)^j = −[(−1)^2·1·(1/m)] = −1/m ✓ consistent. Then +n/m = +1/m: total 0 ✓. The peel: Σ_{Icc 1 1} g = g 1 + Σ_{Icc 2 1} = g 1 + 0 ✓ (sum_Icc_one_eq_add_sum_Icc_two n=1 hn ✓ — its proof via ranges: Icc 2 1 → range(1−1) = range 0 = ∅ ✓ sum_bij on empty ✓ fine).\n\n**Also need for (ii)**: SInfty's tsum — no summability needed (tsum_sum handles) ✓ — wait, actually tsum_finsetSum rewrites ∑' m, Σ_j slice = Σ_j ∑' m, slice — conclusion form: my hswap rewrites the tsum (which appears inside SInfty) — the equality holds regardless of the summability of the m-sum? tsum_finsetSum (hf : ∀ i ∈ s, Summable (f i)) : ∑' a, ∑ i ∈ s, f i a = ∑ i ∈ s, ∑' a, f i a — the LHS tsum EXISTS as a value (junk if not summable — but the EQUALITY holds: when all slices summable, the double is summable too and equality is genuine — Mathlib's tsum_finsetSum: does it conclude summability of the double? The lemma statement gives the tsum equality directly ✓ fine).\n\nNow — assembly of the whole file. One more check on names:\n- `Finset.sum_neg_distrib` ✓\n- `neg_pow` ✓ (Commute.lean — hmm it's `Commute.neg_pow`? line 146: `lemma neg_pow (a : R) (n : ℕ) : (-a)^n = (-1)^n * a^n` — namespace? In Mathlib/Algebra/Ring/Commute.lean — the lemma at 146 — is it inside `namespace Commute`? The file has both root and Commute-namespace lemmas... `neg_pow` at root? Let me check — there's `neg_pow : (-a) ^ n = (-1) ^ n * a ^ n` — I believe it's root-level in Mathlib.Algebra.Ring.Basic or Commute. At line 146 of Commute.lean — if it's inside namespace Commute it'd be Commute.neg_pow. Let me check quickly.\n- `pow_le_pow_right₀ (ha : 1 ≤ a) (h : m ≤ n) : a^m ≤ a^n` ✓\n- `pow_le_pow_right_of_le_one (h0 : 0 ≤ a) (h1 : a ≤ 1) (h : m ≤ n) : a^n ≤ a^m`? — need name check.\n- `one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a` ✓ used in re_li_summand_le ✓ (line 113).\n- `div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b` ✓\n- `Complex.normSq_pos : 0 < normSq z ↔ z ≠ 0` ✓\n- `Complex.normSq_eq_norm_sq : normSq z = ‖z‖^2` ✓ (used in LiSkeleton line 96).\n- `RCLike.norm_natCast` ✓ (LiSkeleton line 251).\n- `Complex.inv_re` ✓.\n- `map_div₀ (starRingEnd ℂ)`? — map_div₀ for a RingEquiv: `map_div₀ (f : R ≃+* S) (a b) : f (a/b) = f a / f b` ✓.\n- `Summable.mul_left : Summable f → Summable (fun b => c * f b)` ✓ (used in liSummable line 300: .mul_left ✓).\n- `Summable.const_mul : Summable f → Summable (fun b => c * f b)` — same as mul_left? `.mul_left` at line 300: (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9/2)*(n:ℝ)²) — so `Summable.mul_left (c) : Summable (fun b => c * f b)` ✓ — that's the name in current Mathlib: Summable.mul_left. So my `.const_mul` should be `.mul_left` ✓ adjust.\n- `tsum_mul_left : ∑' b, c * f b = c * ∑' b, f b` ✓.\n- `Summable.tsum_finsetSum` ✓.\n- `summable_of_nonneg_of_le (hf : 0 ≤ f) (hgf : f ≤ g) (hg : Summable g) : Summable f` ✓ — signature: summable_of_nonneg_of_le (hf : ∀ b, 0 ≤ f b) (hgf : ∀ b, f b ≤ g b) (hg : Summable g) ✓.\n- `Summable.subtype (hf) (p)` ✓ (from Multipliable.subtype to_additive).\n- `pow_le_pow_right_of_le_one`: verify. Alternatives: `pow_le_pow_of_le_one (h0 : 0 ≤ a) (h1 : a ≤ 1) (h : m ≤ n) : a^n ≤ a^m` — I think it's `pow_le_pow_of_le_one`. Grep.\n\nLet me also double check `Nat.choose_one_right : n.choose 1 = n` ✓ and `Nat.choose_zero_right : n.choose 0 = 1` ✓.\n\nAnd neg_pow's namespace. Grep those two.","signature":""},{"type":"text","text":"Two more name checks, then I'll write the file."},{"type":"tool_use","id":"Bash_113","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && sed -n '140,150p' Mathlib/Algebra/Ring/Commute.lean; grep -rn \"theorem pow_le_pow_of_le_one\\b\\|lemma pow_le_pow_of_le_one\\b\\|theorem pow_le_pow_right_of_le_one\\|lemma pow_le_pow_right_of_le_one\" Mathlib/Algebra/Order/ -r --include=\"*.lean\" | head -4","description":"Check neg_pow namespace and pow_le_pow names"},"extra_content":null}]