Current task: —

← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)

#899 assistant 2026-08-21 18:32:34.870 UTC · 1193→3520 tok open ⤢
thinking (5422 chars)
The u=0 evaluation hits the pole even though multiplied by u (0·pole is NaN). Guard: define h(u) with a piecewise at u=0 returning 1... but diff samples near 0, not at 0, usually — the k=1 worked (c₀ = −γ to 25 digits ✓). For k≥2 it seems to evaluate at 0. Let me use a small offset: compute the series at u0 = 0.05 instead of 0 and shift? Simpler: extract via least-squares fit at many small points with higher-order model, at dps 50 with u ~ 1e-3..1e-2 — but that's what I did before with 25-digit c₁. The earlier fit gave c₁ = 0.18754623283535631474 — I'll trust that (it matched γ² + 2γ₁? γ²+2γ₁ = 0.333177 + (−0.145632) = 0.1875462 — EXACT match to the fit). So c₁ = γ² + 2γ₁·(−1)... wait: γ₁ = −0.0728158455; 2γ₁ = −0.1456316910; γ² = 0.333177... γ² + 2γ₁ = 0.1875454... let me not; the fit value 0.18754623283535631 is solid. Hmm wait, actually earlier I derived c₁ should be γ₁+γ² = 0.26036208 from the Stieltjes expansion — but the fit says 0.18754623, and γ²+2γ₁ = 0.18754623?? γ² = 0.5772156649² = 0.3331779559; 2γ₁ = −0.1456316910; sum = 0.1875462649. The fit: 0.18754623283535631. Close (diff 3.2e-8 — fit error). Hmm interesting. So c₁ = γ² + 2γ₁?? But my Laurent derivation gave c₁ = γ₁ + γ². Let me recheck: ζ(1+u) = u⁻¹ + γ − γ₁u + γ₂u²/2 − ... Stieltjes convention: ζ(s) = 1/(s−1) + Σ_{k=0}∞ (−1)^k γ_k/k! (s−1)^k ✓. log ζ(1+u) = −log u + log(1 + γu − γ₁u²/2 + γ₂u³/6 − ...) = −log u + γu + [−γ₁/2 − γ²/2]u² + [γ₂/6 + γγ₁/2 + γ³/3]u³ + ... So d/du log ζ = −1/u + γ − (γ₁+γ²)u + (γ₂/2 + γγ₁ + γ³)u²·... wait derivative of [γ₂/6+γγ₁/2+γ³/3]u³ is 3[...]u² = (γ₂/2 + 3γγ₁/2 + γ³)u². So −ζ′/ζ = 1/u − γ + (γ₁+γ²)u − (γ₂/2 + 3γγ₁/2 + γ³)u² + ... So c₁ = γ₁ + γ² = 0.26036208. But the fit says 0.18754623! These disagree by 0.0728 ≈ −γ₁!! Curious: γ₁+γ² = 0.26036 vs γ²+2γ₁ = 0.18755 — difference = −γ₁ = 0.0728. One of them is wrong — the fit is EMPIRICAL (0.1875462 from actual function values), so my Stieltjes algebra must be wrong. Let me recheck numerically: −ζ′/ζ(1.001): model 1/u + c₀ + c₁u: u=0.001: 1000 − 0.5772157 + c₁·0.001. From the h-diff computation c₀ = −0.57721566490153 ✓. Actual −ζ′/ζ(1.001) = ? compute numerically: I'll trust the fit: c₁ ≈ 0.18754623. Check my algebra: v = γu − γ₁u²/2 + γ₂u³/6. log(1+v) = v − v²/2 + v³/3. v²/2 = (γ²u² − γγ₁u³ + ...)/2. v³/3 = γ³u³/3. Coefficient of u² in log(1+v): −γ₁/2 − γ²/2 ✓. d/du: 2·(−γ₁/2 − γ²/2)u = −(γ₁+γ²)u. So ζ′/ζ = −1/u + γ − (γ₁+γ²)u + O(u²). −ζ′/ζ = 1/u − γ + (γ₁+γ²)u + ... c₁ = γ₁+γ² = 0.26036. But empirical fit: 0.18755. Contradiction with the empirical... UNLESS the empirical fit was contaminated. The fit: 4 points u = 1e-2..1e-5, model c₀+c₁u+c₂u²+c₃u³, exact solve. At u = 1e-2 the c₄u⁴ ~ c₄·1e-8 unmodeled — fine. Hmm, but mpmath's diff(z, 1+u) — numerical derivative of zeta at u=1e-5: default diff h ~ 1e-(dps/3)? The earlier fit at dps 50 gave c1 = 0.18754623283535631474 — and γ²+2γ₁ = 0.18754626?? wait let me compute γ² + 2γ₁ precisely: γ² = 0.333177955... γ = 0.57721566490153286061; γ² = 0.333177955... let me: 0.5772156649² = 0.333177(0.5772² = 0.33316). 2γ₁ = −0.1456316909673534. γ²+2γ₁ = 0.3331780 − 0.1456317 = 0.1875463. The fit 0.1875462328. And γ₁+γ² = −0.0728158455 + 0.333177955 = 0.260362109. Fit says neither exactly but closest to 0.1875463 (diff 3e-8) — so c₁ = γ² + 2γ₁ EMPIRICALLY. So my Stieltjes algebra is wrong somewhere — irrelevant! The empirical wins. And c₂ from the fit: −0.05168858148. Check candidates: −(γ₂/2 + 3γγ₁/2 + γ³): γ₂ = −0.0096903636; γ₂/2 = −0.004845; 3γγ₁/2 = 3(0.5772)(−0.0728)/2 = −0.063037; γ³ = 0.192426. Sum: −0.004845 − 0.063037 + 0.192426 = 0.124544. Negative: −0.124544 ≠ −0.0517. Alternative c₂ = −(γ₂ + 3γγ₁ + γ³)?: −0.009690 − 0.126074 − 0.192426 = −0.328190 no. c₂ = −0.0516886... what combination? −(γ₂/2+γγ₁·2+...)? −0.004845 + 0.084... γγ₁ = −0.042025: −2γγ₁ = 0.084050: −0.004845+0.084050−0.192426·...? Meh. Empirics rule; symbolic Stieltjes relations can be sorted out in D-064 with flint-grade precision. Now the KEY test — the exact identity. Let me set up the full numeric test: - c₀..c₅ via the h-diff at higher order (the u=0 pole issue: use m.diff with h explicitly nonzero, e.g. diff(h, 0, n=k, h=1e-3)? or evaluate the fit more carefully at dps 60 with 6 points). - Res₁(n) = Σ_{j=1}^n C(n,j)c_{j−1} for n = 1..6. - S_∞(n) exact (nsum odd form). - λ_n: compute from zeros (4624 zeros from E-021 cache) + tail estimate. - Then test candidate identities: (a) Sf = S_∞+1−λ_n vs [MASTER]: S_∞+1+triv+Res₁ − sides − tail — can't compute sides easily; instead test the T-independent consequence: Res₁(n) vs S_∞+1−λ_n+triv... Actually the cleanest testable: from [MASTER], B0(n) := S_∞(n)+1+triv(n)+Res₁(n) should equal Sf(n)+sides(T)+tail(T) — not directly testable without sides. BUT sides_k(T) = λ_n(T)+triv+Res₁ (residue theorem) IS testable if I can compute the contour integral numerically! I CAN: integrate k_n(w−1)(−ζ′/ζ) around the rectangle numerically at small n (n ≤ 6, T = √n + 0.5 say — zero-avoiding check by hand) with mpmath. That's the definitive test of the whole chain. Given time, let me do exactly that: full numerical verification of the exact identity at n = 2 and n = 3: compute sides (contour integral), λ_n(T) (from zeros), triv, Res₁; verify sides = λ_n(T) + triv + Res₁ to ~1e-20; and separately verify Sf = S_∞+1−λ_n decomposition; and then compute B0 = S_∞+1+triv+Res₁ and see how big it is / whether it has a closed form.
Good — c₀ = −γ to 25 digits. Let me run the definitive numerical test of the full identity chain (contour integral vs residue sum) at small n.
tool: Bash
input
{
  "command": "cd /d/Python/Quantum && ./.venv/Scripts/python.exe -c \"\nimport mpmath as m\nm.mp.dps = 40\nz = m.zeta\nld = lambda w: -m.diff(z, w)/z(w)   # -zeta'/zeta\ngamma = m.euler\n# Laurent c0..c3 (from prior fit, dps-50 verified): c0=-gamma, c1=0.18754623283535631...\n# refit at dps 40 with 5 unknowns for safety\nus = [m.mpf(10)**(-k) for k in [3,4,5,6,7]]\nA = lambda u: ld(1+u) - 1/u\nM = m.matrix([[u**j for j in range(5)] for u in us])\nb = m.matrix([A(u) for u in us])\nsol = m.lu_solve(M, b)\ncs = [sol[i] for i in range(5)]\nprint('c0..c4:', [m.nstr(c,18) for c in cs])\ndef kn(s, n): return (1+1/s)**n - 1\ndef Res1(n):\n    return m.nsum(lambda j: 0, [1,0]) + sum(m.binomial(n,j)*cs[j-1] for j in range(1,n+1))\ndef triv(n): return 1 - (m.mpf(2)/3)**n\na1 = (m.log(4*m.pi)+gamma)/2\ndef Sinf(n):\n    return (1-a1)*n - 1 + m.nsum(lambda k: (1-1/(2*k+1))**n - 1 + n/(2*k+1), [1, m.inf], tol=m.mpf('1e-30'))\n# zeros from cache\nimport numpy as np\ngam = np.load('research/numerics/data/E-021-zeros-cache.npy')\nprint('zeros:', len(gam), 'max:', gam[-1])\ndef lam_n(n, T=None):\n    tot = m.mpf(0)\n    for g in gam:\n        if T is not None and g > T: break\n        rho = m.mpc(m.mpf('0.5'), m.mpf(float(g)))\n        # pair: rho and conj(rho)\n        tot += (1 - (1-1/rho)**n).real*2\n    return tot\ndef sides(n, T):\n    J = lambda w: kn(w-1, n)*ld(w)\n    s0, s1 = m.mpf('-2.5'), 2*m.sqrt(n)\n    I1 = m.quad(lambda t: J(m.mpc(s1,t)), [-T, T])          # right vertical\n    I3 = m.quad(lambda t: J(m.mpc(s0,t)), [-T, T])          # left vertical\n    I2 = m.quad(lambda x: J(m.mpc(x,T)), [s0, s1])          # top\n    I4 = m.quad(lambda x: J(m.mpc(x,-T)), [s0, s1])         # bottom\n    # CCW: bottom (left->right), right (bottom->top), top (right->left), left (top->bottom)\n    total = I4 + 1j*I1 - I2 - 1j*I3\n    return total/(2*m.pi*1j)\nfor n in [2, 3]:\n    T = m.sqrt(n) + m.mpf('0.5')\n    S = sides(n, T)\n    lamT = lam_n(n, T)\n    print(f'n={n}: sides={m.nstr(S,16)}')\n    print(f'  lam_n(T)={m.nstr(lamT,16)} triv={m.nstr(triv(n),10)} Res1={m.nstr(Res1(n),16)}')\n    print(f'  lam_n(T)+triv+Res1 = {m.nstr(lamT+triv(n)+Res1(n),16)}')\n    print(f'  sides - (lam+triv+Res1) = {m.nstr(S-(lamT+triv(n)+Res1(n)),8)}')\n    Si = Sinf(n); lamF = lam_n(n)\n    Sf = Si + 1 - lamF\n    B0 = Si + 1 + triv(n) + Res1(n)\n    print(f'  Sinf={m.nstr(Si,14)} lambda_full(approx)={m.nstr(lamF,12)} Sf={m.nstr(Sf,12)}')\n    print(f'  B0 = Sinf+1+triv+Res1 = {m.nstr(B0,14)}')\n    print(f'  check MASTER: B0 - sides - tail = {m.nstr(B0 - S - (lamF-lamT),14)}  vs Sf')\n\"",
  "description": "Numerically verify the full contour identity chain at n=2,3",
  "timeout": 300000
}
raw content_json (database row)
[{"type":"thinking","thinking":"The u=0 evaluation hits the pole even though multiplied by u (0·pole is NaN). Guard: define h(u) with a piecewise at u=0 returning 1... but diff samples near 0, not at 0, usually — the k=1 worked (c₀ = −γ to 25 digits ✓). For k≥2 it seems to evaluate at 0. Let me use a small offset: compute the series at u0 = 0.05 instead of 0 and shift? Simpler: extract via least-squares fit at many small points with higher-order model, at dps 50 with u ~ 1e-3..1e-2 — but that's what I did before with 25-digit c₁. The earlier fit gave c₁ = 0.18754623283535631474 — I'll trust that (it matched γ² + 2γ₁? γ²+2γ₁ = 0.333177 + (−0.145632) = 0.1875462 — EXACT match to the fit). So c₁ = γ² + 2γ₁·(−1)... wait: γ₁ = −0.0728158455; 2γ₁ = −0.1456316910; γ² = 0.333177... γ² + 2γ₁ = 0.1875454... let me not; the fit value 0.18754623283535631 is solid.\n\nHmm wait, actually earlier I derived c₁ should be γ₁+γ² = 0.26036208 from the Stieltjes expansion — but the fit says 0.18754623, and γ²+2γ₁ = 0.18754623?? γ² = 0.5772156649² = 0.3331779559; 2γ₁ = −0.1456316910; sum = 0.1875462649. The fit: 0.18754623283535631. Close (diff 3.2e-8 — fit error). Hmm interesting. So c₁ = γ² + 2γ₁?? But my Laurent derivation gave c₁ = γ₁ + γ². Let me recheck: ζ(1+u) = u⁻¹ + γ − γ₁u + γ₂u²/2 − ... Stieltjes convention: ζ(s) = 1/(s−1) + Σ_{k=0}∞ (−1)^k γ_k/k! (s−1)^k ✓. log ζ(1+u) = −log u + log(1 + γu − γ₁u²/2 + γ₂u³/6 − ...) = −log u + γu + [−γ₁/2 − γ²/2]u² + [γ₂/6 + γγ₁/2 + γ³/3]u³ + ... So d/du log ζ = −1/u + γ − (γ₁+γ²)u + (γ₂/2 + γγ₁ + γ³)u²·... wait derivative of [γ₂/6+γγ₁/2+γ³/3]u³ is 3[...]u² = (γ₂/2 + 3γγ₁/2 + γ³)u². So −ζ′/ζ = 1/u − γ + (γ₁+γ²)u − (γ₂/2 + 3γγ₁/2 + γ³)u² + ... So c₁ = γ₁ + γ² = 0.26036208. But the fit says 0.18754623! These disagree by 0.0728 ≈ −γ₁!! Curious: γ₁+γ² = 0.26036 vs γ²+2γ₁ = 0.18755 — difference = −γ₁ = 0.0728. One of them is wrong — the fit is EMPIRICAL (0.1875462 from actual function values), so my Stieltjes algebra must be wrong. Let me recheck numerically: −ζ′/ζ(1.001): model 1/u + c₀ + c₁u: u=0.001: 1000 − 0.5772157 + c₁·0.001. From the h-diff computation c₀ = −0.57721566490153 ✓. Actual −ζ′/ζ(1.001) = ? compute numerically: I'll trust the fit: c₁ ≈ 0.18754623. Check my algebra: v = γu − γ₁u²/2 + γ₂u³/6. log(1+v) = v − v²/2 + v³/3. v²/2 = (γ²u² − γγ₁u³ + ...)/2. v³/3 = γ³u³/3. Coefficient of u² in log(1+v): −γ₁/2 − γ²/2 ✓. d/du: 2·(−γ₁/2 − γ²/2)u = −(γ₁+γ²)u. So ζ′/ζ = −1/u + γ − (γ₁+γ²)u + O(u²). −ζ′/ζ = 1/u − γ + (γ₁+γ²)u + ... c₁ = γ₁+γ² = 0.26036. But empirical fit: 0.18755. Contradiction with the empirical... UNLESS the empirical fit was contaminated. The fit: 4 points u = 1e-2..1e-5, model c₀+c₁u+c₂u²+c₃u³, exact solve. At u = 1e-2 the c₄u⁴ ~ c₄·1e-8 unmodeled — fine. Hmm, but mpmath's diff(z, 1+u) — numerical derivative of zeta at u=1e-5: default diff h ~ 1e-(dps/3)? The earlier fit at dps 50 gave c1 = 0.18754623283535631474 — and γ²+2γ₁ = 0.18754626?? wait let me compute γ² + 2γ₁ precisely: γ² = 0.333177955... γ = 0.57721566490153286061; γ² = 0.333177955... let me: 0.5772156649² = 0.333177(0.5772² = 0.33316). 2γ₁ = −0.1456316909673534. γ²+2γ₁ = 0.3331780 − 0.1456317 = 0.1875463. The fit 0.1875462328. And γ₁+γ² = −0.0728158455 + 0.333177955 = 0.260362109. Fit says neither exactly but closest to 0.1875463 (diff 3e-8) — so c₁ = γ² + 2γ₁ EMPIRICALLY. So my Stieltjes algebra is wrong somewhere — irrelevant! The empirical wins. And c₂ from the fit: −0.05168858148. Check candidates: −(γ₂/2 + 3γγ₁/2 + γ³): γ₂ = −0.0096903636; γ₂/2 = −0.004845; 3γγ₁/2 = 3(0.5772)(−0.0728)/2 = −0.063037; γ³ = 0.192426. Sum: −0.004845 − 0.063037 + 0.192426 = 0.124544. Negative: −0.124544 ≠ −0.0517. Alternative c₂ = −(γ₂ + 3γγ₁ + γ³)?: −0.009690 − 0.126074 − 0.192426 = −0.328190 no. c₂ = −0.0516886... what combination? −(γ₂/2+γγ₁·2+...)? −0.004845 + 0.084... γγ₁ = −0.042025: −2γγ₁ = 0.084050: −0.004845+0.084050−0.192426·...? Meh. Empirics rule; symbolic Stieltjes relations can be sorted out in D-064 with flint-grade precision.\n\nNow the KEY test — the exact identity. Let me set up the full numeric test:\n- c₀..c₅ via the h-diff at higher order (the u=0 pole issue: use m.diff with h explicitly nonzero, e.g. diff(h, 0, n=k, h=1e-3)? or evaluate the fit more carefully at dps 60 with 6 points).\n- Res₁(n) = Σ_{j=1}^n C(n,j)c_{j−1} for n = 1..6.\n- S_∞(n) exact (nsum odd form).\n- λ_n: compute from zeros (4624 zeros from E-021 cache) + tail estimate.\n- Then test candidate identities:\n  (a) Sf = S_∞+1−λ_n vs [MASTER]: S_∞+1+triv+Res₁ − sides − tail — can't compute sides easily; instead test the T-independent consequence: Res₁(n) vs S_∞+1−λ_n+triv... \n  Actually the cleanest testable: from [MASTER], B0(n) := S_∞(n)+1+triv(n)+Res₁(n) should equal Sf(n)+sides(T)+tail(T) — not directly testable without sides. BUT sides_k(T) = λ_n(T)+triv+Res₁ (residue theorem) IS testable if I can compute the contour integral numerically! I CAN: integrate k_n(w−1)(−ζ′/ζ) around the rectangle numerically at small n (n ≤ 6, T = √n + 0.5 say — zero-avoiding check by hand) with mpmath. That's the definitive test of the whole chain.\n\nGiven time, let me do exactly that: full numerical verification of the exact identity at n = 2 and n = 3: compute sides (contour integral), λ_n(T) (from zeros), triv, Res₁; verify sides = λ_n(T) + triv + Res₁ to ~1e-20; and separately verify Sf = S_∞+1−λ_n decomposition; and then compute B0 = S_∞+1+triv+Res₁ and see how big it is / whether it has a closed form.","signature":""},{"type":"text","text":"Good — c₀ = −γ to 25 digits. Let me run the definitive numerical test of the full identity chain (contour integral vs residue sum) at small n."},{"type":"tool_use","id":"Bash_49","name":"Bash","input":{"command":"cd /d/Python/Quantum && ./.venv/Scripts/python.exe -c \"\nimport mpmath as m\nm.mp.dps = 40\nz = m.zeta\nld = lambda w: -m.diff(z, w)/z(w)   # -zeta'/zeta\ngamma = m.euler\n# Laurent c0..c3 (from prior fit, dps-50 verified): c0=-gamma, c1=0.18754623283535631...\n# refit at dps 40 with 5 unknowns for safety\nus = [m.mpf(10)**(-k) for k in [3,4,5,6,7]]\nA = lambda u: ld(1+u) - 1/u\nM = m.matrix([[u**j for j in range(5)] for u in us])\nb = m.matrix([A(u) for u in us])\nsol = m.lu_solve(M, b)\ncs = [sol[i] for i in range(5)]\nprint('c0..c4:', [m.nstr(c,18) for c in cs])\ndef kn(s, n): return (1+1/s)**n - 1\ndef Res1(n):\n    return m.nsum(lambda j: 0, [1,0]) + sum(m.binomial(n,j)*cs[j-1] for j in range(1,n+1))\ndef triv(n): return 1 - (m.mpf(2)/3)**n\na1 = (m.log(4*m.pi)+gamma)/2\ndef Sinf(n):\n    return (1-a1)*n - 1 + m.nsum(lambda k: (1-1/(2*k+1))**n - 1 + n/(2*k+1), [1, m.inf], tol=m.mpf('1e-30'))\n# zeros from cache\nimport numpy as np\ngam = np.load('research/numerics/data/E-021-zeros-cache.npy')\nprint('zeros:', len(gam), 'max:', gam[-1])\ndef lam_n(n, T=None):\n    tot = m.mpf(0)\n    for g in gam:\n        if T is not None and g > T: break\n        rho = m.mpc(m.mpf('0.5'), m.mpf(float(g)))\n        # pair: rho and conj(rho)\n        tot += (1 - (1-1/rho)**n).real*2\n    return tot\ndef sides(n, T):\n    J = lambda w: kn(w-1, n)*ld(w)\n    s0, s1 = m.mpf('-2.5'), 2*m.sqrt(n)\n    I1 = m.quad(lambda t: J(m.mpc(s1,t)), [-T, T])          # right vertical\n    I3 = m.quad(lambda t: J(m.mpc(s0,t)), [-T, T])          # left vertical\n    I2 = m.quad(lambda x: J(m.mpc(x,T)), [s0, s1])          # top\n    I4 = m.quad(lambda x: J(m.mpc(x,-T)), [s0, s1])         # bottom\n    # CCW: bottom (left->right), right (bottom->top), top (right->left), left (top->bottom)\n    total = I4 + 1j*I1 - I2 - 1j*I3\n    return total/(2*m.pi*1j)\nfor n in [2, 3]:\n    T = m.sqrt(n) + m.mpf('0.5')\n    S = sides(n, T)\n    lamT = lam_n(n, T)\n    print(f'n={n}: sides={m.nstr(S,16)}')\n    print(f'  lam_n(T)={m.nstr(lamT,16)} triv={m.nstr(triv(n),10)} Res1={m.nstr(Res1(n),16)}')\n    print(f'  lam_n(T)+triv+Res1 = {m.nstr(lamT+triv(n)+Res1(n),16)}')\n    print(f'  sides - (lam+triv+Res1) = {m.nstr(S-(lamT+triv(n)+Res1(n)),8)}')\n    Si = Sinf(n); lamF = lam_n(n)\n    Sf = Si + 1 - lamF\n    B0 = Si + 1 + triv(n) + Res1(n)\n    print(f'  Sinf={m.nstr(Si,14)} lambda_full(approx)={m.nstr(lamF,12)} Sf={m.nstr(Sf,12)}')\n    print(f'  B0 = Sinf+1+triv+Res1 = {m.nstr(B0,14)}')\n    print(f'  check MASTER: B0 - sides - tail = {m.nstr(B0 - S - (lamF-lamT),14)}  vs Sf')\n\"","description":"Numerically verify the full contour identity chain at n=2,3","timeout":300000},"extra_content":null}]