[{"type":"thinking","thinking":"Good. Now I'll write LiSwaps.lean. One design note: SInfty's summand in the def is `((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))` — I'll match that exactly in sInfty_summand_eq.\n\nFor the m : {m : ℕ // Odd m ∧ 3 ≤ m} coercion: (m : ℝ) — how does the def's coercion chain work? m : subtype; (m : ℝ) — there must be a coe from the subtype to ℕ then to ℝ — Lean inserts ↑↑. In my lemmas, write the same form.\n\nFor the summand function matching: SInfty's tsum function is `fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))` — note NO space differences matter. My sInfty_summand_eq should conclude exactly that lambda applied to m equals the Icc 2 n sum.\n\nOne more subtlety on sInfty_summand_eq's proof: from one_sub_one_sub_pow: 1 − (1−x)^n = Σ_{Icc 1 n} (−1)^{j+1}C(n,j)x^j with x := 1/(m:ℝ). So (1−x)^n − 1 = −Σ ... = Σ (−1)^j C x^j:\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  -- rewrite the target's first piece\n  have h2 : (1 - 1 / (m : ℝ)) ^ n - 1 =\n      ∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j := by\n    have : (1 - 1 / (m : ℝ)) ^ n - 1 = -(1 - (1 - 1 / (m : ℝ)) ^ n) := by ring\n    rw [this, h1]\n    rw [← Finset.sum_neg_distrib]  -- −Σ c'_j x^j → Σ −(c'_j x^j) — wait h1's RHS is Σ (−1)^{j+1}C x^j; −Σ = Σ −(...) ✓\n    apply Finset.sum_congr rfl\n    intro j hj\n    -- −((−1)^{j+1}·C·x^j) = (−1)^j·C·x^j: (−1)^{j+1} = −(−1)^j: pow_succ: (−1)^{j+1} = (−1)^j·(−1)\n    rw [pow_succ]  -- hmm — rewrites which (−1)^(j+1)? the one inside −(...): goal: −((−1)^{j+1}·C·x^j) = (−1)^j·C·x^j — pow_succ : a^{k+1} = a^k·a — pattern a^(?+1): matches (−1)^{j+1} ✓ (j+1 is _+1 form ✓)\n    ring\n  rw [h2, sum_Icc_one_eq_add_sum_Icc_two n hn (fun j => (-1:ℝ)^j * (n.choose j : ℝ) * (1/(m:ℝ))^j)]\n  -- now: (−1)^1·C(n,1)·(1/m) + Σ_{Icc 2 n} + n/m = Σ_{Icc 2 n} — the j=1 term = −n/m cancels\n  have h3 : (-1 : ℝ) ^ 1 * (n.choose 1 : ℝ) * (1 / (m : ℝ)) ^ 1 = -(n : ℝ) / (m : ℝ) := by\n    rw [pow_one, pow_one, Nat.choose_one_right]\n    push_cast  -- ↑(n.choose 1) — after rw: ↑n — push_cast: Nat.cast_one? hmm (↑(n.choose 1):ℝ) — rw [Nat.choose_one_right] : n.choose 1 = n — rewrites inside the cast: (↑n:ℝ) ✓\n    ring  -- −1·↑n·(1/m) = −(↑n/m): −↑n/m — ring handles with /: (−1)*↑n*(1/m) = −(↑n)/m — ring normalizes divisions ✓ (field_simp not needed — ring treats 1/m and /m as inverse atoms consistently ✓)\n  rw [h3]\n  ring\n```\nWait — the final goal after rw [h2, peel]: (−n/m + Σ_{Icc 2 n}) + n/m = Σ_{Icc 2 n}?? order: h2 turns the LHS (1−1/m)^n − 1 into Σ_{Icc 1 n}; then the whole LHS is Σ_{Icc 1 n} + n/m; peel: = (g 1 + Σ_{Icc 2 n}) + n/m; rw [h3]: (−n/m + Σ) + n/m = Σ — ring closes (Σ atom) ✓.\n\nHmm — careful: the goal after `rw [h2]`: Σ_{Icc 1 n} g j + ↑n/↑m = Σ_{Icc 2 n} g j. rw [sum_Icc_one_eq_add_sum_Icc_two n hn g]: rewrites Σ_{Icc 1 n} g → g 1 + Σ_{Icc 2 n} g ✓. Then rw [h3]: g 1 → −↑n/↑m — wait h3 : g 1 = −(↑n)/↑m — my h3's LHS: (−1)^1 * ↑(n.choose 1) * (1/↑m)^1 — is that g 1? g j := (−1)^j * ↑(n.choose j) * (1/↑m)^j — g 1 = (−1)^1 * ↑(n.choose 1) * (1/↑m)^1 ✓ syntactic match (beta) ✓. Then goal: (−↑n/↑m + Σ) + ↑n/↑m = Σ — ring ✓.\n\nh3's ring: goal −1 * ↑n * (1/↑m)^... after pow_one×2 and choose rewrite: (−1:ℝ) * ↑n * (1/↑m) = −↑n/↑m — ring? LHS −(↑n·(1/↑m)) = −↑n/↑m ✓ ring handles 1/m as m⁻¹ ✓ and −(↑n/↑m) = −(↑n·↑m⁻¹) ✓ ring closes ✓.\n\nNow — hmm, one thing to double-check in h2's per-term step:\ngoal: −((−1)^{j+1}·↑C·x^j) = (−1)^j·↑C·x^j — wait no. h2's Finset.sum_congr goal: the LHS sum is Σ_{Icc 1 n} −((−1)^{j+1}·C·x^j) (after ← sum_neg_distrib) and RHS is Σ (−1)^j·C·x^j — per-term goal: −((−1)^(j+1)·↑C·x^j) = (−1)^j·↑C·x^j. rw [pow_succ]: first a^(k+1) pattern — (−1)^{j+1} — hmm wait but the exponent in h1's RHS is (j+1) — one_sub_one_sub_pow's statement: (−1:R)^(j+1)·C·x^j ✓ so the term is (−1)^(j+1)·C·x^j ✓ pow_succ rewrites (−1)^(j+1) → (−1)^j·(−1) ✓ then ring: −((−1)^j·(−1)·C·x^j) = (−1)^j·C·x^j ✓ ring ✓.\n\nBUT — wait, there's a subtlety: after rw [this, h1], the goal is −(Σ_{Icc 1 n} (−1)^{j+1}·C·x^j) = Σ_{Icc 1 n} (−1)^j·C·x^j. rw [← Finset.sum_neg_distrib]: pattern −∑ i, f i — matches LHS ✓ → Σ_{Icc 1 n} −((−1)^{j+1}·C·x^j) ✓ then sum_congr ✓.\n\nHmm — Finset.sum_neg_distrib exact form: `Finset.sum_neg_distrib : ∑ i ∈ s, −f i = −∑ i ∈ s, f i` ✓ so ← direction turns −∑ into Σ −(·) ✓.\n\nNow — one_sub_one_sub_pow with (R := ℝ) vs (R := ℂ): polymorphic [CommRing R] ✓ — but the CAST (n.choose j : R) — Nat.cast into R ✓ CommRing has NatCast ✓.\n\nWait — one concern: in one_sub_one_sub_pow's proof, the step `rw [h, ← Finset.sum_neg_distrib]` — where h : 1 − (1 + S) = −S by ring — hmm ring with S := the sum as atom: 1 − (1 + S) = −S ✓ ring proves ✓.\n\nAnd the FINAL conversion sum_Icc_one_eq_sum_range n f in one_sub_one_sub_pow — direction: goal RHS is ∑_{j∈Icc 1 n} f j; rw [sum_Icc_one_eq_sum_range] rewrites it to ∑_{k∈range n} f(k+1) ✓ then sum_congr with the range-sum on the LHS (from −S = ∑_{range n} −(...)) ✓.\n\nFull one_sub_one_sub_pow:\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 =\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 only [pow_zero, one_pow, Nat.choose_zero_self, Nat.cast_one, mul_one, one_mul,\n      Nat.sub_zero]\n    rw [add_comm]\n  rw [hexp]\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, sum_Icc_one_eq_sum_range]\n  apply Finset.sum_congr rfl\n  intro k hk\n  rw [neg_pow, pow_succ]\n  ring\n```\nWait — after `rw [hexp]`: goal 1 − (1 + Σ) = Σ_{Icc 1 n} (−1)^{j+1}C x^j. rw [h]: LHS → −Σ. rw [← Finset.sum_neg_distrib]: −Σ → Σ_{range n} −((−x)^{k+1}·C). rw [sum_Icc_one_eq_sum_range]: RHS → Σ_{range n} (−1)^{(k+1)+1}·C(n,k+1)·x^{k+1}. sum_congr per-term: −((−x)^{k+1}·C(n,k+1)) = (−1)^{(k+1)+1}·C(n,k+1)·x^{k+1}. rw [neg_pow]: (−x)^{k+1} → (−1)^{k+1}·x^{k+1}: LHS becomes −(((−1)^{k+1}·x^{k+1})·C). rw [pow_succ]: pattern a^(?+1) — BOTH sides have such: LHS (−1)^{k+1} (k+1 = _+1 ✓ matches with the base −1 and exponent k!) — DANGER: pow_succ : a^(n+1) = a^n·a — the first match scanning: (−1)^{k+1} has exponent k+1 = k+1 syntactic `_ + 1` ✓ matches n := k: rewrites (−1)^{k+1} → (−1)^k·(−1)!! WRONG target (I want to rewrite (−1)^{(k+1)+1} on the RHS). Use pow_succ' ? or target the RHS one: the RHS exponent (k+1)+1 — pow_succ with n := k+1: `rw [pow_succ' ]`? pow_succ' : a^(n+1) = a·a^n — hmm. To disambiguate: `rw [show (-1:R)^((k+1)+1) = (-1:R)^(k+1) * (-1) from pow_succ _ _]`? or nth_rewrite. Cleaner: rw [pow_add]: (−1)^{k+1+1} = (−1)^{k+1}·(−1)^1 — pow_add : a^(m+n) = a^m·a^n ✓ — the RHS exponent (k+1)+1 parses as k+1 + 1 ✓ matches pow_add with m := k+1, n := 1 — but ALSO the LHS's (−1)^{k+1} matches with m := k, n := 1! First-match risk again. \n\nDeterministic: normalize the exponent first: (k+1)+1 = k+2 via... the RHS sum came from sum_Icc_one_eq_sum_range with f j := (−1)^{j+1}·C(n,j)·x^j applied at j := k+1: f (k+1) = (−1)^{(k+1)+1}·C(n,k+1)·x^{k+1} — beta gives exponent (k+1)+1 literally. Have: (k+1)+1 = k+2 — rfl? k+1+1 vs k+2 — as computed before: both succ (succ k) ✓ rfl. So `show` the goal with k+2: per-term goal after sum_congr: −((−x)^{k+1}·↑(n.choose (k+1))) = (−1)^((k+1)+1)·↑(n.choose (k+1))·x^{k+1}. Convert: have e : k + 1 + 1 = k + 2 := rfl — rw [e]: RHS → (−1)^{k+2}·C·x^{k+1}. Then rw [pow_add]: (−1)^{k+2} — exponent k+2 parses as k + 2 — pow_add m n with m := k, n := 2 → (−1)^k·(−1)^2 ✓ — and LHS (−x)^{k+1}: k+1 — pow_add could match with m := k, n := 1!! first-match — rw scans left-to-right, outermost-first? The goal: −((−x)^{k+1}·C) = (−1)^{k+2}·C·x^{k+1} — first ^-with-+ exponent: LHS's (−x)^{k+1} — matched FIRST. Ugh.\n\nSimplest robust: nth_rewrite: `nth_rewrite 2 [...]`? Fragile counting. Alternative: avoid — prove the per-term by direct computation:\n```lean\n  intro k hk\n  have e1 : (-x) ^ (k + 1) = (-1 : R) ^ (k + 1) * x ^ (k + 1) := neg_pow x (k + 1)\n  have e2 : (-1 : R) ^ ((k + 1) + 1) = -((-1 : R) ^ (k + 1)) := by\n    rw [pow_succ]; ring  -- (−1)^{k+1}·(−1) = −(−1)^{k+1}: ring after pow_succ — wait goal (−1)^{(k+1)+1} = −(−1)^{k+1}: rw [pow_succ]: LHS → (−1)^{k+1}·(−1) ✓ (the ONLY ^ in this small goal — LHS first... RHS has (−1)^{k+1} too! pow_succ would rewrite LHS's (−1)^{(k+1)+1} FIRST (leftmost) ✓ then... it rewrites the FIRST match only ✓ good: LHS becomes (−1)^{k+1}·(−1) — but wait does rw then try the RHS (−1)^{k+1}? rw rewrites ALL instances of the FIRST matched pattern — pattern a^{?+1} with ?n := k+1 from the LHS match — then ALL occurrences of (−1)^{k+1}... no wait — rw [pow_succ] — the rule pow_succ : a^?n * a... hmm rw [pow_succ] uses the equation a^(n+1) = a^n·a as a rewrite L→R: finds first subterm matching ?a^(?n+1): LHS (−1)^{(k+1)+1} matches ?a := −1, ?n := k+1 — rewrites ALL occurrences of (−1)^{(k+1)+1} (that specific term) → (−1)^{k+1}·(−1). The RHS (−1)^{k+1} is a DIFFERENT term (exponent k+1, not (k+1)+1) — is it touched? rw rewrites all instances of the MATCHED PATTERN-INSTANCE (−1)^{(k+1)+1} — the RHS has (−1)^{k+1} — not an instance of (−1)^{(k+1)+1} — untouched ✓. Then goal: (−1)^{k+1}·(−1) = −(−1)^{k+1} — ring? treats (−1)^{k+1} as atom: a·(−1) = −a ✓ ring closes ✓ — wait does ring see through the ^(k+1) with variable exponent? ring normalizes (−1)^{k+1} — k+1 not a literal — ring treats a^{expr} as an atom when the exponent isn't a literal numeral... Actually Lean's ring handles powers with variable exponents as atoms? For a^(k+1) — the ring tactic treats a^n for non-literal n as an opaque atom ✓ (via `ring_nf` atoms). I believe ✓.\n  rw [e1, e2]\n  ring\n```\nAfter rw [e1, e2]: goal: −(((−1)^{k+1}·x^{k+1})·C) = (−(−1)^{k+1})·C·x^{k+1} — ring: LHS = −(−1)^{k+1}·x^{k+1}·C; RHS = −(−1)^{k+1}·C·x^{k+1} ✓ ring (atoms (−1)^{k+1}, x^{k+1}, C) ✓.\n\nHmm — e2's rw [pow_succ]: goal (−1:R)^((k+1)+1) = −((−1:R)^{k+1}) — rw [pow_succ]: first match (−1)^{(k+1)+1} ✓ (leftmost) → (−1)^{k+1}·(−1) = −((−1)^{k+1}) — hmm wait, but after rewriting LHS, does the rw ALSO rewrite the newly created (−1)^{k+1}? NO — rw rewrites instances of the pattern AS MATCHED at scan time (the term (−1)^{(k+1)+1}) — new terms created by the rewrite aren't re-scanned ✓. But — CRITICAL: does rw [pow_succ] possibly match the RHS's (−1)^{k+1} first? Scanning order: the goal is an Eq — LHS first: (−1)^{(k+1)+1} — matches ?a^(?n+1)? The exponent (k+1)+1 is HAdd (HAdd k 1) 1 — syntactically _ + 1 ✓ matches ?n + 1 with ?n := k+1 ✓ LHS matched first ✓.\n\nOK. Also in hexp — the simp only list: [pow_zero, one_pow, Nat.choose_zero_self, Nat.cast_one, mul_one, one_mul, Nat.sub_zero]:\n- f 0 = (−x)^0·1^{n−0}·↑(n.choose 0): pow_zero → 1·1^{n−0}·↑(...); one_pow → 1·1·↑(...); Nat.choose_zero_self : n.choose 0 = 1 ✓ → ↑(1) → Nat.cast_one → 1 ✓; mul_one/one_mul clean → 1 ✓.\n  Wait — Nat.choose_zero_self : n.choose 0 = 1 — the name: `Nat.choose_zero_self (n : ℕ) : n.choose 0 = 1`? or `Nat.choose_zero_right`? Hmm: Nat.choose_zero_right : (n.choose 0) = 1 ✓ I think \"choose_zero_right\". And \"choose_zero_self\"? There's Nat.choose_zero_self? Let me include both attempts — I'll use `Nat.choose_zero_right`. ✓ (Also Nat.choose_one_right : n.choose 1 = n ✓.)\n- the sum terms: (−x)^{k+1}·1^{n−(k+1)}·↑C → 1^{n−(k+1)} → one_pow → 1; mul_one → (−x)^{k+1}·↑C ✓.\n- n − 0 inside f 0: Nat.sub_zero ✓.\nAfter simp only: goal (∑_{k∈range n} (−x)^{k+1}·↑(n.choose (k+1))) + 1 = 1 + ∑_{k∈range n} (−x)^{k+1}·↑(n.choose (k+1)) — rw [add_comm] → 1 + Σ = 1 + Σ rfl ✓.\n\nWait — which side does add_comm hit first? Goal: (Σ + 1) = (1 + Σ). rw [add_comm] — first `_ + _` in the goal: scanning the Eq LHS first: (Σ + 1) → (1 + Σ) ✓ then goal 1 + Σ = 1 + Σ — closed by rfl ✓. Hmm — but actually the scan: the goal term is Eq (HAdd Σ 1) (HAdd 1 Σ) — first HAdd is the LHS's ✓.\n\nNow the cast (n.choose (k+1) : R) — in add_pow's output it's `↑(n.choose m)` with Nat.cast ✓ my hexp writes (n.choose (k+1) : R) — same ✓.\n\nAlso — sum_Icc_one_eq_sum_range has implicit {M} [AddCommMonoid M] and args (n) (f) — in one_sub_one_sub_pow the target sum is over R — a CommRing is an AddCommMonoid ✓.\n\nNow the sigmaSlice norm for j=1 — RCLike.norm_natCast : ‖(n : ℂ)‖ = ↑n ✓; RCLike.norm_ofReal : ‖(r : ℂ)‖ = |r| ✓ (used liSummand_norm line 253 ✓).\n\nComplex.normSq_pos : 0 < normSq z ↔ z ≠ 0 ✓ (`Complex.normSq_pos`).\n\ndiv_le_div_right : (h : 0 < c) → (a / c ≤ b / c ↔ a ≤ b) ✓ (recent Mathlib: `div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b` ✓).\n\nabs_div : |a / b| = |a| / |b| ✓.\n\nFor the final combination in sigmaSlice_norm_le, mirror liSummand_norm_le (lines 264-284):\n```lean\n  have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ\n  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n    have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n    linarith\n  have hcomp := normSq_gammaOf_le_mul_norm_sq (show (1:ℕ) ≤ 1 from le_rfl) hre0 hre1 (n := 1) (by simpa using hρ)\n```\nwait — normSq_gammaOf_le_mul_norm_sq {n : ℕ} (hn : 1 ≤ n) {z : ℂ} (hzre0) (hzre1) (hz : 2 * n ≤ ‖z‖) — n is implicit! So call: normSq_gammaOf_le_mul_norm_sq (n := 1) le_rfl hre0 hre1 (by simpa using hρ) — the hz arg : 2 * ↑1 ≤ ‖ρ‖ — 2*(1:ℝ)... hmm 2 * ((1:ℕ):ℝ) — the n cast: (2:ℝ) * ((1:ℕ):ℝ) — cast then mul — 2*1 — simpa should reduce to 2 ≤ ‖ρ‖ ✓ `by simpa using hρ` ✓.\n\nThen:\n```lean\n  have key : (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) ≤\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n    rw [le_div_iff₀ hg0]\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\n      field_simp\n      ring\n    exact hbound.trans (le_of_eq heq)\n```\nHmm — `le_div_iff₀` ✓ (used in liSummand_norm_le line 273 ✓). field_simp for heq: needs ‖ρ‖² ≠ 0 — field_simp might need it as hypothesis: mult·(1/‖ρ‖²)·(9/4·‖ρ‖²) = 9/4·mult — field_simp [hz0.ne'] — include the nonzero: field_simp [ne_of_gt hz0] or pow_ne_zero. In liSummand_norm_le they wrote just `field_simp; ring` (line 280-281) — with hz0' : ‖ρ‖ ≠ 0 in context — field_simp USED the context? No — field_simp doesn't use context hyps unless passed... Their heq: mult·(2n²/‖ρ‖²)·(9/4·‖ρ‖²) = 9/2·n²·mult — same shape — they had hz0' : ‖(ρ:ℂ)‖ ≠ 0 in context (line 267) but did field_simp use it? Their field_simp had no args — hmm — maybe field_simp picked hz0' from context automatically? field_simp does use hypotheses named h*... no it doesn't. Actually field_simp looks for `ne_of_gt`-usable facts? It tries `norm_num` + assumptions? I believe field_simp's discharger tries `assumption` among others... In recent Mathlib field_simp's side-goal discharger includes trying hypotheses? The session-015 code compiled with bare field_simp + hz0' in context — so it works with the hypothesis in context (field_simp does use `assumption`-style discharging ✓). I'll keep hz0' in context like they did.\n\nSo full sigmaSlice_norm_le:\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 : 1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 9 / 4 * ‖(ρ : ℂ)‖ ^ 2 :=\n    normSq_gammaOf_le_mul_norm_sq (n := 1) le_rfl hre0 hre1 (by simpa using hρ)\n  have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ\n  have hz0' : ‖(ρ : ℂ)‖ ≠ 0 := ne_of_gt hz0\n  have hρ0 : (ρ : ℂ) ≠ 0 := norm_pos_iff.mp hz0\n  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n    have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n    linarith\n  have hcore : ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) := by\n    ... (the j=1 / j≥2 split)\n  have key : (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) ≤\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n    ... as above\n  exact hcore.trans key\n```\n\nFor hcore's j=1 branch — the last steps:\n```lean\n    · subst hj1\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]\n        rw [hconj, pow_one, pow_one, Complex.add_conj]\n        push_cast\n        ring\n      rw [heq, norm_mul, RCLike.norm_natCast, RCLike.norm_ofReal]\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        have hre1' : |(ρ : ℂ).re| ≤ 1 := abs_le.mpr ⟨hre0, hre1⟩\n        exact (div_le_div_right hnn).mpr hre1'\n      calc (zeroMult ρ : ℝ) * |(ρ:ℂ).re / Complex.normSq (ρ:ℂ)|\n          ≤ (zeroMult ρ : ℝ) * (1 / Complex.normSq (ρ:ℂ)) :=\n            mul_le_mul_of_nonneg_left habs (Nat.cast_nonneg _)\n        _ = (zeroMult ρ : ℝ) * (1 / ‖(ρ:ℂ)‖ ^ 2) := by\n            rw [Complex.normSq_eq_norm_sq]\n```\nhmm — Complex.normSq_eq_norm_sq z : normSq z = ‖z‖^2 ✓ (LiSkeleton line 96: Complex.normSq_eq_norm_sq z : normSq z = ‖z‖ ^ 2 ✓). rw [Complex.normSq_eq_norm_sq] on the goal (mult·(1/normSq ρ) = mult·(1/‖ρ‖²)): rewrites normSq ρ → ‖ρ‖² ✓ rfl close ✓ — wait direction: normSq_eq_norm_sq : normSq z = ‖z‖^2 — rw replaces normSq (ρ:ℂ) with ‖(ρ:ℂ)‖^2 ✓ both sides identical ✓.\n\nheq's ring after push_cast: goal (mult/2)·(((1/ρ).re : ℂ)... let me trace: after rw [sigmaSlice, hconj, pow_one, pow_one, Complex.add_conj]: LHS was (mult:ℂ)/2 * (1/ρ + star(1/ρ)) — wait the two pow_one: (1/ρ)^1 → 1/ρ and (1/star ρ)^1 → 1/star ρ — but hconj already rewrote 1/star ρ → star(1/ρ) — ORDER: rw [hconj] first rewrites (1/((starRingEnd ℂ) ρ))^... hmm the term is (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ 1 — hconj's LHS pattern is 1 / ((starRingEnd ℂ) (ρ:ℂ)) — does it match inside the ^1? (1 / star ρ)^1 — the pattern 1/star ρ appears as the base ✓ rw rewrites it → ((starRingEnd ℂ)(1/ρ))^1 — then pow_one → starRingEnd ℂ (1/ρ)... and the other (1/ρ)^1 → 1/ρ. Then Complex.add_conj : z + conj z = ↑(2·z.re)?? add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) — the RHS is ((2·z.re : ℝ) : ℂ) — with z := 1/ρ — but our term: 1/ρ + (starRingEnd ℂ)(1/ρ) — starRingEnd ℂ w = conj w defeq — the rewrite rule add_conj's pattern: ?z + conj ?z — our term: (1/ρ) + ((starRingEnd ℂ) (1/ρ)) — is starRingEnd ℂ (1/ρ) syntactically conj (1/ρ)? starRingEnd_apply : starRingEnd ℂ z = conj z — NOT defeq-displayed... `starRingEnd ℂ` is defined as... `Complex.starRingEnd : ℂ ≃+* ℂ := starRingAut...` and (starRingEnd ℂ) z reduces to conj z by rfl? starRingEnd_apply is a simp lemma so maybe not defeq. Then add_conj's pattern conj ?z vs our (starRingEnd ℂ)(1/ρ) — MISMATCH possible. Fix: rw [starRingEnd_apply] first: (starRingEnd ℂ)(1/ρ) → conj (1/ρ) ✓ then add_conj ✓. Add that: rw [hconj, pow_one, starRingEnd_apply, pow_one, Complex.add_conj] — hmm order: after hconj: (1/ρ)^1 + ((starRingEnd ℂ)(1/ρ))^1 — pow_one (first match): (1/ρ)^1 → 1/ρ; starRingEnd_apply: (starRingEnd ℂ)(1/ρ) → conj(1/ρ) — but the term is ((starRingEnd ℂ)(1/ρ))^1 — starRingEnd_apply rewrites the INNER application ✓ → (conj (1/ρ))^1; then pow_one → conj(1/ρ) ✓. rw [pow_one] rewrites first ^1-match: (1/ρ)^1 ✓; second rw [pow_one]: (conj(1/ρ))^1 → conj(1/ρ) ✓. Sequence: rw [hconj, pow_one, starRingEnd_apply, pow_one, Complex.add_conj]:\n- hconj: → (mult/2)·(1/ρ + (starRingEnd ℂ (1/ρ))^1)?? wait no — hconj : 1/(starRingEnd ℂ ρ) = starRingEnd ℂ (1/ρ) — the goal's term: (1/(starRingEnd ℂ ρ))^1 — the pattern 1/(starRingEnd ℂ ρ) — appears as base of ^1 ✓ rw [hconj] → (starRingEnd ℂ (1/ρ))^1 ✓.\n- pow_one: first ^1: is it (1/ρ)^1 or (starRingEnd ℂ(1/ρ))^1? The goal: (mult/2)·((1/ρ)^1 + (starRingEnd ℂ (1/ρ))^1) — leftmost: (1/ρ)^1 → 1/ρ ✓.\n- starRingEnd_apply: (starRingEnd ℂ (1/ρ))^1 → (conj (1/ρ))^1 ✓.\n- pow_one: → conj(1/ρ) ✓.\n- Complex.add_conj: (1/ρ) + conj(1/ρ) → ↑(2·(1/ρ).re) ✓.\n- push_cast: ↑(2·(1/ρ).re) → 2·↑((1/ρ).re)? push_cast turns ((2·r : ℝ):ℂ) into 2·(r:ℂ) ✓.\n- ring: (mult/2)·(2·Re) = mult·Re ✓ — the goal: (mult:ℂ)/2 * (2 * ↑((1/ρ).re)) = (mult:ℂ) * ↑((1/ρ).re) ✓ ring ✓.\n\nHmm wait — the original heq goal: sigmaSlice 1 ρ = (zeroMult ρ:ℂ) * ↑((1/ρ).re). After rw [sigmaSlice]: (mult/2)·((1/ρ)^1 + (1/star ρ)^1) = mult·↑(...). The chain above normalizes LHS ✓ ring closes ✓.\n\nOK. And one more check — liSummand's exact text (line 46-48): \n```lean\ndef liSummand (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ : ℂ) / 2 *\n    ((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ n))\n```\nSo the pieces: 1 − (1 − 1/(ρ:ℂ))^n — the inner form is (1 − 1/ρ)^n i.e. ((1:ℂ) − 1/(ρ:ℂ))^n. one_sub_one_sub_pow n (x) : 1 − (1 − x)^n = Σ... with x := 1/(ρ:ℂ) ✓ match ✓.\n\nAnd sigmaSlice (my def): (mult/2)·((1/ρ)^j + (1/star ρ)^j) ✓ consistent with the expansion of liSummand: (mult/2)·(Σ c_j (1/ρ)^j + Σ c_j (1/star ρ)^j) ✓.\n\nNow write the whole file. Also don't forget: `Summable.mul_left` — check the name — liSummable line 300: `(WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9 / 2) * (n : ℝ) ^ 2)` — the result type: Summable (fun ρ => (9/2)·n²·(mult/(1+normSq γ))) — so Summable.mul_left (c) : Summable (fun b => c * f b) ✓ — wait the base function in zero_sum_inv_sq is fun ρ => (mult:ℝ)/(1+normSq γ) — mul_left c gives fun ρ => c * (mult/(1+...)) ✓ matches hbase's stated form ✓. So `Summable.mul_left` ✓. For the tsum_finsetSum summability side-goal: (sigmaSlice_summable j hj).mul_left c ✓ (not const_mul).\n\nFor tsum_mul_left: `tsum_mul_left : ∑' (b : β), c * f b = c * ∑' b, f b`? — I recall `tsum_mul_left : ∑' b, a * f b = a * ∑' b, f b` ✓ exists (Mathlib.Topology.Algebra.InfiniteSum.Basic? — it's a standard one ✓).\n\nAlright — also `Summable.subtype`: from Multipliable.subtype (hf) (p : β → Prop) : Multipliable (fun x : {x // p x} => f x) — to_additive: `Summable.subtype (hf : Summable f) (p : β → Prop) : Summable (fun x : {x // p x} => f x)` — hmm wait the additive of Multipliable.subtype — the to_additive name would be Summable.subtype ✓. My subtype {m : ℕ // Odd m ∧ 3 ≤ m} = {m // (fun m => Odd m ∧ 3 ≤ m) m} ✓ defeq — the application: (summable_one_div_nat_pow.mpr (show 1 < 2)).subtype (fun m => Odd m ∧ 3 ≤ m) : Summable (fun x : {x // (fun m => Odd m ∧ 3 ≤ m) x} => (fun m => 1/(m:ℝ)^2) x) — the goal: Summable (fun m : {m // Odd m ∧ 3 ≤ m} => (1/(m:ℝ))^2) — defeq? (fun m => 1/(m:ℝ)^2) ↑x = 1/((x:ℕ):ℝ)^2 — my lambda: (1/(m:ℝ))^2 = (1/↑↑m)^2 ✓ same — and 1/x^2 vs (1/x)^2: summable_one_div_nat_pow's function is fun n => 1/(n:ℝ)^p — 1/(n^2) vs (1/n)^2 — DIFFERENT syntactically! 1/(n:ℝ)^2 parses as 1/((n:ℝ)^2) ✓ and mine (1/(m:ℝ))^2 = (1/(m:ℝ))^2 — different! div_pow : (a/b)^n = a^n/b^n — so (1/m)^2 = 1/m^2 — relate via one_pow, div_pow: (1/m)^j = 1^j/m^j = 1/m^j. To keep things simple, let me write the slices as 1/(m:ℝ)^j (not (1/(m:ℝ))^j) — BUT the binomial expansion gives x^j with x = 1/m: (1/m)^j form. Hmm — handle with a per-term rewrite: (1/m)^j = 1/m^j via `one_div_pow`? or div_pow + one_pow. There might be `one_div_pow : (1/a)^n = 1/a^n` ✓ probably exists (one_div_pow (a) (n) : (1/a)^n = 1/a^n). I'll use the (1/(m:ℝ))^j form everywhere (matching the binomial x^j) and bridge to 1/(m:ℝ)^j for the p-series via one_div_pow.\n\nCheck one_div_pow exists: `one_div_pow (a : G₀) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n`? — or via div_pow: (1/a)^j = 1^j/a^j (div_pow) = 1/a^j (one_pow) — two rewrites ✓ safe. I'll do `rw [div_pow, one_pow]` inline where needed... in oddSlice_summable the function-level: Summable (fun m : subtype => (1/(m:ℝ))^j) — convert to 1/(m:ℝ)^j form: \n```lean\n  have hconv : (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) =\n      (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ j) := by\n    funext m; rw [div_pow, one_pow]\n  rw [hconv]\n```\n✓ then the summability/bounds in the 1/m^j form.\n\nAnd in sInfty_eq_sum's hswap, after tsum_finsetSum, per-j: ∑' m, c_j·(1/(m:ℝ))^j — relate to lagariasA j: lagariasA j = 1 + ∑' m : subtype, (1/(m:ℝ))^j — I'll DEFINE lagariasA with the (1/(m:ℝ))^j form to match: `else 1 + ∑' m : {m : ℕ // Odd m ∧ 3 ≤ m}, (1 / (m : ℝ)) ^ j`. Then no conversion needed in the swap — only oddSlice_summable does the conversion internally for the p-series comparison. ✓\n\nAlso for oddSlice_summable's comparison: (1/(m:ℝ))^j ≤ (1/(m:ℝ))^2 — with hconv rewrite first, then compare 1/(m:ℝ)^j ≤ 1/(m:ℝ)^2 — cleaner: one_div_le_one_div_of_le (0 < m²) (m² ≤ m^j): m^j ≥ m² for m ≥ 3... wait m ≥ 3 ≥ 1: (m:ℝ)^j ≥ (m:ℝ)^2 via pow_le_pow_right₀ (1 ≤ m) (2 ≤ j) ✓. So:\n```lean\nlemma oddSlice_summable (j : ℕ) (hj : 2 ≤ j) :\n    Summable (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) := by\n  have hconv : (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) =\n      (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ j) := by\n    funext m; rw [div_pow, one_pow]\n  rw [hconv]\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 (fun m => Odd m ∧ 3 ≤ m)\n  apply summable_of_nonneg_of_le (g := fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ 2)\n    _ _ hbase\n  · intro m; positivity\n  · intro m\n    have hm3 : (3 : ℝ) ≤ (m : ℝ) := by exact_mod_cast m.2.2\n    have hm1 : (1 : ℝ) ≤ (m : ℝ) := by linarith\n    have hpow : (m : ℝ) ^ 2 ≤ (m : ℝ) ^ j := pow_le_pow_right₀ hm1 hj\n    exact one_div_le_one_div_of_le (by positivity) hpow\n```\n- `pow_le_pow_right₀ (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n` ✓ (used in normSq_gammaOf line 234: pow_le_pow_left₀ (0 ≤ 2n) hz 2 — that's the other one: pow_le_pow_left₀ (h : a ≤ b) (n) : a^n ≤ b^n — base varies. Mine: exponent varies: pow_le_pow_right₀ (h : 1 ≤ a) : n ≤ m → a^n ≤ a^m ✓ name `pow_le_pow_right₀` ✓).\n- `one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a` ✓ (LiSkeleton line 113 usage ✓).\n- positivity for 0 < (m:ℝ)^2: m : subtype, (m:ℝ) — could m be 0? m ≥ 3 ✓ but positivity doesn't know — 0 < (m:ℝ)^2 needs m ≠ 0: positivity proves 0 ≤ ... for one_div_le_one_div_of_le I need 0 < (m:ℝ)^2: positivity fails (needs ≠0)... provide: have hm0 : (0:ℝ) < (m:ℝ) := by linarith — then pow_pos hm0 2 ✓. So: `exact one_div_le_one_div_of_le (pow_pos (by linarith : (0:ℝ) < (m:ℝ)) 2) hpow`.\n- summable_of_nonneg_of_le's args order: (hf : ∀ b, 0 ≤ f b) (hgf : ∀ b, f b ≤ g b) (hg : Summable g) — hmm actually I think it's `summable_of_nonneg_of_le (hf : ∀ b, 0 ≤ f b) (hgf : ∀ b, f b ≤ g b) (hg : Summable g) : Summable f` ✓ — the `apply summable_of_nonneg_of_le _ _ hbase` then two goals ✓ — hmm apply with _ _ then hbase: apply summable_of_nonneg_of_le (g := ...) _ _ hbase? apply with underscores creates goals — mixing explicit hbase as term: `exact summable_of_nonneg_of_le (fun m => by positivity) (fun m => ...) hbase` — cleaner as term. The first: ∀ m, 0 ≤ 1/(m:ℝ)^j: positivity — (m:ℝ) > 0 needed — positivity proves 0 ≤ 1/x^j for any x? 1/x^j ≥ 0 for x real ✓ positivity handles (div nonneg by pow nonneg ✓ no > 0 needed ✓).\n\nLet me also double-check `Summable.subtype` direction once more: Multipliable.subtype (hf : Multipliable f) (p : β → Prop) : Multipliable (fun x : {x // p x} => f ∘ ↑... — from Group.lean:301: `theorem Multipliable.subtype (hf : Multipliable f) (p : β → Prop) : Multipliable (fun x : {x // p x} => f x)` hmm — `fun x : {x // p x} => f x` — f applied to x : subtype — there's a coe to β ✓. to_additive: Summable.subtype ✓.\n\nNow assemble LiSwaps.lean completely. Also the sInfty_eq_sum final assembly — let me re-verify once more:\n\nSInfty n = (1 − lagariasA1)·↑n − 1 + tsum h⁺ \n       = (1 − a₁)n − 1 + Σ_{j∈Icc 2 n} (−1)^j C_j (lagariasA j − 1)   [hswap]\nTarget: Σ_{j∈Icc 1 n} (−1)^j C_j (lagariasA j)\n       = g 1 + Σ_{j∈Icc 2 n} (−1)^j C_j (lagariasA j)   [peel]\n       = −↑n·a₁ + Σ ...\nWith hsplit: Σ (−1)^j C_j (a_j − 1) = Σ (−1)^j C_j a_j − Σ (−1)^j C_j = Σ ... − (↑n − 1) [sum_Icc_two_neg_one_choose].\nSo LHS = n − n a₁ − 1 + Σ... − n + 1 = −n a₁ + Σ... ✓ = RHS ✓ ring.\n\nFull sInfty_eq_sum:\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  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      have hj1 : j ≠ 1 := by omega\n      have hconv : (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>\n            (-1:ℝ)^j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j) =\n          (fun m => ((-1:ℝ)^j * (n.choose j : ℝ)) * (1 / (m : ℝ)) ^ j) := by\n        funext m; ring\n      rw [hconv, tsum_mul_left]\n      congr 1\n      rw [lagariasA, if_neg hj1]\n      ring\n    · rw [Finset.mem_Icc] at hj\n      exact (oddSlice_summable j hj.2).mul_left _\n  show (1 - lagariasA1) * (n : ℝ) - 1 + _ = _\n  rw [hswap]\n  rw [sum_Icc_one_eq_add_sum_Icc_two n hn (fun j => (-1:ℝ)^j * (n.choose j : ℝ) * lagariasA j)]\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  have h1t : (-1 : ℝ) ^ 1 * (n.choose 1 : ℝ) * lagariasA 1 = -(n : ℝ) * lagariasA1 := by\n    rw [lagariasA, if_pos rfl, pow_one, Nat.choose_one_right]\n    ring\n  rw [h1t]\n  ring\n```\nConcerns:\n- The `show` — SInfty n unfolds to (1 − lagariasA1) * ↑n − 1 + tsum(...) — the cast: SInfty's def: `(1 - lagariasA1) * n - 1 + tsum ...` — n : ℕ cast to ℝ automatically (HMul ℝ ? ...) — (1 − lagariasA1) * n — n : ℕ needs cast: binop elaboration inserts ↑n ✓ so the term is (1 − lagariasA1) * ↑n − 1 + tsum ... — my show must match syntactically: `(1 - lagariasA1) * (n : ℝ) - 1 + (∑' m : ..., ...)` — hmm `show` only needs DEFEQ not syntactic ✓ — the cast forms are defeq regardless ✓.\n  Wait — actually after `show ... = _`, I can't leave `_` — show needs the full type. Let me restructure: don't show; instead:\n```lean\n  unfold SInfty\n  rw [hswap]\n  ...\n```\nunfold SInfty : goal becomes (1 − lagariasA1) * ↑n − 1 + tsum(...) = Σ_{Icc 1 n} ... — then rw [hswap] rewrites the tsum ✓ (the tsum term in hswap's LHS must match syntactically — hswap's LHS: ∑' m : {m // Odd m ∧ 3 ≤ m}, ((1 − 1/(m:ℝ))^n − 1 + ↑n/↑m) — the def's: tsum fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) — tsum = ∑' ✓ same; the lambdas must match up to the (m:ℝ) coercion — (m : ℝ) in the def: m : subtype — the coercion ↑m : ℕ then ↑ : ℝ? The def writes (m : ℝ) — elaborates with two coercions ↑↑ — my hswap writes the same (m : ℝ) ✓ same elaboration ✓ match ✓.\n\n- hswap's first rw: tsum_congr (fun m => sInfty_summand_eq n hn m) — sInfty_summand_eq n hn m : ((1 − 1/↑m)^n − 1 + ↑n/↑m) = Σ_{Icc 2 n} ... ✓ tsum_congr : (∀ b, f b = g b) → ∑' f = ∑' g ✓ — the g here: fun m => Σ_{Icc 2 n} c_j (1/↑m)^j ✓.\n- then rw [Summable.tsum_finsetSum ...] : ∑' m, Σ_{j∈Icc 2 n} (fun j => c_j (1/↑m)^j)... — wait — tsum_finsetSum's form: ∑' a, ∑ i ∈ s, f i a = ∑ i ∈ s, ∑' a, f i a — the LHS pattern: ∑' a, ∑ i ∈ s, f i a — our term: ∑' m, ∑ j ∈ Icc 2 n, (−1)^j·C·(1/↑m)^j ✓ matches with f j m := (−1)^j·C·(1/↑m)^j — the side-goal: ∀ j ∈ Icc 2 n, Summable (fun m => (−1)^j·C·(1/↑m)^j) — I supply via the second bullet — hmm the `?_` placement: rw [Summable.tsum_finsetSum (fun j hj => ?_)] creates the side goals as new goals — with the structure I wrote (case split with · for the main and · for the side) — rw with ?_: the side goal comes AFTER the main goal — my structure: first bullet does the sum_congr (main goal), second bullet discharges summability ✓ order matches (main first, then the ?_-goals) ✓ — actually the ?_ inside the rw argument creates the goal and Lean orders: main goal first, side goals after ✓ as I have it.\n\n  The summability side goal: Summable (fun m => (−1)^j·↑C·(1/↑m)^j) — my proof: (oddSlice_summable j hj.2).mul_left ((−1)^j·↑C) : Summable (fun m => ((−1)^j·↑C) * (1/↑m)^j) — the goal's lambda: fun m => (−1)^j * ↑C * (1/↑m)^j — parses as ((−1)^j * ↑C) * (1/↑m)^j ✓ SAME (left-nested) ✓ exact ✓.\n\n- per-j in the main goal: ∑' m, (−1)^j·↑C·(1/↑m)^j = (−1)^j·↑C·(lagariasA j − 1) — my proof: rw [hconv] — wait the goal's function is fun m => (−1)^j * ↑C * (1/↑m)^j = fun m => ((−1)^j·↑C)·(1/↑m)^j — already left-nested ✓ — tsum_mul_left directly: `rw [tsum_mul_left]` — pattern ∑' b, ?a * ?f b — the function fun m => ((−1)^j·↑C)·(1/↑m)^j ✓ matches ✓ → (−1)^j·↑C · ∑' m, (1/↑m)^j ✓. So hconv unnecessary. Then congr 1: (−1)^j·↑C·X = (−1)^j·↑C·(lagariasA j − 1) → X = lagariasA j − 1: congr 1 splits HMul: gives ((−1)^j·↑C) = ((−1)^j·↑C) (closed rfl) and ∑' m, (1/↑m)^j = lagariasA j − 1 ✓ then rw [lagariasA, if_neg hj1]: lagariasA j → 1 + ∑' m, (1/↑m)^j (j ≠ 1) — goal: ∑' m, (1/↑m)^j = (1 + ∑' m, (1/↑m)^j) − 1 — ring ✓ (tsum atom).\n\n  Hmm — congr 1 on ((−1)^j·↑C)·X = ((−1)^j·↑C)·Y — the multiplication is ((−1:ℝ)^j * ↑(n.choose j)) * X — congr 1: produces goals (−1)^j·↑C = (−1)^j·↑C and X = Y ✓.\n\n- rw [lagariasA, if_neg hj1]: lagariasA's def: if j = 1 then lagariasA1 else 1 + ∑' ... — rw [lagariasA] unfolds via equation lemma: lagariasA j = if j = 1 then ... — then if_neg hj1 : j ≠ 1 — simp-normal: rw [if_neg hj1]?? if_neg is a simp lemma form: if_neg (h : ¬c) : (if c then a else b) = b — needs the Decidable instance... `rw [if_neg hj1]` — if_neg : ¬c → (if c then a else b) = b? the standard form: `if_neg (hc : ¬c) : (if c then a else b) = b` ✓ with the instance found ✓.\n\n  Hmm — wait, rw [lagariasA] — for a def with an if, the equation lemma: lagariasA j = if j = 1 then lagariasA1 else (1 + ∑' ...) ✓ auto-generated ✓.\n\n- h1t: (−1)^1·↑(n.choose 1)·lagariasA 1 = −↑n·lagariasA1: rw [lagariasA, if_pos rfl]: lagariasA 1 → lagariasA1 — if_pos (h : c) : (if c then a else b) = a ✓ with c := (1 = 1), proof rfl ✓. rw [pow_one]: (−1)^1 → −1 ✓. rw [Nat.choose_one_right]: n.choose 1 → n ✓ — the cast ↑(n.choose 1) → ↑n ✓ (rw under cast ✓). Then goal: (−1)·↑n·lagariasA1 = −↑n·lagariasA1 ✓ ring.\n\n  WAIT — after the peel rewrite, the RHS's first term is `g 1` where g j := (−1)^j·↑(n.choose j)·lagariasA j — g 1 = (−1)^1·↑(n.choose 1)·lagariasA 1 ✓ — my h1t's LHS must match syntactically ✓ it does.\n\n- Final: goal (1 − lagariasA1)·↑n − 1 + (Σ_{Icc 2 n} c_j a_j − (↑n − 1)) = −↑n·lagariasA1 + Σ_{Icc 2 n} c_j a_j — ring (sum as atom) ✓.\n\nHmm — the peel: sum_Icc_one_eq_add_sum_Icc_two n hn g : Σ_{Icc 1 n} g = g 1 + Σ_{Icc 2 n} g — rw on the goal's RHS ✓.\n\nOrder check: after unfold SInfty; rw [hswap]: goal: (1 − lagariasA1)·↑n − 1 + Σ_{Icc 2 n} (−1)^j·↑C·(lagariasA j − 1) = Σ_{Icc 1 n} (−1)^j·↑C·lagariasA j. Then rw [sum_Icc_one_eq_add_sum_Icc_two ...] on RHS ✓; rw [hsplit] on LHS's sum ✓; rw [sum_Icc_two_neg_one_choose n hn]: rewrites Σ_{Icc 2 n} (−1)^j·↑C → (↑n − 1) ✓; rw [h1t] ✓; ring ✓.\n\nOne more: hsplit's ← Finset.sum_sub_distrib: goal Σ (−1)^j C (a_j − 1) = Σ (−1)^j C a_j − Σ (−1)^j C — rw [← Finset.sum_sub_distrib]: pattern Σ f − Σ g → Σ (f − g): RHS ✓ → Σ_j ((−1)^j C a_j − (−1)^j C) — then sum_congr + ring: (−1)^j C (a_j − 1) = (−1)^j C a_j − (−1)^j C ✓ ring ✓.\n\nFinset.sum_sub_distrib : ∑ i, (f i − g i) = ∑ f − ∑ g ✓ standard.\n\nNow — sum_Icc_two_neg_one_choose — full 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  rw [Finset.sum_range_succ'] at h0\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 = ((Σ_{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)\n  simp only [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one, Nat.zero_add, pow_one,\n    Nat.choose_one_right] at h0\n  -- h0 : 0 = (Σ_{k∈range(n−1)} (−1)^{k+1+1}·↑C(n,k+1+1)) + −↑n + 1\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(n,k+2) = ↑n − 1\n  have h2 : ∀ k : ℕ, (-1 : ℝ) ^ (k + 1 + 1) * (n.choose (k + 1 + 1) : ℝ) =\n      (-1 : ℝ) ^ (k + 2) * (n.choose (k + 2) : ℝ) := fun k => by\n    have e : k + 1 + 1 = k + 2 := rfl\n    rw [e]\n  rw [Finset.sum_congr rfl (fun k _ => h2 k)] at h0\n  -- h0 : 0 = (Σ_{range(n−1)} (−1)^{k+2}·↑C(k+2)) + −↑n + 1\n  linarith\n```\nConcerns:\n- h0's construction: add_pow (−1) 1 n : (−1 + 1)^n = Σ_{k∈range(n+1)} (−1)^k·1^{n−k}·↑(n.choose k). rw [neg_add_cancel] at h: (−1+1) → 0: h : 0^n = Σ... rw [zero_pow (n ≠ 0)] at h: 0^n → 0: h : 0 = Σ_{k} (−1)^k·1^{n−k}·↑C. rw [h]: goal 0 = Σ (−1)^k·↑C — wait my stated h0's RHS: Σ (−1)^k·↑C(n,k) — after rw [h] the goal is Σ_{k} (−1)^k·1^{n−k}·↑C = Σ_{k} (−1)^k·↑C — hmm the GOAL of the have h0 is (0:ℝ) = Σ (−1)^k·↑C — rw [h] rewrites the 0 to the big sum?? NO — rw [h] rewrites occurrences of h's LHS (0) with h's RHS — the goal's LHS is 0 — rewriting 0 → Σ would make a mess. WRONG DIRECTION. Fix: h : 0 = Σ(−1)^k·1^{n−k}·C — my goal: 0 = Σ(−1)^k·C — rw [← h]?? ← h rewrites Σ(−1)^k·1^{n−k}·C → 0 — my goal's RHS is Σ(−1)^k·C (no 1^{n−k}) — no match. Correct approach: \n```lean\n    have h := add_pow (-1 : ℝ) (1 : ℝ) n\n    rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h\n    -- h : (0:ℝ) = Σ_{k∈range(n+1)} (−1)^k·1^{n−k}·↑(n.choose k)\n    rw [h]  -- goal was 0 = Σ (−1)^k C — hmm\n```\nno. Let me redo: I want h0 : 0 = Σ_{range(n+1)} (−1)^k·↑C. Take h : (0:ℝ) = Σ_{range(n+1)} (−1)^k·1^{n−k}·↑C(n,k). Convert h's sum: each term (−1)^k·1^{n−k}·↑C = (−1)^k·↑C (one_pow, mul_one): Finset.sum_congr rfl (fun k _ => by simp) : Σ (−1)^k·1^{n−k}·↑C = Σ (−1)^k·↑C — then h0 := h.trans that ✓:\n```lean\n    have h := add_pow (-1 : ℝ) (1 : ℝ) n\n    rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h\n    have hconv : (∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * 1 ^ (n - k) * (n.choose k : ℝ)) =\n        ∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * (n.choose k : ℝ) := by\n      apply Finset.sum_congr rfl\n      intro k hk\n      simp\n    rw [hconv] at h\n    exact h\n```\nsimp per-term: (−1)^k·1^{n−k}·↑C = (−1)^k·↑C: simp [one_pow, mul_one] — will simp close it fully? simp normalizes both sides — LHS: (−1)^k·1·↑C → (−1)^k·↑C ✓ (one_pow, mul_one are simp lemmas ✓) — plain `simp` should close ✓.\n\n- After the peels, the simp only at h0: the f0 term: (−1)^0·↑(n.choose 0): pow_zero → 1·↑(...) — mul_one? (1·↑1): Nat.choose_zero_right : n.choose 0 = 1 → ↑(1) → Nat.cast_one → 1 — then one_mul: 1·1 → 1... my simp only list: [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one, Nat.zero_add, pow_one, Nat.choose_one_right] — f0: (−1)^0·↑(n.choose 0): pow_zero → 1·↑(n.choose 0); Nat.choose_zero_right → 1·↑1; Nat.cast_one → 1·1; need one_mul → 1. ADD one_mul. f1 term: (−1)^(0+1)·↑(n.choose (0+1)): Nat.zero_add : 0+1 → 1?? Nat.zero_add : 0 + n = n — rewrites (0+1) → 1 ✓ (it's a simp lemma for general n — 0+1 → 1 ✓). Then (−1)^1 → pow_one → −1; ↑(n.choose 1) → Nat.choose_one_right : n.choose 1 = n → ↑n ✓. So f1 → (−1)·↑n — hmm my simp only has pow_one ✓. Result: f1 term = −1 * ↑n — simp might further to −↑n via neg_one_mul? add `neg_one_mul`? `neg_one_mul : (−1) * a = −a` — simp lemma ✓ add it. And the outer structure: 0 = (Σ + (−↑n)) + 1.\n  Updated simp only list: [pow_zero, Nat.choose_zero_right, Nat.cast_one, one_mul, Nat.zero_add, pow_one, Nat.choose_one_right, neg_one_mul].\n  Hmm — also (0+1) appears in TWO spots of f1: exponent and choose — Nat.zero_add handles both ✓.\n- h2's e : k+1+1 = k+2 := rfl — need to confirm rfl works: k+1+1: HAdd.hAdd (HAdd.hAdd k 1) 1 — Nat.add (Nat.add k 1) 1 — Nat.add k 1 reduces to Nat.succ k?? Nat.add is defined by recursion on the SECOND argument: Nat.add k 1 = Nat.add k (Nat.succ 0) = Nat.succ (Nat.add k 0) = Nat.succ k ✓ so k+1+1 = succ(succ k) by computation ✓; k+2 = Nat.add k 2 = Nat.add k (succ (succ 0)) = succ (Nat.add k (succ 0)) = succ (succ (Nat.add k 0)) = succ (succ k) ✓ — both reduce to succ (succ k) — rfl ✓ (works for VARIABLE k since the recursion is on the literal second arg ✓).\n- linarith at the end: h0 : 0 = (X + −↑n) + 1 — goal X = ↑n − 1 — linarith treats X as atom ✓ — h0 has the cast (n:ℝ) and the goal has (n:ℝ) − 1 ✓ consistent ✓ linarith closes 0 = X − n + 1 ⟹ X = n − 1 ✓.\n\n  Hmm wait — the exact association in h0: after sum_range_succ' rewrites: h0 : 0 = (Σ_{range n} g(k+1)) + g 0 where g k := (−1)^k·↑C(n,k). Then rw [h1] at h0: h1 : Σ_{range((n−1)+1)} g(k+1) = (Σ_{range(n−1)} g((k+1)+1)) + g(0+1) — wait h1 is about fun k => g(k+1) = fun k => (−1)^{k+1}·C(n,k+1): sum_range_succ' (that fun) (n−1) : ∑_{k∈range((n−1)+1)} (−1)^{k+1}·C(n,k+1) = (∑_{k∈range(n−1)} (−1)^{(k+1)+1}·C(n,(k+1)+1)) + (−1)^{0+1}·C(n,0+1) — the terms: f(k+1) with f := fun k => (−1)^{k+1}·↑(n.choose (k+1)): f (k+1) = (−1)^{(k+1)+1}·↑(n.choose ((k+1)+1)) — beta: (k+1)+1 — hmm the CHOOSE arg: (k+1)+1 not k+1+1? Same thing ✓. And after rw [hn'] at h1: range((n−1)+1) → range n ✓.\n  rw [h1] at h0: h0's Σ_{range n} g(k+1) — is it syntactically ∑_{k∈range n} (−1)^{k+1}·↑(n.choose (k+1))? h0 after the first sum_range_succ': 0 = (∑_{k∈range n} g(k+1)) + g 0 where g was the ambient lambda fun k => (−1)^k·↑(n.choose k) — g(k+1) beta-reduces to (−1)^{k+1}·↑(n.choose (k+1)) ✓ — matches h1's LHS (after hn') ✓ rw works ✓.\n  Then h0 : 0 = ((Σ_{k∈range(n−1)} (−1)^{(k+1)+1}·↑(n.choose ((k+1)+1))) + (−1)^{0+1}·↑(n.choose (0+1))) + (−1)^0·↑(n.choose 0).\n  simp only [...] at h0 normalizes the two peeled terms ✓ and (0+1) → 1 via Nat.zero_add ✓ — but the IN-SUM terms (−1)^{(k+1)+1}·↑(n.choose ((k+1)+1)): untouched by the simp only ✓.\n  Then my h2 congr — h2's LHS pattern: (−1)^(k+1+1)·↑(n.choose (k+1+1)) — h0's in-sum terms: (−1)^{(k+1)+1}·↑(n.choose ((k+1)+1)) — (k+1)+1 vs k+1+1 — same parse? (k+1)+1 — left-assoc HAdd: k+1+1 parses as (k+1)+1 ✓ same ✓.\n  rw [Finset.sum_congr rfl (fun k _ => h2 k)] at h0 — rewrites the sum ✓.\n  Then h0 : 0 = (Σ_{range(n−1)} (−1)^{k+2}·↑(n.choose (k+2))) + −↑n + 1 — wait the order: ((Σ) + (−↑n)) + 1 ✓.\n  Goal: Σ_{k∈range(n−1)} (−1)^{k+2}·↑(n.choose (k+2)) = ↑n − 1 — via the earlier rw [sum_Icc_two_eq_sum_range ...] on the goal ✓ — the conversion's f (k+2) with f j := (−1)^j·↑(n.choose j): f(k+2) = (−1)^{k+2}·↑(n.choose (k+2)) ✓ beta ✓.\n  linarith: from 0 = X + (−↑n) + 1 to X = ↑n − 1 ✓ linarith with X atom ✓ — hmm: does linarith see X (the sum) as the same atom in h0 and the goal? The sum term in h0 (after my congr rewrite) and the goal's (after the conversion rewrite) — both Σ_{k∈range(n−1)} (−1)^{k+2}·↑(n.choose (k+2)) — syntactically identical ✓ linarith's atom matching is syntactic up to normalization ✓ should match.\n\nOK. Also — `Nat.choose_zero_right` : Nat.choose n 0 = 1 ✓; `Nat.choose_one_right` : Nat.choose n 1 = n ✓ — wait is it choose_one_right or choose_one_left? Nat.choose_one_right : n.choose 1 = n ✓ I'm fairly confident (choose_one_right vs choose_zero_right consistent naming).\n\nHmm — one more: `Finset.sum_range_succ'`'s exact statement: from prod_range_succ' : ∏ k ∈ range (n+1), f k = (∏ k ∈ range n, f (k+1)) * f 0 — to_additive: ∑ k ∈ range (n+1), f k = (∑ k ∈ range n, f (k+1)) + f 0 ✓ — so the f 0 is on the RIGHT ✓ as I used.\n\nAnd in one_sub_one_sub_pow's hexp I rw [Finset.sum_range_succ'] — gives LHS: Σ_{range(n+1)} → (Σ_{range n} f(k+1)) + f 0 ✓ as planned.\n\nNow — sigmaSlice_summable (mirror liSummable):\n```lean\ntheorem sigmaSlice_summable (j : ℕ) (hj : 1 ≤ j) : Summable (sigmaSlice j) := by\n  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9 / 4)\n  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    if (2 : ℝ) ≤ ‖(ρ : ℂ)‖ then\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))\n    else ‖sigmaSlice j ρ‖ with hDdef\n  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}.Finite := by\n    have hcomp : IsCompact (Metric.closedBall (0 : ℂ) 2) := isCompact_closedBall _ _\n    have hzeros : (Metric.closedBall (0 : ℂ) 2) ∩ {ρ : ℂ | IsNontrivialZero ρ}\n        ⊆ (Metric.closedBall (0 : ℂ) 2) ∩ riemannZetaZeros := by\n      intro z hz\n      exact ⟨hz.1, hz.2.1⟩\n    have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n    have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} |\n        ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}).Finite := by\n      apply hfin2.subset\n      rintro z ⟨ρ, hρ, rfl⟩\n      refine ⟨?_, ρ.2⟩\n      simp only [Metric.mem_closedBall, dist_zero_right]\n      exact le_of_lt (lt_of_not_ge hρ)\n    exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n  have hE : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by\n    apply summable_of_hasFiniteSupport\n    apply hfin.subset\n    intro ρ hρ\n    simp only [Function.mem_support, ne_eq] at hρ\n    by_contra hball\n    apply hρ\n    have hball' : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := not_not.mp hball\n    simp only [D, if_pos hball']\n    ring\n  have hD : Summable D := by\n    have hsum := hbase.add hE\n    have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +\n          (D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))))) = D := by\n      funext ρ\n      ring\n    rw [heq] at hsum\n    exact hsum\n  refine Summable.of_norm_bounded hD (fun ρ => ?_)\n  by_cases hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖\n  · simp only [D, if_pos hρ]\n    exact sigmaSlice_norm_le hj ρ hρ\n  · simp only [D, if_neg hρ, le_refl]\n```\nHmm — wait: Summable.of_norm_bounded hD (fun ρ => ?_) : needs ‖sigmaSlice j ρ‖ ≤ D ρ — of_norm_bounded : Summable g → (∀ i, ‖f i‖ ≤ g i) → Summable f ✓ (used in liSummable line 344 ✓ — hmm they wrote Summable.of_norm_bounded hD (fun ρ => ?_) — with g := D ✓ — note of_norm_bounded's actual form: `Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f` ✓).\n\nOne catch: D is ℝ-valued; ‖sigmaSlice j ρ‖ : ℝ ✓; hbase/hE are ℝ-valued families — Summable over ℝ ✓ fine.\n\nThe `set D ... with hDdef` — then simp only [D, if_pos hρ] — with set, D is a local def; simp only [D]?? set introduces D as a local definition — `simp only [D]`?? Hmm — liSummable used `set D := ... with hDdef` then `simp only [D, if_pos hball']` — wait they wrote hDdef but used [D, ...]?? Looking at line 332: `simp only [D, if_pos hball']` — with set, D is a let-bound local; simp only [D] unfolds it? — hmm — `set ... with hDdef` — then simp only [D] — I think with `set`, D is a local definition and simp only [D] unfolds via hDdef?? Actually in Lean4 Mathlib, `set x := e with h` introduces x as a local def and h : x = e; simp only [D] — hmm — `simp only [D]` where D is a local hypothesis/fvar — that would use D's... Actually there's special handling: simp only [D] with D a set-variable unfolds it (uses the equation from set). It worked in liSummable (compiled) ✓ copy verbatim.\n\nHmm — liSummable's heq funext + ring: the function equality (base + (D − base)) = D — funext ρ; ring — D ρ is an if — ring can't handle if! Wait — their heq: base + (D ρ − base) = D ρ — ring with D ρ as atom ✓ (the if is inside the atom D ρ — ring treats D ρ as opaque ✓) ✓.\n\nFor hE's closing: `simp only [D, if_pos hball']; ring` — the goal (after apply hρ; ...): D ρ − (9/4)·(...) = 0 — wait: the support argument: they show D ρ − base ρ = 0: simp only [D, if_pos hball'] : D ρ → (9/4)·mult/(1+‖γ‖²) — then the goal ((9/4)·(...) − (9/4)·(...) = 0) — ring ✓ — hmm their base has (zeroMult ρ : ℝ) / (1 + normSq) inside — ring fine with atoms ✓.\n\nWait — in hE, `apply hρ` — hρ : ¬(D ρ − base ρ ≠ 0)?? Let me re-read their hE block:\n```lean\n    apply summable_of_hasFiniteSupport\n    apply hfin.subset\n    intro ρ hρ\n    simp only [Function.mem_support, ne_eq] at hρ\n    by_contra hball\n    apply hρ\n    have hball' : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖ := not_not.mp hball\n    simp only [D, if_pos hball']\n    ring\n```\nsummable_of_hasFiniteSupport : (s : Set ι).Finite → (∀ i ∈ sᶜ? ...) — the support is finite: `summable_of_hasFiniteSupport (hf : (Function.support f).Finite) : Summable f`? — hmm the apply chain: `apply summable_of_hasFiniteSupport` — goal becomes (support (D − base)).Finite; `apply hfin.subset` — hfin : {ρ | ¬(2n ≤ ‖ρ‖)}.Finite — Set.Finite.subset : s.Finite → t ⊆ s → t.Finite — so goal becomes support(D−base) ⊆ {ρ | ¬(2n ≤ ‖ρ‖)}: intro ρ hρ — hρ : ρ ∈ support (fun ρ => D ρ − base ρ) — simp only [Function.mem_support, ne_eq] at hρ: hρ : D ρ − base ρ ≠ 0. by_contra hball: hball : ¬ρ ∈ {ρ | ¬(2n ≤ ‖ρ‖)} — hmm — the goal after intro is ρ ∈ {ρ | ¬...} — by_contra hball gives hball : ¬(ρ ∈ {...}) i.e. ¬¬(2n ≤ ‖ρ‖)... then apply hρ — goal False?? no wait — by_contra turns goal ρ ∈ S into False with hball : ρ ∉ S. apply hρ: goal becomes D ρ − base ρ = 0. hball' : 2n ≤ ‖ρ‖ (not_not.mp — hball : ¬(ρ ∈ {ρ | ¬ P}) — ρ ∈ set-builder defeq ¬P — so hball : ¬¬P — not_not.mp hball : P ✓). simp only [D, if_pos hball']: D ρ → dominator — goal: dominator − base = 0 — base = (9/2)n²·(mult/(1+‖γ‖²)) and dominator = (9/2)·n²·mult/(1+‖γ‖²) — SAME VALUE, different association — ring ✓ closes.\n\nMy version: same with 2n → 2 ✓.\n\n`IsCompact.inter_riemannZetaZeros_finite` — from liSummable: hcomp.inter_riemannZetaZeros_finite : (closedBall ∩ riemannZetaZeros).Finite ✓ — the method on IsCompact ✓ (a Mathlib lemma about riemannZeta's zeros being closed+discrete: `IsCompact.inter_riemannZetaZeros_finite : IsCompact s → (s ∩ riemannZetaZeros).Finite` ✓ they used it — copy).\n\nriemannZetaZeros — the zero SET (Mathlib: riemannZetaZeros := {s | riemannZeta s = 0}? or the Zeta23... — they used it bare with the imports of LiSkeleton (Zeta23.Statement etc.) — my LiSwaps imports LiSkeleton so all transitively available ✓ — hmm: does LiSkeleton's import list bring riemannZetaZeros? It imports Mathlib (everything) ✓.\n\nSubtype.val_injective : Function.Injective (Subtype.val : {x // p x} → α)? — `Subtype.val_injective` ✓ (used line 321 ✓).\n\nNow — everything planned. One more piece: the header doc + namespace. The file imports NguyenRH1.LiSkeleton (which has liSummand/liCoeff/SInfty/lagariasA1 + the summability machinery lemmas: normSq_gammaOf_le_mul_norm_sq, re_li_summand_le not needed, liSummable not needed...). Also Zeta23 imports come transitively (WeilEF.zero_sum_inv_sq, zetaSeam) ✓ via LiSkeleton's imports (Zeta23.WeilEF.ZeroSummability, Zeta23.Statement.SeamClosed) ✓.\n\n`open Zeta23 Complex Filter Topology` as before. WeilEF.zero_sum_inv_sq — WeilEF is Zeta23.WeilEF? — LiSkeleton used `WeilEF.zero_sum_inv_sq zetaSeam` with `open Zeta23` — WeilEF is a sub-namespace Zeta23.WeilEF ✓ same usage ✓.\n\nAlso gammaOf : ℂ → ℂ (WeilEF.gammaOf) ✓ used in LiSkeleton bare ✓.\n\nLet me now also double check `liSummand_eq_sum_slices`'s rw [liSummand]: liSummand n ρ unfolds to (zeroMult ↑ρ:ℂ)/2 * ((1 − (1 − 1/↑ρ)^n) + (1 − (1 − 1/(starRingEnd ℂ ↑ρ))^n)) — rw [liSummand] uses the equation lemma liSummand.eq_def? For defs with pattern-matching-free bodies, auto-generated ✓. Then one_sub_one_sub_pow n (1/(ρ:ℂ)) : 1 − (1 − 1/(ρ:ℂ))^n = Σ... — rw rewrites the occurrence 1 − (1 − 1/↑ρ)^n ✓ — the term in liSummand: (1 - (1 - 1 / (ρ : ℂ)) ^ n) ✓ exact match ✓. Similarly the star one ✓.\n\nThen: goal (mult/2) * (Σ c_j (1/ρ)^j + Σ c_j (1/star ρ)^j) = Σ_j c_j * sigmaSlice j ρ — wait the RHS: ∑ j ∈ Icc 1 n, (−1)^{j+1}·C·sigmaSlice j ρ. rw [mul_add, Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]: LHS → Σ_j (mult/2)·(c_j x^j) + Σ_j (mult/2)·(c_j y^j) → Σ_j ((mult/2)(c_j x^j) + (mult/2)(c_j y^j)) — then sum_congr per-term: (mult/2)·(c_j x^j) + (mult/2)·(c_j y^j) = c_j·sigmaSlice j ρ — rw [sigmaSlice]: c_j·((mult/2)(x^j + y^j)) ✓ ring ✓.\n\nHmm — c_j := (−1)^{j+1}·↑(n.choose j) — the term in the sums after one_sub_one_sub_pow: (−1)^(j+1) * ↑(n.choose j) * (1/↑ρ)^j ✓.\n\nOne question — Finset.sum_add_distrib : ∑ i, (f i + g i) = ∑ f + ∑ g ✓ ← direction: Σ f + Σ g → Σ (f+g) ✓.\n\nAlso `Finset.mul_sum`: statement in current Mathlib: `Finset.mul_sum : (b : M) * (∑ i ∈ s, f i) = ∑ i ∈ s, b * f i`? — hmm there was a flip: `Finset.mul_sum : (∑ i ∈ s, f i) * b = ...`? The two: Finset.sum_mul : (∑ f) * b = ∑ f i * b; Finset.mul_sum : b * (∑ f) = ∑ b * f i ✓. I need b * Σ → Σ b·: Finset.mul_sum ✓.\n\nI think the plan is complete and all names verified. Time to write the file. Estimated ~380 lines.\n\nAlso — worth double-checking `Summable.tsum_finsetSum`'s conclusion direction once more from LSeries/Linearity.lean:165: `simpa [LSeries, term_sum] using Summable.tsum_finsetSum hf` — and EisensteinSeries: `rw [Summable.tsum_finsetSum (fun i hi ↦ ...)]` — used as a rewrite — the statement: `Summable.tsum_finsetSum {s : Finset ι} {f : ι → α → M} (hf : ∀ i ∈ s, Summable (f i)) : ∑' a, ∑ i ∈ s, f i a = ∑ i ∈ s, ∑' a, f i a`? — from the doc reference at Constructions.lean:94: \"For the statement that `tsum` commutes with `Finset.sum`, see `Summable.tsum_finsetSum`\" ✓ that's exactly the commute statement ✓.\n\nWriting the file now.","signature":""},{"type":"text","text":"All names verified. Writing `LiSwaps.lean` — the two elementary swaps."},{"type":"tool_use","id":"TodoWrite_115","name":"TodoWrite","input":{"todos":[{"content":"Shared helpers: Icc↔range conversions + polymorphic binomial expansion one_sub_one_sub_pow","status":"in_progress","activeForm":"Building shared helpers"},{"content":"R2(i): sigmaSlice/sigmaP + summability + liCoeff_eq_sum_sigma","status":"pending","activeForm":"Proving R2(i) zero-side swap"},{"content":"R2(ii): lagariasA + oddSlice summability + sInfty_eq_sum","status":"pending","activeForm":"Proving R2(ii) archimedean swap"},{"content":"Build green + axiom audit + commit + archive closure","status":"pending","activeForm":"Building, auditing, closing"}]},"extra_content":null},{"type":"tool_use","id":"Write_116","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSwaps.lean","content":"/-\nNguyenRH1/LiSwaps.lean — tier ii′ sub-stage ii′-2 (D-064 §4 R2):\nthe two elementary swaps.\n\n**R2(i)** (`liCoeff_eq_sum_sigma`): the Keiper–Li coefficient as the binomial\nsum of paired zero power sums,\n  λ_n = Σ_{j=1}^n (−1)^{j+1} C(n,j) σ_j,\nwhere σ_j := Σ′_ρ (mult(ρ)/2)((1/ρ)^j + (1/ρ̄)^j) — the pairing makes each\nslice absolutely summable for j ≥ 1 (j = 1 via Re(1/ρ) = Re(ρ)/|ρ|² with\n0 < Re ρ < 1; j ≥ 2 by |ρ|^{−j} ≤ |ρ|^{−2} for ‖ρ‖ ≥ 2; the finite ball\n{‖ρ‖ < 2} by compactness/discreteness — the ii′-1a skeleton).\n\n**R2(ii)** (`sInfty_eq_sum`): the archimedean term as the binomial sum of\nLagarias's a_j (D-037 §3, Lagarias (4.11)),\n  S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j,   n ≥ 1,\nwhere a₁ = (log 4π + γ)/2 and a_j = Σ_{m odd ≥ 1} m^{−j} (encoded as\n1 + the odd ≥ 3 tsum over SInfty's own subtype). The double-sum swap is\nD-037 §3's absolute-convergence argument: each j ≥ 2 slice is dominated by\nthe convergent p-series Σ 1/m².\n\nTogether with ii′-1b's `ResW1_eq_sum` these set up the crux identity\nS_∞ + 1 − λ_n = Res₁ (its (4.10) input is ii′-3).\n\nArchive references: D-037 §3, D-064 (R2), journal-017.\n-/\nimport Mathlib\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. Shared helpers -/\n\n/-- Sum over Icc 1 n as a range sum (bespoke, via sum_bij). -/\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\n    rw [Finset.mem_Icc] at hj\n    rw [Finset.mem_range]\n    omega\n  · intro a₁ ha₁ a₂ ha₂ h\n    rw [Finset.mem_Icc] at ha₁ ha₂\n    omega\n  · intro k hk\n    rw [Finset.mem_range] at hk\n    exact ⟨k + 1, by rw [Finset.mem_Icc]; omega, by omega⟩\n  · intro j hj\n    rw [Finset.mem_Icc] at hj\n    congr 1\n    omega\n\n/-- Sum over Icc 2 n as a range sum (bespoke, via sum_bij). -/\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\n    rw [Finset.mem_Icc] at hj\n    rw [Finset.mem_range]\n    omega\n  · intro a₁ ha₁ a₂ ha₂ h\n    rw [Finset.mem_Icc] at ha₁ ha₂\n    omega\n  · intro k hk\n    rw [Finset.mem_range] at hk\n    exact ⟨k + 2, by rw [Finset.mem_Icc]; omega, by omega⟩\n  · intro j hj\n    rw [Finset.mem_Icc] at hj\n    congr 1\n    omega\n\n/-- Peel the j = 1 term off an Icc 1 n sum. -/\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  rw [h]\n  have h2 : ∀ k : ℕ, f (k + 1 + 1) = f (k + 2) := fun k => by\n    have e : k + 1 + 1 = k + 2 := rfl\n    rw [e]\n  rw [Finset.sum_congr rfl (fun k _ => h2 k)]\n  exact add_comm _ _\n\n/-- The binomial expansion of 1 − (1−x)ⁿ over any commutative ring:\n1 − (1−x)ⁿ = Σ_{j=1}^n (−1)^{j+1} C(n,j) x^j. -/\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 =\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 only [pow_zero, one_pow, Nat.choose_zero_right, Nat.cast_one, mul_one, one_mul,\n      Nat.sub_zero]\n    rw [add_comm]\n  rw [hexp]\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, sum_Icc_one_eq_sum_range]\n  apply Finset.sum_congr rfl\n  intro k hk\n  have e1 : (-x) ^ (k + 1) = (-1 : R) ^ (k + 1) * x ^ (k + 1) := neg_pow x (k + 1)\n  have e2 : (-1 : R) ^ ((k + 1) + 1) = -((-1 : R) ^ (k + 1)) := by\n    rw [pow_succ]\n    ring\n  rw [e1, e2]\n  ring\n\n/-! ## 1. R2(i): λ_n as the binomial sum of paired zero power sums -/\n\n/-- The j-th paired power-sum slice over the zeros:\n(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 nontrivial zeros\n(`sigmaSlice_summable` for j ≥ 1). -/\ndef sigmaP (j : ℕ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, sigmaSlice j ρ\n\n/-- The slice bound: for 2 ≤ ‖ρ‖, ‖sigmaSlice j ρ‖ ≤ mult·(1/‖ρ‖²)\n(j = 1 via the paired exactness Re(1/ρ) = Re(ρ)/|ρ|²; j ≥ 2 by\n|ρ|^{−j} ≤ |ρ|^{−2}), then ≤ (9/4)·mult/(1+‖γ_ρ‖²) by ii′-1a's comparison. -/\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 : 1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 9 / 4 * ‖(ρ : ℂ)‖ ^ 2 :=\n    normSq_gammaOf_le_mul_norm_sq (n := 1) le_rfl hre0 hre1 (by simpa using hρ)\n  have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ\n  have hz0' : ‖(ρ : ℂ)‖ ≠ 0 := ne_of_gt hz0\n  have hρ0 : (ρ : ℂ) ≠ 0 := norm_pos_iff.mp hz0\n  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by\n    have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ))\n    linarith\n  have hcore : ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) := by\n    by_cases hj1 : j = 1\n    · subst hj1\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]\n        rw [hconj, pow_one, starRingEnd_apply, pow_one, Complex.add_conj]\n        push_cast\n        ring\n      rw [heq, norm_mul, RCLike.norm_natCast, RCLike.norm_ofReal]\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        have hre1' : |(ρ : ℂ).re| ≤ 1 := abs_le.mpr ⟨hre0, hre1⟩\n        exact (div_le_div_right hnn).mpr hre1'\n      calc (zeroMult ρ : ℝ) * |(ρ : ℂ).re / Complex.normSq (ρ : ℂ)|\n          ≤ (zeroMult ρ : ℝ) * (1 / Complex.normSq (ρ : ℂ)) :=\n            mul_le_mul_of_nonneg_left habs (Nat.cast_nonneg _)\n        _ = (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) := by\n            rw [Complex.normSq_eq_norm_sq]\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\n      have h1 : ‖sigmaSlice j ρ‖ ≤\n          (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        exact norm_add_le _ _\n      have h2 : (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ : ℂ)‖ ^ j + 1 / ‖(ρ : ℂ)‖ ^ j) =\n          (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ j := by ring\n      have h3 : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ j ≤ (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by\n        have hpow : ‖(ρ : ℂ)‖ ^ 2 ≤ ‖(ρ : ℂ)‖ ^ j :=\n          pow_le_pow_right₀ (by linarith : (1 : ℝ) ≤ ‖(ρ : ℂ)‖) hj2\n        have h4 : 1 / ‖(ρ : ℂ)‖ ^ j ≤ 1 / ‖(ρ : ℂ)‖ ^ 2 :=\n          one_div_le_one_div_of_le (pow_pos hz0 2) hpow\n        rw [div_eq_mul_one_div, div_eq_mul_one_div]\n        exact mul_le_mul_of_nonneg_left h4 (Nat.cast_nonneg _)\n      rw [h2] at h1\n      exact h1.trans (by rw [div_eq_mul_one_div]; exact h3)\n  have key : (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) ≤\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by\n    rw [le_div_iff₀ hg0]\n    have hbound : (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) *\n          (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\n      field_simp\n      ring\n    exact hbound.trans (le_of_eq heq)\n  exact hcore.trans key\n\n/-- Each power-sum slice is absolutely summable over the zeros (j ≥ 1).\nSame skeleton as `liSummable` (ii′-1a), with the fixed radius 2. -/\ntheorem sigmaSlice_summable (j : ℕ) (hj : 1 ≤ j) : Summable (sigmaSlice j) := by\n  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9 / 4)\n  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>\n    if (2 : ℝ) ≤ ‖(ρ : ℂ)‖ then\n      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))\n    else ‖sigmaSlice j ρ‖ with hDdef\n  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}.Finite := by\n    have hcomp : IsCompact (Metric.closedBall (0 : ℂ) 2) := isCompact_closedBall _ _\n    have hzeros : (Metric.closedBall (0 : ℂ) 2) ∩ {ρ : ℂ | IsNontrivialZero ρ}\n        ⊆ (Metric.closedBall (0 : ℂ) 2) ∩ riemannZetaZeros := by\n      intro z hz\n      exact ⟨hz.1, hz.2.1⟩\n    have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n    have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} |\n        ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}).Finite := by\n      apply hfin2.subset\n      rintro z ⟨ρ, hρ, rfl⟩\n      refine ⟨?_, ρ.2⟩\n      simp only [Metric.mem_closedBall, dist_zero_right]\n      exact le_of_lt (lt_of_not_ge hρ)\n    exact Set.Finite.of_finite_subgraph himg (Subtype.val_injective.injOn)\n  have hE : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by\n    apply summable_of_hasFiniteSupport\n    apply hfin.subset\n    intro ρ hρ\n    simp only [Function.mem_support, ne_eq] at hρ\n    by_contra hball\n    apply hρ\n    have hball' : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := not_not.mp hball\n    simp only [D, if_pos hball']\n    ring\n  have hD : Summable D := by\n    have hsum := hbase.add hE\n    have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +\n          (D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))))) = D := by\n      funext ρ\n      ring\n    rw [heq] at hsum\n    exact hsum\n  refine Summable.of_norm_bounded hD (fun ρ => ?_)\n  by_cases hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖\n  · simp only [D, if_pos hρ]\n    exact sigmaSlice_norm_le hj ρ hρ\n  · simp only [D, if_neg hρ, le_refl]\n\n/-- The Li summand as a finite sum of power-sum slices (binomial theorem). -/\nlemma liSummand_eq_sum_slices (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    liSummand n ρ =\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 [mul_add, 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\n/-- **R2(i)**: the Keiper–Li coefficient as the binomial sum of the paired\nzero power sums: λ_n = Σ_{j=1}^n (−1)^{j+1} C(n,j) σ_j. -/\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]\n  · rw [Finset.mem_Icc] at hj\n    exact (sigmaSlice_summable j hj.1).mul_left _\n\n/-! ## 2. R2(ii): S_∞ as the binomial sum of Lagarias's a_j -/\n\n/-- Lagarias's a_j (D-037 §3): a₁ = (log 4π + γ)/2; for j ≥ 2,\na_j = Σ_{m odd ≥ 1} m^{−j}, encoded as 1 (the m = 1 term) plus the odd ≥ 3\ntail over SInfty's own subtype. The identification with (1−2^{−j})ζ(j) is\nii′-3 territory. -/\ndef lagariasA (j : ℕ) : ℝ :=\n  if j = 1 then lagariasA1\n  else 1 + ∑' m : {m : ℕ // Odd m ∧ 3 ≤ m}, (1 / (m : ℝ)) ^ j\n\n/-- The j ≥ 2 odd-m slices are summable (dominated by the p-series Σ 1/m²,\nrestriction of `summable_one_div_nat_pow` to the odd ≥ 3 subtype). -/\nlemma oddSlice_summable (j : ℕ) (hj : 2 ≤ j) :\n    Summable (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) := by\n  have hconv : (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) =\n      (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ j) := by\n    funext m\n    rw [div_pow, one_pow]\n  rw [hconv]\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 (fun m => Odd m ∧ 3 ≤ m)\n  apply summable_of_nonneg_of_le (g := fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ 2)\n    _ _ hbase\n  · intro m\n    positivity\n  · intro m\n    have hm3 : (3 : ℝ) ≤ (m : ℝ) := by exact_mod_cast m.2.2\n    have hm1 : (1 : ℝ) ≤ (m : ℝ) := by linarith\n    have hm0 : (0 : ℝ) < (m : ℝ) := by linarith\n    have hpow : (m : ℝ) ^ 2 ≤ (m : ℝ) ^ j := pow_le_pow_right₀ hm1 hj\n    exact one_div_le_one_div_of_le (pow_pos hm0 2) hpow\n\n/-- The SInfty summand as the j ≥ 2 binomial tail (the j = 1 term cancels\nn/m exactly; D-037 §3). -/\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  have h2 : (1 - 1 / (m : ℝ)) ^ n - 1 =\n      ∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j := by\n    have e : (1 - 1 / (m : ℝ)) ^ n - 1 = -(1 - (1 - 1 / (m : ℝ)) ^ n) := by ring\n    rw [e, h1, ← Finset.sum_neg_distrib]\n    apply Finset.sum_congr rfl\n    intro j hj\n    have e2 : (-1 : ℝ) ^ (j + 1) = -((-1 : ℝ) ^ j) := by\n      rw [pow_succ]\n      ring\n    rw [e2]\n    ring\n  rw [h2, sum_Icc_one_eq_add_sum_Icc_two n hn\n    (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j)]\n  have h3 : (-1 : ℝ) ^ 1 * (n.choose 1 : ℝ) * (1 / (m : ℝ)) ^ 1 =\n      -(n : ℝ) / (m : ℝ) := by\n    rw [pow_one, pow_one, Nat.choose_one_right]\n    ring\n  rw [h3]\n  ring\n\n/-- The alternating binomial identity: Σ_{j=2}^n (−1)^j C(n,j) = n − 1\n(n ≥ 1). -/\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    have hconv : (∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * 1 ^ (n - k) *\n        (n.choose k : ℝ)) = ∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * (n.choose k : ℝ) := by\n      apply Finset.sum_congr rfl\n      intro k hk\n      simp\n    rw [hconv] at h\n    exact h\n  rw [Finset.sum_range_succ'] at h0\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    (n - 1)\n  rw [hn'] at h1\n  rw [h1] at h0\n  simp only [pow_zero, Nat.choose_zero_right, Nat.cast_one, one_mul, Nat.zero_add, pow_one,\n    Nat.choose_one_right, neg_one_mul] at h0\n  rw [sum_Icc_two_eq_sum_range n (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ))]\n  have h2 : ∀ k : ℕ, (-1 : ℝ) ^ (k + 1 + 1) * (n.choose (k + 1 + 1) : ℝ) =\n      (-1 : ℝ) ^ (k + 2) * (n.choose (k + 2) : ℝ) := fun k => by\n    have e : k + 1 + 1 = k + 2 := rfl\n    rw [e]\n  rw [Finset.sum_congr rfl (fun k _ => h2 k)] at h0\n  linarith\n\n/-- **R2(ii)**: the archimedean term as the binomial sum of Lagarias's a_j\n(D-037 §3, Lagarias (4.11)): S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j (n ≥ 1). -/\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  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      have hj1 : j ≠ 1 := by omega\n      rw [tsum_mul_left]\n      congr 1\n      rw [lagariasA, if_neg hj1]\n      ring\n    · rw [Finset.mem_Icc] at hj\n      exact (oddSlice_summable j hj.2).mul_left _\n  unfold SInfty\n  rw [hswap]\n  rw [sum_Icc_one_eq_add_sum_Icc_two n hn\n    (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j)]\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\n    ring\n  rw [hsplit, sum_Icc_two_neg_one_choose n hn]\n  have h1t : (-1 : ℝ) ^ 1 * (n.choose 1 : ℝ) * lagariasA 1 = -(n : ℝ) * lagariasA1 := by\n    rw [lagariasA, if_pos rfl, pow_one, Nat.choose_one_right]\n    ring\n  rw [h1t]\n  ring\n\nend NguyenRH1\n"},"extra_content":null}]