Session 030 — 2026-08-23 — ii′-5e-v IN PROGRESS: count bridges + Dirichlet bound + split machinery (5e-v-a + 5e-v-b chunk 1)

Directive

Continue the route per STATE.md: ii′-5e-v (D-068 §5) — the circle bound

• the squeeze ⟹ the ∃ B capstone. User: "Let's work on ii'-5e-v."

Outcome (commits 5d24756, e6a654b; LiCircleBound.lean, ~340 lines so

far, clean elaboration, not yet root-imported)

5e-v-a COMPLETE (§0–§2):

• isNontrivialZero_conj (the conjugate of a nontrivial zero is nontrivial — for the lower-half circle arcs; via Mathlib's unconditional _root_.riemannZeta_conj).
• A0count + Ncount_window_le: Zeta23's RvM local count (Zeta23.RvM.zeta_local_zero_count: Ncount(t, t+1] ≤ A₀·log(|t|+3), zeros WITH multiplicity, two-sided, ALL t — proved unconditionally in Zeta23; A₀ existential ⟹ carried symbolically via Classical.choose).
• Ncount_add_of_le (window additivity, disjoint finsum union) + Ncount_chain_le (N-step chain) + Ncount_le_of_interval + Ncount_le_of_interval_gen (dyadic interval count Ncount(a, b] ≤ A₀·(b−a+1)·log(3·max|a||b|+5), both signs).
• norm_logDeriv_zeta_le_dirichlet: ‖ζ′/ζ s‖ ≤ dirichletC2 for re s ≥ 2 (−ζ′/ζ = LSeries Λ for re > 1 via Mathlib's LSeries_vonMangoldt_eq_deriv_riemannZeta_div; termwise ≤ the s = 2 majorant via LSeries.norm_term_le_of_re_le_re; the ZetaBounds.lean pattern mirrored).

5e-v-b chunk 1 (§3 helpers):

• tsum_split_finset: a summable real tsum = a finset sum + the if-zeroed complement tsum (via tsum_eq_sum + Summable.tsum_add + Summable.of_norm_bounded on the if-forms). [DecidableEq ι] argument; the zero subtype discharges it via the (noncomputable) ℂ instance.
• lowZeros / lowZeroConst: the small-zero symbolic finite constant (‖ρ‖ ≤ 3; each ‖ρ‖ > 0 since re > 0).

Design state for the remainder (all API verified this session)

Target: ‖Fexpr s‖ ≤ C·(log R)³-ish on the 5e-i γ-gap circles (|s| = R_k, k ≥ 4000 so 13/R ≤ 1/(32·Ĉ₀(4k+9/2)) — the numerics: Ĉ₀(16006) ≤ 9.36 via log(16008) ≤ 10 ⟸ 16008 ≤ e^10 ⟸ 2.718281828^10 ≥ 22026 (norm_num chain) and log 10 ≤ 2.4 ⟸ e^{0.4} ≥ 1.4 = 1+0.4 (Real.add_one_le_exp) ⟹ slack 4×).

• seriesFun circle bound (the remaining analytic heart): ONE tsum split (tsum_split_finset) at the finset {‖ρ‖ ≤ 2R}; the finite part splits by Finset.filter into: low (‖ρ‖ ≤ 3: ≤ lowZeroConst), inner (3 < ‖ρ‖ ≤ R−2: term ≤ 2/‖ρ‖ dyadic in ‖ρ‖, and the R/2..R−2 band: term ≤ 2/(R−‖ρ‖) dyadic in R−‖ρ‖; counts via Ncount_le_of_interval_gen with |γ| ≥ ‖ρ‖−1 [via Complex.norm_le_abs_re_add_abs_im]), critical (R−2 < ‖ρ‖ < R+2: the γ-gap — strip arcs |t−γ| ≥ 1/(32Ĉ₀); near-axis arcs ‖s−ρ‖ ≥ √(R²−100)−1 ≥ R/2 — NO gap needed there), upper band (R+2 ≤ ‖ρ‖ ≤ 2R: term ≤ 1/(‖ρ‖−R) dyadic). The tail (‖ρ‖ > 2R): term ≤ (17R/6)·m/(1+γ²) (5e-iii's (17/12) comparison) ⟹ ≤ (17R/6)·(tail of Σ m/(1+γ²) over |γ| > 2R−1).
• the tail bound (the last new analytic input): Σ_{|γ|>X} m/(1+γ²) ≤ 16·A₀·log X/X for X ≥ 4·10³-ish — via the ℤ-window fiberwise decomposition (ENNReal.tsum_fiberwise is FREE in ℝ≥0∞ — verified exists) with Zeta23's key machinery (key_lt, le_key_add_one, one_add_sq_ge: 1+γ² ≥ (1+n²)/4 — all in Zeta23/Tail.lean + WeilEF/ZeroSummability.lean) + the window counts + the weight-series tail (weight(n) = log(|n|+3)/(1+n²) ≤ 2√2·|n|^{-3/2} via log y ≤ 2(√y−1) ⟸ Real.log_le_sub_one_of_pos at √y; p-series tail Σ_{n≥N} n^{-3/2} ≤ 3/√N — the p-series tail-bound API to pin down at build time).
• logDeriv ζ on the circle: strip arcs (re ∈ [−5/2, 7/2], |t| ≥ 10 for R ≥ 11): 5c/5d capstones (100000/200000·(log|t|)²) + the near sum ≤ 32Ĉ₀·(2·A₀·log(|t|+4)) [nearZeros ⊆ two Ncount windows] = O((log R)²); right near-axis (re ≥ √(R²−100) ≥ 2): the Dirichlet bound (5e-v-a ✔); left near-axis (re ≤ −√(R²−100)): 5d's logDeriv_zeta_fe pointwise + Dirichlet at 1−s + the ΓR brackets via 5e-ii (A)/(B) + the pointwise logDeriv ΓR identity (5e-ii's (G) for im ≠ 0; the REAL point s = −R via the closure/continuity extension — the bound set is closed and the im ≠ 0 arc points are dense).
• elems: 1/s, 1/(s−1) = O(1/R); ψ(s/2)/2 = O(log R): right arc via 5e-ii (B) (re ≥ 2, |im| ≤ 5); strip arcs via 5d's norm_digamma_sub_log_le_of_two_le_abs_im (|im| ≥ 5 there) + ‖log w‖ ≤ log‖w‖ + π (LiReflect:414); left arc via 5e-ii (A) with dist(s/2, −ℕ) ≥ 1/8 (from dist(R/2, ℤ) ≥ 1/4 and |re s/2| ∈ [√(R²−100)/2, R/2] ⊆ [R/2 − 26/R, R/2], R ≥ 208).
• the squeeze: G(z) := Gentire entire; for fixed z₀, R_k > |z₀|: dist(Gentire z₀, Gentire 0) ≤ (R₂(R_k)/R_k)·|z₀| with R₂(R) = C·(log R)³ + ‖Gentire 0‖ — Mathlib's Schwarz Complex.dist_le_div_mul_dist_of_mapsTo_ball (DifferentiableOn on the ball + MapsTo into closedBall (Gentire 0) R₂ — the mapsTo from the sphere bound via Zeta23's AnalyticOn.norm_le_of_norm_le_on_sphere) ⟹ dist ≤ 0 (the ratio → 0: (log R)³/R ≤ 64·R^{3/4}/R via Real.log_le_rpow-ish) ⟹ Gentire ≡ Gentire 0 =: B. Capstone (D-068 §5): partialFraction_identity (hZC : ZeroCountProp) : ∃ B : ℂ, ∀ s, riemannZeta s ≠ 0 → s ≠ 0 → s ≠ 1 → (∀ n ≥ 1, s ≠ −2n) → logDeriv riemannZeta s = B + seriesFun s − 1/s − 1/(s−1) + (Real.log Real.pi)/2 − Complex.digamma (s/2)/2 — from Gentire s = Fexpr s (5e-iv's gentire_eq_Fexpr at good points) + Gentire ≡ B.

Banked gotchas (session 030 additions)

• le_or_lt does NOT exist (banked session 026) — use le_or_gt.
• finsum API: finsum_mem_union (hst : Disjoint) (hs : s.Finite) (ht : t.Finite) (to_additive of finprod_mem_union — plain grep for "finsum_mem_union" misses it), finsum_mem_empty, and tsum_eq_sum (s := s) (h : ∀ b ∉ s, f b = 0) : ∑' f = ∑ b ∈ s, f b (NOT tsum_eq_sum_of_support_subset — that name does not exist).
• tsum_eq_sum's conclusion RHS keeps the SAME function: the if-form needs a closing Finset.sum_congr with if_pos.
• Bare Nat.cast_nonneg N as a term/have leaves the cast target a metavariable (IsOrderedRing stuck) — always ascribe (show (0:ℝ) ≤ (N:ℝ) from Nat.cast_nonneg N) (recurred 3×).
• AnalyticAt.comp / Ncount_add_of_le HOU: pin the implicit endpoints (a := ..) (b := ..) — by-tactic proof args do NOT determine them (the elaborator assigns garbage from linarith internals).
• A calc ... := by block nested inside a case/induction tactic block at deep indentation BROKE THE PARSER (mysterious "unexpected token '/--'; expected ':='" downstream + "unknown identifier linarith") — restructure to avoid the nested-by calc in that position.
• Set.mem_union.mp doesn't exist — union membership is defeq to Or: rcases h with h1 | h2 directly.
• positivity cannot see through Classical.choose-defined constants (A0count) — use mul_nonneg A0count_pos.le … explicitly.
• norm_num at hd on ‖(1:ℂ) − 0‖ < 1/2 leaked a metavariable side goal — prefer the explicit rw [show ‖..‖ = 1 by simp] at hd; linarith.
• Statement-level if i ∈ s needs decidability BEFORE classical can run: use a [DecidableEq ι] argument (the zero subtype inherits the noncomputable ℂ instance); open Classical in before a doc-commented lemma FAILED to parse in this toolchain.
• riemannZeta_conj is AMBIGUOUS (root Mathlib vs Zeta23's s ≠ 1 version) — use _root_.riemannZeta_conj (unconditional).

Status / next

5e-v-a ✔ + 5e-v-b chunk 1 ✔ committed. Next session: 5e-v-b chunk 2 — the tail bound (zero_tail_inv_sq_le via ENNReal.tsum_fiberwise + Zeta23 key machinery + the weight-series tail) → the main seriesFun circle bound (one tsum split + four finset shell bounds) → 5e-v-c (the logDeriv assembly + elems + Fexpr circle bound) → 5e-v-d (Schwarz squeeze + the ∃ B capstone). Then ii′-5f → ii′-3b → ii′-3c → ii′-6 → ii′-7.