Session 019 — 2026-08-21 — ii′-3 DESIGN (D-066, route β4) + piece (B) PROVED

Directive

Continue tier ii′ per D-064: sub-stage ii′-3 (Lagarias (4.10), the long pole). STATE.md: design note first (read EF_lit_zeta + WeilEF interface), then Lean.

Work done

(1) Route investigation COMPLETE (D-066, commit 62a1ddf). Read: EF_lit_zeta's exact statement (Zeta23/ExplicitFormula.lean — the literature-form Weil EF for k ∈ C²_c, h = paperFT k entire of exp type); its proof structure (WeilEF/Main.lean — full-line contour identity); Lagarias's own §4 proof (archived PDF pp. 14–17: Lemma 4.1 via the Hadamard product, (4.10) by coefficient comparison, (4.19)–(4.22) digamma partial fractions); Mathlib infrastructure inventory.

Route verdicts:

• β1 (Hadamard product) OUT as scoped in D-064: the guessed seed MeromorphicOn.extract_zeros_poles is finite-only (FactorizedRational / CanonicalDecomposition); Mathlib has NO Weierstrass infinite product, NO minimum-modulus theorem, NO order theory.
• β2 (EF reuse) OUT: the moment kernels (1/2+iz)^{−k} are not entire — the zero power sums are outside EF_lit's test-function class.
• β4 ADOPTED: prove the moment identity (M) σ_k = −g^{(k−1)}(0)/(k−1)! directly by the ii′-1b rectangle-residue machinery (w^{−k}·g(w), k ≥ 2; paired kernel g(w)/(2w(1−w)) for k = 1), expanding limit killed by the R-bound (SHARED with ii′-5 — the key dependency insight), vertical lines vanishing by push-off (no poles right of Re 1; decay). Factorization (4.10-a) ⟺ (M) + (A) archimedean + (B) ζ-piece, with the FE reflection g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1) (Mathlib completedRiemannZeta_one_sub). Sanity gates all check numerically (σ₁ Davenport value; τ₀ via digamma_one_half; ψ′(1/2) = π²/8·2 etc.).
• Resequenced pipeline (supersedes D-064's ii′-3-first ordering): ii′-3a (pieces A+B, no contour deps) → ii′-4 (L3+L1) → ii′-5 (R-bound) → ii′-3b (moments) → ii′-3c (assembly → crux sf_eq_resW1) → ii′-6 → 7.
• Key object note: Mathlib's completedRiemannZeta₀ is the WRONG ξ (its zeros are shifted — Λ₀ = Λ + 1/s − 1/(s−1)); the right object is xiL := (s(s−1)/2)·completedRiemannZeta (entire; zeros = IsNontrivialZero via Zeta23 CountByIntegral + factor nonvanishing).
• Mathlib inventory verified live: TendstoLocallyUniformlyOn.differentiableOn (Weierstrass), Complex.digamma_one_half ✓ (τ₀!), digamma_apply_add_one, Gammaℝ_def/one/ne_zero_of_re_pos/eq_zero_iff, LSeries_vonMangoldt_eq_ deriv_riemannZeta_div (−ζ′/ζ Dirichlet series), BohrMollerup tendsto_log_gamma (the digamma-series seed for piece A's j ≥ 1).

(2) Piece (B) PROVED (LiZetaCoeff.lean, ~250 lines): hLiExt s := (1 − hLi(1+s))/s extended by −deriv hLi 1 at 0 — the analytic-at-0 form of 1/s + ζ′/ζ(1+s):

• hLiExt_tendsto (slope limit), hLiExt_analyticAt_zero (removable singularity, the zetaA pattern), hLiExt_mul_id (exact global identity s·hLiExt s = 1 − hLi(1+s)), iteratedDeriv_hLi_one_add (comp bridge via iteratedDeriv_comp_sub_const at c = −1),
• iteratedDeriv_hLiExt: iteratedDeriv j hLiExt 0 = −(j!)·lcoeff j — the Taylor coefficients of 1/s + ζ′/ζ(1+s) at 0 are −c_j. Proof: Leibniz (iteratedDeriv_mul) with the identity factor collapsing the sum to i = 1, then factorial bookkeeping.
• hLiExt_eq_near_zero: hLiExt s = 1/s + ζ′/ζ(1+s) on 𝓝[≠] 0 (the reading as the actual meromorphic function).

Lean notes (hard-won this session, additions to the handoff list)

• HasDerivAt.comp at a composed point: write the outer hypothesis's point SYNTACTICALLY as g x (e.g. 1 + 0), not its reduced form — else the elaborator solves ?g := const.
• 1 + 0 is NOT defeq to 1 for ℂ/ℝ (OfNat/HAdd don't compute) — nhds targets need simpa using bridges, not exact.
• tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within: source filter stays arbitrary (𝓝[≠] 0), first premise Tendsto f l (𝓝 a) — use .mono_left nhdsWithin_le_nhds.
• iteratedDeriv_succ' : iteratedDeriv (n+1) f = iteratedDeriv n (deriv f) (deriv INSIDE; iteratedDeriv_succ is the other order).
• iteratedDeriv_const : = if n = 0 then c else 0 (no side hypothesis).
• deriv_id'' : deriv (fun x => x) = fun x => 1 (function equality, not pointwise — don't apply it to an argument).
• ContDiffAt ℂ (j+1) lives at order ℕ∞: the ↑?n = ↑j + 1 unification leaves beta-redex artifacts downstream — pin iteratedDeriv_mul's conclusion with an explicit type ascription (clean Finset.range (j+2)).
• add_eq_left : a + b = a ↔ b = 0 (add_eq_right is the other one).
• iteratedDeriv_comp_sub_const m f c produces the LAMBDA fun z => f (z − c) (not the ∘ form).

State at stop

ii′-3a piece (B) COMPLETE. Remaining in ii′-3a: piece (A) — the archimedean τ-evaluation (τ₀ via digamma_one_half; j ≥ 1 via the digamma series built from BohrMollerup's logGammaSeq + termwise derivation + the odd-m reindexing to lagariasA). Then ii′-4 (L3+L1), ii′-5 (R-bound), ii′-3b (moments), ii′-3c (assembly).