← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (7444 chars)
`logGammaSeq x n = x * log n + log (n!) − ∑_{m=0}^n log(x+m)` and `tendsto_log_gamma (hx : 0 < x) : Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))` ✓ (Real.Gamma, real x). This is the seed for the digamma series build.
I now have a complete picture. Time to write the design note D-066 and register the route decision. Let me define the architecture:
**ii′-3 architecture (route β4 — "contour moments + coefficient split"), replacing/ refining D-064's R2(iii) β1/β2 sketch:**
Target: for k ≥ 1, the a-form identity c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}, where:
- c_{k−1} = lcoeff (k−1) (LiResidue) — Taylor coefficients of hLi at 1.
- a_k = lagariasA k (LiSwaps) — archimedean odd-zeta values.
- σ_k = sigmaP k (LiSwaps) — paired zero power sums.
**The factorization:** With g := logDeriv xiL (xiL := (s(s−1)/2)·completedRiemannZeta, entire, FE xiL(1−s) = xiL(s)):
(4.10)-a ⟺ (M) + (A) + (B) where:
- (M) [the analytic heart — moment identity]: σ_k = −g^{(k−1)}(0)/(k−1)! for all k ≥ 1.
- (A) [archimedean]: τ_j := (j-th Taylor coefficient of ΓR′/ΓR(1+·) at 0)/j! = (−1)^{j+1}a_{j+1} for all j ≥ 0.
- (B) [ζ-piece, mostly done]: coefficient of s^j in (1/s + ζ′/ζ(1+s)) at 0 = −c_j.
Assembly (algebra, verified numerically session 014 + re-verified in this design): from xiL's logDeriv decomposition at 1+s and the FE reflection g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1), the identity (4.10)-a follows by coefficient comparison. [I verified this chain twice above.]
**Piece inventory & costs:**
- (B): LiResidue has hLi/lcoeff/hLi_analyticAt_one/hLi_eq_near_one/hLi_iteratedDeriv_div_factorial. Remaining: the coefficient-extraction packaging: (fun s ↦ (1/s + ζ′/ζ(1+s))) equals −Σ c_j s^j near 0 — i.e. (fun s ↦ 1 + s·ζ′/ζ(1+s))... = −hLi(1+s) eventually, analytic at 0, iteratedDeriv j = −j!·... — the iteratedDeriv_comp_add_const bridge + analytic continuation of coefficients. SMALL (~0.3 sess).
- (A): j = 0 via Complex.digamma_one_half ✓ Mathlib. j ≥ 1: build the real digamma series from BohrMollerup.logGammaSeq (tendsto_log_gamma ✓ Mathlib): ψ_real(x) := deriv (log ∘ Gamma) x = −γ − 1/x + Σ_{m≥1}(1/m − 1/(x+m)), termwise j-fold derivative at x = 1/2 (uniform-on-compacts M-test + deriv-of-limit), ψ^{(j)}(1/2) = (−1)^{j+1}j!Σ_{m≥0}(m+1/2)^{−(j+1)}; reindex Σ_{m≥0}(2m+1)^{−(j+1)} = lagariasA(j+1) (bespoke equiv m ↦ 2m+1 / peel); complex-bridge iteratedDeriv of ΓR′/ΓR(1+·) at 0 = real-line derivatives (ofRealCLM comp). MODERATE-HEAVY (~1–1.5 sess).
- (C) — the moments (M):
(C-i) rectangle residue theorem for the integrand w^{−k}·g(w): ppart-at-0 port of LiPrincipal's machinery (the Acoeff/ppart/rectInt'_ppart pattern with the center generalized) + residue-at-zeros via my Rfun_residue_at pattern (logDeriv NF). Need xiL entire + zero-set identification (zeros of xiL = {IsNontrivialZero} off {0,1} via Zeta23's completedRiemannZeta-zero iff + the factor s(s−1)/2 nonzero elsewhere + value 1/2 at 0,1) + order = zeroMult (order multiplicativity). MODERATE (~0.5–1 sess).
(C-ii) the T → ∞ horizontal decay: needs the R-bound (|ζ′/ζ(w) − Σ_{|γ−t|<1}1/(w−ρ)| ≤ A log(|t|+2) + B₀) on the R-zone + direct Euler-product bound (−ζ′/ζ = Σ Λ(n)n^{−s} ✓ `ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div` Mathlib has) off it + digamma growth bound (|ψ(w)| = O(log|w|) for re w ≥ 3 — from the (A) series) + zero-avoiding T (pigeonhole on perimeter N(T)). THE R-BOUND IS ii′-5's CONTENT — shared dependency.
(C-iii) vertical evaluations: V(3) = 0 / V(−A) → 0 (push-right/left with no-poles + decay; Laplace-term vanishing for the ζ-piece via x = 1/n < 1 closing right — actually WAIT — for the moments I showed the verticals vanish by push-right/left with NO pole-crossing — the ζ-piece's termwise vanishing needs the Laplace integral (1/2πi)∫_{(c)} w^{−k}n^{−w}dw = 0 for n ≥ 2 — hmm — actually NO: my final argument was simpler: V(3) = 0 by pushing the whole line right (integrand has no poles with re > 1... wait g's poles are ρ's with re < 1 ✓ and the kernel pole at 0 ✓ so NO poles with re > 1 — the push-right needs only horizontal decay + vertical integrability — NO termwise Laplace needed!!). Let me re-examine: V(3) = 0 because: rectangle [3, A]×[−T, T] contains no poles; T → ∞: horizontals → 0 (direct bounds: ζ′/ζ Euler-series bound for re ≥ 3 ✓ |ζ′/ζ(σ+it)| ≤ Σ Λ(n)n^{−3} ✓ t-INDEPENDENT — even better; digamma O(log) ✓); A → ∞: V(A) → 0 (|w^{−k}g| ~ log|t|·|w|^{−k} integrable tails ✓). ✓✓ NO Laplace evaluations needed at all! The verticals vanish for FREE (no poles to the right of Re = 1, decay). Same for k=1's kernel (poles at 0,1 only; no poles right of 2 → V(2) = 0; V(−A) → 0 as A → ∞ since no poles left of −A for A ≥ 0 and decay ✓). GREAT — so (C-iii) is just integrability/decay bookkeeping, no integral evaluations.
So the moment identity: Σ_{|γ|<T} mult·ρ^{−k} + Res_0 = (1/2πi)(V(3) − V(−A)) → 0 − 0. MODERATE.
(C-iv) k = 1: the paired kernel 1/(2w(1−w))·g(w): rectangle [−A, 2]... wait — need poles 0 and 1 INSIDE: rectangle [−A, 2]×[−T, T] contains 0, 1 ✓ (re ∈ (−A, 2)); the ρ's ✓. T → ∞: Σ mult/(2ρ(1−ρ)) + Res_{w=0} + Res_{w=1} = (1/2πi)(V(2) − V(−A)) = 0. Residues: at 0: g(0)·(1/2); at 1: g(1)·(−1/2)·... K(w) = 1/(2w(1−w)): at w=0: residue 1/2·g(0); at w=1: 1/(2w(1−w)) = −1/(2w(w−1)): residue −g(1)/2. So Σ mult/(2ρ(1−ρ)) = (g(1) − g(0))/2 = −g(0) (FE: g(1) = −g(0)) ✓. Then sigmaP 1 = that sum (reflect/conj rearrangement — needs zeroMult conj-invariance: analyticOrderAt ζ (conj ρ) = analyticOrderAt ζ ρ — via riemannZeta_conj — check Mathlib for `riemannZeta_conj`!) — SMALL-MODERATE.
(C-v) FE reflection of derivatives: iteratedDeriv m g 0 = (−1)^{m+1}·... g(s) = −g(1−s): iteratedDeriv m g 0 = (−1)^{m+1} g^{(m)}(1)·... — the chain: g(s) = −g(1−s) ⟹ g^{(m)}(s) = (−1)^{m+1}g^{(m)}(1−s) ⟹ at 0: (−1)^{m+1}g^{(m)}(1). SMALL (iteratedDeriv comp lemma).
- (D) assembly: coefficient comparison — SMALL.
**Sequencing recommendation:** the R-bound (C-ii's core) is ii′-5's content and also feeds ii′-6 — so reorder: **ii′-3a := (B) + (A)** [no contour dependencies; start next session]; **ii′-4** (L3 zero-avoiding T + L1 kernel bounds — elementary); **ii′-5** (R-bound via D-064 R3 local route); **ii′-3b := (C) moments**; **ii′-3c := (D) assembly (4.10)**; then ii′-6, ii′-7. This respects D-064's map with the moments re-seated after the R-bound.
Sanity gates (per D-064): k=1: σ₁ = 1 + γ/2 − ½log4π (verified 15 digits numerically, session 014); j=0: τ₀ = −a₁ via digamma_one_half — the γ/log4π combination ✓; the full (4.10)-a at k=1: c₀ = 1 − a₁ − σ₁ ✓ (γ matches: c₀ = −γ ⟸ 1 − (log4π+γ)/2 − (1+γ/2−½log4π) = 1 − log4π/2 − γ/2 − 1 − γ/2 + log4π/2 = −γ ✓).
Now — should I START ii′-3a this session? The session has been a design session (per STATE: "First task: read EF_lit_zeta's exact statement + write the ii′-3 design note (D-066) before any Lean"). The design note is the deliverable. Let me write D-066 now, then decide about starting Lean work on Piece B (small) this session. Given the depth of exploration done, writing D-066 carefully + possibly starting Piece B (the coefficient-extraction packaging, ~0.3 sess) is a good scope. Let me write D-066 first.
Actually — let me reconsider the scope: the session protocol says save artifacts immediately. The design note is the main artifact. Let me write it comprehensively, then assess time/energy for starting Piece B. Actually the instructions say avoid time estimates; just do it. Let me write D-066.
I have the complete architecture. Writing the design note D-066 now.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\derivations\\D-066-ii-prime-3-design.md",
"content": "# D-066 \u2014 Tier ii\u2032 sub-stage ii\u2032-3 design: Lagarias (4.10) via contour moments + coefficient split\nDate: 2026-08-21 | Session: 019 | Task: 5.1 tier ii\u2032 sub-stage 3 (design)\nStatus: design COMPLETE \u2014 route decided (\u03b24 below, replacing D-064's \u03b21/\u03b22\nsketch); dependency resequencing identified (R-bound shared with ii\u2032-5).\n\n## 0. What ii\u2032-3 must prove\n\nThe a-form of Lagarias's (4.10) (derived from D-064's \u03c4-form with\n\u03c4_{j\u22121} = (\u22121)^j a_j; conventions: D-037/D-064, LiSwaps.lean):\n\n **(4.10-a)** for all k \u2265 1: `lcoeff (k\u22121) = (\u22121)^k \u00b7 (lagariasA k + sigmaP k) + (\u22121)^{k\u22121}`\n\ni.e. c_{k\u22121} = (\u22121)^k(a_k + \u03c3_k) + (\u22121)^{k\u22121}, where\n- c_{k\u22121} = `lcoeff (k\u22121)` \u2014 Taylor coefficients of hLi at 1 (ii\u2032-1b(i));\n- a_k = `lagariasA k` \u2014 a\u2081 = (log 4\u03c0+\u03b3)/2, a_j = 1 + \u03a3_{m odd \u2265 3} m^{\u2212j} (ii\u2032-2);\n- \u03c3_k = `sigmaP k` \u2014 paired zero power sums (ii\u2032-2).\n\nTogether with ii\u2032-2's two swaps and ii\u2032-1b(i)'s `ResW1_eq_sum`, this gives the\ncrux `Sf(n) = ResW1 n` for n \u2265 1 (the bookkeeping verified numerically in\nD-064 \u00a73: exact to 2e-21 at n = 2, 3).\n\n## 1. Route decision: \u03b24 (contour moments + coefficient split)\n\nD-064 scoped two routes: **\u03b21** (Hadamard product of \u03be) and **\u03b22** (reuse\nZeta23's proved `EF_lit_zeta`). Session-019 inventory results:\n\n- **\u03b21 is OUT as scoped**: D-064 guessed `MeromorphicOn.extract_zeros_poles`\n could seed the product \u2014 it cannot (it is the FINITE factorized-rational\n decomposition on compacts, FactorizedRational.lean; CanonicalDecomposition.lean\n is finite Blaschke on disks). Mathlib has NO Weierstrass/Hadamard infinite\n product, NO minimum-modulus theorem, NO order theory. Building those is a\n separate multi-session project with real risk.\n- **\u03b22 is OUT**: `EF_lit_zeta` evaluates \u03a3 mult\u00b7h(\u03b3_\u03c1) only for h = paperFT k\n with k \u2208 C\u00b2_c (entire of exponential type). The moment kernels\n (1/2+iz)^{\u2212k} are not entire \u2014 moments are outside the EF's test class;\n extracting them needs a \u03b4-limit re-proving a special EF instance. No savings.\n- **\u03b24 (ADOPTED)**: prove the moment identity **(M)** directly by the\n rectangle-residue machinery ALREADY BUILT in ii\u2032-1b (residueTheorem_finset,\n logDeriv normal-form residues, ppart subtraction), with the expanding-limit\n killed by the R-bound (shared with ii\u2032-5) and vertical lines vanishing by\n push-off (no poles to the right of Re = 1; decay \u2014 \u00a73.3 below). This is\n Lagarias's Lemma 4.1 content, but proved by residues instead of the product.\n\n## 2. The factorization of (4.10-a)\n\nLet xiL := (s(s\u22121)/2)\u00b7completedRiemannZeta (the entire \u03be; Mathlib's\n`completedRiemannZeta` is \u039b = \u0393R\u00b7\u03b6 with poles at 0,1; xiL removes them;\n`completedRiemannZeta_one_sub` (Mathlib) gives xiL(1\u2212s) = xiL(s); Mathlib's\n`completedRiemannZeta\u2080` is the WRONG object \u2014 its zeros are shifted, \u00a74 note).\ng := logDeriv xiL. Then (4.10-a) \u27fa (M) + (A) + (B):\n\n- **(M) moments**: \u03c3_k = \u2212g^{(k\u22121)}(0)/(k\u22121)! for all k \u2265 1. [the analytic heart]\n- **(A) archimedean**: \u03c4_j := (1/j!)\u00b7(d/ds)^j|\u2080 \u0393R\u2032/\u0393R(1+s) = (\u22121)^{j+1} a_{j+1}\n for all j \u2265 0.\n- **(B) \u03b6-piece**: coefficient of s^j in (1/s + \u03b6\u2032/\u03b6(1+s)) at 0 is \u2212c_j. [90% done\n in LiResidue \u2014 hLi(1+s) = (1+s\u22121)(\u2212\u03b6\u2032/\u03b6(1+s)) punctured, analytic at 0 with\n Taylor coefficients lcoeff; needs the iteratedDeriv_comp_add_const packaging.]\n\n**Assembly algebra** (verified twice, once numerically): g(1+s) =\n1/(1+s) + [1/s + \u03b6\u2032/\u03b6(1+s)] + \u0393R\u2032/\u0393R(1+s) has s^{k\u22121}-coefficient\n(\u22121)^{k\u22121} \u2212 c_{k\u22121} + \u03c4_{k\u22121}; the FE gives g^{(k\u22121)}(0) = (\u22121)^k g^{(k\u22121)}(1);\n(M) says \u03c3_k = \u2212g^{(k\u22121)}(0)/(k\u22121)!. Chaining:\n\u03c3_k = (\u22121)^{k+1}[(\u22121)^{k\u22121} \u2212 c_{k\u22121} + \u03c4_{k\u22121}] = 1 + (\u22121)^k c_{k\u22121} + (\u22121)^{k+1}\u03c4_{k\u22121},\nsolve for c_{k\u22121}, insert (A): c_{k\u22121} = (\u22121)^k(a_k + \u03c3_k) + (\u22121)^{k\u22121}. \u220e\n\nSanity gates: k = 1 with c\u2080 = \u2212\u03b3, a\u2081 = (log4\u03c0+\u03b3)/2 gives \u03c3\u2081 = 1 + \u03b3/2 \u2212\n\u00bdlog 4\u03c0 \u2014 the Davenport value, verified to 15 digits (session 014, D-064 \u00a73).\n\n## 3. Piece (M): the moment identities by contour (ii\u2032-3b)\n\nFor k \u2265 2, integrate w^{\u2212k}\u00b7g(w) on the rectangle [\u2212A, 3]\u00d7[\u2212T, T], T\nzero-avoiding (perimeter N(T) + pigeonhole \u2014 ii\u2032-4's L3):\n\n (1/2\u03c0i)\u222e = \u03a3_{|\u03b3|<T} mult\u00b7\u03c1^{\u2212k} + Res_{w=0}[w^{\u2212k}g],\n Res_{w=0} = g^{(k\u22121)}(0)/(k\u22121)!.\n\n- **Zeros = {IsNontrivialZero}**: off {0,1}, xiL s = 0 \u27fa \u039b s = 0 \u27fa\n IsNontrivialZero (Zeta23 RvM/CountByIntegral.lean:66, PROVED); xiL(0) =\n xiL(1) = 1/2 (from `completedRiemannZeta_residue_one` + FE transport);\n order of xiL at \u03c1 = zeroMult \u03c1 (factor nonvanishing + \u039b = \u0393R\u00b7\u03b6 with\n \u0393R(\u03c1) \u2260 0 \u2014 `Complex.Gamma\u211d_ne_zero_of_re_pos` \u2713 Mathlib).\n- **Residue machinery**: zeros via the ii\u2032-1b(iii) logDeriv-NF pattern\n (`Rfun_residue_at`); the order-k pole at 0 via a small generalization of\n ii\u2032-1b(ii)'s ppart subtraction (port Acoeff/ppart/rectInt'_ppart from\n center 1 to a general center/general analytic numerator F).\n- **T \u2192 \u221e**: horizontals die (T^{\u2212k}\u00b7O(log\u00b2T)): the R-bound\n |\u03b6\u2032/\u03b6(w) \u2212 \u03a3_{|\u03b3\u2212t|<1} 1/(w\u2212\u03c1)| \u2264 A log(|t|+2) + B\u2080 on \u03c3 \u2208 [\u22125/2, 4]\n (ii\u2032-5/R3 content \u2014 Borel\u2013Carath\u00e9odory + Jensen + Blaschke, D-064 R3\n inventory) + the direct Euler-series bound |\u03b6\u2032/\u03b6| \u2264 \u03a3 \u039b(n)n^{\u2212re} for\n re \u2265 3 (Mathlib `ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div` \u2713)\n + digamma growth O(log|w|) (from the (A) series) + trivial pieces.\n- **Verticals vanish for free**: g's poles are all in 0 < re < 1 and the\n kernel's pole is at 0 \u2014 no poles with re > 1, so V(3) = 0 by push-right\n (horizontal decay as above; |w^{\u2212k}g(a+it)| ~ log|t|\u00b7|w|^{\u2212k} integrable,\n V(A) \u2192 0 as A \u2192 \u221e). NO Laplace-integral evaluations needed (the \u03b6-piece's\n n^{\u2212w} terms close right for n \u2265 2 \u2014 not even needed; the whole line moves).\n Similarly V(\u2212A) \u2192 0 as A \u2192 \u221e (FE-reflected bounds).\n \u27f9 \u03a3_\u03c1 mult\u00b7\u03c1^{\u2212k} = \u2212g^{(k\u22121)}(0)/(k\u22121)!, k \u2265 2.\n (For k \u2265 2 the unpaired sum converges absolutely and equals sigmaP k:\n \u03a3 mult\u00b7\u03c1^{\u2212k} is conj-invariant hence real, = \u03a3 mult\u00b7Re(\u03c1^{\u2212k}) = sigmaP k.)\n- **k = 1** (the paired kernel): integrate g(w)/(2w(1\u2212w)) on [\u2212A, 2]\u00d7[\u2212T, T]:\n \u03a3_{|\u03b3|<T} mult/(2\u03c1(1\u2212\u03c1)) + g(0)/2 \u2212 g(1)/2 = (1/2\u03c0i)(V(2) \u2212 V(\u2212A)) \u2192 0,\n so \u03a3 mult/(2\u03c1(1\u2212\u03c1)) = (g(1)\u2212g(0))/2 = \u2212g(0) (FE). Then\n sigmaP 1 = \u03a3 mult\u00b7Re(1/\u03c1) = \u03a3 mult/(2\u03c1(1\u2212\u03c1)): the reflect-pair vs conj-pair\n rearrangement \u2014 (1/2)\u03a3 mult(re/|\u03c1|\u00b2 + (1\u2212re)/|1\u2212\u03c1|\u00b2), reindex \u03c1 \u21a6 1\u2212\u03c1\n (bijection on zeros, mult-preserving: conj via `riemannZeta_conj` (check),\n reflect via Zeta23 seam mult_reflect), absolute convergence throughout.\n \u27f9 sigmaP 1 = \u2212g(0) = \u2212g^{(0)}(0)/0! \u2014 (M) at k = 1.\n\n## 4. Piece (A): the archimedean coefficients (ii\u2032-3a, no contour deps)\n\n\u03c4_j = (1/j!)\u00b7iteratedDeriv j (fun s => logDeriv Gamma\u211d (1+s)) 0 = (\u22121)^{j+1} a_{j+1}.\n\n- \u0393R logDeriv split: logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7digamma((1+s)/2)\n (Gamma\u211d_def = \u03c0^{\u2212s/2}\u0393(s/2) \u2713 Mathlib; logDeriv product/comp algebra).\n- **j = 0**: \u03c4\u2080 = \u2212(log \u03c0)/2 + (1/2)\u00b7digamma(1/2) = \u2212(log \u03c0)/2 + (1/2)(\u22122log2 \u2212 \u03b3)\n = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212a\u2081 \u2014 via `Complex.digamma_one_half` \u2713 MATHLIB HAS IT.\n- **j \u2265 1**: \u03c8^{(j)}(1/2) = (\u22121)^{j+1} j! \u03a3_{m\u22650} (m+1/2)^{\u2212(j+1)}, then\n \u03a3_{m\u22650}(m+1/2)^{\u2212(j+1)} = 2^{j+1}\u00b7lagariasA(j+1) (reindex m \u21a6 2m+1: \u2115 \u2243\n {odd naturals}, peel m = 0 \u2194 the \"1 +\" in lagariasA; tsum_eq_zero_add +\n Equiv.tsum_eq).\n The digamma series is NOT in Mathlib; build from BohrMollerup's\n `logGammaSeq x n = x log n + log n! \u2212 \u03a3_{m=0}^n log(x+m)` with\n `tendsto_log_gamma` \u2713 (real, x > 0):\n (i) \u03c8_real x := deriv (log \u2218 Gamma) x = lim_n [log n \u2212 \u03a3_{m=0}^n 1/(x+m)]\n = \u2212\u03b3 \u2212 1/x + \u03a3_{m\u22651}(1/m \u2212 1/(x+m)) for x > 0 \u2014 deriv under the\n locally-uniform limit (real deriv-limit lemma; the derived sequence is\n uniformly Cauchy on compacts by the \u03a3 1/m\u00b2 tail);\n (ii) termwise j-fold derivation (induction; each derivative series M-tested):\n \u03c8_real^{(j)}(x) = (\u22121)^{j+1} j! \u03a3_{m\u22650} (x+m)^{\u2212(j+1)} (j \u2265 1);\n (iii) complex bridge: iteratedDeriv j (\u0393R\u2032/\u0393R(1+\u00b7)) 0 (complex) =\n real-line j-th derivative at 0 (ofReal comp; analytic at 0 since\n Gamma\u211d(1) = 1 \u2260 0 \u2014 `Gamma\u211d_one`, `Gamma\u211d_ne_zero_of_re_pos` \u2713).\n Cost: the heaviest single rock of ii\u2032-3a (self-contained real analysis).\n\n## 5. Sequencing (supersedes D-064's ii\u2032-3 position)\n\nThe R-bound ((M)'s horizontal decay) is ii\u2032-5/R3's content and is ALSO needed\nby ii\u2032-6's side estimates \u2014 build it ONCE, before the moments:\n\n- **ii\u2032-3a** (next): piece (B) packaging + piece (A). [no contour deps]\n- **ii\u2032-4** (unchanged): L3 zero-avoiding T (pigeonhole on perimeter C\u2080/FAlt)\n + L1 kernel bounds (|k_n| \u2264 2, e\u2074+1, e^{\u221an/2}+1; trivial residue).\n- **ii\u2032-5** (unchanged): R-bound via the D-064 R3 local route\n (Borel\u2013Carath\u00e9odory + Jensen + Blaschke/StrongPNTPrefix + FE strip bound\n via riemannZeta_one_sub + Stirling; digamma Lemma D).\n- **ii\u2032-3b**: piece (M) moments (uses ii\u2032-4's zero-avoiding T + ii\u2032-5's\n R-bound + the rectangle machinery).\n- **ii\u2032-3c**: the (4.10-a) assembly (\u00a72 algebra) \u2192 the crux\n `sf_eq_resW1 : Sf n = (ResW1 n).re` for n \u2265 1.\n- **ii\u2032-6, ii\u2032-7** unchanged (L0 assembly + closure).\n\n## 6. Mathlib inventory used (all verified to exist, session 019)\n\n`TendstoLocallyUniformlyOn.differentiableOn` (Weierstrass convergence);\n`Complex.digamma_one_half`, `digamma_one`, `digamma_apply_add_one`,\n`meromorphic_digamma`; `Gamma\u211d_def`, `Gamma\u211d_one`, `Gamma\u211d_ne_zero_of_re_pos`,\n`Gamma\u211d_eq_zero_iff` (zeros of \u0393R = {\u22122n} \u2014 also the future trivial-zero\nsimplicity input); `completedRiemannZeta_one_sub`, `completedRiemannZeta_residue_one`;\n`ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div` (\u2212\u03b6\u2032/\u03b6\nDirichlet series, re > 1); `BohrMollerup.tendsto_log_gamma` + `logGammaSeq`;\nZeta23: `completedRiemannZeta s = 0 \u2194 IsNontrivialZero s` (CountByIntegral.lean),\nseam `mult_reflect`, `WeilEF.zero_sum_inv_sq`. NOT in Mathlib (relevant gaps):\nWeierstrass/Hadamard products, polygamma, digamma partial fractions (built\nin ii\u2032-3a), `riemannZeta_conj` (conj-invariance of \u03b6 \u2014 to check/derive via\nthe LSeries/integral definition), trivial-zero simplicity deriv \u03b6(\u22122) \u2260 0\n(deferred from ii\u2032-1b(iii); route: FE + Gamma\u211d_eq_zero_iff + \u03b6(3) \u2260 0).\n\n## 7. Risks\n\n- The digamma-series build (ii\u2032-3a) is the kind of real-analysis grind that\n can sprawl (deriv-under-limit + iteration + complex bridge). Mitigation:\n it is self-contained and has the numeric gates (\u03c8\u2032(1/2) = \u03c0\u00b2/2 etc.).\n- (M)'s k = 1 rearrangement needs zeroMult conj-invariance \u2014 small proof via\n `riemannZeta (conj s) = conj (riemannZeta s)` (to be located in Mathlib or\n proved from the definition).\n- The R-bound remains the long pole of ii\u2032-5 per D-064 R3 (2\u20133 sessions);\n ii\u2032-3b waits on it. Paper A stays frozen/submittable throughout (freeze\n protocol; only new files + root imports are touched).\n"
}
result 2026-08-22 05:13:27Z → 2026-08-25 04:50:43Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-030-honest-Bn-fold.py",
"content": "#!/usr/bin/env python3\n\"\"\"E-030 \u2014 ii\u2032-6 design validation: the honest assembly vs the baked B(n)\nand vs the corrected (honest) Bn. Session 038 (ii\u2032-6-0, D-071).\n\nFindings preserved (user protocol step 8 \u2014 audit history):\n F-A: the residue sum \u03bb_n(T) runs over BOTH signs of \u03b3 \u27f9 honest bridge\n |\u03bb_n(T)| \u2264 4\u00b7FAlt(T); D-036/D-037/E-023's B(n) charges 2\u00b7FAlt\n (factor-2 accounting slip; R-004 unaffected: \u226a margins).\n F-B: I_III's near-sum needs the two-unit count (2/3)\u00b7Z2 vs baked\n (2/3)\u0108\u2080 (D-069 Finding 2's predicted (4/3)-ish correction).\n F-C: with the baked Bn the honest assembly overshoots for n \u2273 5\u00d710\u2077\n (ratio 1.012 at 10\u00b9\u00b2); with the corrected Bn (4F, (2/3)Z2) the\n fold is the identity (provable), and margin > 0 is preserved\n with huge slack on the whole range [8\u00d710\u2074, N\u2081].\n\nChecks:\n V1: baked-vs-honest ratio table (the F-C overshoot demonstration).\n V2: corrected-Bn margin > 0 on a log grid over [8\u00d710\u2074, N\u2081], and\n margin \u2265 baked margin at the certified base points (values improve).\n V3: the horizontal segment-integral form \u2264 its baked share\n (NI + 5.5\u00b7(10.5 log + 48) + 3.3 \u2264 7\u00b7Hhat + 3.3) on the grid.\n\"\"\"\nimport json\nimport sys\nfrom pathlib import Path\n\nimport mpmath as mp\n\nmp.mp.dps = 50\n\nDATA = Path(__file__).resolve().parent.parent / \"data\"\nCSV = DATA / \"E-030-honest-Bn-fold.csv\"\nJSON = DATA / \"E-030-honest-Bn-fold.json\"\n\npi, e = mp.pi, mp.e\n\n\ndef C0hat(t):\n return mp.mpf(\"0.433\") * mp.log(t + 2) + mp.mpf(\"0.886\") * mp.log(mp.log(t + 2)) + mp.mpf(\"2.9\")\n\n\ndef Z2(t):\n return mp.mpf(\"0.6\") * mp.log(t + 2) + mp.mpf(\"0.886\") * mp.log(mp.log(t + 2)) + mp.mpf(\"2.7\")\n\n\ndef FAlt(T):\n return ((1 / (2 * pi)) * (T * mp.log(T)) + mp.mpf(\"0.137\") * mp.log(T)\n + mp.mpf(\"0.443\") * mp.log(mp.log(T)) + (mp.mpf(7) / 8 + mp.mpf(\"1.588\")))\n\n\ndef Hhat(T):\n return 3 * C0hat(T) ** 2 + mp.mpf(\"10.5\") * mp.log(T + 2) + 48\n\n\ndef IIMaj(n):\n return 2 * (mp.sqrt(n) + 1) * (mp.e ** (mp.sqrt(n) / 2) + 1) * mp.mpf(\"0.57\") * 2 ** (-(2 * mp.sqrt(n) - 2))\n\n\ndef Bn_baked(n):\n T = mp.sqrt(n) + 1\n return (2 * FAlt(T) + 4 * T * ((mp.mpf(2) / 3) * C0hat(T) + mp.mpf(\"10.5\") * mp.log(T + 2) + 48)\n + 40 * mp.mpf(\"1.3352\") + 2 * (e ** 4 + 1) * (7 * Hhat(T) + mp.mpf(\"3.3\")) + IIMaj(n) + 1)\n\n\ndef Bn_honest(n):\n \"\"\"Corrected Bn: bridge 4F, I_III (2/3)Z2.\"\"\"\n T = mp.sqrt(n) + 1\n return (4 * FAlt(T) + 4 * T * ((mp.mpf(2) / 3) * Z2(T) + mp.mpf(\"10.5\") * mp.log(T + 2) + 48)\n + 40 * mp.mpf(\"1.3352\") + 2 * (e ** 4 + 1) * (7 * Hhat(T) + mp.mpf(\"3.3\")) + IIMaj(n) + 1)\n\n\ndef honest_assembly(n):\n \"\"\"The pieces the Lean assembly will actually prove (horizontal\n segment-integral form; Finding-2-extended pigeonhole clearance).\"\"\"\n T = mp.sqrt(n) + 1\n a = mp.sqrt(n)\n c = 1 / (9 * C0hat(a + 2)) # 3-unit pigeonhole clearance\n NI = Z2(T) * 2 * mp.log(mp.mpf(\"16.5\") / c) # near-sum integral on the horizontal\n bridge = 4 * FAlt(T)\n left = 4 * T * ((mp.mpf(2) / 3) * Z2(T) + mp.mpf(\"10.5\") * mp.log(T + 2) + 48)\n horiz = 2 * (e ** 4 + 1) * (NI + mp.mpf(\"5.5\") * (mp.mpf(\"10.5\") * mp.log(T + 2) + 48) + mp.mpf(\"3.3\"))\n return bridge + left + 40 * mp.mpf(\"1.3352\") + horiz + IIMaj(n) + 1, NI\n\n\ndef sInftyLower(n):\n return mp.mpf(\"0.5\") * n * mp.log(n) + (mp.mpf(\"-1.41894\")) * n - 4\n\n\ndef main() -> int:\n if JSON.exists() and \"--force\" not in sys.argv:\n print(f\"cached: {JSON} (use --force to recompute)\")\n return 0\n\n rows = []\n grid = [mp.mpf(10) ** 5, mp.mpf(\"1.2e5\"), mp.mpf(\"1.5e5\"), mp.mpf(\"2e5\"), mp.mpf(\"5e5\"),\n mp.mpf(10) ** 6, mp.mpf(10) ** 7, mp.mpf(10) ** 8, mp.mpf(10) ** 9, mp.mpf(10) ** 10,\n mp.mpf(10) ** 12, mp.mpf(10) ** 16, mp.mpf(10) ** 20, mp.mpf(\"9e24\")]\n for n in grid:\n h, NI = honest_assembly(n)\n T = mp.sqrt(n) + 1\n hbaked_share = 7 * Hhat(T) + mp.mpf(\"3.3\")\n hinside = NI + mp.mpf(\"5.5\") * (mp.mpf(\"10.5\") * mp.log(T + 2) + 48) + mp.mpf(\"3.3\")\n rows.append({\n \"n\": mp.nstr(n, 8),\n \"Bn_baked\": mp.nstr(Bn_baked(n), 12),\n \"Bn_honest\": mp.nstr(Bn_honest(n), 12),\n \"honest_assembly\": mp.nstr(h, 12),\n \"assembly_over_baked\": mp.nstr(h / Bn_baked(n), 6),\n \"assembly_over_honestBn\": mp.nstr(h / Bn_honest(n), 6),\n \"horizIntegral_over_bakedShare\": mp.nstr(hinside / hbaked_share, 6),\n \"margin_honestBn\": mp.nstr(sInftyLower(n) - Bn_honest(n) + 1, 12),\n \"margin_bakedBn\": mp.nstr(sInftyLower(n) - Bn_baked(n) + 1, 12),\n })\n\n # V1: overshoot demonstration (baked)\n v1 = any(mp.mpf(r[\"assembly_over_baked\"]) > 1 for r in rows)\n # V2: margin with corrected Bn positive on the whole grid\n v2 = all(mp.mpf(r[\"margin_honestBn\"]) > 0 for r in rows)\n # V3: horizontal segment-integral fits under its baked share\n v3 = all(mp.mpf(r[\"horizIntegral_over_bakedShare\"]) < 1 for r in rows)\n # assembly always under the CORRECTED Bn (the fold works)\n v4 = all(mp.mpf(r[\"assembly_over_honestBn\"]) < 1 for r in rows)\n\n DATA.mkdir(exist_ok=True)\n with CSV.open(\"w\") as f:\n f.write(\",\".join(rows[0].keys()) + \"\\n\")\n for r in rows:\n f.write(\",\".join(r.values()) + \"\\n\")\n sidecar = {\n \"experiment\": \"E-030\",\n \"title\": \"ii\u2032-6 design validation: honest assembly vs baked Bn and corrected Bn\",\n \"session\": \"038 (ii\u2032-6-0)\",\n \"design_doc\": \"D-071\",\n \"checks\": {\"V1_baked_overshoot_present\": v1, \"V2_margin_honestBn_positive\": v2,\n \"V3_horizontal_integral_fits\": v3, \"V4_fold_under_corrected_Bn\": v4},\n \"all_checks_pass\": v1 and v2 and v3 and v4,\n \"dps\": 50,\n \"notes\": \"F-A bridge factor-2 (both-signs), F-B I_III two-unit count, \"\n \"F-C baked Bn overshoot beyond ~5e7; corrected Bn (4F, (2/3)Z2) \"\n \"makes the fold the identity; margin positive everywhere.\",\n }\n with JSON.open(\"w\") as f:\n json.dump(sidecar, f, indent=2)\n print(f\"V1 overshoot present: {v1} | V2 margin>0: {v2} | V3 horiz fits: {v3} | V4 fold works: {v4}\")\n print(f\"wrote {CSV} + {JSON}\")\n return 0 if sidecar[\"all_checks_pass\"] else 1\n\n\nif __name__ == \"__main__\":\n sys.exit(main())\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"`logGammaSeq x n = x * log n + log (n!) − ∑_{m=0}^n log(x+m)` and `tendsto_log_gamma (hx : 0 < x) : Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))` ✓ (Real.Gamma, real x). This is the seed for the digamma series build.\n\nI now have a complete picture. Time to write the design note D-066 and register the route decision. Let me define the architecture:\n\n**ii′-3 architecture (route β4 — \"contour moments + coefficient split\"), replacing/ refining D-064's R2(iii) β1/β2 sketch:**\n\nTarget: for k ≥ 1, the a-form identity c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}, where:\n- c_{k−1} = lcoeff (k−1) (LiResidue) — Taylor coefficients of hLi at 1.\n- a_k = lagariasA k (LiSwaps) — archimedean odd-zeta values.\n- σ_k = sigmaP k (LiSwaps) — paired zero power sums.\n\n**The factorization:** With g := logDeriv xiL (xiL := (s(s−1)/2)·completedRiemannZeta, entire, FE xiL(1−s) = xiL(s)):\n\n(4.10)-a ⟺ (M) + (A) + (B) where:\n- (M) [the analytic heart — moment identity]: σ_k = −g^{(k−1)}(0)/(k−1)! for all k ≥ 1.\n- (A) [archimedean]: τ_j := (j-th Taylor coefficient of ΓR′/ΓR(1+·) at 0)/j! = (−1)^{j+1}a_{j+1} for all j ≥ 0.\n- (B) [ζ-piece, mostly done]: coefficient of s^j in (1/s + ζ′/ζ(1+s)) at 0 = −c_j.\n\nAssembly (algebra, verified numerically session 014 + re-verified in this design): from xiL's logDeriv decomposition at 1+s and the FE reflection g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1), the identity (4.10)-a follows by coefficient comparison. [I verified this chain twice above.]\n\n**Piece inventory & costs:**\n- (B): LiResidue has hLi/lcoeff/hLi_analyticAt_one/hLi_eq_near_one/hLi_iteratedDeriv_div_factorial. Remaining: the coefficient-extraction packaging: (fun s ↦ (1/s + ζ′/ζ(1+s))) equals −Σ c_j s^j near 0 — i.e. (fun s ↦ 1 + s·ζ′/ζ(1+s))... = −hLi(1+s) eventually, analytic at 0, iteratedDeriv j = −j!·... — the iteratedDeriv_comp_add_const bridge + analytic continuation of coefficients. SMALL (~0.3 sess).\n- (A): j = 0 via Complex.digamma_one_half ✓ Mathlib. j ≥ 1: build the real digamma series from BohrMollerup.logGammaSeq (tendsto_log_gamma ✓ Mathlib): ψ_real(x) := deriv (log ∘ Gamma) x = −γ − 1/x + Σ_{m≥1}(1/m − 1/(x+m)), termwise j-fold derivative at x = 1/2 (uniform-on-compacts M-test + deriv-of-limit), ψ^{(j)}(1/2) = (−1)^{j+1}j!Σ_{m≥0}(m+1/2)^{−(j+1)}; reindex Σ_{m≥0}(2m+1)^{−(j+1)} = lagariasA(j+1) (bespoke equiv m ↦ 2m+1 / peel); complex-bridge iteratedDeriv of ΓR′/ΓR(1+·) at 0 = real-line derivatives (ofRealCLM comp). MODERATE-HEAVY (~1–1.5 sess).\n- (C) — the moments (M): \n (C-i) rectangle residue theorem for the integrand w^{−k}·g(w): ppart-at-0 port of LiPrincipal's machinery (the Acoeff/ppart/rectInt'_ppart pattern with the center generalized) + residue-at-zeros via my Rfun_residue_at pattern (logDeriv NF). Need xiL entire + zero-set identification (zeros of xiL = {IsNontrivialZero} off {0,1} via Zeta23's completedRiemannZeta-zero iff + the factor s(s−1)/2 nonzero elsewhere + value 1/2 at 0,1) + order = zeroMult (order multiplicativity). MODERATE (~0.5–1 sess).\n (C-ii) the T → ∞ horizontal decay: needs the R-bound (|ζ′/ζ(w) − Σ_{|γ−t|<1}1/(w−ρ)| ≤ A log(|t|+2) + B₀) on the R-zone + direct Euler-product bound (−ζ′/ζ = Σ Λ(n)n^{−s} ✓ `ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div` Mathlib has) off it + digamma growth bound (|ψ(w)| = O(log|w|) for re w ≥ 3 — from the (A) series) + zero-avoiding T (pigeonhole on perimeter N(T)). THE R-BOUND IS ii′-5's CONTENT — shared dependency.\n (C-iii) vertical evaluations: V(3) = 0 / V(−A) → 0 (push-right/left with no-poles + decay; Laplace-term vanishing for the ζ-piece via x = 1/n < 1 closing right — actually WAIT — for the moments I showed the verticals vanish by push-right/left with NO pole-crossing — the ζ-piece's termwise vanishing needs the Laplace integral (1/2πi)∫_{(c)} w^{−k}n^{−w}dw = 0 for n ≥ 2 — hmm — actually NO: my final argument was simpler: V(3) = 0 by pushing the whole line right (integrand has no poles with re > 1... wait g's poles are ρ's with re < 1 ✓ and the kernel pole at 0 ✓ so NO poles with re > 1 — the push-right needs only horizontal decay + vertical integrability — NO termwise Laplace needed!!). Let me re-examine: V(3) = 0 because: rectangle [3, A]×[−T, T] contains no poles; T → ∞: horizontals → 0 (direct bounds: ζ′/ζ Euler-series bound for re ≥ 3 ✓ |ζ′/ζ(σ+it)| ≤ Σ Λ(n)n^{−3} ✓ t-INDEPENDENT — even better; digamma O(log) ✓); A → ∞: V(A) → 0 (|w^{−k}g| ~ log|t|·|w|^{−k} integrable tails ✓). ✓✓ NO Laplace evaluations needed at all! The verticals vanish for FREE (no poles to the right of Re = 1, decay). Same for k=1's kernel (poles at 0,1 only; no poles right of 2 → V(2) = 0; V(−A) → 0 as A → ∞ since no poles left of −A for A ≥ 0 and decay ✓). GREAT — so (C-iii) is just integrability/decay bookkeeping, no integral evaluations.\n So the moment identity: Σ_{|γ|<T} mult·ρ^{−k} + Res_0 = (1/2πi)(V(3) − V(−A)) → 0 − 0. MODERATE.\n (C-iv) k = 1: the paired kernel 1/(2w(1−w))·g(w): rectangle [−A, 2]... wait — need poles 0 and 1 INSIDE: rectangle [−A, 2]×[−T, T] contains 0, 1 ✓ (re ∈ (−A, 2)); the ρ's ✓. T → ∞: Σ mult/(2ρ(1−ρ)) + Res_{w=0} + Res_{w=1} = (1/2πi)(V(2) − V(−A)) = 0. Residues: at 0: g(0)·(1/2); at 1: g(1)·(−1/2)·... K(w) = 1/(2w(1−w)): at w=0: residue 1/2·g(0); at w=1: 1/(2w(1−w)) = −1/(2w(w−1)): residue −g(1)/2. So Σ mult/(2ρ(1−ρ)) = (g(1) − g(0))/2 = −g(0) (FE: g(1) = −g(0)) ✓. Then sigmaP 1 = that sum (reflect/conj rearrangement — needs zeroMult conj-invariance: analyticOrderAt ζ (conj ρ) = analyticOrderAt ζ ρ — via riemannZeta_conj — check Mathlib for `riemannZeta_conj`!) — SMALL-MODERATE.\n (C-v) FE reflection of derivatives: iteratedDeriv m g 0 = (−1)^{m+1}·... g(s) = −g(1−s): iteratedDeriv m g 0 = (−1)^{m+1} g^{(m)}(1)·... — the chain: g(s) = −g(1−s) ⟹ g^{(m)}(s) = (−1)^{m+1}g^{(m)}(1−s) ⟹ at 0: (−1)^{m+1}g^{(m)}(1). SMALL (iteratedDeriv comp lemma).\n- (D) assembly: coefficient comparison — SMALL.\n\n**Sequencing recommendation:** the R-bound (C-ii's core) is ii′-5's content and also feeds ii′-6 — so reorder: **ii′-3a := (B) + (A)** [no contour dependencies; start next session]; **ii′-4** (L3 zero-avoiding T + L1 kernel bounds — elementary); **ii′-5** (R-bound via D-064 R3 local route); **ii′-3b := (C) moments**; **ii′-3c := (D) assembly (4.10)**; then ii′-6, ii′-7. This respects D-064's map with the moments re-seated after the R-bound.\n\nSanity gates (per D-064): k=1: σ₁ = 1 + γ/2 − ½log4π (verified 15 digits numerically, session 014); j=0: τ₀ = −a₁ via digamma_one_half — the γ/log4π combination ✓; the full (4.10)-a at k=1: c₀ = 1 − a₁ − σ₁ ✓ (γ matches: c₀ = −γ ⟸ 1 − (log4π+γ)/2 − (1+γ/2−½log4π) = 1 − log4π/2 − γ/2 − 1 − γ/2 + log4π/2 = −γ ✓).\n\nNow — should I START ii′-3a this session? The session has been a design session (per STATE: \"First task: read EF_lit_zeta's exact statement + write the ii′-3 design note (D-066) before any Lean\"). The design note is the deliverable. Let me write D-066 now, then decide about starting Lean work on Piece B (small) this session. Given the depth of exploration done, writing D-066 carefully + possibly starting Piece B (the coefficient-extraction packaging, ~0.3 sess) is a good scope. Let me write D-066 first.\n\nActually — let me reconsider the scope: the session protocol says save artifacts immediately. The design note is the main artifact. Let me write it comprehensively, then assess time/energy for starting Piece B. Actually the instructions say avoid time estimates; just do it. Let me write D-066.","signature":""},{"type":"text","text":"I have the complete architecture. Writing the design note D-066 now."},{"type":"tool_use","id":"Write_184","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\derivations\\D-066-ii-prime-3-design.md","content":"# D-066 — Tier ii′ sub-stage ii′-3 design: Lagarias (4.10) via contour moments + coefficient split\nDate: 2026-08-21 | Session: 019 | Task: 5.1 tier ii′ sub-stage 3 (design)\nStatus: design COMPLETE — route decided (β4 below, replacing D-064's β1/β2\nsketch); dependency resequencing identified (R-bound shared with ii′-5).\n\n## 0. What ii′-3 must prove\n\nThe a-form of Lagarias's (4.10) (derived from D-064's τ-form with\nτ_{j−1} = (−1)^j a_j; conventions: D-037/D-064, LiSwaps.lean):\n\n **(4.10-a)** for all k ≥ 1: `lcoeff (k−1) = (−1)^k · (lagariasA k + sigmaP k) + (−1)^{k−1}`\n\ni.e. c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}, where\n- c_{k−1} = `lcoeff (k−1)` — Taylor coefficients of hLi at 1 (ii′-1b(i));\n- a_k = `lagariasA k` — a₁ = (log 4π+γ)/2, a_j = 1 + Σ_{m odd ≥ 3} m^{−j} (ii′-2);\n- σ_k = `sigmaP k` — paired zero power sums (ii′-2).\n\nTogether with ii′-2's two swaps and ii′-1b(i)'s `ResW1_eq_sum`, this gives the\ncrux `Sf(n) = ResW1 n` for n ≥ 1 (the bookkeeping verified numerically in\nD-064 §3: exact to 2e-21 at n = 2, 3).\n\n## 1. Route decision: β4 (contour moments + coefficient split)\n\nD-064 scoped two routes: **β1** (Hadamard product of ξ) and **β2** (reuse\nZeta23's proved `EF_lit_zeta`). Session-019 inventory results:\n\n- **β1 is OUT as scoped**: D-064 guessed `MeromorphicOn.extract_zeros_poles`\n could seed the product — it cannot (it is the FINITE factorized-rational\n decomposition on compacts, FactorizedRational.lean; CanonicalDecomposition.lean\n is finite Blaschke on disks). Mathlib has NO Weierstrass/Hadamard infinite\n product, NO minimum-modulus theorem, NO order theory. Building those is a\n separate multi-session project with real risk.\n- **β2 is OUT**: `EF_lit_zeta` evaluates Σ mult·h(γ_ρ) only for h = paperFT k\n with k ∈ C²_c (entire of exponential type). The moment kernels\n (1/2+iz)^{−k} are not entire — moments are outside the EF's test class;\n extracting them needs a δ-limit re-proving a special EF instance. No savings.\n- **β4 (ADOPTED)**: prove the moment identity **(M)** directly by the\n rectangle-residue machinery ALREADY BUILT in ii′-1b (residueTheorem_finset,\n logDeriv normal-form residues, ppart subtraction), with the expanding-limit\n killed by the R-bound (shared with ii′-5) and vertical lines vanishing by\n push-off (no poles to the right of Re = 1; decay — §3.3 below). This is\n Lagarias's Lemma 4.1 content, but proved by residues instead of the product.\n\n## 2. The factorization of (4.10-a)\n\nLet xiL := (s(s−1)/2)·completedRiemannZeta (the entire ξ; Mathlib's\n`completedRiemannZeta` is Λ = ΓR·ζ with poles at 0,1; xiL removes them;\n`completedRiemannZeta_one_sub` (Mathlib) gives xiL(1−s) = xiL(s); Mathlib's\n`completedRiemannZeta₀` is the WRONG object — its zeros are shifted, §4 note).\ng := logDeriv xiL. Then (4.10-a) ⟺ (M) + (A) + (B):\n\n- **(M) moments**: σ_k = −g^{(k−1)}(0)/(k−1)! for all k ≥ 1. [the analytic heart]\n- **(A) archimedean**: τ_j := (1/j!)·(d/ds)^j|₀ ΓR′/ΓR(1+s) = (−1)^{j+1} a_{j+1}\n for all j ≥ 0.\n- **(B) ζ-piece**: coefficient of s^j in (1/s + ζ′/ζ(1+s)) at 0 is −c_j. [90% done\n in LiResidue — hLi(1+s) = (1+s−1)(−ζ′/ζ(1+s)) punctured, analytic at 0 with\n Taylor coefficients lcoeff; needs the iteratedDeriv_comp_add_const packaging.]\n\n**Assembly algebra** (verified twice, once numerically): g(1+s) =\n1/(1+s) + [1/s + ζ′/ζ(1+s)] + ΓR′/ΓR(1+s) has s^{k−1}-coefficient\n(−1)^{k−1} − c_{k−1} + τ_{k−1}; the FE gives g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1);\n(M) says σ_k = −g^{(k−1)}(0)/(k−1)!. Chaining:\nσ_k = (−1)^{k+1}[(−1)^{k−1} − c_{k−1} + τ_{k−1}] = 1 + (−1)^k c_{k−1} + (−1)^{k+1}τ_{k−1},\nsolve for c_{k−1}, insert (A): c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}. ∎\n\nSanity gates: k = 1 with c₀ = −γ, a₁ = (log4π+γ)/2 gives σ₁ = 1 + γ/2 −\n½log 4π — the Davenport value, verified to 15 digits (session 014, D-064 §3).\n\n## 3. Piece (M): the moment identities by contour (ii′-3b)\n\nFor k ≥ 2, integrate w^{−k}·g(w) on the rectangle [−A, 3]×[−T, T], T\nzero-avoiding (perimeter N(T) + pigeonhole — ii′-4's L3):\n\n (1/2πi)∮ = Σ_{|γ|<T} mult·ρ^{−k} + Res_{w=0}[w^{−k}g],\n Res_{w=0} = g^{(k−1)}(0)/(k−1)!.\n\n- **Zeros = {IsNontrivialZero}**: off {0,1}, xiL s = 0 ⟺ Λ s = 0 ⟺\n IsNontrivialZero (Zeta23 RvM/CountByIntegral.lean:66, PROVED); xiL(0) =\n xiL(1) = 1/2 (from `completedRiemannZeta_residue_one` + FE transport);\n order of xiL at ρ = zeroMult ρ (factor nonvanishing + Λ = ΓR·ζ with\n ΓR(ρ) ≠ 0 — `Complex.Gammaℝ_ne_zero_of_re_pos` ✓ Mathlib).\n- **Residue machinery**: zeros via the ii′-1b(iii) logDeriv-NF pattern\n (`Rfun_residue_at`); the order-k pole at 0 via a small generalization of\n ii′-1b(ii)'s ppart subtraction (port Acoeff/ppart/rectInt'_ppart from\n center 1 to a general center/general analytic numerator F).\n- **T → ∞**: horizontals die (T^{−k}·O(log²T)): the R-bound\n |ζ′/ζ(w) − Σ_{|γ−t|<1} 1/(w−ρ)| ≤ A log(|t|+2) + B₀ on σ ∈ [−5/2, 4]\n (ii′-5/R3 content — Borel–Carathéodory + Jensen + Blaschke, D-064 R3\n inventory) + the direct Euler-series bound |ζ′/ζ| ≤ Σ Λ(n)n^{−re} for\n re ≥ 3 (Mathlib `ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div` ✓)\n + digamma growth O(log|w|) (from the (A) series) + trivial pieces.\n- **Verticals vanish for free**: g's poles are all in 0 < re < 1 and the\n kernel's pole is at 0 — no poles with re > 1, so V(3) = 0 by push-right\n (horizontal decay as above; |w^{−k}g(a+it)| ~ log|t|·|w|^{−k} integrable,\n V(A) → 0 as A → ∞). NO Laplace-integral evaluations needed (the ζ-piece's\n n^{−w} terms close right for n ≥ 2 — not even needed; the whole line moves).\n Similarly V(−A) → 0 as A → ∞ (FE-reflected bounds).\n ⟹ Σ_ρ mult·ρ^{−k} = −g^{(k−1)}(0)/(k−1)!, k ≥ 2.\n (For k ≥ 2 the unpaired sum converges absolutely and equals sigmaP k:\n Σ mult·ρ^{−k} is conj-invariant hence real, = Σ mult·Re(ρ^{−k}) = sigmaP k.)\n- **k = 1** (the paired kernel): integrate g(w)/(2w(1−w)) on [−A, 2]×[−T, T]:\n Σ_{|γ|<T} mult/(2ρ(1−ρ)) + g(0)/2 − g(1)/2 = (1/2πi)(V(2) − V(−A)) → 0,\n so Σ mult/(2ρ(1−ρ)) = (g(1)−g(0))/2 = −g(0) (FE). Then\n sigmaP 1 = Σ mult·Re(1/ρ) = Σ mult/(2ρ(1−ρ)): the reflect-pair vs conj-pair\n rearrangement — (1/2)Σ mult(re/|ρ|² + (1−re)/|1−ρ|²), reindex ρ ↦ 1−ρ\n (bijection on zeros, mult-preserving: conj via `riemannZeta_conj` (check),\n reflect via Zeta23 seam mult_reflect), absolute convergence throughout.\n ⟹ sigmaP 1 = −g(0) = −g^{(0)}(0)/0! — (M) at k = 1.\n\n## 4. Piece (A): the archimedean coefficients (ii′-3a, no contour deps)\n\nτ_j = (1/j!)·iteratedDeriv j (fun s => logDeriv Gammaℝ (1+s)) 0 = (−1)^{j+1} a_{j+1}.\n\n- ΓR logDeriv split: logDeriv Gammaℝ (1+s) = −(log π)/2 + (1/2)·digamma((1+s)/2)\n (Gammaℝ_def = π^{−s/2}Γ(s/2) ✓ Mathlib; logDeriv product/comp algebra).\n- **j = 0**: τ₀ = −(log π)/2 + (1/2)·digamma(1/2) = −(log π)/2 + (1/2)(−2log2 − γ)\n = −(log 4π + γ)/2 = −a₁ — via `Complex.digamma_one_half` ✓ MATHLIB HAS IT.\n- **j ≥ 1**: ψ^{(j)}(1/2) = (−1)^{j+1} j! Σ_{m≥0} (m+1/2)^{−(j+1)}, then\n Σ_{m≥0}(m+1/2)^{−(j+1)} = 2^{j+1}·lagariasA(j+1) (reindex m ↦ 2m+1: ℕ ≃\n {odd naturals}, peel m = 0 ↔ the \"1 +\" in lagariasA; tsum_eq_zero_add +\n Equiv.tsum_eq).\n The digamma series is NOT in Mathlib; build from BohrMollerup's\n `logGammaSeq x n = x log n + log n! − Σ_{m=0}^n log(x+m)` with\n `tendsto_log_gamma` ✓ (real, x > 0):\n (i) ψ_real x := deriv (log ∘ Gamma) x = lim_n [log n − Σ_{m=0}^n 1/(x+m)]\n = −γ − 1/x + Σ_{m≥1}(1/m − 1/(x+m)) for x > 0 — deriv under the\n locally-uniform limit (real deriv-limit lemma; the derived sequence is\n uniformly Cauchy on compacts by the Σ 1/m² tail);\n (ii) termwise j-fold derivation (induction; each derivative series M-tested):\n ψ_real^{(j)}(x) = (−1)^{j+1} j! Σ_{m≥0} (x+m)^{−(j+1)} (j ≥ 1);\n (iii) complex bridge: iteratedDeriv j (ΓR′/ΓR(1+·)) 0 (complex) =\n real-line j-th derivative at 0 (ofReal comp; analytic at 0 since\n Gammaℝ(1) = 1 ≠ 0 — `Gammaℝ_one`, `Gammaℝ_ne_zero_of_re_pos` ✓).\n Cost: the heaviest single rock of ii′-3a (self-contained real analysis).\n\n## 5. Sequencing (supersedes D-064's ii′-3 position)\n\nThe R-bound ((M)'s horizontal decay) is ii′-5/R3's content and is ALSO needed\nby ii′-6's side estimates — build it ONCE, before the moments:\n\n- **ii′-3a** (next): piece (B) packaging + piece (A). [no contour deps]\n- **ii′-4** (unchanged): L3 zero-avoiding T (pigeonhole on perimeter C₀/FAlt)\n + L1 kernel bounds (|k_n| ≤ 2, e⁴+1, e^{√n/2}+1; trivial residue).\n- **ii′-5** (unchanged): R-bound via the D-064 R3 local route\n (Borel–Carathéodory + Jensen + Blaschke/StrongPNTPrefix + FE strip bound\n via riemannZeta_one_sub + Stirling; digamma Lemma D).\n- **ii′-3b**: piece (M) moments (uses ii′-4's zero-avoiding T + ii′-5's\n R-bound + the rectangle machinery).\n- **ii′-3c**: the (4.10-a) assembly (§2 algebra) → the crux\n `sf_eq_resW1 : Sf n = (ResW1 n).re` for n ≥ 1.\n- **ii′-6, ii′-7** unchanged (L0 assembly + closure).\n\n## 6. Mathlib inventory used (all verified to exist, session 019)\n\n`TendstoLocallyUniformlyOn.differentiableOn` (Weierstrass convergence);\n`Complex.digamma_one_half`, `digamma_one`, `digamma_apply_add_one`,\n`meromorphic_digamma`; `Gammaℝ_def`, `Gammaℝ_one`, `Gammaℝ_ne_zero_of_re_pos`,\n`Gammaℝ_eq_zero_iff` (zeros of ΓR = {−2n} — also the future trivial-zero\nsimplicity input); `completedRiemannZeta_one_sub`, `completedRiemannZeta_residue_one`;\n`ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div` (−ζ′/ζ\nDirichlet series, re > 1); `BohrMollerup.tendsto_log_gamma` + `logGammaSeq`;\nZeta23: `completedRiemannZeta s = 0 ↔ IsNontrivialZero s` (CountByIntegral.lean),\nseam `mult_reflect`, `WeilEF.zero_sum_inv_sq`. NOT in Mathlib (relevant gaps):\nWeierstrass/Hadamard products, polygamma, digamma partial fractions (built\nin ii′-3a), `riemannZeta_conj` (conj-invariance of ζ — to check/derive via\nthe LSeries/integral definition), trivial-zero simplicity deriv ζ(−2) ≠ 0\n(deferred from ii′-1b(iii); route: FE + Gammaℝ_eq_zero_iff + ζ(3) ≠ 0).\n\n## 7. Risks\n\n- The digamma-series build (ii′-3a) is the kind of real-analysis grind that\n can sprawl (deriv-under-limit + iteration + complex bridge). Mitigation:\n it is self-contained and has the numeric gates (ψ′(1/2) = π²/2 etc.).\n- (M)'s k = 1 rearrangement needs zeroMult conj-invariance — small proof via\n `riemannZeta (conj s) = conj (riemannZeta s)` (to be located in Mathlib or\n proved from the definition).\n- The R-bound remains the long pole of ii′-5 per D-064 R3 (2–3 sessions);\n ii′-3b waits on it. Paper A stays frozen/submittable throughout (freeze\n protocol; only new files + root imports are touched).\n"},"extra_content":null}]