D-070 — ii′-3b route revision: the moments (M) from the 5e partial-fraction identity (no contours)

Date: 2026-08-24 | Session: 037 | Task: 5.1 tier ii′ sub-stage 3b (route revision) Status: design COMPLETE — supersedes D-066 §3's rectangle-contour plan. Commit: (this file)

1. What ii′-3b must prove (unchanged from D-066)

Piece (M) of the (4.10-a) factorization: for all k ≥ 1,

(M) sigmaP k = −(iteratedDeriv (k−1) gFun 0)/(k−1)!

where gFun = logDeriv xiL, xiL = (s(s−1)/2)·completedRiemannZeta (the entire ξ), sigmaP k = Σ_ρ (mult/2)·(ρ^{−k} + ρ̄^{−k}) (ii′-2 paired power sums).

Sanity gate (D-066 §2): k = 1 gives σ₁ = −gFun(0) = −B = 1 + γ/2 − ½log 4π ≈ 0.0230957 (the Davenport value; B ≈ −0.0230957 numerically from the 5e identity at s → 0: B = ζ′/ζ(0) − 1 − (log π)/2 − γ/2 = log 2π − 1 − (log π)/2 − γ/2).

2. The route change and why

D-066 (session 019) planned rectangle contours: ∫ w^{−k}g(w) over [−A,3]×[−T,T] with T zero-avoiding, horizontals killed by the R-bound, verticals by push-off. That was designed BEFORE the 5e route crystallized (D-068, session 026) and before ii′-5e-…-5f actually proved the partial-fraction identity.

The 5e capstone partialFraction_identity (hZC : ZeroCountProp) IS the contour work, done once and for all. The moment identities are a CONSEQUENCE by pure algebra + termwise series calculus:

gFun(s) = 1/s + 1/(s−1) + logDeriv ΓR(s) + logDeriv ζ(s) = 1/s + 1/(s−1) + [−(log π)/2 + ψ(s/2)/2] + [B + seriesFun(s) − 1/s − 1/(s−1) + (log π)/2 − ψ(s/2)/2] = B + seriesFun(s) (G)

at every good point (s ≠ 0, 1; ζ s ≠ 0; s ≠ −2n, n ≥ 1) — the Hadamard-product log-derivative expansion of ξ, obtained with NO Hadamard machinery.

Then:

• k ≥ 2: differentiate (G) (k−1) times at 0 (termwise, M-test on an avoiding ball; the LiDigamma §7–8 iteratedDerivWithin_tsum pattern): gFun^{(k−1)}(0) = Σ mult·(−1)^{k−1}(k−1)!·(−ρ)^{−k} = −(k−1)!·Σ mult·ρ^{−k}, and Σ mult·ρ^{−k} = sigmaP k (the sum is conj-invariant: conj-equiv reindex
• zeroMult_conj; sigmaP k = ½(S+S) = S).
• k = 1: sigmaP 1 = ½·Σ mult/(ρ(1−ρ)) = ½·seriesFun(1) via V := Σ mult·(1/conjρ − 1/(1−ρ)) = 0 — the summand is O(|1−2re|/(‖ρ‖‖1−ρ‖)) = O(γ^{−2}) (absolutely summable), and the composed conj/reflect reindexes give V = −V (zeroMult_conj + zeroMult_one_sub). With seriesFun(0) = 0, gFun(1) = B + seriesFun(1), gFun(0) = B, and the FE sign gFun(1) = −gFun(0) (xiL(1−s) = xiL(s), chain rule), get sigmaP 1 = (gFun(1) − gFun(0))/2 = −gFun(0).

NO re/conj-of-tsum bridges are needed anywhere: every reality argument is a subtype-equiv reindex (conjEquiv, oneSubEquiv on {ρ // IsNontrivialZero ρ}).

3. Key construction choices

• xiL via the entire closed form: xiL(s) := (s(s−1)/2)·Λ₀(s) − (s−1)/2 + s/2 (Mathlib completedRiemannZeta_eq: Λ = Λ₀ − 1/s − 1/(1−s), Λ₀ entire). Manifestly entire (no removable-singularity proofs); xiL(s) = (s(s−1)/2)·Λ(s) for s ∉ {0,1} by one rewrite; xiL(0) = xiL(1) = 1/2 by direct evaluation; xiL(1−s) = xiL(s) by cases (off {0,1} via completedRiemannZeta_one_sub; at 0,1 by the values). (D-066's "Λ₀ is the WRONG object" warning is about Λ₀'s ZEROS, which are never used — only Λ₀'s entirety.)
• Values at 0, 1 by punctured continuity: (G) holds at good points, which accumulate at 0 (ζ(0) = −1/2 ≠ 0) and at 1 (zetaA factor: ζ(s) = zetaA(s)/(s−1), zetaA(1) = 1); both sides continuous at 0,1 (gFun: xiL analytic + xiL ≠ 0; seriesFun: 0,1 not nontrivial zeros). So (G) holds AT 0 and 1 too — and gFun =ᶠ[𝓝 0] (B + seriesFun), giving iteratedDeriv-congruence at 0 (LiDigamma's iteratedDeriv_congr_of_eventuallyEq).
• Summability budget: one master lemma Σ mult/‖ρ‖² (the ii′-2 (9/4)- comparison + Zeta23 zero_sum_inv_sq) + the avoiding-ball radius δ₀ at 0 (‖ρ‖ ≥ δ₀ uniform) + reindex transfer for the 1−ρ families + AM-GM 1/(‖ρ‖‖1−ρ‖) ≤ ½(‖ρ‖^{−2} + ‖1−ρ‖^{−2}) for the mixed terms. No im-lower- bound (no NoLowZeros) needed anywhere.

4. Cost/benefit vs the D-066 §3 contour plan

D-066 §3 needed: the rectangle residue machine at a general center (port of ii′-1b(ii)), zero-avoiding T limits (T → ∞), horizontal decay from the tight R-bound, vertical push-off arguments, the k = 1 paired-kernel rectangle with the (g(1)−g(0))/2 evaluation anyway. All of that is REPLACED by: (G) (one logDeriv algebra chain) + termwise series calculus + two equiv reindexes. The only perimeter hypothesis carried is ZeroCountProp (from 5e) — in the declared class (D-062 §4); note the tight R-bound (5f, hZC2/hNLZ) is NOT needed for the moments.

5. Deliverable statement (Lean)

theorem sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC : ZeroCountProp)
    {k : ℕ} (hk : 1 ≤ k) :
    sigmaP k = -(iteratedDeriv (k - 1) gFun 0) / ((k - 1)! : ℂ)

(k = 1 included: iteratedDeriv 0 = id, 0! = 1.) File: LiMoments.lean. Consumed by ii′-3c's (4.10-a) assembly (D-066 §2) together with the FE derivative relation gFun^{(k−1)}(0) = (−1)^k·gFun^{(k−1)}(1) (ii′-3c territory).