Current task: —

← Session 5 — Phase 0: paper deep-read + Bombieri–Lagarias literature

#163 assistant 2026-08-18 01:41:14.585 UTC · 1454→4624 tok open ⤢
thinking (12481 chars)
Conventions clear. Now write E-009a: implement Suzuki's g(t). Formula (eq. 1.3): g(t) = −4(e^{t/2}+e^{−t/2}−2) + Σ_{n≤e^{|t|}} (Λ(n)/√n)(|t|−log n) − (|t|/2)(ψ(1/4) − log π) − ¼[Φ(1,2,¼) − e^{−|t|/2}Φ(e^{−2|t|},2,¼)] Validation vs eq. 2.2 near origin: g(t) = ½|t|log|t| + A|t| + (prime sum) + r(t), r even C² O(t²), A = ½(log(2π) − ψ(2)) = ½(log(2π) + γ_E − 1) ≈ 0.707546. Check: ψ(2) = 1 − γ_E, so ½(log(2π) − (1−γ_E)) = ½(log(2π) + γ_E − 1). Compute: log(2π)=1.8378770664, γ_E=0.5772156649; sum−1 = 1.4150927313; half = 0.7075463657. ✔ Also compute the constant: −(1/2)(ψ(1/4) − log π). ψ(1/4) = −γ − π/2 cot(π/4) − 3 log 2 = −γ − π/2 − 3 log 2 ≈ −0.5772156649 − 1.5707963268 − 2.0794415417 = −4.2274535334. log π = 1.1447298858. ψ(1/4)−logπ = −5.3721834192. So −(|t|/2)(−5.372...) = +2.68609...|t|. Φ(1,2,1/4) = Σ_{k≥0} 1/(k+1/4)² = 16·ψ₁(1/4)... Actually Σ 1/(k+1/4)² = polygamma(1, 1/4) = ψ'(1/4). So Φ(1,2,1/4) = ψ'(1/4) ≈ 17.197329... (ψ'(1/4) = π²/sin²(π/4)·... anyway mpmath computes it). Validation approach in E-009a: 1. Implement g(t) directly. 2. Near-origin test: for small t (say t = 1e-3..1e-1, below ½log2≈0.3466 so prime sum = 0), compute g(t) − ½|t|log|t| − A|t| and check it's O(t²), i.e., ratio /t² converges to a constant as t→0. Also r must be even. 3. Evenness check: g(−t) = g(t). 4. Tabulate g on a mesh for later Galerkin use? D-018 says "tabulate g on a mesh (cached CSV)". The Galerkin needs g(x−y) for x,y ∈ [−a,a], i.e., g on [−2a, 2a]. Mesh with fine resolution near 0. Maybe produce a table at a values TBD in E-009b. For E-009a, tabulate g(t) on a mesh of [0, 2a_max] with a_max maybe 10? Let's decide: E-009b uses a few a values; g needs values up to 2a. Let's tabulate on a nonuniform mesh? Simplest: compute g at requested points on demand in E-009b with caching. But D-018 explicitly says tabulate. I'll tabulate on a uniform fine mesh on [0, 2A] for A=... let's pick a_max = 4 (so t up to 8, prime sum up to e^8 ≈ 2981 terms — fine). Actually Galerkin matrix entries are double integrals over element pairs; we can integrate numerically using g evaluations. A cached table + interpolation could speed. But singularity |t|log|t| at 0 — interpolation near 0 needs care. Alternative: E-009b computes double integrals via quadrature calling g directly; cost = (pairs of elements) × quadrature points. With 300 elements, ~45k diagonal-ish pairs... double integrals expensive but doable with caching: entries depend only on |i−j| offsets (Toeplitz-like structure on uniform mesh!). Q(u,v)=⟨G_a u′,v′⟩ with hat functions: u′ piecewise constant on elements; the form matrix becomes a Toeplitz matrix of second differences of G's second integral. Actually with uniform mesh and hat functions, the matrix is Toeplitz: entries depend on i−j only. Great — we only need ∫∫ g over offset pairs for O(N) distinct offsets, not O(N²). Even better: define F(s) = ∫₀^s ∫₀^? ... The entry for offset k is a double integral of g(x−y) over two unit elements at distance k, which is a second-difference stencil of the second antiderivative of g. We can compute G2(t) = second integral of g numerically on the mesh, then entries are finite differences. That requires computing G2 via cumulative quadrature — g has |t|log|t| singularity, integrable; use analytic handling of the singular part plus numerical integration of the regular part. Better plan for E-009b: decompose g(t) = ½|t|log|t| + A|t| + P(t) + r(t) where the first two are analytic (second integrals known exactly), P(t) is the prime sum (piecewise linear in |t|! since Σ(Λ(n)/√n)(|t|−log n) for n ≤ e^{|t|} — it's piecewise linear in |t| with kinks at log n; second antiderivative piecewise cubic, computable exactly), and r(t) = remaining smooth even part = the digamma/lerch terms plus the −4(cosh−2) adjustments... wait need care: the direct formula includes −4(e^{t/2}+e^{−t/2}−2) which is smooth, plus the |t| digamma term, plus the Lerch term. The decomposition eq 2.2 says the sum of those smooth terms minus their linear part gives r. Simplest: define r(t) = g(t) − [½|t|log|t| + A|t| + P(t)] numerically, then integrate r numerically (smooth, C²). This is clean and avoids differentiating anything. So E-009a deliverables: - g(t) mpmath implementation. - Self-tests: evenness, eq 2.2 asymptotic (ratio → constant), known constant values (e.g., Φ(1,2,1/4) = ψ'(1/4) check). - Tabulate g(t) on a mesh [0, T_max] with T_max maybe 12, step fine near 0 (e.g., geometric+uniform hybrid or just uniform small step 1e-3 → 12000 points; each g eval involves a prime sum up to e^{12}≈162755 terms — that's heavy: 12000 × up to 160k terms. Too heavy at high precision? We can compute with floats for the sum since Λ(n)/√n terms; do it in numpy with log tables, vectorized per t. 12000 t-values × 160k = 2e9 ops — heavy but GPU/numpy can handle ~minutes. Alternatively restrict mesh to what's needed in E-009b: a values maybe 2–6, so t up to 12. Hmm. Wait — actually what a range makes sense? Bottom eigenvalues of A_a should relate to zeros γ: the interval length 2a, and the spectral scaling... Kim et al. report Archimedean spectral law. For first comparisons, small a (like a = 1..5) with the first zeros γ₁=14.13. The natural scaling: the operator approximates eigenvalues via z = γ·a? In Suzuki's convergence, W(a,θ;z) zeros → zeros of ξ(½−iz), i.e., z = γ at real values as a→∞. But finite-a bottom eigenvalues will be larger than γ₁ (finite-interval compression). So we need a as large as feasible to see approach. Let's plan a ∈ {1, 2, 3, 4, 5} first pass. t ∈ [−2a, 2a] → t up to 10. Prime sum up to e^{10} ≈ 22026 terms per evaluation. Manageable. For E-009a tabulation: uniform mesh h = 1e-3 on [0, 10]? That's 10k points; each point sums over primes ≤ e^t. Vectorized in numpy: for each t, sum over n ≤ e^t. Precompute log n and Λ(n)/√n arrays up to e^10 = 22027 integers. For 10k t values, total work ~ 10k × average ~10k terms = 1e8 — numpy fine (chunked). Actually simpler: the prime-sum part P(t) is piecewise linear in t with breakpoints at log n! P(t) = Σ_{n≤e^t}(Λ(n)/√n)(t − log n) = M₁(t)·t − M₀(t) where M₁(t)=Σ_{n≤e^t} Λ(n)/√n, M₀ = Σ (Λ(n)/√n) log n — step functions. We can evaluate exactly at any t with a searchsorted + cumsum. Super fast, no mesh needed. So g can be evaluated efficiently at arbitrary t without a precomputed table. So E-009a: implement g with exact prime-sum via cumsum arrays, validate, then tabulate a modest CSV (mesh for Galerkin use or for plotting). I'll tabulate on [0, 10] at step 1e-3 in float64 (CSV) — cheap given fast evaluation. Also validation: r(t) = O(t²) even C². Compute r(t) for t in {1e-1, 3e-2, 1e-2, 3e-3, 1e-3}, r(t)/t² should converge to a constant; also r(−t)=r(t). We can also derive the exact limiting constant: r(t)/t² limit = ½ r″(0). We can just report empirical convergence. Additionally, a second self-check: compute g(t) two ways — direct definition vs the eq 2.2 decomposition with r computed... that's circular. Better independent check: the von Mangoldt explicit formula connection. Hmm. Another sanity check: g(0) = 0. Direct: at t=0: −4(1+1−2)=0; prime sum 0; digamma term 0; −¼[Φ(1,2,¼) − 1·Φ(1,2,¼)] = 0. So g(0)=0 trivially. Better nontrivial check: derivative? g'(0+) = A (from 2.2, since ½|t|log|t| derivative → 0, prime sum 0 near 0, r=O(t²)). Compute numerically g(t)/t → A as t→0+. g(t)/t = ½ log t + A + o(1) → diverges... no: ½|t|log|t|/t → ½ log t → −∞. Hmm so g(t)/t ~ ½ log t + A. Check g(t)/t − ½ log t → A. That's a good test. Use mpmath at dps 30 for validation at small t, and float64 for the table. Constant Φ(1,2,1/4): mpmath lerchphi(1,2,0.25). Note mpmath lerchphi(z,s,a) = Σ z^k/(a+k)^s. So Φ(e^{−2t},2,1/4) = lerchphi(exp(-2t), 2, 0.25). ✔ ψ(1/4) = mpmath.digamma(0.25). Λ(n): von Mangoldt — Λ(n) = log p if n = p^k else 0. Compute via sympy or simple sieve. For n up to e^10 ≈ 22027, easy sieve. Let me also record: A = 0.7075463656... and digamma coefficient −½(ψ(1/4)−log π) = +2.6860917096...? compute: 5.3721834192/2 = 2.6860917096. The script: research/numerics/scripts/E-009-suzuki-screw-function.py, outputs E-009-suzuki-screw-function.csv (+ .json). Register in db via db.py log-experiment afterward. Design: - Part A (validation, mpmath dps 30): evenness at several t; eq 2.2 limit r(t)/t² convergence for t→0 (t ≤ 0.3, below ½log2); g(t)/t − ½log t → A; lerchphi identity check Φ(1,2,1/4) = polygamma(1,1/4). - Part B (tabulation, float64): mesh t_k = k·h, h=1e-3, [0,10], columns t, g, plus decomposition columns maybe (singular, prime, smooth). CSV with metadata json. - Part C maybe: small-a Galerkin preview? No, that's E-009b. Write the script now. For high-precision prime sums, do them with mpmath too but n ≤ e^{0.3} tiny. For table part use float64 cumsum. Edge: at t where e^t crosses integers, sum over n ≤ e^t inclusive. Use n_max = floor(exp(t)+1e-12). With cumsum arrays indexed by n, searchsorted(logn_array, t) with side='right' on logs of integers. Precompute for n=2..N: lam[n] (Λ(n)/√n) and lamlog[n]. Cumsums C1[n], C0[n]. P(t) = C1[m]·t − C0[m], m = #{n≥2 : log n ≤ t} = floor(e^t) (careful float). Use m = int(floor(exp(t) * (1+1e-15)))... for t up to 10 fine in double. Or searchsorted on log array with t + tiny epsilon. Let me write the script. Sieve for Λ: standard: lam_log[n] = log p if n is a prime power. Sieve: for each prime p ≤ N, for multiples p^k set Λ = log p (only the highest power gets it since we overwrite sequentially per p: for each p, for m in powers: lam[m]=log p; since different p's powers don't collide except n=1, fine). CSV: keep moderate. h=1e-3 → 10001 rows. Fine. Validation tolerances: - evenness: |g(t)−g(−t)| tiny (mpmath, exact same computation basically — but still run). - A-limit: t=1e-4: g(t)/t − ½ log t ≈ A + O(t) → tolerance 1e-3. - r ratio convergence: r(t)/t² for t = 0.2, 0.1, 0.05, 0.02, 0.01: should stabilize (differences decreasing, ~linear in t since r = c₂t² + O(t³)? r is even C², but is it C³? even C² means r(t)=c₂t²+o(t²), and evenness forces r(t)=c₂t²+O(t⁴)? Not necessarily — even C² function: r(t) = r(0)+r'(0)t+½r''(0)t²+o(t²); evenness kills r'(0) only if differentiable. r even C² ⇒ r'(0)=0, r(t)=½r''(0)t²+o(t²). Ratio converges to ½r''(0). Check successive values differ by decreasing amounts; report last two difference < threshold like 0.05 relative. Also we can compute r''(0) analytically for comparison? r(t) = smooth part of g minus A|t|... The smooth terms: −4(e^{t/2}+e^{−t/2}−2) = −8(cosh(t/2)−1) = −t²/2·... cosh(t/2)−1 = t²/8 + t⁴/384..., so −8·t²/8 = −t². So this term contributes −t², i.e., ½r''(0) gets −1 from here. The Lerch term: L(t) = −¼[Φ(1,2,¼) − e^{−t/2}Φ(e^{−2t},2,¼)] for t>0. At t=0, L=0. Expand: e^{−t/2}Φ(e^{−2t},2,¼) = Σ_k e^{−2tk}/(k+¼)² · e^{−t/2} = Σ_k e^{−t(2k+½)}/(k+¼)². Let u_k = 2k+½ = 2(k+¼). So term = Σ_k e^{−t·2(k+¼)}/(k+¼)². At t: Σ [1 − 2(k+¼)t + 2(k+¼)²t² − ...]/(k+¼)² = Φ(1,2,¼) − 2t Φ(1,1,¼) + 2t² Φ(1,0,¼) − ... where Φ(1,0,¼) = Σ 1 diverges! Hmm, Φ(1,0,¼) = Σ 1 diverges, so the t² coefficient diverges — meaning the expansion has non-analytic terms (t² log t?) — consistent with the ½|t|log|t| singular structure. So don't expand analytically; skip. The digamma linear term: −(t/2)(ψ(1/4)−logπ) for t>0. The full linear coefficient in t: from digamma term: −½(ψ(1/4)−logπ) = 2.686...; from Lerch term: +¼·2Φ(1,1,¼) = ½Φ(1,1,¼) = ½·ψ(1/4)... Φ(1,1,¼) = Σ 1/(k+¼) diverges! Also divergent. Right — the ½|t|log|t| singularity comes from combining these. So no simple analytic r''(0). Fine — empirical convergence only, plus the A-limit test which is clean. Hmm wait, actually the A-limit test: g(t)/t − ½ log t → A as t→0+. From 2.2: g(t) = ½t log t + A t + r(t), r=O(t²) ⇒ g(t)/t − ½ log t = A + O(t). ✔ Clean test. Another validation: compare g computed from direct formula against an independent numerical evaluation? We could validate the whole formula against the Weil explicit formula numerically — that's what E-009b does implicitly via spectrum. Alternatively validate via Suzuki eq 1.3's origin... skip; the internal checks + literature constants suffice for E-009a. Also check Φ(1,2,1/4) = polygamma(1, 1/4) in mpmath — verifies our lerchphi argument convention. And A constant check. Alright, write the script. For the JSON sidecar: follow E-008's pattern (metadata, parameters, checks, results summary, runtime). I'll mirror its structure; let me look at the rest of E-008 to copy JSON conventions.
Conventions noted. Let me see the JSON sidecar pattern in E-008's tail before writing E-009a.
tool: Read ok
input
{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-008-li-coefficients.py",
  "offset": 80
}
result 2026-08-18 01:41:14Z → 2026-08-26 01:37:35Z
{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\derivations\\D-071-ii-prime-6-design.md",
    "content": "# D-071 \u2014 Tier ii\u2032 sub-stage ii\u2032-6 design: the L0 assembly + the honest-Bn correction\nDate: 2026-08-24 | Session: 038 (ii\u2032-6-0) | Task: 5.1 tier ii\u2032 sub-stage 6 (design)\nStatus: design COMPLETE \u2014 findings F-A/F-B/F-C documented, user approvals\nrecorded, sub-stage map ii\u2032-6-a..e decided. Numerical validation: E-030\n(ALL CHECKS PASS).\n\n## 0. What ii\u2032-6 must prove\n\n```\nSfBoundProp : \u2200 n : \u2115, 10\u2075 \u2264 n \u2192 (n : \u211d) \u2264 (3\u00b710\u00b9\u00b2 \u2212 1)\u00b2 \u2192 |Sf n| \u2264 Bn FAlt n\n```\n\nThe chain (D-064 \u00a75, all inputs now in hand): the crux `sf_eq_resW1`\n(ii\u2032-3c) turns Sf into ResW1; `rectInt'_Jlag` (ii\u2032-1b) on the D-036\nvariant-B rectangle (\u03c3\u2080 = \u22125/2, \u03c3\u2081 = 2\u221an, im = \u00b1T, T zero-avoiding in\n[\u221an, \u221an+1]) gives ResW1 = RectInt \u2212 \u03bb_n(T) \u2212 triv(\u22122); the four sides are\nbounded by the L1 kernel bounds (ii\u2032-4) + the tight R-bound (ii\u2032-5f) +\nM\u2080; the bridge bounds |\u03bb_n(T)| via RHUpTo + the global Trudgian count.\n\n## 1. THREE FINDINGS (this session; the fold analysis)\n\n### F-A: the bridge factor-2 (paper erratum, R-004 unaffected)\nThe residue sum \u03bb_n(T) = \u03a3_{\u03c1 \u2208 Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f) runs over zeros\nwith |\u03b3| \u2264 T \u2014 BOTH signs. On the line (RHUpTo), |\u03c1/(\u03c1\u22121)| = 1, so each\nterm \u2264 2\u00b7mult, giving the honest bound\n\n  |\u03bb_n(T)| \u2264 2\u00b7(mult-weighted both-signs count) \u2264 4\u00b7FAlt(T),\n\nsince the mult-weighted one-sign count \u2264 FAlt(T) (Trudgian N(T) \u2264\nF + S_b upgraded to FAlt, LiSkeleton:2396). D-036 \u00a74 / D-037 (4.1) /\nE-023's `B_bound` charge **2\u00b7FAlt** (their N(T) is the one-sign count\nbut the sum is both-signs) \u2014 a factor-2 accounting slip inherited into\nBn's `2 * F T` term. Impact: +2F \u2248 +589 at n = 10\u2075 (0.17% of Bn),\n\u2248 +2.8\u00d710\u00b9\u00b3 at N\u2081 vs margin(N\u2081) = 2.458\u00d710\u00b2\u2076 \u2014 **R-004's theorem is\nunaffected**; the Lean assembly must charge 4F; the paper gets an\nexplicit correction note at ii\u2032-7 (user protocol step 7).\n\n### F-B: I_III's near-sum needs the two-unit count (D-069 Finding 2 confirmed)\nOn the left vertical \u03c3\u2080 = \u22125/2 every zero is at distance \u2265 3/2, so the\nnear sum \u2264 (2/3)\u00b7(near count) \u2014 but the near window |\u03b3\u2212t| < 1 is a\nTWO-unit window, honestly counted by Z2(t) = 0.6\u00b7log(t+2) +\n0.886\u00b7log log(t+2) + 2.7 (ZeroCountProp2), not by \u0108\u2080(t) =\n0.433\u00b7log(t+2) + 0.886\u00b7log log(t+2) + 2.9. Bn's baked `(2/3) * C0hat T`\nundercounts by (2/3)(Z2 \u2212 \u0108\u2080) \u2248 (2/3)(0.167\u00b7log T \u2212 0.2). This is the\nD-069 Finding-2 \"(4/3)-ish\" correction made exact.\n\n### F-C: the baked Bn is unprovable beyond n \u2248 5\u00d710\u2077 (E-030 V1)\nThe two killers (F-A's +2F, F-B's +(2/3)(Z2\u2212\u0108\u2080)\u00b74T) grow like T\u00b7log T\nand eventually outgrow the horizontal slack (which grows like (log T)\u00b2):\nthe honest assembly / baked Bn ratio is 0.656 at 10\u2075, 0.980 at 10\u2078,\n**1.012 at 10\u00b9\u00b2, 1.015 at N\u2081**. With the baked Bn the fold FAILS\nasymptotically \u2014 `SfBoundProp` as baked is true but not provable via\nthe contour assembly.\n\n**Resolution (user-approved, session 038)**: redefine `Bn` to the\nhonest form \u2014 bridge `2F \u2192 4F`, I_III `(2/3)\u0108\u2080 \u2192 (2/3)Z2` \u2014 a\nfreeze-protocol exception approved by the user with the 8-step protocol\nof \u00a75. The fold then works on all of [10\u2075, N\u2081] (E-030 V4), the margin\nstays positive everywhere (V2: margin with corrected Bn > 0 on the\ngrid, and LARGER than the baked margin near 10\u2075 \u2014 the corrected Bn is\nsmaller there), and the horizontal segment-integral fits under its\nbaked share by 2.5\u20134\u00d7 everywhere (V3: ratio 0.24\u20130.40).\n\n## 2. The corrected Bn (user protocol step 1)\n\n```\nBn(F, n) := 4\u00b7F(T) + 4T[(2/3)\u00b7Z2(T) + 10.5\u00b7log(T+2) + 48] + 40\u00b71.3352\n          + 2(e\u2074+1)\u00b7[7\u00b7H\u0302(T) + 3.3] + IIMaj(n) + 1,   T = \u221an + 1\n```\n\nwith the NEW `Z2hat t := 0.6\u00b7log(t+2) + 0.886\u00b7log log(t+2) + 2.7` (the\nZeroCountProp2 bound form, named for use in Bn; ZeroCountProp2's\nstatement is untouched \u2014 its consumers (5f) are unaffected; Z2hat is\ndefinitionally the same closed form). H\u0302, IIMaj, C0hat unchanged. The\nidentifier `Bn` is retained with an explicit correction comment (user\nprotocol step 2) pointing here and to E-030; the old form is preserved\nin git history + the audit trail (step 8).\n\nPer-piece fold (the assembly proves these, then sums):\n| piece | Lean charge | Bn share | fit |\n|---|---|---|---|\n| bridge | 4\u00b7FAlt T | 4\u00b7F T | identity |\n| I_III long | 4T[(2/3)Z2 + 10.5 log + 48] | same | identity |\n| I_III short | 40\u00b7M\u2080 | 40\u00b71.3352 | identity |\n| horizontals | 2(e\u2074+1)\u00b7[NI + 5.5(10.5 log + 48) + 3.3] | 2(e\u2074+1)[7H\u0302+3.3] | V3: \u2264 0.40 |\n| I_I | IIMaj n | IIMaj n | identity |\n| triv | \u2264 1 | +1 | identity |\n\nNI(T) := Z2(T)\u00b72\u00b7log(16.5/c), c = 1/(9\u00b7C0hat(\u221an+3)) the extended\npigeonhole clearance (\u00a74.3).\n\n## 3. Perimeter additions (user-approved session 038; D-062 \u00a74 classes)\n\n- **ZeroCountGlobalProp** : `\u2200 T : \u211d, 2 \u2264 T \u2192\n  (mult-weighted one-sign count of nontrivial zeros with 0 < \u03b3 \u2264 T : \u211d)\n  \u2264 FAlt T`. The global Trudgian N(T) form (the same declared source as\n  ZeroCountProp, which is its unit-window corollary; the unit form does\n  NOT imply the global form at the FAlt level \u2014 summing windows gives\n  0.433\u00b7T\u00b7log T > 0.159\u00b7T\u00b7log T). Used by the bridge.\n- **MZeroProp** : `\u2200 t : \u211d, |t| \u2264 10 \u2192\n  \u2016logDeriv riemannZeta (-5/2 + t\u00b7I)\u2016 \u2264 1.3352`. The M\u2080 = 1.3352\n  interval-certificate (E-023 grid + sampled-Lipschitz \u00d72; the D-062 \u00a74\n  L6 entry, E-023b acb upgrade optional). Used by I_III's short piece.\n\n## 4. Component designs (the five pieces)\n\n### 4.1 The sides identity\n`rectInt'_Jlag` on the rectangle z = \u22125/2 \u2212 iT, w = 2\u221an + iT:\n- 1 interior: re 1 \u2208 (\u22125/2, 2\u221an) \u2713, im 0 \u2208 (\u2212T, T) \u2713.\n- \u03b6 \u2260 0 on the border: horizontals via the zero-avoiding T (im = \u00b1T,\n  and trivial zeros have im = 0); left vertical \u03c3 = \u22125/2 via the zero\n  classification (zeros = nontrivial \u222a {0} \u222a {\u22122n}: none at re = \u22125/2);\n  right vertical \u03c3 = 2\u221an \u2265 2 via re > 1 nonvanishing.\n- Sz = {nontrivial zeros with |\u03b3| \u2264 T} \u222a {\u22122} (zeroMult(\u22122) = 1, ii\u2032-4);\n  \u03b6(0) = \u22121/2 \u2260 0.\n\u27f9 ResW1 n = RectInt \u2212 \u03a3_{Sz} mult\u00b7(1\u2212(\u03c1/(\u03c1\u22121))\u207f), and\n|Sf n| = |(ResW1 n).re| \u2264 \u2016ResW1 n\u2016 \u2264 \u2016RectInt\u2016 + |\u03bb_n(T)| + |triv|.\nRectangleIntegral' is (2\u03c0i)\u207b\u00b9-normalized: \u2016RectInt\u2016 \u2264 (\u03a3 side\nintegrals)/(2\u03c0) \u2264 \u03a3 side integrals \u2014 Bn charges the raw side bounds\n(the paper's convention; the 2\u03c0 factor is spare slack).\n\n### 4.2 The bridge (uses hRH + ZeroCountGlobalProp)\nT = \u221an + 1 \u2264 3\u00d710\u00b9\u00b2 (from n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2): every zero in Sz is\non the line (hRH) \u27f9 |\u03c1/(\u03c1\u22121)| = 1 (|\u03c1|\u00b2 = |1\u2212\u03c1|\u00b2 at re = 1/2) \u27f9\n|1\u2212(\u03c1/(\u03c1\u22121))\u207f| \u2264 2\u00b7mult. Count: both-signs = 2\u00b7(one-sign) \u2264 2\u00b7FAlt(T)\n(conj symmetry, no real zeros).\n\u27f9 |\u03bb_n(T)| \u2264 2\u00b7mult\u00b7count \u2264 4\u00b7FAlt(T).\n(The conj-pairing |2 \u2212 w\u207f \u2212 w\u207b\u207f| \u2264 4 gives the same constant \u2014 recorded\nas the alternative accounting; no improvement possible: n\u03b8 can be\nextremal.)\n\n### 4.3 The extended pigeonhole (Finding-2 repair)\n`exists_zero_avoiding_T_wide`: T \u2208 [a, a+1] with clearance\nc = 1/(9\u00b7C0hat(a+2)) against ALL zeros with im \u2208 (a\u22121, a+2) (3-unit\nwindow count \u2264 3\u00b7C0hat(a+2) from ZeroCountProp applied to the three\nunit sub-windows \u2014 NO new perimeter needed; the midpoint-pigeonhole\nmachinery of exists_zero_avoiding_T cloned at 3\u00d7 count, a \u2265 3 so\na\u22121 \u2265 2 \u2713; \u221an \u2265 316 \u226b 3 \u2713).\n\n### 4.4 The four sides\n- **I_III (left vertical \u03c3 = \u22125/2, length 2T)**: kernel \u2264 2\n  (kFun_norm_le_two \u2713). For |t| \u2265 10: tight R-bound (5f capstone,\n  \u03c3 \u2208 [\u22125/2, 3] \u2713) + near sum \u2264 (2/3)\u00b7Z2 (|w\u2212\u03c1| \u2265 3/2 since re \u03c1 \u2264 1).\n  For |t| \u2264 10: MZeroProp \u27f9 |\u03b6\u2032/\u03b6| \u2264 1.3352, segment length 20, kernel\n  \u2264 2 \u27f9 \u2264 40\u00b71.3352.\n- **I_II/I_IV (horizontals, the crux)**: kernel \u2264 e\u2074+1 on [\u22123, 3]\n  (kFun_shift_norm_le_exp_four_add_one \u2713). Tight R-bound at height T\n  (T \u2265 \u221a10\u2075 \u2265 316 \u2265 10 \u2713). The near-sum INTEGRAL (NOT the max\u00d7length \u2014\n  this is what makes the fold fit): with w = x + iT, x \u2208 [\u22125/2, 3],\n  \u03c1 = \u03b2 + i\u03b3, \u03b4 = |T\u2212\u03b3| \u2265 c (extended pigeonhole):\n  \u222b_{-5/2}^{3} dx/|w\u2212\u03c1| \u2264 asinh((3\u2212\u03b2)/\u03b4) + asinh((\u03b2+5/2)/\u03b4)\n  \u2264 2\u00b7asinh(5.5/\u03b4) \u2264 2\u00b7log(16.5/c),\n  so \u03a3_{near} mult\u00b7\u222b \u2264 Z2(T)\u00b72\u00b7log(16.5/c) =: NI(T). The R-part\n  integrates to 5.5\u00b7(10.5\u00b7log(T+2) + 48). The right tail [3, 2\u221an]:\n  Dirichlet stepping (|\u03b6\u2032/\u03b6(\u03c3+iT)| \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 via the\n  LSeries vonMangoldt form; geometric sum \u2264 e\u00b7dirichletC2\u00b72 \u2264 3.3 with\n  the kernel stepping kFun_shift_norm_le_exp_sqrt_half_add_one \u2014 the\n  (6.12) argument). Total per horizontal: (e\u2074+1)\u00b7[NI + 5.5\u00b7(10.5 log +\n  48) + 3.3]; E-030 V3 certifies NI + 5.5\u00b7(10.5 log + 48) + 3.3 \u2264\n  0.40\u00b7(7H\u0302 + 3.3) on the grid (and the formal fold needs only \u2264 7H\u0302 +\n  3.3 \u2014 the \u0108\u2080\u00b2 term dwarfs everything: NI ~ 1.2\u00b7L\u00b7log L vs 21\u0108\u2080\u00b2 ~\n  3.94\u00b7L\u00b2).\n- **I_I (right vertical \u03c3\u2081 = 2\u221an)**: |\u03b6\u2032/\u03b6| \u2264 2^{\u2212(\u03c3\u2081\u22122)}\u00b7dirichletC2\n  (Dirichlet stepping) \u2264 2^{\u2212(2\u221an\u22122)}\u00b70.57; kernel \u2264 e^{\u221an/2}+1\n  (kFun_shift_norm_le_exp_sqrt_half_add_one \u2713); length 2T \u27f9 \u2264 IIMaj n.\n- **triv(\u22122)**: term = mult\u00b7(1\u2212((\u22122)/(\u22123))\u207f) = 1 \u2212 (2/3)\u207f \u2264 1\n  (zeroMult_neg_two = 1 \u2713; |2/3|\u207f \u2264 1).\n\n### 4.5 The fold\n|Sf n| \u2264 \u2016RectInt\u2016 + |\u03bb_n(T)| + |triv|\n\u2264 [NI + 5.5(10.5 log + 48) + 3.3]\u00b72(e\u2074+1)/(2\u03c0)\u00b7... \u2014 NO: Bn charges the\nraw side bounds (the paper's convention; RectangleIntegral' is\n2\u03c0-normalized so \u2016RectInt\u2016 \u2264 \u03a3 sides/(2\u03c0) \u2264 \u03a3 sides \u2713 the fold is\nimmediate per-piece). The per-piece fits of \u00a72 give |Sf n| \u2264 Bn FAlt n\non [10\u2075, N\u2081] \u2014 the only real-analytic comparison needed is the\nhorizontal share NI + 5.5\u00b7(10.5 log + 48) + 3.3 \u2264 7H\u0302 + 3.3, an explicit\ninequality in L = log T, LL = log log T for L \u2265 log(\u221a10\u2075+1) (the\npinch-lemma pattern from 5f-iii: certified endpoint evaluation +\ngrowth-direction argument; E-030 V3 is the numeric witness: ratio\n0.398 \u2192 0.241 decreasing).\n\n## 5. The user-approved 8-step protocol (session 038, verbatim decision)\n\n1. Change `Bn` to the honest expression: 2F \u2192 4F, (2/3)\u0108\u2080 \u2192 (2/3)Z2.\n2. Fresh explicitly-documented corrected definition (identifier `Bn`\n   retained, correction comment + pointer here).\n3. Re-run the structural convexity proof (marginTilde_convex \u2014 prove\n   again, don't assume survival).\n4. Re-certify both base points with rational interval arithmetic\n   (margin\u0303(8\u00d710\u2074), margin\u0303(10\u2075) \u2014 values IMPROVE: the corrected Bn is\n   smaller there).\n5. Re-run the endpoint margin calculations.\n6. Complete ii\u2032-6 against the corrected Bn.\n7. At ii\u2032-7: Paper A correction note (both-signs factor + I_III\n   two-unit count).\n8. Preserve the old results in the audit history (git history +\n   E-030 + this document + the journal).\n\n## 6. Sub-stage map\n\n| # | Content | Depends | Est. |\n|---|---------|---------|------|\n| ii\u2032-6-a | Bn redefinition + Z2hat def + marginTilde/marginExpanded lockstep + convexity re-proof (steps 1\u20133) + base-point re-certification (step 4) + endpoint margins (step 5) | \u2014 | 1 sess |\n| ii\u2032-6-b | perimeter Props (ZeroCountGlobalProp, MZeroProp) + extended pigeonhole + sides identity + bridge | 6-a | 1 sess |\n| ii\u2032-6-c | the four side bounds (horizontals = the segment-integral machine; the long pole) | 6-b | 1\u20132 sess |\n| ii\u2032-6-d | the fold (per-piece assembly + the horizontal pinch) \u27f9 `sfBoundProp : SfBoundProp` | 6-c | 0.5\u20131 sess |\n| ii\u2032-7 | closure: lambda_pos_finite_height_closed, full axiom audit, paper correction note (step 7), tag upgrade, archive closure | 6-d | 1 sess |\n\n## 7. Affected declarations of the Bn redefinition (mapped, session 038)\n\n- `Bn` (LiSkeleton:2413), `marginTilde` (754 \u2014 the duplicated\n  expression, lockstep), `marginExpanded` + the mK constant (1819 \u2014\n  the I_III constant block changes (2/3)\u00b72.9 \u2192 (2/3)\u00b72.7 and the\n  F-block doubles), `marginTilde_eq_expanded` (bookkeeping re-run),\n  `marginTilde_convex` (\u03c8-table: the 4F block scales \u00d72 \u2014 still\n  negative; the I_III (2/3)Z2 block \u2014 same log/loglog form as the\n  (2/3)\u0108\u2080 block \u2014 re-prove the two changed rows), `marginTilde_eq_sub`\n  (bookkeeping re-run).\n- LiBasePoints: `marginTilde_FAlt_80000_pos`,\n  `marginTilde_FAlt_80000_lt_100000` \u2014 re-certify with rational\n  interval arithmetic (same machinery; the values grow by the\n  baked\u2212corrected difference \u2248 1.2\u00d710\u00b3 at 8\u00d710\u2074 / 1.24\u00d710\u00b3 at 10\u2075).\n- `lambda_pos_finite_height_verified` \u2014 statement Bn-independent\n  (0 < (liCoeff n).re); proof re-checks against the changed pieces.\n\n## 8. Risks\n\n- The convexity re-proof's changed rows may need new psi-arguments if\n  the Z2 block's \u03c8 \u2260 the \u0108\u2080 block's \u03c8 shape (both are\n  \u03b1\u00b7log(T+2)+\u03b2\u00b7log log(T+2)+const with \u03b1 > 0, \u03b2 \u2265 0 \u2014 D-057's rows\n  cover this form structurally; expected mechanical).\n- The horizontal segment-integral's asinh/log elementary bounds are\n  the usual certified-numerics grind (LiTightR piece-3-class; budgeted).\n- The bridge's both-signs count uses conj symmetry of the zero set\n  (isNontrivialZero_conj \u2713 in hand) \u2014 mechanical.",
    "numLines": 235,
    "startLine": 1,
    "totalLines": 235
  }
}
raw content_json (database row) 
[{"type":"thinking","thinking":"Conventions clear. Now write E-009a: implement Suzuki's g(t).\n\nFormula (eq. 1.3):\ng(t) = −4(e^{t/2}+e^{−t/2}−2) + Σ_{n≤e^{|t|}} (Λ(n)/√n)(|t|−log n)\n       − (|t|/2)(ψ(1/4) − log π) − ¼[Φ(1,2,¼) − e^{−|t|/2}Φ(e^{−2|t|},2,¼)]\n\nValidation vs eq. 2.2 near origin: g(t) = ½|t|log|t| + A|t| + (prime sum) + r(t), r even C² O(t²), A = ½(log(2π) − ψ(2)) = ½(log(2π) + γ_E − 1) ≈ 0.707546.\n\nCheck: ψ(2) = 1 − γ_E, so ½(log(2π) − (1−γ_E)) = ½(log(2π) + γ_E − 1). Compute: log(2π)=1.8378770664, γ_E=0.5772156649; sum−1 = 1.4150927313; half = 0.7075463657. ✔\n\nAlso compute the constant: −(1/2)(ψ(1/4) − log π). ψ(1/4) = −γ − π/2 cot(π/4) − 3 log 2 = −γ − π/2 − 3 log 2 ≈ −0.5772156649 − 1.5707963268 − 2.0794415417 = −4.2274535334. log π = 1.1447298858. ψ(1/4)−logπ = −5.3721834192. So −(|t|/2)(−5.372...) = +2.68609...|t|.\n\nΦ(1,2,1/4) = Σ_{k≥0} 1/(k+1/4)² = 16·ψ₁(1/4)... Actually Σ 1/(k+1/4)² = polygamma(1, 1/4) = ψ'(1/4). So Φ(1,2,1/4) = ψ'(1/4) ≈ 17.197329... (ψ'(1/4) = π²/sin²(π/4)·... anyway mpmath computes it).\n\nValidation approach in E-009a:\n1. Implement g(t) directly.\n2. Near-origin test: for small t (say t = 1e-3..1e-1, below ½log2≈0.3466 so prime sum = 0), compute g(t) − ½|t|log|t| − A|t| and check it's O(t²), i.e., ratio /t² converges to a constant as t→0. Also r must be even.\n3. Evenness check: g(−t) = g(t).\n4. Tabulate g on a mesh for later Galerkin use? D-018 says \"tabulate g on a mesh (cached CSV)\". The Galerkin needs g(x−y) for x,y ∈ [−a,a], i.e., g on [−2a, 2a]. Mesh with fine resolution near 0. Maybe produce a table at a values TBD in E-009b. For E-009a, tabulate g(t) on a mesh of [0, 2a_max] with a_max maybe 10? Let's decide: E-009b uses a few a values; g needs values up to 2a. Let's tabulate on a nonuniform mesh? Simplest: compute g at requested points on demand in E-009b with caching. But D-018 explicitly says tabulate. I'll tabulate on a uniform fine mesh on [0, 2A] for A=... let's pick a_max = 4 (so t up to 8, prime sum up to e^8 ≈ 2981 terms — fine). Actually Galerkin matrix entries are double integrals over element pairs; we can integrate numerically using g evaluations. A cached table + interpolation could speed. But singularity |t|log|t| at 0 — interpolation near 0 needs care. Alternative: E-009b computes double integrals via quadrature calling g directly; cost = (pairs of elements) × quadrature points. With 300 elements, ~45k diagonal-ish pairs... double integrals expensive but doable with caching: entries depend only on |i−j| offsets (Toeplitz-like structure on uniform mesh!). Q(u,v)=⟨G_a u′,v′⟩ with hat functions: u′ piecewise constant on elements; the form matrix becomes a Toeplitz matrix of second differences of G's second integral. Actually with uniform mesh and hat functions, the matrix is Toeplitz: entries depend on i−j only. Great — we only need ∫∫ g over offset pairs for O(N) distinct offsets, not O(N²). Even better: define F(s) = ∫₀^s ∫₀^? ... The entry for offset k is a double integral of g(x−y) over two unit elements at distance k, which is a second-difference stencil of the second antiderivative of g. We can compute G2(t) = second integral of g numerically on the mesh, then entries are finite differences. That requires computing G2 via cumulative quadrature — g has |t|log|t| singularity, integrable; use analytic handling of the singular part plus numerical integration of the regular part.\n\nBetter plan for E-009b: decompose g(t) = ½|t|log|t| + A|t| + P(t) + r(t) where the first two are analytic (second integrals known exactly), P(t) is the prime sum (piecewise linear in |t|! since Σ(Λ(n)/√n)(|t|−log n) for n ≤ e^{|t|} — it's piecewise linear in |t| with kinks at log n; second antiderivative piecewise cubic, computable exactly), and r(t) = remaining smooth even part = the digamma/lerch terms plus the −4(cosh−2) adjustments... wait need care: the direct formula includes −4(e^{t/2}+e^{−t/2}−2) which is smooth, plus the |t| digamma term, plus the Lerch term. The decomposition eq 2.2 says the sum of those smooth terms minus their linear part gives r. Simplest: define r(t) = g(t) − [½|t|log|t| + A|t| + P(t)] numerically, then integrate r numerically (smooth, C²). This is clean and avoids differentiating anything.\n\nSo E-009a deliverables:\n- g(t) mpmath implementation.\n- Self-tests: evenness, eq 2.2 asymptotic (ratio → constant), known constant values (e.g., Φ(1,2,1/4) = ψ'(1/4) check).\n- Tabulate g(t) on a mesh [0, T_max] with T_max maybe 12, step fine near 0 (e.g., geometric+uniform hybrid or just uniform small step 1e-3 → 12000 points; each g eval involves a prime sum up to e^{12}≈162755 terms — that's heavy: 12000 × up to 160k terms. Too heavy at high precision? We can compute with floats for the sum since Λ(n)/√n terms; do it in numpy with log tables, vectorized per t. 12000 t-values × 160k = 2e9 ops — heavy but GPU/numpy can handle ~minutes. Alternatively restrict mesh to what's needed in E-009b: a values maybe 2–6, so t up to 12. Hmm.\n\nWait — actually what a range makes sense? Bottom eigenvalues of A_a should relate to zeros γ: the interval length 2a, and the spectral scaling... Kim et al. report Archimedean spectral law. For first comparisons, small a (like a = 1..5) with the first zeros γ₁=14.13. The natural scaling: the operator approximates eigenvalues via z = γ·a? In Suzuki's convergence, W(a,θ;z) zeros → zeros of ξ(½−iz), i.e., z = γ at real values as a→∞. But finite-a bottom eigenvalues will be larger than γ₁ (finite-interval compression). So we need a as large as feasible to see approach. Let's plan a ∈ {1, 2, 3, 4, 5} first pass. t ∈ [−2a, 2a] → t up to 10. Prime sum up to e^{10} ≈ 22026 terms per evaluation. Manageable.\n\nFor E-009a tabulation: uniform mesh h = 1e-3 on [0, 10]? That's 10k points; each point sums over primes ≤ e^t. Vectorized in numpy: for each t, sum over n ≤ e^t. Precompute log n and Λ(n)/√n arrays up to e^10 = 22027 integers. For 10k t values, total work ~ 10k × average ~10k terms = 1e8 — numpy fine (chunked). Actually simpler: the prime-sum part P(t) is piecewise linear in t with breakpoints at log n! P(t) = Σ_{n≤e^t}(Λ(n)/√n)(t − log n) = M₁(t)·t − M₀(t) where M₁(t)=Σ_{n≤e^t} Λ(n)/√n, M₀ = Σ (Λ(n)/√n) log n — step functions. We can evaluate exactly at any t with a searchsorted + cumsum. Super fast, no mesh needed. So g can be evaluated efficiently at arbitrary t without a precomputed table. \n\nSo E-009a: implement g with exact prime-sum via cumsum arrays, validate, then tabulate a modest CSV (mesh for Galerkin use or for plotting). I'll tabulate on [0, 10] at step 1e-3 in float64 (CSV) — cheap given fast evaluation.\n\nAlso validation: r(t) = O(t²) even C². Compute r(t) for t in {1e-1, 3e-2, 1e-2, 3e-3, 1e-3}, r(t)/t² should converge to a constant; also r(−t)=r(t). We can also derive the exact limiting constant: r(t)/t² limit = ½ r″(0). We can just report empirical convergence.\n\nAdditionally, a second self-check: compute g(t) two ways — direct definition vs the eq 2.2 decomposition with r computed... that's circular. Better independent check: the von Mangoldt explicit formula connection. Hmm. Another sanity check: g(0) = 0. Direct: at t=0: −4(1+1−2)=0; prime sum 0; digamma term 0; −¼[Φ(1,2,¼) − 1·Φ(1,2,¼)] = 0. So g(0)=0 trivially. \n\nBetter nontrivial check: derivative? g'(0+) = A (from 2.2, since ½|t|log|t| derivative → 0, prime sum 0 near 0, r=O(t²)). Compute numerically g(t)/t → A as t→0+. g(t)/t = ½ log t + A + o(1) → diverges... no: ½|t|log|t|/t → ½ log t → −∞. Hmm so g(t)/t ~ ½ log t + A. Check g(t)/t − ½ log t → A. That's a good test.\n\nUse mpmath at dps 30 for validation at small t, and float64 for the table.\n\nConstant Φ(1,2,1/4): mpmath lerchphi(1,2,0.25). Note mpmath lerchphi(z,s,a) = Σ z^k/(a+k)^s. So Φ(e^{−2t},2,1/4) = lerchphi(exp(-2t), 2, 0.25). ✔\n\nψ(1/4) = mpmath.digamma(0.25).\n\nΛ(n): von Mangoldt — Λ(n) = log p if n = p^k else 0. Compute via sympy or simple sieve. For n up to e^10 ≈ 22027, easy sieve.\n\nLet me also record: A = 0.7075463656... and digamma coefficient −½(ψ(1/4)−log π) = +2.6860917096...? compute: 5.3721834192/2 = 2.6860917096.\n\nThe script: research/numerics/scripts/E-009-suzuki-screw-function.py, outputs E-009-suzuki-screw-function.csv (+ .json). Register in db via db.py log-experiment afterward.\n\nDesign:\n- Part A (validation, mpmath dps 30): evenness at several t; eq 2.2 limit r(t)/t² convergence for t→0 (t ≤ 0.3, below ½log2); g(t)/t − ½log t → A; lerchphi identity check Φ(1,2,1/4) = polygamma(1,1/4).\n- Part B (tabulation, float64): mesh t_k = k·h, h=1e-3, [0,10], columns t, g, plus decomposition columns maybe (singular, prime, smooth). CSV with metadata json.\n- Part C maybe: small-a Galerkin preview? No, that's E-009b.\n\nWrite the script now.\n\nFor high-precision prime sums, do them with mpmath too but n ≤ e^{0.3} tiny. For table part use float64 cumsum.\n\nEdge: at t where e^t crosses integers, sum over n ≤ e^t inclusive. Use n_max = floor(exp(t)+1e-12). With cumsum arrays indexed by n, searchsorted(logn_array, t) with side='right' on logs of integers. Precompute for n=2..N: lam[n] (Λ(n)/√n) and lamlog[n]. Cumsums C1[n], C0[n]. P(t) = C1[m]·t − C0[m], m = #{n≥2 : log n ≤ t} = floor(e^t) (careful float). Use m = int(floor(exp(t) * (1+1e-15)))... for t up to 10 fine in double. Or searchsorted on log array with t + tiny epsilon.\n\nLet me write the script.\n\nSieve for Λ: standard: lam_log[n] = log p if n is a prime power. Sieve: for each prime p ≤ N, for multiples p^k set Λ = log p (only the highest power gets it since we overwrite sequentially per p: for each p, for m in powers: lam[m]=log p; since different p's powers don't collide except n=1, fine).\n\nCSV: keep moderate. h=1e-3 → 10001 rows. Fine.\n\nValidation tolerances:\n- evenness: |g(t)−g(−t)| tiny (mpmath, exact same computation basically — but still run).\n- A-limit: t=1e-4: g(t)/t − ½ log t ≈ A + O(t) → tolerance 1e-3.\n- r ratio convergence: r(t)/t² for t = 0.2, 0.1, 0.05, 0.02, 0.01: should stabilize (differences decreasing, ~linear in t since r = c₂t² + O(t³)? r is even C², but is it C³? even C² means r(t)=c₂t²+o(t²), and evenness forces r(t)=c₂t²+O(t⁴)? Not necessarily — even C² function: r(t) = r(0)+r'(0)t+½r''(0)t²+o(t²); evenness kills r'(0) only if differentiable. r even C² ⇒ r'(0)=0, r(t)=½r''(0)t²+o(t²). Ratio converges to ½r''(0). Check successive values differ by decreasing amounts; report last two difference < threshold like 0.05 relative.\n\nAlso we can compute r''(0) analytically for comparison? r(t) = smooth part of g minus A|t|... The smooth terms: −4(e^{t/2}+e^{−t/2}−2) = −8(cosh(t/2)−1) = −t²/2·... cosh(t/2)−1 = t²/8 + t⁴/384..., so −8·t²/8 = −t². So this term contributes −t², i.e., ½r''(0) gets −1 from here.\n\nThe Lerch term: L(t) = −¼[Φ(1,2,¼) − e^{−t/2}Φ(e^{−2t},2,¼)] for t>0. At t=0, L=0. Expand: e^{−t/2}Φ(e^{−2t},2,¼) = Σ_k e^{−2tk}/(k+¼)² · e^{−t/2} = Σ_k e^{−t(2k+½)}/(k+¼)². Let u_k = 2k+½ = 2(k+¼). So term = Σ_k e^{−t·2(k+¼)}/(k+¼)². At t: Σ [1 − 2(k+¼)t + 2(k+¼)²t² − ...]/(k+¼)² = Φ(1,2,¼) − 2t Φ(1,1,¼) + 2t² Φ(1,0,¼) − ... where Φ(1,0,¼) = Σ 1 diverges! Hmm, Φ(1,0,¼) = Σ 1 diverges, so the t² coefficient diverges — meaning the expansion has non-analytic terms (t² log t?) — consistent with the ½|t|log|t| singular structure. So don't expand analytically; skip. The digamma linear term: −(t/2)(ψ(1/4)−logπ) for t>0.\n\nThe full linear coefficient in t: from digamma term: −½(ψ(1/4)−logπ) = 2.686...; from Lerch term: +¼·2Φ(1,1,¼) = ½Φ(1,1,¼) = ½·ψ(1/4)... Φ(1,1,¼) = Σ 1/(k+¼) diverges! Also divergent. Right — the ½|t|log|t| singularity comes from combining these. So no simple analytic r''(0). Fine — empirical convergence only, plus the A-limit test which is clean.\n\nHmm wait, actually the A-limit test: g(t)/t − ½ log t → A as t→0+. From 2.2: g(t) = ½t log t + A t + r(t), r=O(t²) ⇒ g(t)/t − ½ log t = A + O(t). ✔ Clean test.\n\nAnother validation: compare g computed from direct formula against an independent numerical evaluation? We could validate the whole formula against the Weil explicit formula numerically — that's what E-009b does implicitly via spectrum. Alternatively validate via Suzuki eq 1.3's origin... skip; the internal checks + literature constants suffice for E-009a. Also check Φ(1,2,1/4) = polygamma(1, 1/4) in mpmath — verifies our lerchphi argument convention. And A constant check.\n\nAlright, write the script.\n\nFor the JSON sidecar: follow E-008's pattern (metadata, parameters, checks, results summary, runtime). I'll mirror its structure; let me look at the rest of E-008 to copy JSON conventions.","signature":""},{"type":"text","text":"Conventions noted. Let me see the JSON sidecar pattern in E-008's tail before writing E-009a."},{"type":"tool_use","id":"Read_7","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\numerics\\scripts\\E-008-li-coefficients.py","offset":80},"extra_content":null}]