← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (133 chars)
Session 019 closed. Let me give the summary. Three commits: 62a1ddf (D-066 design), e28a81e (LiZetaCoeff piece B), df74ad6 (closure).
**Session 019 complete** — ii′-3 designed (route β4) + piece (B) proved. Three commits: 62a1ddf, e28a81e, df74ad6.
## The route decision (D-066)
Read EF_lit_zeta, its proof, Lagarias's §4 (pp. 14–17 of the archived PDF), and did a full Mathlib infrastructure inventory:
- **β1 (Hadamard product) — OUT**: D-064's guessed seed `extract_zeros_poles` is finite-only; Mathlib has no Weierstrass infinite product, no minimum-modulus theorem, no order theory
- **β2 (EF reuse) — OUT**: the moment kernels (1/2+iz)^{−k} aren't entire — zero power sums live outside EF_lit's test-function class
- **β4 — ADOPTED**: prove the moment identity **σ_k = −(ξ′/ξ)⁽ᵏ⁻¹⁾(0)/(k−1)!** directly by the ii′-1b rectangle machinery, with the expanding limit killed by the R-bound and vertical lines vanishing by push-off (no poles right of Re 1 — no Laplace evaluations needed)
**Key structural finding**: the R-bound is shared between ii′-3's moments and ii′-6's side estimates — so the pipeline resequences to: ii′-3a (A+B, no contour deps) → ii′-4 (L3+L1) → ii′-5 (R-bound) → ii′-3b (moments) → ii′-3c (assembly → crux).
Also flagged: Mathlib's `completedRiemannZeta₀` is the *wrong* ξ (its zeros are shifted); the right object is (s(s−1)/2)·completedRiemannZeta.
## Piece (B) proved (LiZetaCoeff.lean, 6 declarations, axiom-clean)
`iteratedDeriv_hLiExt`: the Taylor coefficients of 1/s + ζ′/ζ(1+s) at 0 are exactly **−j!·lcoeff j** — via the exact identity s·hLiExt s = 1 − hLi(1+s), the Leibniz collapse, and the comp bridge. Build GREEN (8747 jobs).
## Next (session 020)
**Piece (A)** — the archimedean τ-evaluation: τ₀ via Mathlib's `digamma_one_half` (confirmed present), and j ≥ 1 via the digamma series built from Bohr–Mollerup's `logGammaSeq`. That's the heaviest remaining rock of ii′-3a, all self-contained real/complex analysis.
Continue with piece (A)?
raw content_json (database row)
[{"type":"thinking","thinking":"Session 019 closed. Let me give the summary. Three commits: 62a1ddf (D-066 design), e28a81e (LiZetaCoeff piece B), df74ad6 (closure).","signature":""},{"type":"text","text":"**Session 019 complete** — ii′-3 designed (route β4) + piece (B) proved. Three commits: 62a1ddf, e28a81e, df74ad6.\n\n## The route decision (D-066)\n\nRead EF_lit_zeta, its proof, Lagarias's §4 (pp. 14–17 of the archived PDF), and did a full Mathlib infrastructure inventory:\n\n- **β1 (Hadamard product) — OUT**: D-064's guessed seed `extract_zeros_poles` is finite-only; Mathlib has no Weierstrass infinite product, no minimum-modulus theorem, no order theory\n- **β2 (EF reuse) — OUT**: the moment kernels (1/2+iz)^{−k} aren't entire — zero power sums live outside EF_lit's test-function class\n- **β4 — ADOPTED**: prove the moment identity **σ_k = −(ξ′/ξ)⁽ᵏ⁻¹⁾(0)/(k−1)!** directly by the ii′-1b rectangle machinery, with the expanding limit killed by the R-bound and vertical lines vanishing by push-off (no poles right of Re 1 — no Laplace evaluations needed)\n\n**Key structural finding**: the R-bound is shared between ii′-3's moments and ii′-6's side estimates — so the pipeline resequences to: ii′-3a (A+B, no contour deps) → ii′-4 (L3+L1) → ii′-5 (R-bound) → ii′-3b (moments) → ii′-3c (assembly → crux).\n\nAlso flagged: Mathlib's `completedRiemannZeta₀` is the *wrong* ξ (its zeros are shifted); the right object is (s(s−1)/2)·completedRiemannZeta.\n\n## Piece (B) proved (LiZetaCoeff.lean, 6 declarations, axiom-clean)\n\n`iteratedDeriv_hLiExt`: the Taylor coefficients of 1/s + ζ′/ζ(1+s) at 0 are exactly **−j!·lcoeff j** — via the exact identity s·hLiExt s = 1 − hLi(1+s), the Leibniz collapse, and the comp bridge. Build GREEN (8747 jobs).\n\n## Next (session 020)\n\n**Piece (A)** — the archimedean τ-evaluation: τ₀ via Mathlib's `digamma_one_half` (confirmed present), and j ≥ 1 via the digamma series built from Bohr–Mollerup's `logGammaSeq`. That's the heaviest remaining rock of ii′-3a, all self-contained real/complex analysis.\n\nContinue with piece (A)?"}]