Session 032 — 2026-08-23 — ii′-5e-v-b chunk 3 COMPLETE: the series circle bound

Directive

Continue ii′-5e-v per STATE.md: chunk 3 — the main seriesFun circle bound seriesFun_norm_le_gapCircle. User: "let's continue with the Next session (032): 5e-v-b chunk 3".

Outcome: chunk 3 COMPLETE (commits 787b9c0, 727f656, d2bfde6,

222d65d, + capstone; LiCircleBound.lean now ~2867 lines, clean elaboration, zero warnings, not yet root-imported)

seriesFun_norm_le_gapCircle: for k ≥ 4000, R with 4k+5/2 ≤ R and the γ-gap ordinate clearance, ‖s‖ = R: ‖seriesFun s‖ ≤ 2·lowZeroConst + 2900·A₀·Ĉ₀(4k+9/2)·(log R)².

Structure as designed (STATE 031 → 032 NEXT ACTION), with these realized constants:

• 3a gapCircle_threshold (416·Ĉ₀(4k+9/2) ≤ 4k+5/2, k ≥ 4000): base Ĉ₀ ≤ 9.3564 (log 16006.5 ≤ 10 via 2.7¹⁰ ≥ 16006.5; log log ≤ log 10 ≤ 2.4 via e^{2.4} ≥ 7.29·1.4 = 10.2) + increments 0.532·(x−16004.5)/16006.5 via log(a/b) ≤ a/b − 1 twice (log 16006.5 ≥ 9 via 2.72⁹ ≤ 16006.5). not_isNontrivialZero_on_gapCircle: the circle is zero-free (a zero would have ordinate within 1/R of R < 1/(16Ĉ₀); conj for negative ordinates). abs_im_ge_norm_sub_one.
• 3b seriesTerm_norm_eq_div (‖seriesTerm s ρ‖ = m·R/(‖ρ‖·‖s−ρ‖) on the zero-free circle); circleZeros R (the finite part {‖ρ‖ < 2R+1}); sum_zeroMult_le_of_im_band (the reusable count brick: a band a ≤ |γ| ≤ b with sign-separation c, 1 ≤ max a c ≤ b, gives mult-sum ≤ 3·A₀·(b−a+2)·log(3·max|a||b|+5) — the two-window cover (M−1, b] ∪ (−b−1, −M], M := max a c; the −1 paddings absorb the non-strict band bounds; the negative window's log loses +1 via 3b+8 ≤ 2(3b+5)); series_tail_le (the tail ‖ρ‖ ≥ 2R+1 ≤ 91·A₀·log R via seriesTerm_norm_le + 1/(1+‖γ‖²) ≤ 1/(1+im²) + zero_tail_inv_sq_le at X = 2R−1); seriesFun_norm_le_split.
• 3c-i half_le_log_two, Nat.log_floor_two_le (J ≤ 2·log R), log_three_le_two_log (log(3x+5) ≤ 2·log R for x ≤ 3R), two_pow_log_floor_le; dyadic_family_le (the generic dyadic machine: fiberwise decomposition via Finset.sum_fiberwise_of_maps_to with t := Ico 1 (J+1) DIRECTLY — sidesteps the Fintype-ℕ instance gap of sum_fiberwise; per-fiber count brick + per-element term bound ⟹ Σ g ≤ Σ_{j∈Ico} (C₁/2^j)·cnt j); shell_low (≤ 2·lowZeroConst).
• 3c-ii shell_inlo (3 < ‖ρ‖ ≤ R/2, dyadic in ‖ρ‖, ≤ 60·A₀·(log R)²); shell_inhi (R/2 < ‖ρ‖ ≤ R−2, dyadic in R−‖ρ‖, ≤ 60·A₀·(log R)², with the 2^j ≥ R/2 empty-fiber sub-case); shell_up (R+2 ≤ ‖ρ‖, dyadic in ‖ρ‖−R — the dyadic class can reach J+1 since ⌊‖ρ‖−R⌋₊ can be ⌊R⌋₊+1, so shell count J+1 ≤ 3·log R; ≤ 45·A₀·(log R)²).
• 3c-iii norm_circle_sub_abs_im_le (R−|im s| = re²/(R+|im|) ≤ B/R); shell_crit (the critical annulus R−2 < ‖ρ‖ < R+2): the uniform separation 1/(32·Ĉ₀) ≤ ‖s−ρ‖ — strip arcs (re² ≤ 13): |t−γ| ≥ ||γ|−R| − 13/R ≥ 1/(16Ĉ₀) − 1/(32Ĉ₀) = 1/(32Ĉ₀) by the γ-gap (applied to conj ρ for γ < 0) + the threshold; near-axis arcs (re² > 13): ‖s−ρ‖ ≥ √13−1 ≥ 2. Term ≤ 64·Ĉ₀·m; single-window count 42·A₀·log R; ≤ 2688·Ĉ₀·A₀·log R. Capstone seriesFun_norm_le_gapCircle: the five-way partition (iterated Finset.sum_filter_add_sum_filter_not + filter_filter + three congruences dropping the redundant ¬q1/¬q2 conjuncts via the range implications) + absorption (165A₀L² + 2688ĈA₀L + 91A₀L ≤ 2900·A₀·Ĉ₀·L² by nlinarith with the L ≤ L² and Ĉ₀ ≥ 2 hints).

Axiom audit (audit-session032-axioms.txt): 19 declarations, all [propext, Classical.choice, Quot.sound] only.

Banked gotchas (session 032 additions)

• linarith CANNOT relate distinct reciprocal atoms: 1/(16·Ĉ) and 1/(32·Ĉ) are opaque; bridge P = 2Q explicitly by field_simp [hne]; ring BEFORE the linarith combination (the shell_crit arc-analysis chain failed silently on exactly this).
• Finset.sum_fiberwise needs [Fintype κ] (its proof goes through univ) — for ℕ-valued class functions use Finset.sum_fiberwise_of_maps_to with t := the explicit range finset (Ico 1 (J+1)) directly: no image-subset step needed at all.
• Finset.sum_image's implicit g is the IMAGE function; the summand f is auto-bound — pin (f := ...) in term position (HOU otherwise).
• Finset.eq_empty_iff_forall_notMem (camelCase, like indicator_of_notMem).
• div_le_div_of_nonneg_right (hab) (hc : 0 ≤ c) : a/c ≤ b/c exists; div_le_div_right does NOT.
• linarith can't use floor-integrality: ⌊R⌋₊ < 2^{J+1} must be routed through ⌊R⌋₊+1 ≤ 2^{J+1} (ℕ, defeq of <) + cast, THEN linarith.
• Filter-conjunction anonymous constructors: the F-MEMBERSHIP proof is the FIRST component of the outer pair (⟨hF, pred-proof⟩), nested conjunctions inside pred-proof (⟨hF, ⟨⟨p1, h2⟩, h3⟩⟩) — the Quot.lift membership error means the nesting is off.
• lt_of_not_le does NOT exist — lt_of_not_ge (again).
• Real.log_pow on (16:ℝ) = 2^4: rw [show (16:ℝ) = 2^4 by norm_num, Real.log_pow]; push_cast; ring ⟹ log 16 = 4·log 2.
• bash heredoc << 'EOF' for large python content BROKE (unexpected EOF at a pow_succ' apostrophe?) — use the Edit tool for large Lean insertions instead.

Status / next

5e-v-b FULLY COMPLETE (chunks 1+2+3): the series circle bound is proved. Next: 5e-v-c — the logDeriv assembly + the elementary terms ⟹ ‖Fexpr s‖ ≤ C·(log R)³ on the gap circles (design in journal-030: strip arcs via the 5c/5d capstones + the near-sum via the gap; right near-axis via the Dirichlet bound; left near-axis via FE + the ΓR brackets (5e-ii A/B + G with the dist(R/2,ℤ) ≥ 1/4 clearance); elems 1/s, 1/(s−1) = O(1/R), ψ(s/2)/2 = O(log R)) → then 5e-v-d (the Schwarz squeeze ⟹ Gentire ≡ B ⟹ the ∃ B capstone partialFraction_identity under ZeroCountProp) → ii′-5f → ii′-3b → ii′-3c → ii′-6 → ii′-7.