← Session 28 — ii′-5e: partial-fraction identity (zero series + F entire)
thinking (2681 chars)
`Complex.Gamma_ne_zero {s : ℂ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0` ✓ (Beta.lean). So:
`analyticAt_digamma (hw : ∀ m : ℕ, w ≠ -m) : AnalyticAt ℂ digamma w` — build: on a ball around w avoiding {0}∪−ℕ (discrete set), every point differentiable: digamma y = deriv Gamma y / Gamma y = logDeriv Gamma y ✓ (digamma_def + logDeriv_apply): DifferentiableAt (deriv Gamma / Gamma) at y from differentiableAt_Gamma + .deriv + .div (Gamma_ne_zero) ✓ ⟹ DifferentiableOn ball ⟹ analyticOnNhd ⟹ AnalyticAt. I'll write this small helper lemma `analyticAt_digamma` in LiFEntire.
Wait — check LiDigamma line 472 area: they already did something like this: `(Complex.Gamma_ne_zero (hpole s hs))` and `digamma_analyticOn : AnalyticOnNhd ℂ Complex.digamma dpsiDomain` — dpsiDomain = Metric.ball (1/2) (1/2)?? If dpsiDomain is just that ball, not general. Let me look at what `digamma_analyticOn` covers and the general pattern they used — line 454-463 area from my earlier read: `apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen; have hGammaAn : AnalyticOnNhd ℂ Complex.Gamma dpsiDomain := by apply DifferentiableOn.analyticOnNhd...`. dpsiDomain — from LiDigamma line ~386: `dpsiDomain`, `dpsiDomain_re_pos`, `dpsiDomain_isOpen` — looks like dpsiDomain = {s | 0 < s.re}? (re_pos lemma + ‖s‖ ≤ 1 ball bound in the M-test... hmm line 387: hs : s ∈ dpsiDomain gives ‖s‖ ≤ 1?? and re > 0: dpsiDomain = ball (1/2) (1/2)? wait line 388-397: `dpsiDomain, Metric.mem_ball, dist_eq_norm` with ‖1/2‖ = 1/2: so dpsiDomain = Metric.ball (1/2 : ℂ) (1/2)?? and ‖s‖ ≤ 1 from that ✓. Hmm no wait — dpsiDomain_re_pos : s ∈ dpsiDomain → 0 < s.re; ball(1/2, 1/2) gives re ∈ (0,1) ✓ consistent. OK so their analyticity was local to that ball; I need the general point version — easy variant with a custom ball around w avoiding {0}∪−ℕ.
Ball around w avoiding −ℕ∪{0}: the set {0}∪{−1,−2,...} is closed+discrete (as a subset of ℂ — it's (−ℕ∪{0}) embedded — closed since discrete... in ℂ: the set {−n : n : ℕ} has no finite accumulation ✓ closed). w ∉ it ⟹ positive distance? closed + w ∉ ⟹ ∃ ball avoiding ✓ (isClosed_compl... `IsClosed.mem_nhds`? a closed set's complement is open ⟹ w ∈ open complement ⟹ ball ⊆ ✓). Is it worth proving closedness of {−n}? Alternatively constructive: δ := min over the finitely many −n with |−n − w| ≤ ‖w‖+1... Simpler constructive: dist to the two nearest integers: let m := ⌈‖w‖⌉₊; the candidates −n with ‖w−(−n)‖ ≤ ‖w‖ + 1... finite. δ := min(1, min over n ≤ m+1 of |w+n|)/2. Each |w+n| > 0 by hw ✓. Constructive finite-min, mirrors nontrivialZero_isolated ✓.
Fine. Now the classification lemma pieces. Let me read LiDisc's zeroDisc_isNontrivial to see the re ≤ 0 argument.
Now let me study the LiDisc zero-classification argument (re ≤ 0 via ΓR-pole/FE) and the Zeta23 digamma series statement.
tool: Read ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
"offset": 36,
"limit": 75
}
result 2026-08-23 14:57:03Z → 2026-08-27 02:51:31Z
{
"type": "text",
"file": {
"filePath": "D:\\Python\\Quantum\\research\\paper\\paperA.tex",
"content": "($\\mathrm{margin}(8{\\cdot}10^4) > 0$ and\n$\\mathrm{margin}(10^5) > \\mathrm{margin}(8{\\cdot}10^4)$) are discharged\nin the development itself, by certified rational interval bounds on\n$\\log$, $\\exp$, and $\\sqrt{\\cdot}$ (\\texttt{LiBasePoints.lean}). The\nmargin majorant in the development is a mildly enlarged Trudgian-shape\nfunction (a negative-weight term dropped, at a cost of $\\approx\n0.9\\sqrt n$ in the bound) chosen so that every convexity block has\nprovably negative $\\psi$; the axiom profile is unchanged --- the three\nstandard axioms, no \\texttt{sorryAx}, audited declaration-by-declaration\non the full chain.\n\nThe finite-height Li theorem remains, by design, \\emph{conditional} on",
"numLines": 12,
"startLine": 580,
"totalLines": 632
}
}
raw content_json (database row)
[{"type":"thinking","thinking":"`Complex.Gamma_ne_zero {s : ℂ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0` ✓ (Beta.lean). So:\n\n`analyticAt_digamma (hw : ∀ m : ℕ, w ≠ -m) : AnalyticAt ℂ digamma w` — build: on a ball around w avoiding {0}∪−ℕ (discrete set), every point differentiable: digamma y = deriv Gamma y / Gamma y = logDeriv Gamma y ✓ (digamma_def + logDeriv_apply): DifferentiableAt (deriv Gamma / Gamma) at y from differentiableAt_Gamma + .deriv + .div (Gamma_ne_zero) ✓ ⟹ DifferentiableOn ball ⟹ analyticOnNhd ⟹ AnalyticAt. I'll write this small helper lemma `analyticAt_digamma` in LiFEntire.\n\nWait — check LiDigamma line 472 area: they already did something like this: `(Complex.Gamma_ne_zero (hpole s hs))` and `digamma_analyticOn : AnalyticOnNhd ℂ Complex.digamma dpsiDomain` — dpsiDomain = Metric.ball (1/2) (1/2)?? If dpsiDomain is just that ball, not general. Let me look at what `digamma_analyticOn` covers and the general pattern they used — line 454-463 area from my earlier read: `apply DifferentiableOn.analyticOnNhd _ dpsiDomain_isOpen; have hGammaAn : AnalyticOnNhd ℂ Complex.Gamma dpsiDomain := by apply DifferentiableOn.analyticOnNhd...`. dpsiDomain — from LiDigamma line ~386: `dpsiDomain`, `dpsiDomain_re_pos`, `dpsiDomain_isOpen` — looks like dpsiDomain = {s | 0 < s.re}? (re_pos lemma + ‖s‖ ≤ 1 ball bound in the M-test... hmm line 387: hs : s ∈ dpsiDomain gives ‖s‖ ≤ 1?? and re > 0: dpsiDomain = ball (1/2) (1/2)? wait line 388-397: `dpsiDomain, Metric.mem_ball, dist_eq_norm` with ‖1/2‖ = 1/2: so dpsiDomain = Metric.ball (1/2 : ℂ) (1/2)?? and ‖s‖ ≤ 1 from that ✓. Hmm no wait — dpsiDomain_re_pos : s ∈ dpsiDomain → 0 < s.re; ball(1/2, 1/2) gives re ∈ (0,1) ✓ consistent. OK so their analyticity was local to that ball; I need the general point version — easy variant with a custom ball around w avoiding {0}∪−ℕ.\n\nBall around w avoiding −ℕ∪{0}: the set {0}∪{−1,−2,...} is closed+discrete (as a subset of ℂ — it's (−ℕ∪{0}) embedded — closed since discrete... in ℂ: the set {−n : n : ℕ} has no finite accumulation ✓ closed). w ∉ it ⟹ positive distance? closed + w ∉ ⟹ ∃ ball avoiding ✓ (isClosed_compl... `IsClosed.mem_nhds`? a closed set's complement is open ⟹ w ∈ open complement ⟹ ball ⊆ ✓). Is it worth proving closedness of {−n}? Alternatively constructive: δ := min over the finitely many −n with |−n − w| ≤ ‖w‖+1... Simpler constructive: dist to the two nearest integers: let m := ⌈‖w‖⌉₊; the candidates −n with ‖w−(−n)‖ ≤ ‖w‖ + 1... finite. δ := min(1, min over n ≤ m+1 of |w+n|)/2. Each |w+n| > 0 by hw ✓. Constructive finite-min, mirrors nontrivialZero_isolated ✓.\n\nFine. Now the classification lemma pieces. Let me read LiDisc's zeroDisc_isNontrivial to see the re ≤ 0 argument.","signature":""},{"type":"text","text":"Now let me study the LiDisc zero-classification argument (re ≤ 0 via ΓR-pole/FE) and the Zeta23 digamma series statement."},{"type":"tool_use","id":"Read_104","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean","offset":36,"limit":75},"extra_content":null}]