Session 027 — 2026-08-22 — ii′-5e-i + 5e-ii COMPLETE: γ-gap circles + the two digamma bounds

Directive

Continue tier ii′-5 per STATE.md: ii′-5e-i (γ-gap circles) then 5e-ii (the digamma bounds). User: "let's move forward to the next session."

Outcome: 5e-i + 5e-ii COMPLETE (commits e28eff6, 0e9336e, ec13029)

5e-i (LiGapCircles.lean, 2 decls audited clean): C0hat_mono + exists_gapCircle_radius — for each k ≥ 1 a radius R ∈ [4k+5/2, 4k+3] with (i) dist(R/2, ℤ) ≥ 1/4 (the trivial-zero clearance) and (ii) every zero ordinate either ≥ 1 away or at clearance ≥ 1/(16·C0hat(4k+9/2)) (the critical-annulus gap). The ×2-RESCALE TRICK on ii′-4's exists_avoiding_midpoint (at a = 8k+5 on the ×2 ordinate finset of the three-unit-window cover; count ≤ 3·C0hat(4k+9/2) via the perimeter ZeroCountProp + C0hat_mono) — zero new pigeonhole code (the 5c ×10-trick verbatim).

5e-ii (LiDigammaLeft.lean, 15 decls audited clean), the four pieces of D-068 §1 C2 plus the telescope:

• tsum_one_div_sub_telescope: ∑'ₙ (1/(n+N) − 1/(n+N+1)) = 1/N (partial-sum telescope sum_range_sub' + squeeze_zero).
• (B) norm_digamma_le_of_two_le_re: ‖ψ(w)‖ ≤ 20·log(2+‖w‖) for re w ≥ 2, |im w| ≤ 5 — the Weierstrass series (Zeta23 DigammaSeries.digamma_series) split at N = ⌈re w⌉₊: head by the harmonic bound (Mathlib harmonic_le_one_add_log), tail by the telescope; the positive-integer case via digamma_natCast_eq (ψ(n) = −γ + H_{n−1}, induction off digamma_one).
• (C) digamma_recip_sum_le: Σ_{j<m} ‖(w+j)⁻¹‖ ≤ 2/c + 2 + 2·log m for dist(w, −ℕ) ≥ c — the V-split at j₀ = ⌈−re w⌉₊ (one term per side by the dist condition, the rest 1-separated into the harmonic bound via recip_norm_le_right/left + sum_bij reindexing).
• (A) norm_digamma_le_of_dist_nat: ‖ψ(w)‖ ≤ (46 + 2/c) + 23·log(2+‖w‖) for re w ≤ 2, dist(w,−ℕ) ≥ c — the recurrence to re ∈ [3,4) (digamma_add_natCast' — the pole-avoidance form of the recurrence, since the near-axis application includes REAL points where 5d's im ≠ 0 hypothesis fails) + (C) + the landing-zone bound (StirlingVert for |im| ≥ 1/2; (B) at the shifted point for |im| < 1/2 — no compactness-existential needed, the constant is explicit).
• (G) logDeriv_Gammaℝ_eq: logDeriv ΓR s = −(log π)/2 + ½ψ(s/2) for im s ≠ 0 — the m-fold shift (m = ⌈max 0 (−re s/2)⌉₊ + 1) via gamma_mul_prod (session 026) + the EventuallyEq machinery of 5d + logDeriv_prod_range_linear (induction on logDeriv_mul); the ½ψ-shift terms cancel EXACTLY by digamma_add_natCast.

Full build GREEN (8764 jobs, LiDigammaLeft root-imported).

Banked gotchas (session 027 additions)

• Nat.cast_nonneg n needs an ascription (have h : (0:ℝ) ≤ (n:ℝ) := Nat.cast_nonneg n) — bare have h := Nat.cast_nonneg n leaves the ordered-ring typeclass stuck. Same class of failure for any bare cast lemma have.
• Nat-sub casts: ↑(a − b : ℕ) does NOT rewrite via push_cast — needs Nat.cast_sub (h : b ≤ a) first; and the elaborator LIFTS Real.log (m − k) to the real-sub form ↑m − ↑k (mismatch with Nat.cast_sub forms) — pin the cast: Real.log (↑(m − k) : ℝ).
• Summable.tsum_le_tsum (protected, NOT plain tsum_le_tsum); Summable.sum_add_tsum_nat_add (k) (hf) : ∑ range k + ∑' (n+k) = ∑' — the shifted terms are beta-REDEXES: state split-goals with the explicit (fun m => body) (n + N) redex form (exact h.symm closes then; reduced forms do NOT match syntactically).
• Finset.prod_range_succ (f) (n) — f EXPLICIT first in this Mathlib; Finset.sum_range_succ' appends the term on the RIGHT: ∑_{n+1} = (∑_n shifted) + f 0.
• Finset.Ico_erase_left : (Ico a b).erase a = Ioo a b (NOT Ico (a+1) b) — the Ioo bridge is Finset.Ico_succ_left_eq_Ioo with Order.succ — avoid via range-forms (sum_Ico_eq_sum_range + sum_range_succ').
• harmonic_le_one_add_log (n) : (↑(harmonic n) : ℝ) ≤ 1 + log n EXISTS (NumberTheory/Harmonic/Bounds.lean); Real.log_two_gt_d9, Real.eulerMascheroniConstant_lt_two_thirds, Real.one_half_lt_eulerMascheroniConstant exist.
• div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a/c ≤ a/b — pass hb ASCRIBED ((show (0:ℝ) < X by positivity)); bare by positivity args elaborate before unification (stuck typeclass) — same elaboration-order issue as bare cast haves.
• squeeze_zero (f := ...) (g := ...) ?_ ?_ hg — name f and g or the typeclass gets stuck.
• norm_inv is a ∀-form lemma here (use rw [norm_inv], not have h := norm_inv).
• IsCompact-free landing zones: 5e-ii-(B) at the shifted point replaces the compactness bound entirely (explicit constants).

Status / next

ii′-5e-i + 5e-ii COMPLETE. Next: ii′-5e-iii (the zero series: summability via the ii′-1a dominator + zero_sum_inv_sq; analytic off the zeros via locally-uniform limits; isolation at each zero), then 5e-iv (F entire by principal-part splits: at nontrivial zeros via ii′-1b logDeriv-NF + zeroMult_neg_two_mul; at 1 via ii′-1b's zetaA logDeriv; at 0 and the ψ-poles via the digamma-series splits), 5e-v (the circle bound O((log R)³) + max-modulus squeeze ⟹ F ≡ const; capstone ∃ B identity; uses 5e-i's circles + 5e-ii's digamma bounds

• 5c/5d's R-bounds + the Dirichlet bound for re ≥ 2). Then ii′-5f, ii′-3b, ii′-3c, ii′-6, ii′-7.