← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (11993 chars)
CRITICAL correction: **c₁ = +0.1875462** — so c₁ = −(γ₁ − ...)? Let's see: c₁ = 0.1875462. And −0.1875462 was my "η₁" candidate from the S_f(2) consistency requirement. So c₁ = +0.1875462, meaning η₁ = c₁ = +0.1875462 and S_f(2) = 2η₀ − η₁ = −1.154432 − 0.1875462 = −1.341978?? But S_∞(2)+1−λ₂ = −0.966922. STILL inconsistent!
Wait — actually let me recompute. c₁ = +0.1875462. What combination of Stieltjes is that? γ₁ = −0.0728158, γ² = 0.333177. c₁ = 0.1875462 = γ² − 2γ₁·...? γ² − 2γ₁ = 0.333177 + 0.145632 = 0.478809. No. −(γ₁ + γ²/2) = −(−0.072816 + 0.166589) = −0.093773. ×(−2) = 0.187546 ✓!! c₁ = −2(γ₁ + γ²/2)·(−1)... i.e., c₁ = −(2γ₁ + γ²)·(−1) = 2γ₁ + γ² = −0.145632 + 0.333177 = 0.187546 ✓. So c₁ = γ² + 2γ₁ (NEGATIVE of what I guessed for η₁).
Hmm so c₁ = γ² + 2γ₁ = 0.1875462. Then Res₁(2) = 2c₀ + c₁ = −1.154432 + 0.1875462 = −0.966886 ≈ −0.966922 = S_f(2) (diff 3.6e-5 — my λ₂ was imprecise!). And S_f(2) = Σ(−1)^{j−1}C(2,j)c_{j−1} = 2c₀ − c₁ = −1.154432 − 0.1875462 = −1.341978 ≠ S_f(2). So:
**Res₁(n) = S_f(n) = S_∞(n) + 1 − λ_n** EXACTLY (n=1: −0.577216 ✓, n=2: −0.966886 ✓ vs −0.966922, diff from λ₂ truncation error)!!
Let me verify: Res₁(n) = Σ_j C(n,j)c_{j−1}, and S_f(n) = Σ_j (−1)^{j−1}C(n,j)c_{j−1}. At n=2: Res₁(2) = 2c₀+c₁ = −0.966886; S_f-form = 2c₀−c₁ = −1.341978. True S_f(2) = −0.966922. So **Res₁(2) ≈ S_f(2)** and the (4.13)-form with alternating signs is WRONG for our S_f. So D-037's "S_f = Σ(−1)^{j−1}C(n,j)η_{j−1}" — wait no, that's Lagarias's (4.13). Hmm, but the numbers say S_f(2) ≈ Res₁(2) = Σ C(n,j)c_{j−1} WITHOUT alternating signs.
Hmm, wait — maybe Lagarias's η_j include the sign: (4.12): −ζ′/ζ(s+1) = 1/s + Σ η_j s^j — η_j = c_j by definition. Then (4.13): S_f(n,π_triv) = Σ_j (−1)^{j−1}C(n,j)η_{j−1} = 2c₀ − c₁ at n=2 = −1.341978. But the TRUE S_f(2) = −0.966922. So Lagarias's (4.13) as printed does not match S_∞−λ+1?! Unless λ_n in Lagarias's convention differs (e.g. λ_n = Σ[1−(1−1/ρ)ⁿ] vs Σ over Z(π∨)...). Whatever — the literature conventions are treacherous here; what matters for US is the NUMERICALLY VERIFIED identity:
**Res₁(n) = Σ_{j=1}^n C(n,j)c_{j−1} = S_∞(n) + 1 − λ_n = Sf(n)** ✓ (verified n=1,2 to ~4e-5, and the c-extraction is exact to 25 digits; will re-verify to full precision in D-064).
Hmm wait, let me double-check with n=2 more precisely: need λ₂ precisely. λ₂ (true) = 0.0923830392... Let me compute S_∞(2)+1−λ₂ = −1.87453936173 + 1 − 0.09238303922 = −0.96692240095. And Res₁(2) = 2c₀+c₁ = −1.15443132980 + 0.18754623283 = −0.96688509697. Difference: −0.96692240 vs −0.96688510 = 3.73e-5. NOT exactly equal — off by 3.7e-5. Hmm! So Res₁(2) ≠ Sf(2) exactly either. 3.7e-5 discrepancy — what's that? c₂/2-ish? Or my c-extraction error? c-extraction: fit on u = 1e-2..1e-5 with c₃ u³ terms: at u=1e-2, c₃·1e-6 ~ few e-8·c₃ — the fit should be fine to ~1e-10 relative... unless the diff(z,1+u) numerical derivative loses precision. mpmath diff default step ~ 1e-(dps/2)-ish; at dps 50 fine.
Alternatively the relation is Res₁(n) = Sf(n) + δ(n) with δ(1) = 0, δ(2) = +3.73e-5?? Weird. OR my λ₂ is off: λ₂ true = 0.09238303922? From Maślanka's table: λ_2 = 0.092383039...? Let me get λ₂ exactly via E-015's value: λ_2 = 0.092383039225... I think it's right. Then Sf(2) = −0.966922401. Res₁(2) = −0.966885097. δ = +3.73e-5.
Hmm — so Res₁(n) ≠ Sf(n) exactly. What is δ(2) = 3.73e-5? Maybe related to c-extraction error after all: let me test c-extraction accuracy: the fit used 4 unknowns and 4 points at u = 1e-2,...,1e-5; the u=1e-2 point has c₃u³ ~ c₃e-6 and c₄u⁴ ~ c₄e-8 — unmodeled c₄ term biases c₀ by ~c₄·1e-8-ish and c₁ by ~c₄·1e-6·... condition number of the Vandermonde-ish system at u=1e-2..1e-5: moderate. c₁ error ~1e-4·|c₄|? Possible. So δ might be pure extraction error in c₁ (c₁ = 0.1875462 vs true maybe 0.1875835?). 2c₀+c₁ needs c₁ to ~1e-7. My extraction: c₁ to ~1e-6-ish maybe not.
ENOUGH — the design doesn't hinge on 4e-5. The STRUCTURAL conclusion is now clear and solid:
**The exact identity chain:**
1. Residue theorem: sides_k(T) = λ̃_n(T) + triv + Res₁(n) — exact.
2. Finite reindexing: λ̃_n(T) = λ_n(T) — exact.
3. Definition: Sf = S_∞ + 1 − λ_n(T) − tail(T).
4. ⟹ Sf = [S_∞ + 1 + triv + Res₁] − sides_k − tail — exact, [MASTER].
And the numerical evidence says: S_∞+1+triv+Res₁ ≈ [small]: at n=1: −0.798?! NO WAIT — if Res₁ ≈ Sf, then [MASTER] reads Sf = S_∞+1+triv+Sf−sides−tail ⟹ 0 = S_∞+1+triv−sides−tail ⟹ sides = S_∞+1+triv−tail. At n=1: sides_k(2) = −0.243883; S_∞(1)+1+triv(1)−tail(2) = −1.554120+1+0.333333−0.023096 = −0.243883 ✓✓✓ EXACT!!! So the relation "Res₁ = Sf" is EQUIVALENT to "sides_k = S_∞ + 1 + triv − tail" — and the latter is numerically EXACT at n=1 (to my 6-digit precision). So:
**THE W=1 IDENTIFICATION: Res₁(n) = S_∞(n) + 1 − λ_n(n)... i.e., Σ_{j=1}^n C(n,j)c_{j−1} = S_∞(n) + 1 − λ_n** — and equivalently the contour integral sides_k(T) = S_∞(n) + 1 + triv(n) − tail(T) for EVERY zero-avoiding T. Both sides of the latter are T-dependent (sides and tail) with the T-dependence canceling.
Hmm wait, but that can't be the right way to state it — sides_k(T) is T-dependent, S_∞+1+triv is T-independent, tail(T) is T-dependent. Fine.
But hold on — is "Res₁ = Sf" a COINCIDENCE at these small n or the true identity? Let me test n=3: Sf(3) = S_∞(3)+1−λ₃. λ₃ ≈ 0.2076389205 (known). S_∞(3) = (1−a₁)3 − 1 + Σ_odd[(1−1/m)³−1+3/m]. And Res₁(3) = 3c₀ + 3c₁ + c₂ = 3(−0.577216) + 3(0.1875462) + (−0.05168858) = −1.731647 + 0.562639 − 0.051689 = −1.220697. S_∞(3) ≈ ? Σ term: (1−1/m)³−1+3/m = 3/m²−3/m³+... ≈ 3/m²: Σ_odd 3/m² ≈ 3(π²/8−1) = 0.7011 plus corrections −3Σ1/m³ ~ −3(0.268...)·... ≈ 0.7011 − 0.6 + ... ≈ 0.1-0.2. S_∞(3) ≈ 3(−0.554120) − 1 + ~0.15 ≈ −1.662359 − 1 + 0.15 = −2.51. Sf(3) ≈ −2.51 + 1 − 0.2076 = −1.72. But Res₁(3) = −1.22. NOT CLOSE. So "Res₁ = Sf" FAILS at n=3!! (My S_∞(3) is a rough estimate, ±0.05 — but the gap is ~0.5.) So the n=1,2 agreements were... at n=2 the agreement was to 3.7e-5 (suspicious but roughly consistent), at n=3 it's WAY off. So Res₁ ≠ Sf in general. Hmm!!
OK so what IS the true identity? From [MASTER] (exact): Sf = S_∞+1+triv+Res₁−sides−tail. The BOUND needs |Sf| ≤ |S_∞+1+triv+Res₁| + |sides| + |tail|. The bracket at n=1: −0.798, n=2: −1.213, n=3: S_∞(3)+1+triv(3)+Res₁(3) ≈ −2.51+1+0.7037−1.220697 = −2.03. Growing. And D-037's B(n) accounts: |Sf| ≤ 2N(T) + sides + 1. So the intended identity must convert bracket into λ_n(T)-form. From the exact λ_n(T) = sides − triv − Res₁: bracket = S_∞+1+triv+Res₁ = S_∞+1+triv + (sides − triv − λ_n(T)) = S_∞ + 1 + sides − λ_n(T). So [MASTER] becomes: Sf = S_∞ + 1 + sides − λ_n(T) − sides − tail = S_∞ + 1 − λ_n(T) − tail — which is just the definition again (Sf = S_∞+1−λ_n). CIRCULAR — of course; the residue theorem merely rewrites λ_n(T). The CONTENT is: to bound |Sf| = |S_∞+1−λ_n|, use λ_n = λ_n(T) + tail with λ_n(T) = sides−triv−Res₁:
|Sf| ≤ |S_∞ + 1 − λ_n(T)| + |tail| — and S_∞+1−λ_n(T) = S_∞+1−sides+triv+Res₁ — hmm.
The structure that makes D-037's B(n) work: |Sf| ≤ |λ_n(T)| + |tail| + |S_∞ + 1 + Res₁ + triv − λ_n(T) − sides + ... | — I keep going in circles because the residue theorem relates λ_n(T) to sides, and Sf = S_∞+1−λ_n(T)−tail; substituting: Sf = S_∞+1+Res₁+triv−sides−tail — the bracket B0 := S_∞+1+Res₁+triv is a FIXED function of n (no T!). And Sf = B0(n) − sides(T) − tail(T) for EVERY zero-avoiding T. Since Sf is T-independent: sides(T) + tail(T) = B0(n) − Sf(n) is T-independent ✓ consistency.
For the BOUND: choose T = the zero-avoiding height in [√n, √n+1]:
|Sf| ≤ |B0(n)| + |sides(T)| + |tail(T)|.
D-037's B(n) = 2N(T) + sides-pieces + 40M₀ + 1 + I_I. So D-037's accounting must be: |B0(n)| ≤ 2N(T)?? At n=1: |B0| = 0.798 vs 2N(2) = 0 — false at n=1 but n ≥ 10⁵ range... At large n: B0(n) = S_∞+1+triv+Res₁. How big is B0(n)? Since Sf = B0 − sides − tail and |Sf| ≤ ~14 (measured small), |sides| ≤ ~√n log n·(big const), |tail| ≤ ~√n log n — B0 could be as big as √n log n. In fact B0(n) = Sf(n) + sides(T) + tail(T) — evaluating at any T: B0(n) ≈ sides + tail ~ O(√n log n). So |B0| ≤ |Sf| + |sides| + |tail| — again circular for an independent bound!
The ONLY non-circular bound: |Sf| ≤ |λ_n(T)| + |Sf − λ_n(T)| where Sf − λ_n(T) = S_∞+1−λ_n−λ_n(T)... no.
Hmm, let me think about Lagarias's Thm 6.1 statement again (D-032 line 39): "S_f(n) = λ_n(√n) + O(√n log n)". So Lagarias bounds |S_f − λ_n(√n)| = O(√n log n) — THAT difference is the contour output! S_f(n) − λ_n(T) = S_∞+1−λ_n−λ_n(T) = S_∞+1−λ_n(T)−tail−λ_n(T)?? No: S_f − λ_n(T) = (S_∞+1−λ_n) − λ_n(T) = S_∞+1−2λ_n(T)−tail?? That has 2λ_n(T) ~ 4N(T) — too big. Unless λ_n in Lagarias's 6.1 means something else — λ_n(√n) might be the truncated sum with a DIFFERENT sign/form. OR the statement is S_f(n) = −λ_n(√n) + O(...)? With S_f = S_∞+1−λ_n and λ_n = λ_n(√n)+tail: S_f + λ_n(√n) = S_∞+1−tail — and S_∞+1 ~ ½n log n — no.
I clearly cannot resolve the exact classical bookkeeping by pure thought at 11pm-brain — BUT I don't need to for the design! The DESIGN conclusion is robust:
**Whatever the exact final identity, the formalization needs these exact components:**
(i) Residue theorem for the integrand on the rectangle (L0 machinery) — giving sides_k(T) = λ_n(T) + triv + Res₁(n) EXACTLY.
(ii) The bridge |λ_n(T)| ≤ 2N(T) (+ window) from hRH.
(iii) The w=1 residue Res₁(n) = Σ_j C(n,j)c_{j−1} — computable EXACTLY as a finite sum ONCE c_j are defined as Laurent coefficients; NO Stieltjes identification needed if we keep c_j abstract!
(iv) The tail bound |tail(T)| ≤ [explicit].
(v) THE CRUX: relate Res₁(n) to S_∞(n): from [MASTER], Sf = [S_∞+1+triv+Res₁] − sides − tail. Since |Sf| is what's bounded, and |sides|, |tail| are bounded by contour pieces, the bracket S_∞+1+triv+Res₁ must be bounded by ~2N(T)+... — and since bracket is T-independent, we can evaluate it... AT A SPECIFIC T?! **KEY INSIGHT: bracket(n) = Sf(n) + sides(T) + tail(T) holds for EVERY T. Choose T = T₀-side evaluation... no — bracket(n) is a specific real number; we need |bracket(n)| ≤ [something explicit]. The only way to bound it is to know what it IS. And the answer from the numerics: bracket(1) = −0.798, bracket(2) = −1.213, bracket(3) ≈ −2.03 — hmm these look like they might be −λ_n − ...? −λ_1−0.77? Let me test: bracket(n) =? −Σ_j (−1)^{j−1}C(n,j)a_j-type... Actually: bracket = S_∞+1+triv+Res₁; using Res₁ = S_∞−λ_n+1 (my earlier derivation which numerically failed at n=2 — let me re-examine WHY: Res₁ = Σ_j C(n,j)η_{j−1} with η = c: at n=2: 2c₀+c₁ = −0.966886. S_∞−λ₂+1 = −1.874539−0.092383+1 = −0.966922. Difference 3.6e-5 — SMALL but nonzero. At n=3: Res₁(3) = 3c₀+3c₁+c₂ = −1.220697; S_∞(3)−λ₃+1 ≈ −2.51−0.2076+1 = −1.72. NOT close. So Res₁ = S_∞−λ_n+1 fails at n=3. My S_∞(3) estimate was rough (±0.1?) — let me not trust it. Hmm, if S_∞(3) were −1.72+... let me refine: actually the failure at n=3 vs agreement at n=2 (3.6e-5) — the n=2 near-agreement suggests c-extraction noise at n=2 AND a real failure at n=3. OR my rough S_∞(3) is off by 0.5 — unlikely (the nsum converges well).
I need to stop the hand-analysis and compute all pieces precisely for n = 1..6. THEN the exact identity will reveal itself. This is exactly D-064's job ("make the o(eᵃ)... the exact bookkeeping quantitative"). Let me do the precise numeric NOW since everything hinges on it — compute for n = 1..6: c₀..c₅ (Laurent coeffs of −ζ′/ζ at 1, high precision), Res₁(n) = Σ C(n,j)c_{j−1}, S_∞(n) exact, λ_n exact-ish (via E-015's arithmetic route would be heavy; instead use the PRIME-side η definition? OR use the identity λ_n = S_∞+1−Sf with Sf = Σ(−1)^{j−1}C(n,j)c_{j−1} IF Lagarias's 4.13 holds... circular. Use λ_n from zeros with many zeros + tail bound: λ_n = Σ_{k} pair + tail; with 10⁴ zeros (E-021 cache exists: E-021-zeros-cache.npy 4624 zeros!) the tail beyond γ_4624 ~ 5500: for n ≤ 6 the tail Σ 2n/γ²·n? |tail| ≤ Σ_{γ>5500} 2n·|1/ρ|·e^{...} ≈ 2n·log(5500)/(2π·5500) ~ n·2.5e-4 — small enough for 4-digit checks of n ≤ 6.
Let me just do it — load the E-021 zeros cache.
The hand bookkeeping has hit its limit — let me settle the exact identity numerically with the cached zeros (E-021's 4624-zero cache) before designing.
tool: Bash
input
{
"command": "cd /d/Python/Quantum && ls research/numerics/data/ | grep -i \"zeros\" | head; ./.venv/Scripts/python.exe -c \"\nimport mpmath as m\nm.mp.dps = 50\n# Laurent coefficients c0..c6 of -zeta'/zeta at s=1 via mpmath taylor\nz = m.zeta\nf = lambda u: -m.diff(z, 1+u)/z(1+u) - 1/u\nts = m.taylor(f, 0, 6)\nprint('taylor of -z\\'/z(1+u)-1/u:')\nfor j,c in enumerate(ts):\n print(' c%d ='%j, m.nstr(c, 20))\n\"",
"description": "High-precision Laurent coefficients via mpmath taylor",
"timeout": 180000
}
raw content_json (database row)
[{"type":"thinking","thinking":"CRITICAL correction: **c₁ = +0.1875462** — so c₁ = −(γ₁ − ...)? Let's see: c₁ = 0.1875462. And −0.1875462 was my \"η₁\" candidate from the S_f(2) consistency requirement. So c₁ = +0.1875462, meaning η₁ = c₁ = +0.1875462 and S_f(2) = 2η₀ − η₁ = −1.154432 − 0.1875462 = −1.341978?? But S_∞(2)+1−λ₂ = −0.966922. STILL inconsistent!\n\nWait — actually let me recompute. c₁ = +0.1875462. What combination of Stieltjes is that? γ₁ = −0.0728158, γ² = 0.333177. c₁ = 0.1875462 = γ² − 2γ₁·...? γ² − 2γ₁ = 0.333177 + 0.145632 = 0.478809. No. −(γ₁ + γ²/2) = −(−0.072816 + 0.166589) = −0.093773. ×(−2) = 0.187546 ✓!! c₁ = −2(γ₁ + γ²/2)·(−1)... i.e., c₁ = −(2γ₁ + γ²)·(−1) = 2γ₁ + γ² = −0.145632 + 0.333177 = 0.187546 ✓. So c₁ = γ² + 2γ₁ (NEGATIVE of what I guessed for η₁).\n\nHmm so c₁ = γ² + 2γ₁ = 0.1875462. Then Res₁(2) = 2c₀ + c₁ = −1.154432 + 0.1875462 = −0.966886 ≈ −0.966922 = S_f(2) (diff 3.6e-5 — my λ₂ was imprecise!). And S_f(2) = Σ(−1)^{j−1}C(2,j)c_{j−1} = 2c₀ − c₁ = −1.154432 − 0.1875462 = −1.341978 ≠ S_f(2). So:\n\n**Res₁(n) = S_f(n) = S_∞(n) + 1 − λ_n** EXACTLY (n=1: −0.577216 ✓, n=2: −0.966886 ✓ vs −0.966922, diff from λ₂ truncation error)!!\n\nLet me verify: Res₁(n) = Σ_j C(n,j)c_{j−1}, and S_f(n) = Σ_j (−1)^{j−1}C(n,j)c_{j−1}. At n=2: Res₁(2) = 2c₀+c₁ = −0.966886; S_f-form = 2c₀−c₁ = −1.341978. True S_f(2) = −0.966922. So **Res₁(2) ≈ S_f(2)** and the (4.13)-form with alternating signs is WRONG for our S_f. So D-037's \"S_f = Σ(−1)^{j−1}C(n,j)η_{j−1}\" — wait no, that's Lagarias's (4.13). Hmm, but the numbers say S_f(2) ≈ Res₁(2) = Σ C(n,j)c_{j−1} WITHOUT alternating signs.\n\nHmm, wait — maybe Lagarias's η_j include the sign: (4.12): −ζ′/ζ(s+1) = 1/s + Σ η_j s^j — η_j = c_j by definition. Then (4.13): S_f(n,π_triv) = Σ_j (−1)^{j−1}C(n,j)η_{j−1} = 2c₀ − c₁ at n=2 = −1.341978. But the TRUE S_f(2) = −0.966922. So Lagarias's (4.13) as printed does not match S_∞−λ+1?! Unless λ_n in Lagarias's convention differs (e.g. λ_n = Σ[1−(1−1/ρ)ⁿ] vs Σ over Z(π∨)...). Whatever — the literature conventions are treacherous here; what matters for US is the NUMERICALLY VERIFIED identity:\n\n**Res₁(n) = Σ_{j=1}^n C(n,j)c_{j−1} = S_∞(n) + 1 − λ_n = Sf(n)** ✓ (verified n=1,2 to ~4e-5, and the c-extraction is exact to 25 digits; will re-verify to full precision in D-064).\n\nHmm wait, let me double-check with n=2 more precisely: need λ₂ precisely. λ₂ (true) = 0.0923830392... Let me compute S_∞(2)+1−λ₂ = −1.87453936173 + 1 − 0.09238303922 = −0.96692240095. And Res₁(2) = 2c₀+c₁ = −1.15443132980 + 0.18754623283 = −0.96688509697. Difference: −0.96692240 vs −0.96688510 = 3.73e-5. NOT exactly equal — off by 3.7e-5. Hmm! So Res₁(2) ≠ Sf(2) exactly either. 3.7e-5 discrepancy — what's that? c₂/2-ish? Or my c-extraction error? c-extraction: fit on u = 1e-2..1e-5 with c₃ u³ terms: at u=1e-2, c₃·1e-6 ~ few e-8·c₃ — the fit should be fine to ~1e-10 relative... unless the diff(z,1+u) numerical derivative loses precision. mpmath diff default step ~ 1e-(dps/2)-ish; at dps 50 fine.\n\nAlternatively the relation is Res₁(n) = Sf(n) + δ(n) with δ(1) = 0, δ(2) = +3.73e-5?? Weird. OR my λ₂ is off: λ₂ true = 0.09238303922? From Maślanka's table: λ_2 = 0.092383039...? Let me get λ₂ exactly via E-015's value: λ_2 = 0.092383039225... I think it's right. Then Sf(2) = −0.966922401. Res₁(2) = −0.966885097. δ = +3.73e-5.\n\nHmm — so Res₁(n) ≠ Sf(n) exactly. What is δ(2) = 3.73e-5? Maybe related to c-extraction error after all: let me test c-extraction accuracy: the fit used 4 unknowns and 4 points at u = 1e-2,...,1e-5; the u=1e-2 point has c₃u³ ~ c₃e-6 and c₄u⁴ ~ c₄e-8 — unmodeled c₄ term biases c₀ by ~c₄·1e-8-ish and c₁ by ~c₄·1e-6·... condition number of the Vandermonde-ish system at u=1e-2..1e-5: moderate. c₁ error ~1e-4·|c₄|? Possible. So δ might be pure extraction error in c₁ (c₁ = 0.1875462 vs true maybe 0.1875835?). 2c₀+c₁ needs c₁ to ~1e-7. My extraction: c₁ to ~1e-6-ish maybe not. \n\nENOUGH — the design doesn't hinge on 4e-5. The STRUCTURAL conclusion is now clear and solid:\n\n**The exact identity chain:**\n1. Residue theorem: sides_k(T) = λ̃_n(T) + triv + Res₁(n) — exact.\n2. Finite reindexing: λ̃_n(T) = λ_n(T) — exact.\n3. Definition: Sf = S_∞ + 1 − λ_n(T) − tail(T).\n4. ⟹ Sf = [S_∞ + 1 + triv + Res₁] − sides_k − tail — exact, [MASTER].\n\nAnd the numerical evidence says: S_∞+1+triv+Res₁ ≈ [small]: at n=1: −0.798?! NO WAIT — if Res₁ ≈ Sf, then [MASTER] reads Sf = S_∞+1+triv+Sf−sides−tail ⟹ 0 = S_∞+1+triv−sides−tail ⟹ sides = S_∞+1+triv−tail. At n=1: sides_k(2) = −0.243883; S_∞(1)+1+triv(1)−tail(2) = −1.554120+1+0.333333−0.023096 = −0.243883 ✓✓✓ EXACT!!! So the relation \"Res₁ = Sf\" is EQUIVALENT to \"sides_k = S_∞ + 1 + triv − tail\" — and the latter is numerically EXACT at n=1 (to my 6-digit precision). So:\n\n**THE W=1 IDENTIFICATION: Res₁(n) = S_∞(n) + 1 − λ_n(n)... i.e., Σ_{j=1}^n C(n,j)c_{j−1} = S_∞(n) + 1 − λ_n** — and equivalently the contour integral sides_k(T) = S_∞(n) + 1 + triv(n) − tail(T) for EVERY zero-avoiding T. Both sides of the latter are T-dependent (sides and tail) with the T-dependence canceling.\n\nHmm wait, but that can't be the right way to state it — sides_k(T) is T-dependent, S_∞+1+triv is T-independent, tail(T) is T-dependent. Fine.\n\nBut hold on — is \"Res₁ = Sf\" a COINCIDENCE at these small n or the true identity? Let me test n=3: Sf(3) = S_∞(3)+1−λ₃. λ₃ ≈ 0.2076389205 (known). S_∞(3) = (1−a₁)3 − 1 + Σ_odd[(1−1/m)³−1+3/m]. And Res₁(3) = 3c₀ + 3c₁ + c₂ = 3(−0.577216) + 3(0.1875462) + (−0.05168858) = −1.731647 + 0.562639 − 0.051689 = −1.220697. S_∞(3) ≈ ? Σ term: (1−1/m)³−1+3/m = 3/m²−3/m³+... ≈ 3/m²: Σ_odd 3/m² ≈ 3(π²/8−1) = 0.7011 plus corrections −3Σ1/m³ ~ −3(0.268...)·... ≈ 0.7011 − 0.6 + ... ≈ 0.1-0.2. S_∞(3) ≈ 3(−0.554120) − 1 + ~0.15 ≈ −1.662359 − 1 + 0.15 = −2.51. Sf(3) ≈ −2.51 + 1 − 0.2076 = −1.72. But Res₁(3) = −1.22. NOT CLOSE. So \"Res₁ = Sf\" FAILS at n=3!! (My S_∞(3) is a rough estimate, ±0.05 — but the gap is ~0.5.) So the n=1,2 agreements were... at n=2 the agreement was to 3.7e-5 (suspicious but roughly consistent), at n=3 it's WAY off. So Res₁ ≠ Sf in general. Hmm!!\n\nOK so what IS the true identity? From [MASTER] (exact): Sf = S_∞+1+triv+Res₁−sides−tail. The BOUND needs |Sf| ≤ |S_∞+1+triv+Res₁| + |sides| + |tail|. The bracket at n=1: −0.798, n=2: −1.213, n=3: S_∞(3)+1+triv(3)+Res₁(3) ≈ −2.51+1+0.7037−1.220697 = −2.03. Growing. And D-037's B(n) accounts: |Sf| ≤ 2N(T) + sides + 1. So the intended identity must convert bracket into λ_n(T)-form. From the exact λ_n(T) = sides − triv − Res₁: bracket = S_∞+1+triv+Res₁ = S_∞+1+triv + (sides − triv − λ_n(T)) = S_∞ + 1 + sides − λ_n(T). So [MASTER] becomes: Sf = S_∞ + 1 + sides − λ_n(T) − sides − tail = S_∞ + 1 − λ_n(T) − tail — which is just the definition again (Sf = S_∞+1−λ_n). CIRCULAR — of course; the residue theorem merely rewrites λ_n(T). The CONTENT is: to bound |Sf| = |S_∞+1−λ_n|, use λ_n = λ_n(T) + tail with λ_n(T) = sides−triv−Res₁:\n\n|Sf| ≤ |S_∞ + 1 − λ_n(T)| + |tail| — and S_∞+1−λ_n(T) = S_∞+1−sides+triv+Res₁ — hmm.\n\nThe structure that makes D-037's B(n) work: |Sf| ≤ |λ_n(T)| + |tail| + |S_∞ + 1 + Res₁ + triv − λ_n(T) − sides + ... | — I keep going in circles because the residue theorem relates λ_n(T) to sides, and Sf = S_∞+1−λ_n(T)−tail; substituting: Sf = S_∞+1+Res₁+triv−sides−tail — the bracket B0 := S_∞+1+Res₁+triv is a FIXED function of n (no T!). And Sf = B0(n) − sides(T) − tail(T) for EVERY zero-avoiding T. Since Sf is T-independent: sides(T) + tail(T) = B0(n) − Sf(n) is T-independent ✓ consistency.\n\nFor the BOUND: choose T = the zero-avoiding height in [√n, √n+1]:\n|Sf| ≤ |B0(n)| + |sides(T)| + |tail(T)|.\n\nD-037's B(n) = 2N(T) + sides-pieces + 40M₀ + 1 + I_I. So D-037's accounting must be: |B0(n)| ≤ 2N(T)?? At n=1: |B0| = 0.798 vs 2N(2) = 0 — false at n=1 but n ≥ 10⁵ range... At large n: B0(n) = S_∞+1+triv+Res₁. How big is B0(n)? Since Sf = B0 − sides − tail and |Sf| ≤ ~14 (measured small), |sides| ≤ ~√n log n·(big const), |tail| ≤ ~√n log n — B0 could be as big as √n log n. In fact B0(n) = Sf(n) + sides(T) + tail(T) — evaluating at any T: B0(n) ≈ sides + tail ~ O(√n log n). So |B0| ≤ |Sf| + |sides| + |tail| — again circular for an independent bound!\n\nThe ONLY non-circular bound: |Sf| ≤ |λ_n(T)| + |Sf − λ_n(T)| where Sf − λ_n(T) = S_∞+1−λ_n−λ_n(T)... no.\n\nHmm, let me think about Lagarias's Thm 6.1 statement again (D-032 line 39): \"S_f(n) = λ_n(√n) + O(√n log n)\". So Lagarias bounds |S_f − λ_n(√n)| = O(√n log n) — THAT difference is the contour output! S_f(n) − λ_n(T) = S_∞+1−λ_n−λ_n(T) = S_∞+1−λ_n(T)−tail−λ_n(T)?? No: S_f − λ_n(T) = (S_∞+1−λ_n) − λ_n(T) = S_∞+1−2λ_n(T)−tail?? That has 2λ_n(T) ~ 4N(T) — too big. Unless λ_n in Lagarias's 6.1 means something else — λ_n(√n) might be the truncated sum with a DIFFERENT sign/form. OR the statement is S_f(n) = −λ_n(√n) + O(...)? With S_f = S_∞+1−λ_n and λ_n = λ_n(√n)+tail: S_f + λ_n(√n) = S_∞+1−tail — and S_∞+1 ~ ½n log n — no.\n\nI clearly cannot resolve the exact classical bookkeeping by pure thought at 11pm-brain — BUT I don't need to for the design! The DESIGN conclusion is robust:\n\n**Whatever the exact final identity, the formalization needs these exact components:**\n(i) Residue theorem for the integrand on the rectangle (L0 machinery) — giving sides_k(T) = λ_n(T) + triv + Res₁(n) EXACTLY.\n(ii) The bridge |λ_n(T)| ≤ 2N(T) (+ window) from hRH.\n(iii) The w=1 residue Res₁(n) = Σ_j C(n,j)c_{j−1} — computable EXACTLY as a finite sum ONCE c_j are defined as Laurent coefficients; NO Stieltjes identification needed if we keep c_j abstract!\n(iv) The tail bound |tail(T)| ≤ [explicit].\n(v) THE CRUX: relate Res₁(n) to S_∞(n): from [MASTER], Sf = [S_∞+1+triv+Res₁] − sides − tail. Since |Sf| is what's bounded, and |sides|, |tail| are bounded by contour pieces, the bracket S_∞+1+triv+Res₁ must be bounded by ~2N(T)+... — and since bracket is T-independent, we can evaluate it... AT A SPECIFIC T?! **KEY INSIGHT: bracket(n) = Sf(n) + sides(T) + tail(T) holds for EVERY T. Choose T = T₀-side evaluation... no — bracket(n) is a specific real number; we need |bracket(n)| ≤ [something explicit]. The only way to bound it is to know what it IS. And the answer from the numerics: bracket(1) = −0.798, bracket(2) = −1.213, bracket(3) ≈ −2.03 — hmm these look like they might be −λ_n − ...? −λ_1−0.77? Let me test: bracket(n) =? −Σ_j (−1)^{j−1}C(n,j)a_j-type... Actually: bracket = S_∞+1+triv+Res₁; using Res₁ = S_∞−λ_n+1 (my earlier derivation which numerically failed at n=2 — let me re-examine WHY: Res₁ = Σ_j C(n,j)η_{j−1} with η = c: at n=2: 2c₀+c₁ = −0.966886. S_∞−λ₂+1 = −1.874539−0.092383+1 = −0.966922. Difference 3.6e-5 — SMALL but nonzero. At n=3: Res₁(3) = 3c₀+3c₁+c₂ = −1.220697; S_∞(3)−λ₃+1 ≈ −2.51−0.2076+1 = −1.72. NOT close. So Res₁ = S_∞−λ_n+1 fails at n=3. My S_∞(3) estimate was rough (±0.1?) — let me not trust it. Hmm, if S_∞(3) were −1.72+... let me refine: actually the failure at n=3 vs agreement at n=2 (3.6e-5) — the n=2 near-agreement suggests c-extraction noise at n=2 AND a real failure at n=3. OR my rough S_∞(3) is off by 0.5 — unlikely (the nsum converges well).\n\nI need to stop the hand-analysis and compute all pieces precisely for n = 1..6. THEN the exact identity will reveal itself. This is exactly D-064's job (\"make the o(eᵃ)... the exact bookkeeping quantitative\"). Let me do the precise numeric NOW since everything hinges on it — compute for n = 1..6: c₀..c₅ (Laurent coeffs of −ζ′/ζ at 1, high precision), Res₁(n) = Σ C(n,j)c_{j−1}, S_∞(n) exact, λ_n exact-ish (via E-015's arithmetic route would be heavy; instead use the PRIME-side η definition? OR use the identity λ_n = S_∞+1−Sf with Sf = Σ(−1)^{j−1}C(n,j)c_{j−1} IF Lagarias's 4.13 holds... circular. Use λ_n from zeros with many zeros + tail bound: λ_n = Σ_{k} pair + tail; with 10⁴ zeros (E-021 cache exists: E-021-zeros-cache.npy 4624 zeros!) the tail beyond γ_4624 ~ 5500: for n ≤ 6 the tail Σ 2n/γ²·n? |tail| ≤ Σ_{γ>5500} 2n·|1/ρ|·e^{...} ≈ 2n·log(5500)/(2π·5500) ~ n·2.5e-4 — small enough for 4-digit checks of n ≤ 6.\n\nLet me just do it — load the E-021 zeros cache.","signature":""},{"type":"text","text":"The hand bookkeeping has hit its limit — let me settle the exact identity numerically with the cached zeros (E-021's 4624-zero cache) before designing."},{"type":"tool_use","id":"Bash_47","name":"Bash","input":{"command":"cd /d/Python/Quantum && ls research/numerics/data/ | grep -i \"zeros\" | head; ./.venv/Scripts/python.exe -c \"\nimport mpmath as m\nm.mp.dps = 50\n# Laurent coefficients c0..c6 of -zeta'/zeta at s=1 via mpmath taylor\nz = m.zeta\nf = lambda u: -m.diff(z, 1+u)/z(1+u) - 1/u\nts = m.taylor(f, 0, 6)\nprint('taylor of -z\\'/z(1+u)-1/u:')\nfor j,c in enumerate(ts):\n print(' c%d ='%j, m.nstr(c, 20))\n\"","description":"High-precision Laurent coefficients via mpmath taylor","timeout":180000},"extra_content":null}]