D-066 — Tier ii′ sub-stage ii′-3 design: Lagarias (4.10) via contour moments + coefficient split

Date: 2026-08-21 | Session: 019 | Task: 5.1 tier ii′ sub-stage 3 (design) Status: design COMPLETE — route decided (β4 below, replacing D-064's β1/β2 sketch); dependency resequencing identified (R-bound shared with ii′-5).

0. What ii′-3 must prove

The a-form of Lagarias's (4.10) (derived from D-064's τ-form with τ_{j−1} = (−1)^j a_j; conventions: D-037/D-064, LiSwaps.lean):

(4.10-a) for all k ≥ 1: lcoeff (k−1) = (−1)^k · (lagariasA k + sigmaP k) + (−1)^{k−1}

i.e. c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}, where

• c_{k−1} = lcoeff (k−1) — Taylor coefficients of hLi at 1 (ii′-1b(i));
• a_k = lagariasA k — a₁ = (log 4π+γ)/2, a_j = 1 + Σ_{m odd ≥ 3} m^{−j} (ii′-2);
• σ_k = sigmaP k — paired zero power sums (ii′-2).

Together with ii′-2's two swaps and ii′-1b(i)'s ResW1_eq_sum, this gives the crux Sf(n) = ResW1 n for n ≥ 1 (the bookkeeping verified numerically in D-064 §3: exact to 2e-21 at n = 2, 3).

1. Route decision: β4 (contour moments + coefficient split)

D-064 scoped two routes: β1 (Hadamard product of ξ) and β2 (reuse Zeta23's proved EF_lit_zeta). Session-019 inventory results:

• β1 is OUT as scoped: D-064 guessed MeromorphicOn.extract_zeros_poles could seed the product — it cannot (it is the FINITE factorized-rational decomposition on compacts, FactorizedRational.lean; CanonicalDecomposition.lean is finite Blaschke on disks). Mathlib has NO Weierstrass/Hadamard infinite product, NO minimum-modulus theorem, NO order theory. Building those is a separate multi-session project with real risk.
• β2 is OUT: EF_lit_zeta evaluates Σ mult·h(γ_ρ) only for h = paperFT k with k ∈ C²_c (entire of exponential type). The moment kernels (1/2+iz)^{−k} are not entire — moments are outside the EF's test class; extracting them needs a δ-limit re-proving a special EF instance. No savings.
• β4 (ADOPTED): prove the moment identity (M) directly by the rectangle-residue machinery ALREADY BUILT in ii′-1b (residueTheorem_finset, logDeriv normal-form residues, ppart subtraction), with the expanding-limit killed by the R-bound (shared with ii′-5) and vertical lines vanishing by push-off (no poles to the right of Re = 1; decay — §3.3 below). This is Lagarias's Lemma 4.1 content, but proved by residues instead of the product.

2. The factorization of (4.10-a)

Let xiL := (s(s−1)/2)·completedRiemannZeta (the entire ξ; Mathlib's completedRiemannZeta is Λ = ΓR·ζ with poles at 0,1; xiL removes them; completedRiemannZeta_one_sub (Mathlib) gives xiL(1−s) = xiL(s); Mathlib's completedRiemannZeta₀ is the WRONG object — its zeros are shifted, §4 note). g := logDeriv xiL. Then (4.10-a) ⟺ (M) + (A) + (B):

• (M) moments: σ_k = −g^{(k−1)}(0)/(k−1)! for all k ≥ 1. [the analytic heart]
• (A) archimedean: τ_j := (1/j!)·(d/ds)^j|₀ ΓR′/ΓR(1+s) = (−1)^{j+1} a_{j+1} for all j ≥ 0.
• (B) ζ-piece: coefficient of s^j in (1/s + ζ′/ζ(1+s)) at 0 is −c_j. [90% done in LiResidue — hLi(1+s) = (1+s−1)(−ζ′/ζ(1+s)) punctured, analytic at 0 with Taylor coefficients lcoeff; needs the iteratedDeriv_comp_add_const packaging.]

Assembly algebra (verified twice, once numerically): g(1+s) = 1/(1+s) + [1/s + ζ′/ζ(1+s)] + ΓR′/ΓR(1+s) has s^{k−1}-coefficient (−1)^{k−1} − c_{k−1} + τ_{k−1}; the FE gives g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1); (M) says σ_k = −g^{(k−1)}(0)/(k−1)!. Chaining: σ_k = (−1)^{k+1}[(−1)^{k−1} − c_{k−1} + τ_{k−1}] = 1 + (−1)^k c_{k−1} + (−1)^{k+1}τ_{k−1}, solve for c_{k−1}, insert (A): c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}. ∎

