← Session 24 — ii′-2…4: swaps, (4.10) design, contour + website roadmap fixes
thinking (2223 chars)
`LSeries_zeta_mul_Lseries_moebius (hs : 1 < s.re) : L ↗ζ s * L ↗μ s = 1` (Dirichlet.lean:293) — the L-series product. So 1/ζ(s) = L μ s = Σ μ(n)/n^s for re s > 1 (via L ↗ζ s = riemannZeta s — `LSeries_riemannZeta_eq`? the ζ L-series = riemannZeta for re > 1: `LSeries_zeta_eq_riemannZeta`? there's `LSeries_zeta_eq_riemannZeta`? whatever — exists). So |1/ζ(2+it)| = |Σ μ(n)/n^{2+it}| ≤ Σ |μ(n)|/n² ≤ Σ 1/n² = ζ(2) ⟹ |ζ(2+it)| ≥ 1/ζ(2) ✓.
LSeries μ s = tsum (fun n => μ n / n^s) — the bound: ‖Σ μ(n)/n^s‖ ≤ Σ ‖μ(n)/n^s‖ ≤ Σ 1/n^{re s} = ζ(re s) — via tsum norm bounds + the LSeriesSummable. And ζ(2) = π²/6 — need an upper bound on ζ(2): ζ(2) ≤ 2 (elementary: Σ1/n² ≤ 1 + ∫₁^∞ dx/x² = 2 ✓ or ζ(2) = π²/6 < 5/3). So |ζ(2+it)| ≥ 1/ζ(2) ≥ 1/2. The L-series evaluation Σ 1/n² = ζ(2) = π²/6 in Mathlib: `hasSum_zeta_two`? or `riemannZeta_two`: `riemannZeta_two : riemannZeta 2 = π²/6`? I believe Mathlib has that... maybe not actually — the Basel value might not be in Mathlib. Elementary bound Σ1/n² ≤ 2: via the telescoping 1/n² ≤ 1/(n(n−1)): Mathlib: `hasSum_one_div_nat_pow`? For the upper bound Σ_{n≥1} 1/n² ≤ 2: could use the IntegralComparison or the known ζ(2) value. I'll handle at build; there might be `summable_one_div_nat_pow` + comparison.
OK — now let me draft the 5c file content. Structure (appending to LiRBound.lean — hmm, it's already 640 lines; maybe a new file LiDisc.lean? D-064's module map says LiContour/LiResidue/LiCrux/LiRBound — I'll put the disc argument in LiRBound.lean §6+ since it's the R-bound's home. Actually the file is getting big; make a new file `LiDisc.lean` for the disc argument. It imports LiRBound + LiContour.)
Section plan for LiDisc.lean (ii′-5c):
§1. The zero collection: for s₀ = 2+it (|t| ≥ 10): Zc := {ρ ∈ closedBall s₀ (5/2) | riemannZeta ρ = 0} finite.
- finiteness: the closed ball is compact; zeros of ζ in it — `IsCompact.inter_riemannZetaZeros_finite`? hmm — what did ii′-1a actually use? Let me check LiSkeleton.lean for that lemma's usage/name. Actually from the NGUYEN.md ii′-1a note: "finite ball via IsCompact.inter_riemannZetaZeros_finite" — let me grep the vendored Zeta23/Mathlib for it.
Let me grep for that finiteness lemma first — it's the foundation.
The center lower bound route is confirmed (`LSeries_zeta_mul_Lseries_moebius`). Now the zero-collection finiteness — checking the exact lemma ii′-1a used.
tool: Bash
input
{
"command": "cd D:/Python/Quantum && grep -rn \"inter_riemannZetaZeros_finite\\|ZetaZeros_finite\\|zeros_finite\" research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean zeta-23-lean/Zeta23/ --include=*.lean -r | head -8",
"description": "Find the zero-finiteness lemma used in ii\u2032-1a"
}
raw content_json (database row)
[{"type":"thinking","thinking":"`LSeries_zeta_mul_Lseries_moebius (hs : 1 < s.re) : L ↗ζ s * L ↗μ s = 1` (Dirichlet.lean:293) — the L-series product. So 1/ζ(s) = L μ s = Σ μ(n)/n^s for re s > 1 (via L ↗ζ s = riemannZeta s — `LSeries_riemannZeta_eq`? the ζ L-series = riemannZeta for re > 1: `LSeries_zeta_eq_riemannZeta`? there's `LSeries_zeta_eq_riemannZeta`? whatever — exists). So |1/ζ(2+it)| = |Σ μ(n)/n^{2+it}| ≤ Σ |μ(n)|/n² ≤ Σ 1/n² = ζ(2) ⟹ |ζ(2+it)| ≥ 1/ζ(2) ✓.\n\nLSeries μ s = tsum (fun n => μ n / n^s) — the bound: ‖Σ μ(n)/n^s‖ ≤ Σ ‖μ(n)/n^s‖ ≤ Σ 1/n^{re s} = ζ(re s) — via tsum norm bounds + the LSeriesSummable. And ζ(2) = π²/6 — need an upper bound on ζ(2): ζ(2) ≤ 2 (elementary: Σ1/n² ≤ 1 + ∫₁^∞ dx/x² = 2 ✓ or ζ(2) = π²/6 < 5/3). So |ζ(2+it)| ≥ 1/ζ(2) ≥ 1/2. The L-series evaluation Σ 1/n² = ζ(2) = π²/6 in Mathlib: `hasSum_zeta_two`? or `riemannZeta_two`: `riemannZeta_two : riemannZeta 2 = π²/6`? I believe Mathlib has that... maybe not actually — the Basel value might not be in Mathlib. Elementary bound Σ1/n² ≤ 2: via the telescoping 1/n² ≤ 1/(n(n−1)): Mathlib: `hasSum_one_div_nat_pow`? For the upper bound Σ_{n≥1} 1/n² ≤ 2: could use the IntegralComparison or the known ζ(2) value. I'll handle at build; there might be `summable_one_div_nat_pow` + comparison.\n\nOK — now let me draft the 5c file content. Structure (appending to LiRBound.lean — hmm, it's already 640 lines; maybe a new file LiDisc.lean? D-064's module map says LiContour/LiResidue/LiCrux/LiRBound — I'll put the disc argument in LiRBound.lean §6+ since it's the R-bound's home. Actually the file is getting big; make a new file `LiDisc.lean` for the disc argument. It imports LiRBound + LiContour.)\n\nSection plan for LiDisc.lean (ii′-5c):\n\n§1. The zero collection: for s₀ = 2+it (|t| ≥ 10): Zc := {ρ ∈ closedBall s₀ (5/2) | riemannZeta ρ = 0} finite.\n - finiteness: the closed ball is compact; zeros of ζ in it — `IsCompact.inter_riemannZetaZeros_finite`? hmm — what did ii′-1a actually use? Let me check LiSkeleton.lean for that lemma's usage/name. Actually from the NGUYEN.md ii′-1a note: \"finite ball via IsCompact.inter_riemannZetaZeros_finite\" — let me grep the vendored Zeta23/Mathlib for it.\n\nLet me grep for that finiteness lemma first — it's the foundation.","signature":""},{"type":"text","text":"The center lower bound route is confirmed (`LSeries_zeta_mul_Lseries_moebius`). Now the zero-collection finiteness — checking the exact lemma ii′-1a used."},{"type":"tool_use","id":"Bash_335","name":"Bash","input":{"command":"cd D:/Python/Quantum && grep -rn \"inter_riemannZetaZeros_finite\\|ZetaZeros_finite\\|zeros_finite\" research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean zeta-23-lean/Zeta23/ --include=*.lean -r | head -8","description":"Find the zero-finiteness lemma used in ii′-1a"},"extra_content":null}]