[{"type":"thinking","thinking":"Audit clean: all 22 declarations — 3 standard axioms only, no sorryAx.\n\nii′-5e-iii COMPLETE. Now the session-end protocol:\n1. journal/session-028.md\n2. Update derivations index? (No new derivation file — this was a build sub-stage; D-068 already covers the design. The journal documents it.)\n3. NGUYEN.md §5 checklist update (ii′-5e line: mark 5e-iii complete).\n4. STATE.md update (NEXT ACTION: 5e-iv).\n5. db registration — session 028 via direct sqlite3 insert (journal_file column).\n6. git commit.\n\nLet me write the journal first. Include banked gotchas from this session:\n- `rw [heq]` on a redex RHS then `show` to beta-reduce before rewriting `smul_eq_mul` (the • is hidden under the unreduced lambda application).\n- `rw [not_lt] at h` fails when h is `ρ ∉ {x | p x}` (setOf-membership folded); insert `show p-form` or use the defeq coercion first.\n- `Finset.image (fun ρ => ...)`: pin the bound variable's TYPE explicitly when the body has a coercion (`fun ρ : {ρ // P ρ} => ...`) — else the elaborator picks the coerced type and the Finset argument mismatches.\n- Never `rw [hd]` (a `set` equation) at a hypothesis whose type depends on the set-variable (e.g. Finset.min'_mem d hdne — hdne : d.Nonempty makes the motive ill-typed). Route: prove a standalone membership iff (rw [hd] in the GOAL only, no dependent hypotheses) and use .mp/.mpr.\n- `obtain ⟨..., rfl⟩` fails when the equation's other side is not a local variable (e.g. ‖…‖ = d.min' hdne) — use a named heq + rw [← heq].\n- rw [if_pos]/rw [if_neg] cannot rewrite under a binder (inside fun s => if ...) — use simp only [if_pos h].\n- `Set.mem_setOf_eq` deprecated → membership in setOf is defeq; use defeq ascriptions/show instead.\n- push_neg deprecated in this Mathlib → rw [not_le] etc.\n- File ending convention: `end NguyenRH1` THEN `end` (section outside namespace).\n- rw [h]; rfl needed when the residual equality is defeq-only (tsum vs seriesFunSub def-unfolding) — rw's auto-rfl doesn't unfold plain defs.\n- AnalyticOnNhd f s = ∀ x ∈ s, AnalyticAt f x (pointwise def) — apply directly.\n- simp only [Finset.mem_image, Set.Finite.mem_toFinset] can close the iff goal entirely (rfl-closure) — adding constructor bullets then errors \"no goals\".\n\nAlso mark NGUYEN.md 5e progress. The NGUYEN.md §5 ii′-5e entry currently says: \"**5e-ii COMPLETE (session 027)**: ... Remaining: 5e-iii (series) → 5e-iv (F entire) → 5e-v (capstone ∃ B).\" Need to update: add 5e-iii COMPLETE line.\n\nLet me also update STATE.md fully.\n\nJournal file: research/journal/session-028.md.","signature":""},{"type":"text","text":"Audit clean — 22 decls, 3 standard axioms only. Writing the session artifacts now."},{"type":"tool_use","id":"Write_79","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\journal\\session-028.md","content":"# Session 028 — 2026-08-23 — ii′-5e-iii COMPLETE: the zero series (LiSeries.lean)\n\n## Directive\nContinue tier ii′-5 per STATE.md: ii′-5e-iii (D-068 §3) — the zero-side\npartial-fraction series: summability, analyticity off the zeros,\nisolation at each zero. User: \"let continue with the next stage.\"\n\n## Outcome: 5e-iii COMPLETE (LiSeries.lean, ~600 lines, 22 decls, all\naudited clean: 3 standard axioms only; full build GREEN 8765 jobs,\nLiSeries root-imported)\n\n**§0–2 (summability)**: `seriesTerm s ρ := (zeroMult ρ : ℂ)·(1/(s−ρ) + 1/ρ)`\nover the nontrivial-zero subtype; `seriesFun s := ∑' ρ, seriesTerm s ρ`.\nThe tail algebra `one_div_sub_add_one_div` (1/(s−ρ)+1/ρ = s/(ρ(s−ρ)))\ngives ‖term‖ ≤ 2‖s‖/‖ρ‖² for 2 ≤ ‖ρ‖, 2‖s‖ ≤ ‖ρ‖; the comparison\n`one_add_normSq_gammaOf_le` (1 + ‖γ_ρ‖² ≤ (17/12)‖ρ‖² for ‖ρ‖ ≥ 2:\n‖γ‖² = im² + (1/2−re)² ≤ im² + 1/4 and im² ≥ 3) converts to the ii′-1a\ndominator (17/6)(‖s‖+1)·mult/(1+‖γ‖²), summable by Zeta23\n`WeilEF.zero_sum_inv_sq zetaSeam`; the head is finite\n(`finite_subtype_norm_lt`, the liSummable compact-finiteness pattern).\n`seriesSummable : ∀ s, Summable (seriesTerm s)` — UNCONDITIONAL (the\njunk value at s = ρ is harmless), cloned from the liSummable D-trick.\n\n**§3–4 (analyticity off the zeros)**: `exists_ball_avoid_nontrivialZeros`\n— around any s₀ with ¬IsNontrivialZero s₀ a ball avoiding the nontrivial\nzeros, by the three-case split: ζ s₀ ≠ 0 → continuity ball\n(analyticAt_riemannZeta.continuousAt.eventually_ne); ζ s₀ = 0, s₀ ≠ 1 →\nthe order normal form (analyticOrderAt_ne_top.mp of\nzeta_order_ne_top_of_ne: ζ = (z−s₀)^m·h, h ≠ 0 nearby ⟹ the only\npossible zero in the ball is s₀ itself, excluded by hypothesis); s₀ = 1\n→ the zetaA factorization (zetaA_ne_zero_near_one + zetaA_apply:\nζ = zetaA/(w−1) ≠ 0 off 1 in a ball; ρ ≠ 1 since re ρ < 1).\nThen `seriesFun_analyticAt`/`seriesFun_analyticOnNhd`: the Weierstrass\nM-test `HasSumUniformlyOn.of_norm_le_summable_eventually` on the\navoiding ball (cofinite = complement of the finite head via\n`eventually_cofinite`; the (17/6)M·mult/(1+‖γ‖²) majorant) →\nTendstoLocallyUniformlyOn.differentiableOn (finite partial sums\ndifferentiable termwise) → .analyticOnNhd Metric.isOpen_ball → apply at\nthe center — the journal-020/021-banked pattern verbatim.\n\n**§5 (isolation + the reduced series)**: `nontrivialZero_isolated` —\n∃ δ > 0, all OTHER nontrivial zeros at distance ≥ δ (the finite\nunit-ball subtype finset, the min-distance halved; empty case δ = 1/2).\n`seriesTermSub ρ₀` (the ρ₀-term zeroed) / `seriesFunSub ρ₀`: summable\neverywhere (norm ≤ ‖seriesTerm‖), analytic AT ρ₀\n(`seriesFunSub_analyticAt` — the same M-test on the isolation half-ball;\nthe zeroed term is the constant 0, the others are pole-free by the\nisolation). Pointwise split `seriesFun_eq_sub_add` (tsum_congr +\nSummable.tsum_add + tsum_eq_single) ⟹ `seriesFun_sub_term`:\nseriesFun s − seriesTerm s ρ₀ = seriesFunSub ρ₀ s EVERYWHERE. Capstones:\n`seriesFun_sub_self_term_analyticAt` (AnalyticAt.congr) and\n`seriesFun_sub_polar_analyticAt` — s ↦ seriesFun s − mult(ρ₀)/(s−ρ₀)\nanalytic at ρ₀ (the +mult/ρ₀ part is a constant) — exactly the\nresidue-cancellation input 5e-iv needs at the nontrivial zeros.\n\n## Banked gotchas (session 028 additions)\n- **`rw [heq]` leaves a beta-redex RHS**: after rewriting with an\n  EventuallyEq-style fact `(fun z => ... • h z) ↑ρ`, the `•` is hidden\n  under the unreduced application — `rw [smul_eq_mul]` fails. Fix:\n  `show (↑ρ − s₀)^m * h ↑ρ ≠ 0` (defeq via beta + smul=mul on ℂ).\n- **`rw [not_lt] at h` fails on `ρ ∉ {x | p x}`** (setOf-membership is\n  folded): insert `show p ρ`-form for the goal or restructure; the\n  membership itself IS defeq to the predicate, so `apply hρ` on\n  hρ : ρ ∈ {x | ¬ P x} turns the goal into P directly.\n- **Finset.image lambdas need the bound var's TYPE pinned** when the\n  body coerces: `fun ρ : {ρ // P ρ} => ‖(ρ:ℂ) − ρ₀‖` — otherwise the\n  elaborator types the lambda at ℂ (identity coe) and the Finset\n  argument mismatches.\n- **NEVER `rw [hd]` at a hypothesis whose type depends on the set-var**\n  (e.g. `Finset.min'_mem d hdne` — hdne : d.Nonempty makes the motive\n  ill-typed). Route: a standalone membership iff hdm (rw [hd] in the\n  GOAL only — no dependent hypotheses there) + .mp/.mpr everywhere.\n- **`obtain ⟨..., rfl⟩` fails when the equation's other side is not a\n  local variable** (e.g. ‖…‖ = d.min' hdne): name it (heq) and\n  rw [← heq].\n- **`rw [if_pos h]`/`if_neg` cannot rewrite under a binder** (inside\n  fun s => if ...): use `simp only [if_pos h]` (simp goes under).\n- `Set.mem_setOf_eq` is DEPRECATED (→ Set.mem_ofPred_eq); setOf\n  membership is defeq anyway — prefer defeq ascriptions.\n- `push_neg` is DEPRECATED in this Mathlib: use `rw [not_le]` etc.\n- File-ending convention: `end NguyenRH1` THEN `end` (the noncomputable\n  section wraps the namespace).\n- `rw [hsingle]`-then-goal-open when the residual equality is\n  defeq-only (tsum vs the seriesFunSub def): close with an explicit\n  `rfl` (rw's auto-rfl won't unfold plain defs).\n- AnalyticOnNhd f s is literally ∀ x ∈ s, AnalyticAt f x — apply the\n  AnalyticOnNhd hypothesis at the center with Metric.mem_ball_self.\n- `simp only [Finset.mem_image, Set.Finite.mem_toFinset]` can close an\n  iff goal entirely (rfl-closure) — a following constructor bullet then\n  errors \"no goals\"; drop it.\n- `Summable.of_norm_bounded` needs a REAL-valued dominator: for\n  ℂ-valued f use `(hf).norm` (Summable.norm) as the comparison input.\n\n## Status / next\nii′-5e-iii COMPLETE. Next: **ii′-5e-iv** (D-068 §4): F entire by\nprincipal-part splits — at nontrivial zeros via ii′-1b's logDeriv-NF +\n`seriesFun_sub_polar_analyticAt` (this session) + the elementary terms\nanalytic there (re ρ ∈ (0,1) avoids 0, 1, −2n); at s = 1 via ii′-1b's\nzetaA logDeriv (logDeriv zetaA analytic at 1, zetaA 1 = 1); at s = 0 via\nthe digamma-series split (−½ψ(s/2) = 1/s − ½h₀(s), h₀ analytic — the\nWeierstrass machinery of this session applies to the digamma series\nterms, |term| ≤ C/(n+1)² on ‖w‖ ≤ 1/2); at s = −2n via ii′-1b NF +\n`zeroMult_neg_two_mul` (session 026) + the ψ-pole split (the j = n−1\nterm). Then 5e-v (the circle bound O((log R)³) + max-modulus squeeze ⟹\nF ≡ const; capstone ∃ B identity) → ii′-5f → ii′-3b → ii′-3c → ii′-6 →\nii′-7.\n"},"extra_content":null}]