Sanity gates: k = 1 with c₀ = −γ, a₁ = (log4π+γ)/2 gives σ₁ = 1 + γ/2 − ½log 4π — the Davenport value, verified to 15 digits (session 014, D-064 §3).

3. Piece (M): the moment identities by contour (ii′-3b)

For k ≥ 2, integrate w^{−k}·g(w) on the rectangle [−A, 3]×[−T, T], T zero-avoiding (perimeter N(T) + pigeonhole — ii′-4's L3):

(1/2πi)∮ = Σ_{|γ|<T} mult·ρ^{−k} + Res_{w=0}[w^{−k}g], Res_{w=0} = g^{(k−1)}(0)/(k−1)!.

• Zeros = {IsNontrivialZero}: off {0,1}, xiL s = 0 ⟺ Λ s = 0 ⟺ IsNontrivialZero (Zeta23 RvM/CountByIntegral.lean:66, PROVED); xiL(0) = xiL(1) = 1/2 (from completedRiemannZeta_residue_one + FE transport); order of xiL at ρ = zeroMult ρ (factor nonvanishing + Λ = ΓR·ζ with ΓR(ρ) ≠ 0 — Complex.Gammaℝ_ne_zero_of_re_pos ✓ Mathlib).
• Residue machinery: zeros via the ii′-1b(iii) logDeriv-NF pattern (Rfun_residue_at); the order-k pole at 0 via a small generalization of ii′-1b(ii)'s ppart subtraction (port Acoeff/ppart/rectInt'_ppart from center 1 to a general center/general analytic numerator F).
• T → ∞: horizontals die (T^{−k}·O(log²T)): the R-bound |ζ′/ζ(w) − Σ_{|γ−t|<1} 1/(w−ρ)| ≤ A log(|t|+2) + B₀ on σ ∈ [−5/2, 4] (ii′-5/R3 content — Borel–Carathéodory + Jensen + Blaschke, D-064 R3 inventory) + the direct Euler-series bound |ζ′/ζ| ≤ Σ Λ(n)n^{−re} for re ≥ 3 (Mathlib ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div ✓)
• digamma growth O(log|w|) (from the (A) series) + trivial pieces.
• Verticals vanish for free: g's poles are all in 0 < re < 1 and the kernel's pole is at 0 — no poles with re > 1, so V(3) = 0 by push-right (horizontal decay as above; |w^{−k}g(a+it)| ~ log|t|·|w|^{−k} integrable, V(A) → 0 as A → ∞). NO Laplace-integral evaluations needed (the ζ-piece's n^{−w} terms close right for n ≥ 2 — not even needed; the whole line moves). Similarly V(−A) → 0 as A → ∞ (FE-reflected bounds). ⟹ Σ_ρ mult·ρ^{−k} = −g^{(k−1)}(0)/(k−1)!, k ≥ 2. (For k ≥ 2 the unpaired sum converges absolutely and equals sigmaP k: Σ mult·ρ^{−k} is conj-invariant hence real, = Σ mult·Re(ρ^{−k}) = sigmaP k.)
• k = 1 (the paired kernel): integrate g(w)/(2w(1−w)) on [−A, 2]×[−T, T]: Σ_{|γ|<T} mult/(2ρ(1−ρ)) + g(0)/2 − g(1)/2 = (1/2πi)(V(2) − V(−A)) → 0, so Σ mult/(2ρ(1−ρ)) = (g(1)−g(0))/2 = −g(0) (FE). Then sigmaP 1 = Σ mult·Re(1/ρ) = Σ mult/(2ρ(1−ρ)): the reflect-pair vs conj-pair rearrangement — (1/2)Σ mult(re/|ρ|² + (1−re)/|1−ρ|²), reindex ρ ↦ 1−ρ (bijection on zeros, mult-preserving: conj via riemannZeta_conj (check), reflect via Zeta23 seam mult_reflect), absolute convergence throughout. ⟹ sigmaP 1 = −g(0) = −g^{(0)}(0)/0! — (M) at k = 1.

4. Piece (A): the archimedean coefficients (ii′-3a, no contour deps)

τ_j = (1/j!)·iteratedDeriv j (fun s => logDeriv Gammaℝ (1+s)) 0 = (−1)^{j+1} a_{j+1}.

• ΓR logDeriv split: logDeriv Gammaℝ (1+s) = −(log π)/2 + (1/2)·digamma((1+s)/2) (Gammaℝ_def = π^{−s/2}Γ(s/2) ✓ Mathlib; logDeriv product/comp algebra).
• j = 0: τ₀ = −(log π)/2 + (1/2)·digamma(1/2) = −(log π)/2 + (1/2)(−2log2 − γ) = −(log 4π + γ)/2 = −a₁ — via Complex.digamma_one_half ✓ MATHLIB HAS IT.
• j ≥ 1: ψ^{(j)}(1/2) = (−1)^{j+1} j! Σ_{m≥0} (m+1/2)^{−(j+1)}, then Σ_{m≥0}(m+1/2)^{−(j+1)} = 2^{j+1}·lagariasA(j+1) (reindex m ↦ 2m+1: ℕ ≃ {odd naturals}, peel m = 0 ↔ the "1 +" in lagariasA; tsum_eq_zero_add + Equiv.tsum_eq). The digamma series is NOT in Mathlib; build from BohrMollerup's logGammaSeq x n = x log n + log n! − Σ_{m=0}^n log(x+m) with tendsto_log_gamma ✓ (real, x > 0): (i) ψ_real x := deriv (log ∘ Gamma) x = lim_n [log n − Σ_{m=0}^n 1/(x+m)] = −γ − 1/x + Σ_{m≥1}(1/m − 1/(x+m)) for x > 0 — deriv under the locally-uniform limit (real deriv-limit lemma; the derived sequence is uniformly Cauchy on compacts by the Σ 1/m² tail); (ii) termwise j-fold derivation (induction; each derivative series M-tested): ψ_real^{(j)}(x) = (−1)^{j+1} j! Σ_{m≥0} (x+m)^{−(j+1)} (j ≥ 1); (iii) complex bridge: iteratedDeriv j (ΓR′/ΓR(1+·)) 0 (complex) = real-line j-th derivative at 0 (ofReal comp; analytic at 0 since Gammaℝ(1) = 1 ≠ 0 — Gammaℝ_one, Gammaℝ_ne_zero_of_re_pos ✓). Cost: the heaviest single rock of ii′-3a (self-contained real analysis).

5. Sequencing (supersedes D-064's ii′-3 position)

The R-bound ((M)'s horizontal decay) is ii′-5/R3's content and is ALSO needed by ii′-6's side estimates — build it ONCE, before the moments:

• ii′-3a (next): piece (B) packaging + piece (A). [no contour deps]
• ii′-4 (unchanged): L3 zero-avoiding T (pigeonhole on perimeter C₀/FAlt)
• L1 kernel bounds (|k_n| ≤ 2, e⁴+1, e^{√n/2}+1; trivial residue).
• ii′-5 (unchanged): R-bound via the D-064 R3 local route (Borel–Carathéodory + Jensen + Blaschke/StrongPNTPrefix + FE strip bound via riemannZeta_one_sub + Stirling; digamma Lemma D).
• ii′-3b: piece (M) moments (uses ii′-4's zero-avoiding T + ii′-5's R-bound + the rectangle machinery).
• ii′-3c: the (4.10-a) assembly (§2 algebra) → the crux sf_eq_resW1 : Sf n = (ResW1 n).re for n ≥ 1.
• ii′-6, ii′-7 unchanged (L0 assembly + closure).

6. Mathlib inventory used (all verified to exist, session 019)

TendstoLocallyUniformlyOn.differentiableOn (Weierstrass convergence); Complex.digamma_one_half, digamma_one, digamma_apply_add_one, meromorphic_digamma; Gammaℝ_def, Gammaℝ_one, Gammaℝ_ne_zero_of_re_pos, Gammaℝ_eq_zero_iff (zeros of ΓR = {−2n} — also the future trivial-zero simplicity input); completedRiemannZeta_one_sub, completedRiemannZeta_residue_one; ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div (−ζ′/ζ Dirichlet series, re > 1); BohrMollerup.tendsto_log_gamma + logGammaSeq; Zeta23: completedRiemannZeta s = 0 ↔ IsNontrivialZero s (CountByIntegral.lean), seam mult_reflect, WeilEF.zero_sum_inv_sq. NOT in Mathlib (relevant gaps): Weierstrass/Hadamard products, polygamma, digamma partial fractions (built in ii′-3a), riemannZeta_conj (conj-invariance of ζ — to check/derive via the LSeries/integral definition), trivial-zero simplicity deriv ζ(−2) ≠ 0 (deferred from ii′-1b(iii); route: FE + Gammaℝ_eq_zero_iff + ζ(3) ≠ 0).

7. Risks

• The digamma-series build (ii′-3a) is the kind of real-analysis grind that can sprawl (deriv-under-limit + iteration + complex bridge). Mitigation: it is self-contained and has the numeric gates (ψ′(1/2) = π²/2 etc.).
• (M)'s k = 1 rearrangement needs zeroMult conj-invariance — small proof via riemannZeta (conj s) = conj (riemannZeta s) (to be located in Mathlib or proved from the definition).
• The R-bound remains the long pole of ii′-5 per D-064 R3 (2–3 sessions); ii′-3b waits on it. Paper A stays frozen/submittable throughout (freeze protocol; only new files + root imports are touched).