← Session 36 — ii′-6-DL dog-leg + side bounds; Paper A review
thinking (1416 chars)
Key archive facts:
- R-004 line 72: "Voros 1703.02844 [Misguich numerics]" — so the arXiv is 1703.02844 and the numerics are MISGUICH's (reported in Voros's paper? or a separate Misguich source?). The D-037 line 174: "Misguich–Voros (Voros 1703.02844 reports λ_n > 0 computed to n = 5·10⁵; also Keiper to 7000, Maślanka to 3300)".
- journal/session-013.md:121: "journal; correct: Voros, "Discretized Keiper/Li approach to the..." — so session 013 already flagged a citation correction (the referee-list.md:25 says "verification to n = 5×10⁵ with Misguich (Exp. Math. 29(4), 2020)").
So the archive's understanding: Voros (arXiv:1703.02844, Exp. Math. 29(4):452–469, 2020) REPORTS λ_n > 0 computed to n = 5×10⁵ with Misguich's numerics. The arXiv ID 1703.02844 — let me fetch its abstract to verify what exactly is computed (ordinary λ_n or discretized).
arXiv:1703.02844 — that's "Discretized Keiper/Li approach to the Riemann hypothesis" by André Voros? Let me fetch the abstract.
The user wants: "I would not allow that citation to carry the finite splice unless you have checked, theorem-by-theorem, that the 5×10⁵ computation is for the ordinary λ_n appearing in your theorem rather than a discretized/modified sequence. ... If your actual Lean theorem instead takes LiVerifiedUpTo as an explicit certificate, state that directly and cite the real certificate."
Let me fetch the arXiv abstract of 1703.02844.
The archive cites arXiv:1703.02844 (Voros, with Misguich numerics). Fetching its actual abstract to verify what's computed.
tool: WebFetch ok
input
{
"url": "https://arxiv.org/abs/1703.02844",
"prompt": "What is this paper's title, authors, and what does it actually compute or prove? Specifically: does it verify positivity of the ORDINARY Keiper\u2013Li coefficients lambda_n (defined as the infinite sum over nontrivial zeros of 1-(1-1/rho)^n), or a discretized/modified sequence? Up to what n? Quote the abstract and any theorem statements about the range of verification."
}
result 2026-08-26 21:41:42Z → 2026-08-26 21:42:25Z
bytes=41478 code=200 code_text='OK' result='**Title:** "Discretized Keiper/Li approach to the Riemann Hypothesis"\n\n**Author:** André Voros\n\n**What it does — modified sequence, not the ordinary λ_n:**\n\nThe paper does *not* compute the ordinary Keiper–Li coefficients. The abstract describes the original sequence as "highly elusive both analytically and numerically" and states: "We deform it to fully explicit sequences, simpler to analyze and to compute." So the verification concerns a **discretized/deformed sequence**, not the infinite-sum λ_n you defined.\n\n**Range of verification:**\n\nThe abstract gives the bound "(up to $n=5 \\cdot 10^5$ by G. Misguich)" — i.e., n up to 500,000, with the computation credited to G. Misguich. This applies to the deformed explicit sequences.\n\n**Counterexample testing:**\n\nThe abstract notes the method "also works on the Davenport--Heilbronn counterexamples" and that the author can "demonstrate explicit tests that selectively react to zeros off the critical line" — meaning the deformed sequences can distinguish functions with off-critical-line zeros.\n\n**Theorem statements:**\n\nThe abstract page contains no formal theorem statements, so I can\'t quote any theorems specifying a verification range; the only range given is the abstract\'s n = 5·10⁵ figure. The full text (PDF/HTML) would be needed to confirm whether any theorem formally states positivity results for that range.' duration_ms=43013.522499997634 url='https://arxiv.org/abs/1703.02844'
raw content_json (database row)
[{"type":"thinking","thinking":"Key archive facts:\n- R-004 line 72: \"Voros 1703.02844 [Misguich numerics]\" — so the arXiv is 1703.02844 and the numerics are MISGUICH's (reported in Voros's paper? or a separate Misguich source?). The D-037 line 174: \"Misguich–Voros (Voros 1703.02844 reports λ_n > 0 computed to n = 5·10⁵; also Keiper to 7000, Maślanka to 3300)\".\n- journal/session-013.md:121: \"journal; correct: Voros, \"Discretized Keiper/Li approach to the...\" — so session 013 already flagged a citation correction (the referee-list.md:25 says \"verification to n = 5×10⁵ with Misguich (Exp. Math. 29(4), 2020)\").\n\nSo the archive's understanding: Voros (arXiv:1703.02844, Exp. Math. 29(4):452–469, 2020) REPORTS λ_n > 0 computed to n = 5×10⁵ with Misguich's numerics. The arXiv ID 1703.02844 — let me fetch its abstract to verify what exactly is computed (ordinary λ_n or discretized).\n\narXiv:1703.02844 — that's \"Discretized Keiper/Li approach to the Riemann hypothesis\" by André Voros? Let me fetch the abstract.\n\nThe user wants: \"I would not allow that citation to carry the finite splice unless you have checked, theorem-by-theorem, that the 5×10⁵ computation is for the ordinary λ_n appearing in your theorem rather than a discretized/modified sequence. ... If your actual Lean theorem instead takes LiVerifiedUpTo as an explicit certificate, state that directly and cite the real certificate.\"\n\nLet me fetch the arXiv abstract of 1703.02844.","signature":""},{"type":"text","text":"The archive cites arXiv:1703.02844 (Voros, with Misguich numerics). Fetching its actual abstract to verify what's computed."},{"type":"tool_use","id":"WebFetch_268","name":"WebFetch","input":{"url":"https://arxiv.org/abs/1703.02844","prompt":"What is this paper's title, authors, and what does it actually compute or prove? Specifically: does it verify positivity of the ORDINARY Keiper–Li coefficients lambda_n (defined as the infinite sum over nontrivial zeros of 1-(1-1/rho)^n), or a discretized/modified sequence? Up to what n? Quote the abstract and any theorem statements about the range of verification."},"extra_content":null}]