← Session 28 — ii′-5e: partial-fraction identity (zero series + F entire)
thinking (2028 chars)
`tsum_eq_single (a) (h : ∀ b ≠ a, f b = 0) : ∑' b, f b = f a` ✓ and `summable_of_hasFiniteSupport` ✓.
Now set up tasks and write the file. Let me create the todo list first, then write LiSeries.lean.
Actually one more check — `WeilEF.gammaOf_re`, `WeilEF.gammaOf_im` (used in LiSkeleton line 243). And `zeroMult` — takes ℂ: `zeroMult (ρ : ℂ) : ℕ` — with subtype coercion ✓.
Also for `IsNontrivialZero` — it's a plain def (And-structure), `ρ.2 : IsNontrivialZero ρ` unfolds via `.1`/`.2.1`/`.2.2` ✓ (as used).
Also `isOpen_ball` ✓ Mathlib. `Metric.mem_ball`, `mem_ball_self` ✓.
`TendstoUniformlyOn.tendstoLocallyUniformlyOn` ✓ used in LiDigamma.
`hasSumUniformlyOn_iff_tendstoUniformlyOn` ✓ used.
`TendstoLocallyUniformlyOn.differentiableOn` signature: in LiDigamma `htend.differentiableOn _ dpsiDomain_isOpen` where the `_` : `Filter.Eventually.of_forall`-produced ∀ᶠ t, DifferentiableOn. Let me double check the exact argument order: `apply htend.differentiableOn _ dpsiDomain_isOpen` then the remaining goal was the ∀ᶠ t ... hypothesis. So signature: (hd : ∀ᶠ n in l, DifferentiableOn ℂ (F n) s) (hs : IsOpen s) — applied with _ first then isOpen, leaving hd as goal. ✓ I'll mirror the LiDigamma code exactly.
One design question: seriesTerm uses `1 / (s - ρ) + 1 / ρ` with ρ : subtype coerced. Fine.
Now — where does `normSq (gammaOf ...)` lemmas live: `WeilEF.gammaOf_re : (gammaOf ρ).re = ρ.im`? From LiSkeleton: `rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]` giving `ρ.im ^ 2 + (1 / 2 - z.re) ^ 2` — so gammaOf_re : (gammaOf z).re = z.im and gammaOf_im : (gammaOf z).im = 1/2 − z.re (with normSq_apply: normSq z = z.re² + z.im²) ✓.
Imports for LiSeries.lean: Mathlib, Zeta23.Statement, Zeta23.WeilEF.ZeroSummability, Zeta23.Statement.SeamClosed, NguyenRH1.LiResidue (zetaA), NguyenRH1.LiSides (zeta_order_ne_top_of_ne). LiSides imports LiResidue presumably; importing LiSides alone might suffice, but explicit is better: import both.
Let me check LiSides' header imports to mirror conventions.
All names verified. Setting up the session tasks, then writing `LiSeries.lean`.
tool: TodoWrite
input
{
"todos": [
{
"content": "Write LiSeries.lean \u00a70\u2013\u00a72: seriesTerm/seriesFun defs, norm comparison, tail bound, seriesSummable",
"status": "in_progress",
"activeForm": "Writing LiSeries.lean core (defs + summability)"
},
{
"content": "\u00a73\u2013\u00a74: finite subtype balls, ball-avoidance at non-zero points, seriesFun analytic off the zeros",
"status": "pending",
"activeForm": "Proving analyticity off the zeros"
},
{
"content": "\u00a75: isolation at each zero + reduced-series analyticity + polar-part subtraction",
"status": "pending",
"activeForm": "Proving isolation + reduced series"
},
{
"content": "Iterate lake build to GREEN; root-import LiSeries",
"status": "pending",
"activeForm": "Building to GREEN"
},
{
"content": "Axiom audit session-028 (3 standard axioms only)",
"status": "pending",
"activeForm": "Running axiom audit"
},
{
"content": "Session-end protocol: journal-028, STATE.md, NGUYEN.md, db, commit",
"status": "pending",
"activeForm": "Closing session 028"
}
]
}
raw content_json (database row)
[{"type":"thinking","thinking":"`tsum_eq_single (a) (h : ∀ b ≠ a, f b = 0) : ∑' b, f b = f a` ✓ and `summable_of_hasFiniteSupport` ✓.\n\nNow set up tasks and write the file. Let me create the todo list first, then write LiSeries.lean.\n\nActually one more check — `WeilEF.gammaOf_re`, `WeilEF.gammaOf_im` (used in LiSkeleton line 243). And `zeroMult` — takes ℂ: `zeroMult (ρ : ℂ) : ℕ` — with subtype coercion ✓.\n\nAlso for `IsNontrivialZero` — it's a plain def (And-structure), `ρ.2 : IsNontrivialZero ρ` unfolds via `.1`/`.2.1`/`.2.2` ✓ (as used).\n\nAlso `isOpen_ball` ✓ Mathlib. `Metric.mem_ball`, `mem_ball_self` ✓.\n\n`TendstoUniformlyOn.tendstoLocallyUniformlyOn` ✓ used in LiDigamma.\n`hasSumUniformlyOn_iff_tendstoUniformlyOn` ✓ used.\n\n`TendstoLocallyUniformlyOn.differentiableOn` signature: in LiDigamma `htend.differentiableOn _ dpsiDomain_isOpen` where the `_` : `Filter.Eventually.of_forall`-produced ∀ᶠ t, DifferentiableOn. Let me double check the exact argument order: `apply htend.differentiableOn _ dpsiDomain_isOpen` then the remaining goal was the ∀ᶠ t ... hypothesis. So signature: (hd : ∀ᶠ n in l, DifferentiableOn ℂ (F n) s) (hs : IsOpen s) — applied with _ first then isOpen, leaving hd as goal. ✓ I'll mirror the LiDigamma code exactly.\n\nOne design question: seriesTerm uses `1 / (s - ρ) + 1 / ρ` with ρ : subtype coerced. Fine.\n\nNow — where does `normSq (gammaOf ...)` lemmas live: `WeilEF.gammaOf_re : (gammaOf ρ).re = ρ.im`? From LiSkeleton: `rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]` giving `ρ.im ^ 2 + (1 / 2 - z.re) ^ 2` — so gammaOf_re : (gammaOf z).re = z.im and gammaOf_im : (gammaOf z).im = 1/2 − z.re (with normSq_apply: normSq z = z.re² + z.im²) ✓.\n\nImports for LiSeries.lean: Mathlib, Zeta23.Statement, Zeta23.WeilEF.ZeroSummability, Zeta23.Statement.SeamClosed, NguyenRH1.LiResidue (zetaA), NguyenRH1.LiSides (zeta_order_ne_top_of_ne). LiSides imports LiResidue presumably; importing LiSides alone might suffice, but explicit is better: import both.\n\nLet me check LiSides' header imports to mirror conventions.","signature":""},{"type":"text","text":"All names verified. Setting up the session tasks, then writing `LiSeries.lean`."},{"type":"tool_use","id":"TodoWrite_33","name":"TodoWrite","input":{"todos":[{"content":"Write LiSeries.lean §0–§2: seriesTerm/seriesFun defs, norm comparison, tail bound, seriesSummable","status":"in_progress","activeForm":"Writing LiSeries.lean core (defs + summability)"},{"content":"§3–§4: finite subtype balls, ball-avoidance at non-zero points, seriesFun analytic off the zeros","status":"pending","activeForm":"Proving analyticity off the zeros"},{"content":"§5: isolation at each zero + reduced-series analyticity + polar-part subtraction","status":"pending","activeForm":"Proving isolation + reduced series"},{"content":"Iterate lake build to GREEN; root-import LiSeries","status":"pending","activeForm":"Building to GREEN"},{"content":"Axiom audit session-028 (3 standard axioms only)","status":"pending","activeForm":"Running axiom audit"},{"content":"Session-end protocol: journal-028, STATE.md, NGUYEN.md, db, commit","status":"pending","activeForm":"Closing session 028"}]},"extra_content":null}]