[{"type":"thinking","thinking":"Session 018: ii′-2 — R2(i)/(ii) elementary swaps:\n(i) λ_n = Σ_j (−1)^{j+1}C(n,j)σ_j — binomial expansion of the liSummand paired form + swap of finite j-sum with paired zero tsum\n(ii) S_∞ = Σ_j C(n,j)τ_{j−1} — the Lean SInfty odd-m tsum ↔ binomial/τ form\n\nLet me start by reading the relevant definitions: LiSkeleton.lean's liSummand/liCoeff (paired form, session 015), SInfty definition, and D-064 §4 R2 for the exact design. Also D-037 §3 for the swap argument.\n\nLet me read LiSkeleton.lean fully to understand the current state (liSummand, liCoeff, SInfty, Sf, etc.), and D-064's R2 section (I read lines 142-171 already — R2 details). Let me re-read the R2 part:\n\nFrom D-064 §4:\n- R2(i): λ_n = Σ_j (−1)^{j+1}C(n,j)σ_j — binomial expansion of the summand + swap finite j-sum with paired zero sum (pair bound + zero_sum_inv_sq comparison; j = 1 term needs the paired form — same machinery as the §1 fix). ELEMENTARY-side.\n- R2(ii): S_∞(n) = Σ_j C(n,j)τ_{j−1} — identity between the Lean SInfty odd-m tsum and the binomial/τ form (Lagarias (4.11) ↔ (4.7) via digamma partial fractions (4.19)–(4.22); the double-sum swap is D-037 §3's absolute-convergence argument). ELEMENTARY-side (tier-(i)-class).\n\nFirst I need to see:\n1. LiSkeleton.lean — the liSummand/liCoeff paired form, SInfty def, Sf def, and what σ_j/τ_j would be.\n2. D-037 §3 — the S_∞ ↔ τ identity and its absolute convergence.\n3. Lagarias paper §4 for (4.10), (4.11), (4.7), (4.19)-(4.22) — definitions of σ_j, τ_j, η_j.\n\nActually wait — do σ_j and τ_j exist in Lean yet? Probably not — ii′-2 must DEFINE them:\n- σ_j := Σ_ρ mult·ρ^{−j} (paired power sums of zeros) — for j ≥ 1. Hmm, for j = 1: Σ mult/ρ — NOT absolutely summable — needs the paired form: Σ_ρ mult·(1/ρ + 1/ρ̄)/2 = Σ mult·Re(1/ρ) = Σ mult·σ/|ρ|²... The paired form: σ_j paired = Σ mult·(ρ^{−j} + ρ̄^{−j})/2. For j ≥ 2 absolutely summable via zero_sum_inv_sq; for j = 1 the pairing gives |1/ρ + 1/ρ̄|/2 = |Re ρ|/|ρ|² ≤ 1/|ρ|² — summable ✓.\n\n- λ_n = Σ_j (−1)^{j+1} C(n,j) σ_j: from 1 − (1−1/ρ)ⁿ = 1 − Σ_j C(n,j)(−1/ρ)^j... let me expand: (1−1/ρ)ⁿ = Σ_{j=0}^{n} C(n,j)(−1/ρ)^j = 1 + Σ_{j=1}^n C(n,j)(−1)^j ρ^{−j}. So 1−(1−1/ρ)ⁿ = −Σ_{j=1}^n C(n,j)(−1)^j ρ^{−j} = Σ_{j=1}^n (−1)^{j+1} C(n,j) ρ^{−j}. ✓ matches λ_n = Σ_j (−1)^{j+1} C(n,j) σ_j with σ_j = Σ mult ρ^{−j}.\n\n  In the PAIRED form: liSummand n ρ = mult/2·(f ρ + f ρ̄) with f ρ = 1−(1−1/ρ)ⁿ. Expand: f ρ + f ρ̄ = Σ_j (−1)^{j+1} C(n,j) (ρ^{−j} + ρ̄^{−j}). So liCoeff n = Σ_ρ mult/2 Σ_j (−1)^{j+1}C(n,j)(ρ^{−j}+ρ̄^{−j}) = Σ_j (−1)^{j+1} C(n,j) Σ_ρ mult/2 (ρ^{−j}+ρ̄^{−j}) = Σ_j (−1)^{j+1} C(n,j) σ_j where σ_j := Σ_ρ (mult/2)(ρ^{−j}+ρ̄^{−j}) (paired power sum — absolutely summable for j ≥ 1 ✓ since |ρ^{−j}+ρ̄^{−j}|/2 ≤ |ρ|^{−j} ≤ |ρ|^{−2}... wait for j = 1: |ρ⁻¹ + ρ̄⁻¹|/2 = |(ρ+ρ̄)/2|/|ρ|² = |Re ρ|/|ρ|² ≤ 1/|ρ|² since |Re ρ| ≤ |ρ| ≤ ... |Re ρ|/|ρ|² ≤ |ρ|/|ρ|² = 1/|ρ| ≤ 1 (|ρ| ≥ ... zeros have |ρ| ≥ something — actually smallest |ρ| ~ 14). Hmm: |Re ρ|/|ρ|² ≤ 1/|ρ| — that's not directly ≤ C/|ρ|². But Re ρ ∈ (0,1) (IsNontrivialZero: 0 < re < 1) so |Re ρ| ≤ 1 ⟹ |Re ρ|/|ρ|² ≤ 1/|ρ|² ✓. \n\n  So the swap: ∑' over paired zeros of a finite sum = finite sum of ∑'s — needs each j-slice summable (they are, j ≥ 1) + the total (liSummable, PROVED). The swap itself: Summable.tsum_sum or Finset.tsum_sum: ∑' ρ, Σ j ∈ Finset, g j ρ = Σ j, ∑' ρ, g j ρ when each g j summable — Mathlib: `tsum_sum` : (∀ j ∈ s, Summable (g j)) → ∑' ρ, Σ j ∈ s, g j ρ = Σ j ∈ s, ∑' ρ, g j ρ ✓ (`tsum_sum` exists in Mathlib.Topology.Algebra.InfiniteSum.Basic? I recall `tsum_sum`).\n\n  So R2(i): define σSum (j : ℕ) : ℂ := ∑' ρ : {ρ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ)/2 * ((ρ:ℂ)⁻ʲ + (star ρ:ℂ)⁻ʲ)... wait — (1/ρ)^j vs ρ^{−j}: f ρ = 1 − (1 − 1/ρ)ⁿ — expansion in powers of 1/ρ: (1/ρ)^j. So the summand: (1/ρ)^j + (1/ρ̄)^j. Define sigmaPaired (j : ℕ) := ∑' ρ, (zeroMult ρ : ℂ)/2 * ((1/(ρ:ℂ))^j + (1/star (ρ:ℂ))^j)? Hmm — 1/star ρ = star (1/ρ)? star ρ = conj — conj (1/ρ) = 1/conj ρ ✓ (map_inv₀... Complex.conj is a ring hom: conj (1/ρ) = 1/conj ρ via map_inv₀/map_div₀ ✓).\n\n  Then the theorem: liCoeff n = Σ_{j=1}^n (−1)^{j+1} C(n,j)·sigmaPaired j. As a ℂ-equality (liCoeff is ℂ, real-valued). \n\n  Then the real part: liCoeff.re = the sum's re — but since everything is manifestly real (liSummand_eq: liSummand = mult·(f ρ).re cast), maybe also show sigmaPaired j is real: (1/ρ)^j + (1/ρ̄)^j = (1/ρ)^j + conj((1/ρ)^j) = 2Re((1/ρ)^j) — real. So sigmaPaired j = ∑' mult·Re((1/ρ)^j) — real-valued. The identity as ℂ is fine; downstream uses .re.\n\n  Actually — WAIT. What does the assembly actually need? ii′-6 L0 assembly: |Sf n| ≤ Bn FAlt n via the crux Sf = ResW1 + (contour sides bridge)... Hmm no — let me re-read D-064's R2 purpose. The crux identity Sf(n) = Res₁(n): Sf := S_∞ + 1 − λ_n (Lean: Sf n = SInfty n + 1 − liCoeff.re). ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff(j−1) (PROVED, ResW1_eq_sum). The crux: SInfty n + 1 − liCoeff n = Σ_j C(n,j)·lcoeff(j−1).\n\n  Path: λ_n = Σ_j (−1)^{j+1}C(n,j)σ_j [R2(i)]; S_∞ = Σ_j C(n,j)τ_{j−1} [R2(ii)]; (4.10): τ_j = c_j + (−1)^j σ_{j+1} − (−1)^j [R2(iii), ii′-3]. Then:\n  S_∞ + 1 − λ_n = Σ_j C(n,j)τ_{j−1} + 1 − Σ_j (−1)^{j+1}C(n,j)σ_j\n  (4.10) with j → j−1: τ_{j−1} = c_{j−1} + (−1)^{j−1}σ_j − (−1)^{j−1} = c_{j−1} + (−1)^{j+1}σ_j + (−1)^j.\n  Σ_j C(n,j)τ_{j−1} = Σ_j C(n,j)c_{j−1} + Σ_j C(n,j)(−1)^{j+1}σ_j + Σ_j C(n,j)(−1)^j\n  = ResW1 n + λ_n + (Σ_j C(n,j)(−1)^j)\n  Σ_{j=1}^n C(n,j)(−1)^j = (1−1)ⁿ − 1 = −1 (for n ≥ 1).\n  So S_∞ + 1 − λ_n = ResW1 + λ_n + (−1) + 1 − λ_n = ResW1 ✓ — the crux, as designed in D-064 §2 (bookkeeping verified there).\n\n  So ii′-2's deliverables are exactly the two swaps (i) and (ii) as Lean theorems:\n  (i) liCoeff n = ∑ j ∈ Finset.Icc 1 n, ((-1:ℂ))^(j+1) * (n.choose j : ℂ) * sigmaPaired j (or as .re form).\n  (ii) SInfty n = ∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * tauCoeff (j−1)? — need to check what SInfty IS in LiSkeleton and what τ_j is.\n\n  τ_j: Lagarias's τ_j = −Σ_{k≥1} ... hmm I need the exact definition. From D-064: \"τ_j the archimedean coefficients (digamma/Hurwitz values)\". Lagarias (4.7)/(4.11): τ_j := ... Let me look at D-037 §3 and the Lagarias paper for the exact definitions, and LiSkeleton's SInfty.\n\nLet me read LiSkeleton.lean first (the SInfty definition and surrounding), then D-037 §3, then the Lagarias PDF section 4 if needed.","signature":""},{"type":"text","text":"Starting session 018 — ii′-2 (elementary swaps). Loading the definitions first."},{"type":"tool_use","id":"Read_73","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","offset":1,"limit":130},"extra_content":null}]