← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (683 chars)
Stirling.lean only has two theorems (digamma differentiability + trigamma series) — not the full Stirling bounds. But the header mentions `Zeta23.GammaFacts.Series`: digamma_series, hasSum_digamma_series, summable_digamma_series, **inv_gamma_eq_prod (Weierstrass product for 1/Γ)**! The Weierstrass product for 1/Γ exists in Zeta23! That's huge for the Γ bounds.
Also "Zeta23/GammaFacts/Mu.lean: ψ on the vertical line Re = 1/4, error O(1/τ²)" — there's a digamma O(1/τ²) bound in GammaFacts/Mu.lean! And "Im log Γ(1/4 + iT/2) main term; |Γ| growth in strips" — the Riemann–von Mangoldt argument has |Γ| growth in strips!
Let me inventory GammaFacts/ and the RvM |Γ|-growth lemmas.
`Stirling.lean` itself is small, but it references `Zeta23.GammaFacts.Series` (digamma series + **Weierstrass product for 1/Γ**) and GammaFacts/Mu with ψ error bounds, plus "|Γ| growth in strips" in the RvM argument. Inventorying.
tool: Bash
input
{
"command": "cd D:/Python/Quantum/zeta-23-lean && ls Zeta23/GammaFacts/ && grep -rn \"theorem\\|lemma\" Zeta23/GammaFacts/Series.lean | grep -v \"^.*--\" | head -20",
"description": "Inventory GammaFacts module"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Stirling.lean only has two theorems (digamma differentiability + trigamma series) — not the full Stirling bounds. But the header mentions `Zeta23.GammaFacts.Series`: digamma_series, hasSum_digamma_series, summable_digamma_series, **inv_gamma_eq_prod (Weierstrass product for 1/Γ)**! The Weierstrass product for 1/Γ exists in Zeta23! That's huge for the Γ bounds.\n\nAlso \"Zeta23/GammaFacts/Mu.lean: ψ on the vertical line Re = 1/4, error O(1/τ²)\" — there's a digamma O(1/τ²) bound in GammaFacts/Mu.lean! And \"Im log Γ(1/4 + iT/2) main term; |Γ| growth in strips\" — the Riemann–von Mangoldt argument has |Γ| growth in strips!\n\nLet me inventory GammaFacts/ and the RvM |Γ|-growth lemmas.","signature":""},{"type":"text","text":"`Stirling.lean` itself is small, but it references `Zeta23.GammaFacts.Series` (digamma series + **Weierstrass product for 1/Γ**) and GammaFacts/Mu with ψ error bounds, plus \"|Γ| growth in strips\" in the RvM argument. Inventorying."},{"type":"tool_use","id":"Bash_160","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean && ls Zeta23/GammaFacts/ && grep -rn \"theorem\\|lemma\" Zeta23/GammaFacts/Series.lean | grep -v \"^.*--\" | head -20","description":"Inventory GammaFacts module"},"extra_content":null}]