[{"type":"thinking","thinking":"I have the complete summability pattern. Key inventory:\n- `WeilEF.zero_sum_inv_sq zetaSeam : Summable (fun ρ => (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))` — used with .mul_left for constants.\n- `WeilEF.gammaOf_re / gammaOf_im` — gammaOf z has re = z.im, im = 1/2 − z.re (from the normSq computation: normSq (gammaOf z) = z.im² + (1/2 − z.re)²).\n- `IsCompact.inter_riemannZetaZeros_finite` — finite zeros in compact balls.\n- The dominator-D/if_pos/finite-support skeleton.\n\nFor the σ-slice summability, the bound I need per slice j ≥ 1, for 2 ≤ ‖ρ‖ (use the constant 2 threshold, or 2·1 with n := 1 in their lemmas):\n|sigmaSlice j ρ| ≤ (zeroMult ρ)/|ρ|² ≤ (9/4)·mult/(1+‖γ‖²).\n\nWait — normSq_gammaOf_le_mul_norm_sq with n := 1: needs 1 ≤ 1 ✓ and 2·1 ≤ ‖ρ‖ i.e. 2 ≤ ‖ρ‖ ✓ gives 1 + ‖γ‖² ≤ (9/4)‖ρ‖². So mult/‖ρ‖² ≤ (9/4)mult/(1+‖γ‖²) for ‖ρ‖ ≥ 2.\n\nAnd |sigmaSlice j ρ| ≤ mult/‖ρ‖² for 2 ≤ ‖ρ‖:\n- sigmaSlice j ρ := (mult/2)((1/ρ)^j + (1/ρ̄)^j). |sigmaSlice| ≤ (mult/2)(|1/ρ|^j + |1/ρ̄|^j) = (mult/2)·2·|ρ|^{−j} = mult·|ρ|^{−j} = mult/|ρ|^j.\n- For j = 1: mult/|ρ| — NOT ≤ mult/|ρ|² for |ρ| ≥ 2... WRONG DIRECTION: 1/|ρ| ≥ 1/|ρ|² for |ρ| ≥ 1! So the raw triangle bound fails for j = 1. USE THE PAIRED STRUCTURE: sigmaSlice 1 ρ = (mult/2)(1/ρ + 1/ρ̄) = (mult/2)·2Re(1/ρ) = mult·Re(1/ρ). Re(1/ρ) = Re(ρ̄/|ρ|²) = Re(ρ)/|ρ|² (since 1/ρ = ρ̄/|ρ|²). So |sigmaSlice 1 ρ| = mult·|Re ρ|/|ρ|² ≤ mult/|ρ|² (0 < Re ρ < 1 ⟹ |Re ρ| ≤ 1 ✓). \n- For j ≥ 2: |ρ| ≥ 2 ⟹ |ρ|^j ≥ |ρ|²·2^{j−2} ≥ |ρ|² ⟹ mult/|ρ|^j ≤ mult/|ρ|² ✓.\n\nSo uniformly: |sigmaSlice j ρ| ≤ mult/‖ρ‖² ≤ (9/4)mult/(1+‖γ‖²) for 2 ≤ ‖ρ‖, j ≥ 1. \n\nHmm wait, but for j = 1 the identity sigmaSlice 1 ρ = mult·Re(1/ρ) needs care in Lean: 1/ρ + 1/conj(ρ) = 1/ρ + conj(1/ρ) (map_inv₀: conj (1/ρ) = conj 1/conj ρ... map_inv₀ (starRingEnd ℂ) ρ : star (ρ⁻¹) = (star ρ)⁻¹ — and 1/ρ = ρ⁻¹: one_div, map_inv₀) = 2·Re(1/ρ) via Complex.add_conj : z + conj z = 2·Re z. So (mult/2)(1/ρ + 1/ρ̄) = (mult/2)·2·Re(1/ρ) = mult·Re(1/ρ) ✓.\n\nThen |Re(1/ρ)| ≤ 1/|ρ|²: Re(1/ρ) = re(ρ)/|ρ|²? 1/ρ = conj ρ/|ρ|² — in Mathlib: `Complex.inv_def`? z⁻¹ = conj z / |z|² — `Complex.inv_def : z⁻¹ = conj z / ‖z‖^2`? something like Complex.inv_def : z⁻¹ = conj z / (normSq z)? Let me check at compile: `Complex.inv_re : (z⁻¹).re = z.re / normSq z`? I recall `Complex.inv_re : (z⁻¹).re = z.re / Complex.normSq z` ✓ exists. And one_div: 1/ρ = ρ⁻¹ ✓. So Re(1/ρ) = re(ρ)/normSq(ρ), |Re(1/ρ)| = |re ρ|/normSq ρ ≤ 1/normSq ρ = 1/‖ρ‖² (normSq_eq_norm_sq ✓) with |re ρ| ≤ 1 from hz.2.2 (re < 1) and hz.2.1 (0 < re) — |re| ≤ 1 ✓.\n\nSo the summability lemma per slice:\n\n```lean\nlemma sigmaSlice_summable (j : ℕ) (hj : 1 ≤ j) : Summable (sigmaSlice j) := by\n  -- mirror liSummable with dominator (9/4)·mult/(1+‖γ‖²) for ‖ρ‖ ≥ 2\n```\n\nFollowing liSummable's skeleton exactly:\n- hbase : Summable (fun ρ => (9/4)·((mult:ℝ)/(1+normSq γ))) := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9/4)\n- D := if 2 ≤ ‖ρ‖ then dominator else ‖sigmaSlice j ρ‖\n- hfin : {ρ | ¬ (2 ≤ ‖ρ‖)}.Finite — same as liSummable's with 2·n replaced by 2: closedBall 0 2 ⋂ zeros finite. (liSummable used 2*n with n ≥ 1; here fixed 2.) The IsCompact.inter_riemannZetaZeros_finite argument identical with radius 2.\n- hE : Summable (D − base) — finite support.\n- hD : Summable D.\n- Summable.of_norm_bounded hD: ‖sigmaSlice j ρ‖ ≤ D ρ: for ‖ρ‖ ≥ 2: the bound proof (j=1 vs j≥2 split); else le_refl.\n\nThe bound lemma:\n```lean\nlemma sigmaSlice_norm_le {j : ℕ} (hj : 1 ≤ j) (ρ : {ρ // IsNontrivialZero ρ})\n    (hρ : (2:ℝ) ≤ ‖(ρ : ℂ)‖) :\n    ‖sigmaSlice j ρ‖ ≤ (9/4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ)))\n```\nProof: \n- ‖sigmaSlice j ρ‖ ≤ mult/‖ρ‖² [sub-lemma below]\n- mult/‖ρ‖² ≤ (9/4)mult/(1+‖γ‖²) via normSq_gammaOf_le_mul_norm_sq (n := 1) — like liSummand_norm_le's key with 2n² replaced by 1.\n\nSub-lemma: ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ)/‖(ρ:ℂ)‖² for 2 ≤ ‖ρ‖:\n```lean\n  have hρ0 : (ρ : ℂ) ≠ 0 := by intro h; rw [h, norm_zero] at hρ; linarith-ish\n  by_cases hj1 : j = 1\n  · -- paired exactness\n    subst hj1\n    have hconj : (1 / ((starRingEnd ℂ) (ρ:ℂ))) = (starRingEnd ℂ) (1 / (ρ:ℂ)) := by\n      rw [map_div₀, map_one]  -- wait: star (1/ρ) = star 1 / star ρ = 1/star ρ — direction: I need 1/(star ρ) = star (1/ρ): (map_div₀ (starRingEnd ℂ) ...).symm? map_div₀ : f (a/b) = f a / f b — so star (1/ρ) = star 1/star ρ = 1/star ρ — so 1/star ρ = star(1/ρ) via .symm: (map_div₀ ... ).symm with map_one simp... \n    -- sigmaSlice 1 ρ = mult · Re(1/ρ)\n    have heq : sigmaSlice 1 ρ = (zeroMult ρ : ℂ) * (((1 / (ρ:ℂ)).re) : ℂ) := by\n      rw [sigmaSlice, hconj, pow_one, pow_one]\n      rw [Complex.add_conj]  -- z + star z = 2·re z: (1/ρ) + star(1/ρ) = 2·Re(1/ρ)... add_conj : z + conj z = 2 * z.re? `Complex.add_conj : z + conj z = 2 * (z.re : ℂ)`? something like that\n      push_cast; ring-ish\n    rw [heq, norm_mul, RCLike.norm_natCast, RCLike.norm_ofReal]\n    -- |mult| · |Re(1/ρ)| = mult·|Re 1/ρ| ≤ mult/‖ρ‖²\n    have hre : ((1 / (ρ:ℂ)).re) = (ρ:ℂ).re / Complex.normSq (ρ:ℂ) := by\n      rw [one_div, Complex.inv_re]  -- Complex.inv_re : (z⁻¹).re = z.re / normSq z\n    rw [hre]\n    have habs : |(ρ:ℂ).re / Complex.normSq (ρ:ℂ)| ≤ 1 / Complex.normSq (ρ:ℂ) := by\n      rw [abs_div]\n      apply div_le_div_of_nonneg_right? ... \n      -- |re| / normSq ≤ 1/normSq since |re| ≤ 1, normSq > 0\n    -- then 1/normSq = 1/‖ρ‖² (normSq_eq_norm_sq) and mult·(...) ≤ mult/‖ρ‖²\n  · -- j ≥ 2\n    have hj2 : 2 ≤ j := by omega\n    calc ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ)/2 * (‖(1/(ρ:ℂ))^j‖ + ‖(1/star ρ)^j‖) := norm-le...\n      _ = mult / ‖ρ‖^j := ...\n      _ ≤ mult / ‖ρ‖² := ...\n```\nFor j ≥ 2: ‖(1/ρ)^j‖ = (1/‖ρ‖)^j = 1/‖ρ‖^j (norm_pow, norm_div, norm_one); ‖1/star ρ‖ = 1/‖ρ‖ (Complex.norm_conj? norm (star ρ) = ‖ρ‖ — `Complex.norm_conj`? starRingEnd norm: `RCLike.norm_conj`? There's Complex.norm_conj : ‖conj z‖ = ‖z‖ ✓). So ‖sigmaSlice‖ ≤ (mult/2)(1/‖ρ‖^j + 1/‖ρ‖^j) = mult/‖ρ‖^j. Then mult/‖ρ‖^j ≤ mult/‖ρ‖²: since ‖ρ‖ ≥ 2 ≥ 1: ‖ρ‖^j ≥ ‖ρ‖² (pow_le_pow_right₀ (by linarith: 1 ≤ ‖ρ‖) hj2... pow_le_pow_right₀ : 1 ≤ a → m ≤ n → a^m ≤ a^n ✓) then 1/‖ρ‖^j ≤ 1/‖ρ‖² (one_div_le_one_div_of_le with positivity) then mul by mult ≥ 0 ✓.\n\nNorm of sigmaSlice: sigmaSlice j ρ = (mult:ℂ)/2 * X where X = (1/ρ)^j + (1/ρ̄)^j: ‖sigmaSlice‖ = ‖(mult:ℂ)/2‖·‖X‖ = (mult/2)·‖X‖ (mult ≥ 0); ‖X‖ ≤ ‖(1/ρ)^j‖ + ‖(1/ρ̄)^j‖ (norm_add_le). So ‖sigmaSlice‖ ≤ (mult/2)(1/‖ρ‖^j + 1/‖ρ‖^j) = mult/‖ρ‖^j ✓.\n\nFor the real-valued comparison at the end: the bound is stated in ℝ with (zeroMult ρ : ℝ) — norms are ℝ ✓.\n\nNow — one design question: should sigmaSlice/sigmaP be over the SAME subtype {ρ // IsNontrivialZero ρ} ✓ yes (matches liSummand's domain).\n\nR2(i) final:\n```lean\ndef sigmaP (j : ℕ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, sigmaSlice j ρ\n\ntheorem liCoeff_eq_sum (n : ℕ) :\n    liCoeff n = ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j + 1) * (n.choose j : ℂ) * sigmaP j\n```\nProof:\n```lean\n  unfold liCoeff sigmaP\n  have h1 : ∀ ρ, liSummand n ρ = ∑ j ∈ Finset.Icc 1 n, (-1:ℂ)^(j+1) * (n.choose j : ℂ) * sigmaSlice j ρ := liSummand_eq_sum_slices n\n  rw [tsum_congr h1]  -- hmm tsum_congr : (∀ b, f b = g b) → ∑' f = ∑' g ✓\n  rw [tsum_sum (fun j hj => ?_)]  -- needs Summable (fun ρ => coeff·sigmaSlice j ρ)\n  · apply Finset.sum_congr rfl; intro j hj\n    rw [tsum_mul_left?]  -- ∑' ρ, c * sigmaSlice j ρ = c * ∑' ρ, sigmaSlice j ρ\n  · exact (sigmaSlice_summable j (by ...)).const_mul _\n```\nWait — tsum_sum gives ∑' ρ, Σ j, f j ρ = Σ j, ∑' ρ, f j ρ with f j ρ = c_j·sigmaSlice j ρ. Then each ∑' ρ, c_j·sigmaSlice j ρ = c_j·σP j via `tsum_mul_left : ∑' b, a * f b = a * ∑' b, f b` ✓. Summability: (sigmaSlice_summable j hj').const_mul c_j — `Summable.const_mul : Summable f → Summable (fun b => c * f b)` ✓.\n\nThe membership j ∈ Icc 1 n gives 1 ≤ j ✓ for sigmaSlice_summable's hypothesis.\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]  -- (mult/2)·[(1−(1−x)ⁿ) + (1−(1−y)ⁿ)], x = 1/ρ, y = 1/ρ̄\n  rw [one_sub_one_sub_pow n (1/(ρ:ℂ)), one_sub_one_sub_pow n (1/star ρ)]\n  -- (mult/2)·[Σ c_j x^j + Σ c_j y^j] = Σ c_j·(mult/2)(x^j+y^j)\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```\nwhere the coefficient structure: one_sub_one_sub_pow n x : 1 − (1−x)^n = Σ_{j ∈ Icc 1 n} (−1)^{j+1}·C(n,j)·x^j. Then (mult/2)·Σ c_j x^j = Σ (mult/2)·c_j x^j via Finset.mul_sum ✓, two of them summed: Finset.sum_add_distrib ✓, then pointwise: (mult/2)c_j x^j + (mult/2)c_j y^j = c_j·(mult/2)(x^j + y^j) = c_j·sigmaSlice j ρ — ring (sigmaSlice unfolds ✓ — need sigmaSlice's def in the ring-normalization — rw [sigmaSlice] first then ring — careful the summand target form: the goal per j: (mult/2)·(c_j x^j) + (mult/2)·(c_j y^j) = c_j·sigmaSlice j ρ — with c_j := (−1)^{j+1}·C(n,j): ring after unfolding sigmaSlice ✓).\n\none_sub_one_sub_pow:\n```lean\nlemma one_sub_one_sub_pow (n : ℕ) (x : ℂ) :\n    1 - (1 - x) ^ n = ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j + 1) * (n.choose j : ℂ) * x ^ j := by\n  have h : (1 - x) ^ n = ∑ k ∈ Finset.range (n + 1), (n.choose k : ℂ) * (-x) ^ k := by\n    rw [show (1 : ℂ) - x = 1 + (-x) from by ring, add_pow]\n    apply Finset.sum_congr rfl\n    intro k hk\n    rw [one_pow, one_mul]  -- add_pow form: 1^(n−k)·(−x)^k·C(n,k) → ...\n  -- extract k = 0\n  ...\n```\nadd_pow : (a + b)^n = ∑ k ∈ range(n+1), a^k · b^(n−k) · C(n,k)? or C(n,k)·a^k·b^(n−k)? The exact Mathlib form: `add_pow (x y : R) (n : ℕ) : (x + y)^n = ∑ k ∈ Finset.range (n+1), x^k * y^(n−k) * Nat.choose n k` — I believe it's x^k·y^(n−k)·choose. With x := 1, y := −x: 1^k·(−x)^{n−k}·C(n,k) — hmm that expands in powers (−x)^{n−k} — the wrong grading. Use (1 + (−x))^n = ((−x) + 1)^n = Σ (−x)^k·1^{n−k}·C(n,k) — set a := −x, b := 1: (−x + 1)^n = Σ_{k} (−x)^k·1^{n−k}·C(n,k) — and (−x)+1 = 1−x by ring ✓. So:\n```lean\n  have h : (1 - x) ^ n = ∑ k ∈ Finset.range (n + 1), (-x) ^ k * 1 ^ (n - k) * (n.choose k : ℂ) := add_pow (-x) 1 n\n```\nif add_pow's form is a^k·b^(n−k)·choose — need to check. Modern Mathlib: `theorem add_pow (x y : R) (n : ℕ) : (x + y) ^ n = ∑ k ∈ Finset.range (n + 1), x ^ k * y ^ (n - k) * Nat.choose n k` — I think there was a refactor; possibly `Commute.add_pow` with binomial ring... there's also `add_pow` stated via `Finset.sum_range (fun k => ...)`. I'll adapt: rw [show (1:ℂ) − x = −x + 1 from by ring]; rw [add_pow]; then simp [one_pow, mul_one] to clean 1^(n−k).\n\nThen:\nΣ_{k=0}^n (−x)^k·C(n,k) = (−x)^0·C(n,0) + Σ_{k=0}^{n−1} (−x)^{k+1}C(n,k+1) [Finset.sum_range_succ'] = 1 + Σ_{k∈range n} (−x)^{k+1}C(n,k+1).\nSo 1 − (1−x)^n = 1 − 1 − Σ... = −Σ_{k∈range n} (−x)^{k+1}C(n,k+1) = Σ_{k∈range n} (−1)^{k+2}... \n\nterm: −(−x)^{k+1}C(n,k+1) = −(−1)^{k+1}x^{k+1}C(n,k+1) = (−1)^{k+2}x^{k+1}C(n,k+1) = (−1)^k x^{k+1}C(n,k+1).\n\nTarget (Icc 1 n form): Σ_{j∈Icc 1 n} (−1)^{j+1}C(n,j)x^j = Σ_{k∈range n} (−1)^{k+2}C(n,k+1)x^{k+1} (via Finset.sum_Icc_eq_sum_range with m=1: ∑_{j∈Icc 1 n} f j = ∑_{k∈range (n+1−1)} f (k+1) = ∑_{k∈range n} f(k+1) ✓).\n\n(−1)^{(k+1)+1} = (−1)^{k+2} = (−1)^k·(−1)² = (−1)^k ✓ consistent with the expansion's (−1)^{k+2}.\n\nSo:\n```lean\nlemma one_sub_one_sub_pow (n : ℕ) (x : ℂ) :\n    1 - (1 - x) ^ n = ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j + 1) * (n.choose j : ℂ) * x ^ j := by\n  have h1 : (1 : ℂ) - x = -x + 1 := by ring\n  rw [h1, add_pow]\n  rw [Finset.sum_range_succ']  -- hmm direction: sum_range_succ' : ∑ k ∈ range(n+1), f k = f 0 + ∑ k ∈ range n, f (k+1)\n  -- LHS: 1 − [f 0 + Σ_{range n} f(k+1)] where f k = (−x)^k·1^{n−k}·C(n,k)\n  simp [...]\n  ...\n```\nLet me structure it as a calc:\n```lean\n  have hexp : (1 - x) ^ n = 1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : ℂ) := by\n    rw [h1, add_pow, Finset.sum_range_succ']\n    simp  -- f 0 = (−x)^0·1^n·C(n,0) = 1; the rest: 1^(n−(k+1)) = 1\n  -- 1 − (1 + S) = −S\n  rw [hexp]\n  have h2 : (1 : ℂ) - (1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : ℂ))\n      = ∑ k ∈ Finset.range n, (-1 : ℂ) ^ k * (n.choose (k + 1) : ℂ) * x ^ (k + 1) := by\n    rw [add_sub_cancel_left]  -- 1 − (1 + S) = −S? add_sub_cancel_left : a + b − a = b — wrong form: 1 − (1 + S): sub_eq... use: rw [sub_add_eq...]; simpler: have : (1:ℂ) − (1 + S) = −S := by ring\n    ...\n```\nHmm getting complicated; do it directly:\n```lean\n  rw [hexp]\n  have hneg : (1 : ℂ) - (1 + S) = -S := by ring  -- with S set\n```\nMaybe cleanest with `set S := ∑ k ∈ Finset.range n, (-x)^(k+1)*(n.choose (k+1):ℂ)`:\n1 − (1 + S) = −S (ring). −S = Σ −(term) (Finset.sum_neg_distrib? `Finset.sum_neg_distrib : ∑ i, −f i = −∑ i, f i` — hmm direction; `Finset.sum_neg_distrib : (∑ i ∈ s, −f i) = −(∑ i ∈ s, f i)`? there's Finset.sum_neg_distrib ✓). Then term: −((−x)^{k+1}·C(n,k+1)) = (−1)^k·C(n,k+1)·x^{k+1}: (−x)^{k+1} = (−1)^{k+1}x^{k+1} (neg_pow); −(−1)^{k+1} = (−1)^{k+2} = (−1)^k ((−1)^{k+2} = (−1)^k·(−1)² = (−1)^k — in Lean: pow_add, (−1:ℂ)² = 1 simp). So per-term: −((−x)^{k+1}·C) = (−1)^k·C·x^{k+1} — ring_nf can do: −(−x)^{k+1}·C(n,k+1) vs (−1)^k·C(n,k+1)·x^{k+1}: (−x)^{k+1} = (−1)^{k+1}·x^{k+1}: is this ring-closable? (−x)^{k+1} — ring normal forms handle (−x)^m by expanding parity? ring doesn't split on parity of VARIABLE exponent k... (−x)^{k+1} is not a ring-normal-form reduction (exponent is a variable expression k+1 — ring handles literal exponents only). So need neg_pow rewrite: `neg_pow : (−a)^n = (−1)^n * a^n` ✓ Mathlib (Ring.neg_pow? `neg_pow (a : R) (n : ℕ) : (−a)^n = (−1)^n * a^n` ✓ exists).\n\nThen the final conversion range n → Icc 1 n:\n```lean\n  rw [Finset.sum_Icc_eq_sum_range]  -- ∑ j ∈ Icc 1 n, f j = ∑ k ∈ range (n+1−1), f (k+1)\n```\nFinset.sum_Icc_eq_sum_range : ∑ i ∈ Finset.Icc m n, f i = ∑ k ∈ Finset.range (n + 1 - m), f (k + m)? — signature check: `Finset.sum_Icc_eq_sum_range (f : ℕ → M) (m n : ℕ) : ∑ i ∈ Finset.Icc m n, f i = ∑ i ∈ Finset.range (n + 1 - m), f (i + m)` ✓ I believe. With m := 1: range (n+1−1) = range n — n+1−1 = n — defeq but syntactically range (n + 1 - 1) — need `show` or simp [Nat.add_sub_cancel]... The target sum: ∑ j ∈ Icc 1 n, (−1)^{j+1}C(n,j)x^j. rw [Finset.sum_Icc_eq_sum_range]: becomes ∑ k ∈ range (n+1−1), (−1)^{(k+1)+1}C(n,k+1)x^{k+1} — n+1−1 needs normalization to n (Nat.add_sub_cancel : n + 1 − 1 = n ✓ simp lemma) — rw might fail on the range mismatch: the lemma's RHS has range (n + 1 - 1) — I can `rw [Finset.sum_Icc_eq_sum_range, Nat.add_sub_cancel]`? Nat.add_sub_cancel : n + m − m = n ✓ rewrites range (n + 1 − 1) → range n ✓. Then the goal: −S-form = ∑ k ∈ range n, (−1)^{k+1+1}C(n,k+1)x^{k+1}. And my derived form: ∑ k ∈ range n, (−1)^k·C(n,k+1)·x^{k+1}. Pointwise: (−1)^k vs (−1)^{k+1+1} = (−1)^{k+2}: equal since (−1)^{k+2} = (−1)^k·(−1)² = (−1)^k: pow_add + simp [(−1:ℂ)^2 = 1] — (−1:ℂ)^2 = 1 via sq... `neg_one_sq`? simp: (-1:ℂ)^2 = 1 by norm_num? There's `neg_one_pow`... simplest: (−1:ℂ)^(k+2) = (−1)^k·(−1)^2 (pow_add) and (−1:ℂ)^2 = 1 (by norm_num or `one_pow`... no: (−1)^2 = 1 — `neg_one_sq : (−1)^2 = 1`? in a ring: `neg_one_sq : (-1)^2 = 1`? might be `sq (-1)`... `by norm_num` works? (−1:ℂ)^2 — norm_num handles? Or `mul_neg_one`... (−1)·(−1) = 1: `neg_mul_neg` + `one_mul`... I'll use: have : ((-1:ℂ))^(k+2) = (-1:ℂ)^k := by rw [pow_add]; simp — simp knows (−1:ℂ)^2 = 1? `show ((−1:ℂ)^2 = 1) from by norm_num`? — safer: rw [pow_add]; norm_num — hmm norm_num on ((-1:ℂ)^k * (−1)^2 = (−1)^k): simp should simplify (−1:ℂ)^2 → 1 via... `pow_two`: (−1)^2 = (−1)·(−1) then neg_mul_neg, one_mul — simp [pow_two] closes ✓. \n\nThen sum_congr rfl with per-term: (−1)^k·C(n,k+1)·x^{k+1} = (−1)^{k+1+1}·C(n,k+1)·x^{k+1} — via the (−1)^{k+2} = (−1)^k fact ✓ ring after rw.\n\nOK this is all standard but fiddly. Fine.\n\n**Now R2(ii)** — the S_∞ swap. Target:\nSInfty n = (1 − a₁)n − 1 + Σ_{m odd ≥ 3} h⁺(m), h⁺(m) = (1−1/m)ⁿ − 1 + n/m [Lean def ✓ existing]\nand want: SInfty n = Σ_{j=1}^n (−1)^j C(n,j) a_j with a₁ = (log 4π+γ)/2 = lagariasA1, a_j = (1−2^{−j})ζ(j) = Σ_{m odd ≥ 1} m^{−j} (j ≥ 2).\n\nProof: expand (1−1/m)ⁿ = Σ_j (−1)^j C(n,j) m^{−j}... wait (1 − 1/m)ⁿ = Σ_{j=0}^n C(n,j)(−1/m)^j = 1 + Σ_{j≥1} C(n,j)(−1)^j m^{−j}. So h⁺(m) = Σ_{j=1}^n (−1)^j C(n,j) m^{−j} + n/m.\n\nΣ_{m odd ≥ 3} h⁺(m) = Σ_{j=2}^n (−1)^j C(n,j) Σ_{m odd ≥ 3} m^{−j} + Σ_{m odd ≥ 3} [j=1 term: −C(n,1)m^{−1} + n/m] \n= Σ_{j=2}^n (−1)^j C(n,j) Σ_{m odd ≥ 3} m^{−j} + Σ_{m odd ≥ 3} 0 — the j = 1 term: (−1)^1 C(n,1) m^{−1} + n/m = −n/m + n/m = 0 ✓ EXACTLY (that's why the odd-m sum starts at 3 — no wait, the j=1 cancellation is exact at every m: −n/m + n/m = 0 ✓).\n\nHmm wait: h⁺(m) = (1−1/m)ⁿ − 1 + n/m = Σ_{j=1}^n (−1)^j C(n,j) m^{−j} + n/m. The j=1 term: (−1)C(n,1)m^{−1} = −n/m. So h⁺(m) = Σ_{j=2}^n (−1)^j C(n,j) m^{−j} + (−n/m + n/m) = Σ_{j=2}^n (−1)^j C(n,j) m^{−j}. ✓ \n\nSo Σ_{m odd ≥ 3} h⁺(m) = Σ_{m odd ≥ 3} Σ_{j=2}^n (−1)^j C(n,j) m^{−j} = Σ_{j=2}^n (−1)^j C(n,j) Σ_{m odd ≥ 3} m^{−j} [swap — absolute convergence: |m^{−j}| ≤ m^{−2} for j ≥ 2 ✓ summable over odd m ≥ 3 ✓].\n\nAnd Σ_{m odd ≥ 3} m^{−j} = a_j − 1 (a_j = Σ_{m odd ≥ 1} m^{−j} = 1 + Σ_{m odd ≥ 3} m^{−j} since the m=1 term is 1^{-j} = 1).\n\nSo Σ_{m odd≥3} h⁺ = Σ_{j=2}^n (−1)^j C(n,j)(a_j − 1).\n\nThen SInfty n = (1−a₁)n − 1 + Σ_{j=2}^n (−1)^j C(n,j)(a_j − 1).\n\nTarget: Σ_{j=1}^n (−1)^j C(n,j) a_j = (−1)C(n,1)a₁ + Σ_{j=2}^n (−1)^j C(n,j)a_j = −n·a₁ + Σ_{j=2}^n ...\n\nDifference: SInfty n − target = (1−a₁)n − 1 + Σ_{j=2}^n (−1)^j C(n,j)(a_j−1) − (−n a₁ + Σ_{j=2}^n (−1)^j C(n,j)a_j)\n= n − n a₁ − 1 + n a₁ + Σ_{j=2}^n (−1)^j C(n,j)(a_j − 1 − a_j)\n= n − 1 + Σ_{j=2}^n (−1)^j C(n,j)·(−1)\n= n − 1 − Σ_{j=2}^n (−1)^j C(n,j).\nΣ_{j=2}^n (−1)^j C(n,j) = (1−1)ⁿ − C(n,0) + C(n,1) = 0 − 1 + n = n − 1.\nSo difference = n − 1 − (n − 1) = 0 ✓✓ the identity holds.\n\nFor n ≥ 1. For n = 0: SInfty 0 = (1−a₁)·0 − 1 + Σ [(1−1/m)⁰ −1 + 0] = −1 + Σ [1−1] = −1; target: Σ_{j=1}^0 = 0 (empty) — MISMATCH: −1 ≠ 0!! So the identity SInfty n = Σ_{j=1}^n (−1)^j C(n,j)a_j FAILS at n = 0. Indeed the identity is for n ≥ 1 (the (1−1)ⁿ − 1 + n formula needs n ≥ 1). So R2(ii) needs hypothesis 1 ≤ n. Downstream (crux) uses n ≥ 1 anyway (D-064's identity is for n ≥ 1; the SfBoundProp range is n ≥ 10⁵). Also — actually let me double check D-064's statement: \"Sf(n) := S_∞(n) + 1 − λ_n = Res₁(n) for all n ≥ 1\" ✓ n ≥ 1.\n\nHmm — also check n = 0 for R2(i): liCoeff 0 = ∑' 0 = ... liSummand 0 ρ = (mult/2)((1−1) + (1−1)) = 0 ✓ liCoeff 0 = 0; Σ_{j∈Icc 1 0} = ∅ = 0 ✓ holds at n = 0 trivially if both sides 0. My proof: liSummand 0 ρ = Σ_{j∈Icc 1 0} ... = 0 ✓ the binomial identity one_sub_one_sub_pow at n = 0: 1 − (1−x)⁰ = 0 = Σ_{j∈Icc 1 0} = 0 ✓ — the proof via sum_range_succ' at n=0: range 0 = ∅... hexp: (1−x)^0 = 1 = 1 + Σ_{k∈range 0} = 1 + 0 ✓ works. OK n=0 fine for (i).\n\nNow — what about the DEF of a_j in Lean? a₁ = lagariasA1 (exists). a_j for j ≥ 2: (1−2^{−j})ζ(j) — with riemannZeta at positive integers ≥ 2 — real ζ. In ℝ: a_j := (1 − (2:ℝ)^{−j})·(riemannZeta j).re? Hmm — ζ(j) for j ≥ 2 is real. riemannZeta (j:ℂ) — its .re... or use the odd-m series directly: a_j := Σ_{m odd ≥ 1} (m:ℝ)^{−j} (tsum over odd naturals). The identity (1−2^{−j})ζ(j) = Σ_{m odd} m^{−j} is a standard Mathlib fact? There might be `riemannZeta` tsum forms: `hasSum_zeta_nat`? or the odd-zeta: `hasSum_odd...`? Hmm. For the swap I need a_j AS the odd-m series (that's what enters). The (1−2^{−j})ζ(j) form is only needed downstream (ii′-3's (4.10) — τ_j = c_j + (−1)^j σ_{j+1} − (−1)^j — there τ involves... hmm, which form does ii′-3 need? τ_j's archimedean content connects to digamma values — the ζ(j) values. But that's ii′-3's problem).\n\nFor ii′-2, the natural definition: a_j as the odd-m tsum for j ≥ 2 and lagariasA1 for j = 1:\n```lean\ndef lagariasA (j : ℕ) : ℝ :=\n  if j = 1 then lagariasA1 else tsum fun m : {m : ℕ // Odd m} => ((m : ℝ)) ^ (-(j : ℝ))  -- rpow? or ^j⁻¹\n```\nHmm — better: use `(m:ℝ)^(−j)` as rpow or `(m:ℂ)^{-j}`... Let me think about the cleanest encoding for the swap. The odd-m set in SInfty: {m : ℕ // Odd m ∧ 3 ≤ m} with summand (1 − 1/(m:ℝ))^n − 1 + n/(m:ℝ) — REAL powers: (1 − 1/m)^n with n : ℕ — that's a real pow via Monoid.npow ✓ and 1/(m:ℝ) division ✓.\n\nFor a_j: Σ_{m odd ≥ 1} m^{−j} — j ≥ 2 — as (m:ℝ)^(−(j:ℤ))? or 1/(m:ℝ)^j — simplest: 1/(m:ℝ)^j with npow ✓.\n\nThe swap proof structure:\nSInfty n = (1−a₁)n − 1 + Σ_{m ∈ {odd, ≥3}} h⁺(m).\nStep 1: h⁺(m) = Σ_{j ∈ Icc 2 n} (−1)^j C(n,j) (1/m)^j — via the binomial expansion (1 − 1/m)^n = Σ_{j=0}^n C(n,j)(−1/m)^j, subtract 1, add n/m, cancel j=1 term with +n/m: \n(1−1/m)ⁿ − 1 + n/m = Σ_{j=1}^n C(n,j)(−1/m)^j + n/m = Σ_{j=2}^n C(n,j)(−1/m)^j + [C(n,1)(−1/m) + n/m] = Σ_{j=2}^n C(n,j)(−1/m)^j + [−n/m + n/m] = Σ_{j=2}^n (−1)^j C(n,j) (1/m)^j... careful (−1/m)^j = (−1)^j(1/m)^j ✓.\n\nFor n ≥ 2 this works (Icc 2 n nonempty-ish handling — for n = 1: Icc 2 1 = ∅: h⁺(m) = (1−1/m) − 1 + n/m = 0 ✓ and Σ_{j∈Icc 2 1} = 0 ✓ OK).\n\nStep 2: Σ_{m odd≥3} Σ_{j∈Icc 2 n} c_j (1/m)^j = Σ_{j∈Icc 2 n} c_j Σ_{m odd≥3} (1/m)^j — tsum_sum over the subtype: needs each slice (1/m)^j summable over {m odd ≥ 3}: |1/m^j| ≤ 1/m² for j ≥ 2 ✓ vs the p-series Σ 1/m² (Mathlib: summable_one_div_nat_pow? `summable_one_div_nat_pow : Summable (fun n => 1/n^p) ↔ 2 ≤ p`? I recall `summable_one_div_nat_pow (p : ℕ) : Summable (fun n => 1/(n:ℝ)^p) ↔ 2 ≤ p`? Something like that exists (`summable_one_div_nat_pow`). Over the subtype {odd ≥ 3}: restriction — Summable.subtype or comparison with the full series: the subtype sum ≤ full sum: `Summable.subtype` : Summable f → Summable (fun x : s => f x)? There's `Summable.subtype (hf : Summable f) (s : Set α) : Summable (fun x : s => f x)`? I recall `Summable.subtype` exists for ℝ≥0/norm... For normed groups: `Summable.subtype (hf : Summable f) (s) : Summable (f ∘ Subtype.val)`? Hmm — there's `summable_subtype_iff_of_nonneg`... For safety: use comparison: Summable (fun m : subtype => 1/(m:ℝ)^j) ⟸ ‖·‖ ≤ 1/(m:ℝ)² and Summable (fun m : subtype => 1/m²) ⟸ Summable.subtype of summable_one_div_nat_pow... circular. Let me look for `Summable.subtype`: I believe `Summable.subtype (hf : Summable f) (s : Set α) : Summable (fun x : ↥s => f x)` exists when the ambient is... hmm no — for arbitrary f it's false (conditionally convergent counterexamples) — for ℝ with absolute convergence it's fine: Summable in ℝ IS absolute. The lemma might be `Summable.comp_injective`? f ∘ Subtype.val with Subtype.val injective: `Summable.comp_injective (hf : Summable f) (hi : Function.Injective g) : Summable (f ∘ g)`? that's also false in general... no wait — Summable.comp_injective IS false for conditionally convergent... Hmm, actually for Summable (= absolute in ℝ/ℂ), restriction to a subset IS summable: the correct Mathlib lemma: `Summable.subtype`? Let me search at compile time. There's definitely `summable_subtype_iff_of_nonneg : (∀ x, 0 ≤ f x) → (Summable (f ∘ Subtype.val : s → ℝ) ↔ Summable (s.indicator f))` and `Summable.indicator`... Also `Summable.comp_injective` exists? For normed spaces with absolute convergence encoded: Summable f in a complete normed space is absolute ⟹ any subseries summable: the lemma `Summable.comp_injective`: I think it exists with the absolute-convergence characterization: (hf : Summable f) (hi : Injective g) : Summable (f ∘ g) — requires g's range... no such general lemma; the real one: `Summable.comp_injective` might not exist, but `Summable.subtype` DOES: I'm fairly confident: `theorem Summable.subtype (hf : Summable f) (s : Set α) : Summable (fun x : s => f x)` — hmm no. Let me just plan: Summable over subtype via `summable_of_summable_norm`? Simplest robust: the subtype {m // Odd m ∧ 3 ≤ m} — map to ℕ via val: Summable (fun m : subtype => g m.val) where g : ℕ → ℝ with g m = 1/m^j: g summable on ℕ (p-series, j ≥ 2): then subtype summability via... `Summable.comp_injective`? — I'll check exact names when writing. There IS `Summable.comp_injective` in Mathlib.Topology.Algebra.InfiniteSum.Basic I believe: \"If f is summable and g is injective, then f ∘ g is summable\"? That can't be right in general (range could pick a conditionally-divergent subseries — but Summable in ℝ is unconditional/absolute, so it IS right for ℝ). Hmm — for ℂ/ℝ, Summable means absolutely convergent (Mathlib's Summable on normed fields = absolute? NO — Mathlib's Summable is just \"has a sum\"; for ℝ it implies absolute). The comp_injective lemma: I recall `Summable.comp_injective (hf : Summable f) (hi : Function.Injective g) : Summable (f ∘ g)` — yes I'm fairly sure this exists and holds BECAUSE Mathlib proves Summable → absolutely... hmm, actually it requires the target to be a complete normed space and uses that Summable ⟹ Cauchy-sums ⟹ bounded partial sums of norms... In ℝ: |Σ_{finite} f(g i)| ≤ ... yes it works via summable_of_summable_norm or Cauchy criteria. Let me just verify names at compile.\n\nActually — better: AVOID the subtype-restriction issue: use the SAME subtype as SInfty: {m : ℕ // Odd m ∧ 3 ≤ m} — and summability of (fun m : subtype => (1/(m:ℝ))^j) directly by comparison with... I need a summable majorant ON the subtype. The natural one: (fun m : subtype => 1/(m:ℝ)²) — is THAT known summable? Same problem. \n\nRoot solution: build the p-series on the subtype from the full one: `Summable (fun m : {m // Odd m ∧ 3 ≤ m} => (1/(m:ℝ))^p)`:\nMathlib: `summable_nat_add_iff`? For the ≥ 3 cutoff: could reindex {m // Odd m} vs {m // Odd m ∧ 3 ≤ m} — differ by {1} (finite) ✓ `summable_subtype_and_compl`? Hmm.\n\nCleanest available: there IS `Summable.subtype`? Let me think about what I KNOW exists:\n- `Summable.indicator (hf : Summable f) (s : Set α) : Summable (s.indicator f)` — needs s ∈ ... no: indicator is always summable if f is? For the indicator: s.indicator f x = f x if x ∈ s else 0 — is that summable? For ℝ-valued: yes (absolute): `Summable.indicator (hf : Summable f) (s : Set α) : Summable (Set.indicator s f)`? I don't think that exists unconditionally either... hmm, actually it does for... no.\n\n- The REAL workhorse: `summable_subtype_iff_of_nonneg` / `summable_subtype_and_compl`: `summable_subtype_and_compl : Summable ((fun x : s => f x) ⊕ (fun x : sᶜ => f x)) ↔ Summable f`? There's `Summable.sum_compl`... \n\nLet me just check during implementation with grep. There's definitely a standard route: for `f : ℕ → ℝ` summable and `s : Set ℕ`, the subtype sum: `hf.subtype s : Summable (fun x : s => f x)`? I'm 80% sure `Summable.subtype` exists exactly like this (it's true since Summable on ℝ ⟹ absolute ⟹ restriction absolute). Hmm — actually for a GENERAL normed group, Summable does not imply absolute convergence... but the restriction of a summable family to a subset IS still summable (partial sums over finite subsets of the subtype are partial sums over finite subsets of the ambient — the Cauchy criterion passes through? For summability via vanishing of tails: yes — Summable f ⟹ the net of finite partial sums is Cauchy ⟹ restricted too? A finite subset of s IS a finite subset of α — the sums over them coincide — Cauchy-ness: for finite F ⊆ s: sum over F of f = sum over (F as subset of α)... the tail bound: |Σ_{F} f| small for F disjoint from a large finite set — same on the subtype ✓. So YES restriction preserves summability in general (even without absolute convergence — via the cauchySeq_of_summable / \"summable_iff_vanishing_norm\" characterization: Summable f ↔ ∀ ε, ∃ finite T, ∀ finite U disjoint from T, ‖Σ_{U} f‖ < ε — restrictions inherit this). I'm now quite sure `Summable.subtype` exists: `theorem Summable.subtype {s : Set α} (hf : Summable f) : Summable (fun x : s => f x)`? hmm or with the set explicit. I'll find it at compile.\n\n- Alternatively use `summable_of_summable_restrict`... whatever — find at compile.\n\nStep 3: relate Σ_{m odd ≥ 3} (1/m)^j to lagariasA j: define lagariasA j := if j = 1 then lagariasA1 else ∑' m : {m // Odd m}, (1/(m:ℝ))^j. Then Σ_{m odd ≥ 3} (1/m)^j = lagariasA j − 1 for j ≥ 2: the subtype {odd ∧ ≥3} vs {odd}: differ by m = 1 (the only odd m < 3): tsum over {odd} = term(1) + tsum over {odd ∧ ≥3}: term(1) = 1/1^j = 1. In Lean: `Summable.tsum_subtype_add_tsum_subtype_compl`? or via: {odd} = {1} ∪ {odd ∧ ≥3} disjoint: `tsum_union`? For set-types: `Summable.tsum_union_disjoint`? Hmm — there's `tsum_subtype_union`... Simplest: \nΣ_{m odd} g(m) = g(1) + Σ_{m odd, m ≠ 1} g(m) via `tsum_eq_add_tsum_omit`? `tsum_eq_add_tsum_omit (hf : Summable f) (i) : ∑' x, f x = f i + ∑' x : {x // x ≠ i}, f x` ✓ exists (tsum_eq_add_tsum_omit). Then {m // Odd m ∧ m ≠ 1} vs {m // Odd m ∧ 3 ≤ m}: the next odd after 1 is 3, so m ≠ 1 ∧ odd ⟺ odd ∧ 3 ≤ m ✓ — a subtype equivalence (Equiv.subtypeEquiv... or just show the summands/tsums equal via an Equiv: {m // Odd m ∧ m ≠ 1} ≃ {m // Odd m ∧ 3 ≤ m} — both are subtypes of ℕ with equivalent predicates — `Equiv.subtypeSubtypeEquivSubtypeInter`? There's `Equiv.subtypeEquiv` : (∀ a, p a ↔ q a) → {a // p a} ≃ {a // q a} ✓ then tsum_congr via the equiv: `Equiv.tsum_eq` : ∑' x, f (e x) = ∑' y, f y ✓.\n\nSo lagariasA j = 1 + Σ_{m odd≥3} (1/m)^j for j ≥ 2 — i.e., Σ_{m odd≥3} = lagariasA j − 1 ✓.\n\nStep 4: assemble:\nΣ_{m odd≥3} h⁺(m) = Σ_{j∈Icc 2 n} (−1)^j C(n,j)·(lagariasA j − 1)   [for the slices: summable, swap]\n\nSInfty n = (1−a₁)n − 1 + that.\n\nTarget: Σ_{j=1}^n (−1)^j C(n,j) lagariasA j = −n a₁ + Σ_{j=2}^n (−1)^j C(n,j) lagariasA j (split j=1: Icc 1 n = {1} ∪ Icc 2 n for n ≥ 1; (−1)^1 C(n,1) a₁ = −n a₁).\n\nSo need: (1−a₁)n − 1 + Σ_{j=2}^n (−1)^j C(n,j)(a_j − 1) = −n a₁ + Σ_{j=2}^n (−1)^j C(n,j) a_j\n⟺ n − a₁n − 1 + n a₁ = Σ_{j=2}^n (−1)^j C(n,j)·a_j − Σ_{j=2}^n (−1)^j C(n,j)(a_j−1) = Σ_{j=2}^n (−1)^j C(n,j)\n⟺ n − 1 = Σ_{j=2}^n (−1)^j C(n,j).\nAnd Σ_{j=2}^n (−1)^j C(n,j) = Σ_{j=0}^n (−1)^j C(n,j) − 1 + n = (1−1)^n − 1 + n = 0 − 1 + n = n − 1 ✓ for n ≥ 1 ((1−1)^n = 0 needs n ≥ 1 ✓).\nMathlib: `add_pow_neg_one`? The alternating binomial sum: Σ_{j=0}^n (−1)^j C(n,j) = (1−1)^n = 0ⁿ = 0 (n ≥ 1): via add_pow 1 (−1) or `(1 + (−1))^n`... `Int/alternating`: there's `Finset.sum_range_choose`... the cleanest: (1 + (−1:ℝ))^n = Σ_j C(n,j)·1^{n−j}·(−1)^j via add_pow; LHS = 0^n = 0 (n ≥ 1, zero_pow). So Σ_{j∈range(n+1)} (−1)^j C(n,j) = 0. Then split off j=0 (1) and j=1 (−n): Σ_{j=2}^n = 0 − 1 + n ✓.\n\nOK. The REAL version (SInfty is ℝ-valued): lagariasA : ℕ → ℝ, the theorem:\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\n```\nAll in ℝ — no ℂ needed for (ii)! The binomial expansion of (1 − 1/m)^n in ℝ ✓ (1/m real). The odd-m tsum in ℝ ✓ matches SInfty's def.\n\nSign convention check vs D-037: \"S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j\" ✓ matches.\n\nNow — what does the CRUX actually need? D-064: S_∞ = Σ_j C(n,j)τ_{j−1} — with τ_{j−1} = (−1)^j a_j. So downstream (ii′-6) will combine: SInfty n = Σ_j (−1)^j C(n,j) a_j [this] with λ_n = Σ_j (−1)^{j+1}C(n,j)σ_j [(i)] and (4.10) [ii′-3]: relating a_j's to c's and σ's. The τ-form is just a reindexing: τ_{j−1} := (−1)^j·lagariasA j — downstream can define that. For THIS sub-stage, deliver:\n(i) `liCoeff_eq_sum_sigma : liCoeff n = ∑ j ∈ Finset.Icc 1 n, (-1:ℂ)^(j+1) * (n.choose j:ℂ) * sigmaP j` — hmm, or real form? liCoeff is ℂ (manifestly real). Downstream Sf uses (liCoeff n).re. The crux: Sf = SInfty + 1 − liCoeff.re = ResW1... The ResW1 is ℂ-valued (lcoeff : ℂ). Hmm — lcoeff k : ℂ (iteratedDeriv quotients — complex). But they're real values (c_k real). The final crux identity: SInfty n + 1 − (liCoeff n).re = (ResW1 n).re? or as ℂ? ResW1 n ∈ ℂ — its real part is what matters. For now: (i) as a ℂ identity is finest (take .re downstream). Should sigmaP j be ℂ? The slice is ℂ-valued but real; the sum ℂ ✓. Fine — ℂ identity; downstream takes re.\n\nHmm wait — actually let me double-check the exact form needed for the crux assembly (ii′-6): Sf := S_∞ + 1 − λ_n. Res₁ := Σ_{j=1}^n C(n,j)c_{j−1} = ResW1 n (Lean, proved). The chain:\nSInfty n + 1 − liCoeff.re \n= [Σ_j (−1)^j C(n,j) a_j] + 1 − [Σ_j (−1)^{j+1}C(n,j) σ_j].re\nand (4.10): a_j in terms of c's and σ's: D-064: τ_j = c_j + (−1)^j σ_{j+1} − (−1)^j with τ_j = (−1)^{j+1} a_{j+1}:\n(−1)^{j+1} a_{j+1} = c_j + (−1)^j σ_{j+1} − (−1)^j.\nWith k := j+1: (−1)^k a_k = c_{k−1} + (−1)^{k−1}σ_k − (−1)^{k−1} = c_{k−1} − (−1)^k σ_k + (−1)^k.\nSo (−1)^k a_k + (−1)^k σ_k = c_{k−1} + (−1)^k — hmm let me redo the crux with a_j convention directly:\nS_∞ + 1 − λ_n = Σ_k C(n,k)[(−1)^k a_k − (−1)^{k+1} σ_k] + 1 = Σ_k C(n,k)(−1)^k[a_k + σ_k] + 1.\nFrom (4.10)-in-a-form: (−1)^k[a_k + σ_k] = c_{k−1} + (−1)^k·(−1)?? let me redo: from above (−1)^k a_k = c_{k−1} + (−1)^{k−1}σ_k − (−1)^{k−1} ⟹ (−1)^k a_k + (−1)^k σ_k = c_{k−1} + (−1)^{k−1}σ_k − (−1)^{k−1} + (−1)^k σ_k = c_{k−1} + σ_k[(−1)^{k−1} + (−1)^k] − (−1)^{k−1} = c_{k−1} − (−1)^{k−1}·(−1)... \n\nhmm let me be careful: (−1)^{k−1}σ_k + (−1)^k σ_k = σ_k(−1)^{k−1}(1 + (−1)) = 0 ✓. So (−1)^k[a_k + σ_k] = c_{k−1} − (−1)^{k−1} = c_{k−1} + (−1)^k.\nThen Σ_k C(n,k)(−1)^k[a_k+σ_k] + 1 = Σ_k C(n,k)c_{k−1} + Σ_k C(n,k)(−1)^k + 1 = ResW1 n + ((1−1)^n − 1) + 1 = ResW1 n ✓ (n ≥ 1). ✓✓ consistent with D-064.\n\nSo (4.10)-in-a-form: **(−1)^k a_k = c_{k−1} + (−1)^{k−1} σ_k − (−1)^{k−1}** for k ≥ 1 — wait let me double-check against the j=0 sanity gate: τ_0 = c_0 + σ_1 − 1 (j=0: τ_0 = c_0 + (−1)^0 σ_1 − (−1)^0 = c_0 + σ_1 − 1). τ_0 = (−1)^1 a_1 = −a₁. So −a₁ = c₀ + σ₁ − 1 ⟹ σ₁ = 1 − a₁ − c₀ = 1 − (log4π+γ)/2 + γ = 1 + γ/2 − (log 4π)/2 ✓✓ the classical Davenport value (verified numerically session 014: σ₁ = 1 + γ/2 − ½log 4π ✓). And in a-form with k=1: (−1)^1 a₁ = c₀ + (−1)^0 σ₁ − (−1)^0 ⟹ −a₁ = c₀ + σ₁ − 1 ✓ same ✓.\n\nSo the ii′-3 target in a-form: for k ≥ 1: c_{k−1} = (−1)^k a_k − (−1)^{k−1}σ_k + (−1)^{k−1} = (−1)^k a_k + (−1)^k σ_k + (−1)^{k−1}. I.e. **c_{k−1} = (−1)^k (a_k + σ_k) + (−1)^{k−1}**. Hmm wait: from (−1)^k a_k = c_{k−1} + (−1)^{k−1}σ_k − (−1)^{k−1}: c_{k−1} = (−1)^k a_k − (−1)^{k−1}σ_k + (−1)^{k−1} = (−1)^k a_k + (−1)^k σ_k + (−1)^{k−1} ✓.\n\nThat's ii′-3's content (the analytic heart — EF route). NOT this sub-stage. This sub-stage: (i) + (ii) only.\n\nDeliverables for ii′-2:\n(i) `sigmaSlice`, `sigmaP`, `sigmaSlice_summable`, `liSummand_eq_sum_slices`, `one_sub_one_sub_pow`, `liCoeff_eq_sum_sigma`.\n(ii) `lagariasA` (j ≥ 2 odd-tsum), `sInfty_summand_eq` (h⁺ expansion), slice summability, the swap, `sInfty_eq_sum`.\n\nHmm — one question on (ii): the a_j for j ≥ 2 as odd-m tsum — the swap produces Σ_{m odd≥3}(1/m)^j = lagariasA j − 1 — I need that lemma too (`lagariasA_sub_one`).\n\nNew file: `NguyenRH1/LiSwaps.lean` importing LiSkeleton (for liSummand/liCoeff/SInfty/lagariasA1) + LiSides not needed. Freeze: new file OK.\n\nLet me now check a few more Mathlib names:\n- `tsum_sum` ✓ (check exact form)\n- `Summable.const_mul` / `tsum_mul_left` ✓\n- `Summable.subtype`?\n- `tsum_eq_add_tsum_omit` ✓\n- `Equiv.subtypeEquiv` + `Equiv.tsum_eq` ✓\n- `summable_one_div_nat_pow`?\n- `Finset.sum_Icc_eq_sum_range`\n- `neg_pow`\n- `Complex.inv_re` : (z⁻¹).re = z.re / normSq z ✓ (check)\n- `Complex.add_conj : z + conj z = 2 * z.re` — form: `Complex.add_conj : z + conj z = 2 * (z.re : ℂ)`? or ↑((2:ℝ)·z.re)? check.\n- map_div₀ for starRingEnd: `map_div₀ (starRingEnd ℂ)`? starRingEnd is a RingEquiv — map_div₀ applies to ring equivs? map_div₀ (f : R ≃+* S) ✓ should.\n- norm of star: `RCLike.norm_conj`? or Complex.norm_conj : ‖conj z‖ = ‖z‖ ✓ (check name — `Complex.norm_conj` exists; starRingEnd ℂ z = conj z — `Complex.starRingEnd_apply : starRingEnd ℂ z = conj z` ✓ simp).\n\nFor the swap in (ii) — the summability of slices over the odd≥3 subtype: |1/m^j| ≤ 1/m² — need Σ over the subtype of 1/m² summable. Route: the map m ↦ (m:ℝ)⁻²... For the subtype {m // Odd m ∧ 3 ≤ m}: Summable (fun m : subtype => ((m:ℝ))^(-2:ℝ))? — hmm rpow vs npow. SInfty's summand uses (1 − 1/(m:ℝ))^n with n : ℕ (npow) — so for slices: 1/(m:ℝ)^j npow ✓.\n\nSummability of fun m : subtype => 1/(m:ℝ)²: \nOption 1: `Summable.subtype` of summable_one_div_nat_pow 2 — check names.\nOption 2: comparison with the full ℕ series via `summable_of_nonneg_of_le` with the full series as majorant?? — the majorant must be summable ON THE SUBTYPE — circular again.\nOption 3: The subtype {m // Odd m ∧ 3 ≤ m} injects into ℕ via val — `Summable.comp_injective`? hmm.\n\nLet me think again about what definitely exists in Mathlib for \"summable on a subtype\":\n`Summable.subtype (hf : Summable f) (s : Set α) : Summable (fun x : s => f x)` — I'm now recalling this DOES exist: Mathlib.Topology.Algebra.InfiniteSum.Basic? or .Constructions — \"Summable.subtype\". Hmm, actually I remember `Summable.subtype` being about `f : α → M` and s : Set α giving Summable (fun x : s => f x) — YES it exists (proof via summable_iff_vanishing_norm, restriction of finite sets). I'll verify by grep.\n\nAlso — SInfty's own tsum: is it known Summable in Lean? For the swap I don't need SInfty's summability separately — the swap rewrites the tsum as the finite j-sum — wait no: I need to rewrite Σ_{m odd≥3} h⁺(m) where h⁺ = finite j-sum: tsum_sum gives Σ_{m} Σ_j = Σ_j Σ_m — the tsum_sum needs each j-slice summable (over the subtype) ✓ and produces tsum of the m-sum = sum of the m-tsums ✓ no separate SInfty summability needed (the equality is between the tsum and the finite sum — tsum_sum's conclusion). ✓ \n\nBut — one more check on tsum_sum's exact signature: `theorem tsum_sum {f : ι → α → M} {s : Finset ι} (hf : ∀ i ∈ s, Summable (f i)) : ∑' a, ∑ i ∈ s, f i a = ∑ i ∈ s, ∑' a, f i a` ✓ I'm fairly confident.\n\nFor (i), the outer structure is over the zero-subtype with ℂ values — same tsum_sum ✓.\n\nNow, let me also double-check `Finset.sum_Icc_eq_sum_range`: `theorem Finset.sum_Icc_eq_sum_range (f : ℕ → M) (m n : ℕ) : ∑ i ∈ Finset.Icc m n, f i = ∑ i ∈ Finset.range (n + 1 - m), f (i + m)` ✓ I believe.\n\nAnd `add_pow`: current Mathlib form (after the binomial refactor): `theorem add_pow (x y : R) (n : ℕ) : (x + y) ^ n = ∑ k ∈ Finset.range (n + 1), x ^ k * y ^ (n - k) * Nat.choose n k`? Hmm — I recall a 2024 refactor made it `∑ k ∈ range (n+1), x^k * y^(n-k) * C(n,k)` with the cast. Let me just grep quickly for all these names before writing. Also `summable_one_div_nat_pow`.\n\nAlso for (ii) — hmm, wait: I should double check the REAL binomial expansion application: (1 − 1/(m:ℝ))^n — 1 − 1/m real ✓ add_pow applies to ℝ ✓.\n\nOne more consideration for (i): liSummand's star form: liSummand n ρ := (zeroMult ρ:ℂ)/2 * ((1 − (1 − 1/(ρ:ℂ))^n) + (1 − (1 − 1/((starRingEnd ℂ)(ρ:ℂ)))^n)). So x := 1/(ρ:ℂ), y := 1/(starRingEnd ℂ (ρ:ℂ)) ✓ direct.\n\nLet me grep the name checks.","signature":""},{"type":"text","text":"I have the full design for both swaps. Verifying the remaining Mathlib names before writing."},{"type":"tool_use","id":"Bash_81","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"theorem tsum_sum \\|lemma tsum_sum \" Mathlib/Topology/Algebra/InfiniteSum/ | head -3; grep -rn \"Summable.subtype\\b\" Mathlib/Topology/Algebra/InfiniteSum/*.lean | head -4; grep -rn \"theorem summable_one_div_nat_pow\\|lemma summable_one_div_nat_pow\" Mathlib/ | head -3; grep -rn \"theorem add_pow \\|lemma add_pow \" Mathlib/Algebra/BigOperators/ Mathlib/Algebra/ 2>/dev/null | head -3","description":"Verify tsum_sum, Summable.subtype, p-series, add_pow names"},"extra_content":null},{"type":"tool_use","id":"Bash_82","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"theorem tsum_eq_add_tsum_omit\\|lemma tsum_eq_add_tsum_omit\" Mathlib/Topology/Algebra/InfiniteSum/ | head -2; grep -rn \"theorem sum_Icc_eq_sum_range\\|lemma sum_Icc_eq_sum_range\" Mathlib/Algebra/BigOperators/ | head -2; grep -rn \"theorem neg_pow \\|lemma neg_pow \" Mathlib/Algebra/ | head -2; grep -rn \"theorem inv_re \\|lemma inv_re \" Mathlib/Data/Complex/ Mathlib/Analysis/Complex/ 2>/dev/null | head -2; grep -rn \"theorem add_conj \\|lemma add_conj \" Mathlib/Data/Complex/ Mathlib/Analysis/SpecialFunctions/ 2>/dev/null | head -3; grep -rn \"Equiv.tsum_eq\\b\" Mathlib/Topology/Algebra/InfiniteSum/ | head -2","description":"Verify omit/range/neg_pow/inv_re/add_conj/Equiv.tsum_eq names"},"extra_content":null}]