Session 024 — 2026-08-22 — ii′-5c COMPLETE: the loose Davenport-disc R-bound

Directive

Continue tier ii′-5 per STATE.md: the ii′-5c back half (R-gap, g, BC assembly). User: "I am ready, let's do it."

Outcome: ii′-5c COMPLETE (commit c7cbae5)

logDeriv_riemannZeta_sub_nearZeros_le PROVED: for s with s.im = t, re s ∈ [1/2, 7/2], |t| ≥ 10, ζ s ≠ 0: ‖logDeriv ζ s − Σ_{ρ ∈ nearZeros t} zeroMult ρ/(s−ρ)‖ ≤ 100000·(log|t|)². Constant deliberately loose (D-067 §6 two-stage plan: this is the GROWTH INPUT for the ii′-5e partial-fraction identity; the tight 10.5/48 come from the identity's analysis in ii′-5f). No perimeter hypothesis needed — the count input is the session-023 Jensen bound, not ZeroCountProp.

Build path (~1000 new lines in LiDisc.lean)

1. norm_scaledZeta_le — the (9/4)|t|² bound extracted from the Jensen proof (standalone, for the outer-circle estimate).
2. Order helpers: scaledZeta_order_ne_top (via AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected, F(0) = 1), one_le_analyticOrderNatAt_scaledZeta.
3. scaledZeroFinset t r (hr : r ≤ 1) (subset-of-unit-disc construction, avoiding the dite-proof finsets of Zeta23's finiteSetOfZeros_mono) + scaledZeroFinset_24_25_eq (toFinset_inj.mpr rfl) bridging to the Jensen finset; scaledZeroFinset_sum_order_le (monotonicity + Jensen), scaledZeroFinset_card_le_sum (orders ≥ 1).
4. R-gap: exists_collection_radius — the ×10 RESCALE TRICK: apply ii′-4's unit-window exists_avoiding_midpoint at a = 23 to the ×10 image of the (5/2)-scaled norm finset, divide by 10 ⟹ R_c ∈ [2.3, 2.4] with clearance 1/(20(k+1)) from every zero-norm — ZERO new pigeonhole code (STATE.md's suggested route). collRadius/rC bundle via Classical.choose; rC_gap (gapD t := 1/(50(k+1)) in the w-scale); collZeros_norm_le (collected zeros satisfy ‖w‖ ≤ r_c − gapD).
5. The Blaschke quotient g := Cf r_c F entirely from Zeta23's Cf API: Cf_eq_div_collProd / Cf_eq_zeroFactor_div (the dite-unfold pair), Cf_collZeros_analytic (CfAnalytic at R = (1+r_c)/2), Cf_collZeros_ne_zero (ZeroFactorization at zeros; else-branch off), Cf_collZeros_log_norm_zero_nonneg (g(0) = 1/∏(−ρ)^m, ‖ρ‖ < 1), Cf_collZeros_norm_le_sphere (sphere zero-free by the gap; each ‖w−ρ‖ ≥ gapD ⟹ ‖g‖ ≤ (9/4)|t|²·gapD^{−M_c}), Cf_collZeros_norm_le_ball (AnalyticOn.norm_le_of_norm_le_on_sphere).
6. Constant fold (all real-analysis, no new input): log_9_4_le_one (9/4 ≤ e), log_33_32_ge (log x ≥ 1−1/x at 33/32 ⟹ ≥ 1/33), two_le_log_abs_t (e² ≤ 2.7183² < 10), jensen_bound_elementary (≤ 33+66L), card96_le, collMultSum_le, log_50_card_le (50(k+1) ≤ 4150L, log 4150 ≤ 9 via e > 2.71, log L ≤ L−1 ⟹ ≤ L+8), Mbound_le (≤ 420L² via (L−2)(354L+131) ≥ 0).
7. Main assembly: w₀ = (2/5)(s−s₀) (‖w₀‖ ≤ 3/5 from s.im = t, σ ∈ [1/2, 7/2]); B =ᶠ[𝓝 w₀] F/P (zero set closed = finset carrier); logDeriv chain (logDeriv_div/prod/comp + per-factor logDeriv_fun_pow ⟹ m/(w₀−ρ)); LogOfAnalyticFunction (r = 3/5, R = r_c) + BorelCaratheodoryDeriv (16·M·r_c²/(r_c−3/5)³ ≤ 450M); deriv J_B w₀ = (5/2)logDeriv ζ s − Σ m/(w₀−ρ); the (2/5)-rescaled sum pushes forward through the affine image (Finset.sum_image + zeroMult_affMap) and splits near/extras (Finset.sum_sdiff); extras ‖s−ρ‖ ≥ |t−γ| ≥ 1 ⟹ ≤ Σm ≤ Jensen. Final: 180·420L² + 42L² = 75642L² ≤ 100000L².

Banked gotchas (session 024 additions)

• Set.Finite.toFinset_inj.mpr rfl equates toFinsets from different finiteness proofs of the same set — the clean way to handle Cf's anonymous dite-bound proof.
• div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a/b ≤ c/d ↔ a*d ≤ c*b (GroupWithZero/Basic); the 4-arg div_le_div does NOT exist in this Mathlib. div_le_iff₀ (hc : 0 < c) : a/c ≤ b ↔ a ≤ b*c.
• EventuallyEq.deriv is the EVENTUALLY version (deriv f =ᶠ deriv g); the pointwise one is Filter.EventuallyEq.deriv_eq.
• Filter.EventuallyEq.eq_of_nhds gives pointwise value equality.
• Finset.sum_sdiff exists via to_additive (prod_sdiff) — grep for "sum_sdiff" fails since it's generated; same for Finset.sum_image (takes Set.InjOn in this Mathlib).
• positivity maxRecDepth-loops on set-bound finsets' card casts — use explicit mul_pos/add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) terms; and Nat.cast_nonneg _ inside compound terms needs an ascribed target type (IsOrderedRing metavariable stuck otherwise).
• Real.log_le_log (0 < x) (x ≤ y), Real.one_sub_inv_le_log_of_pos, Real.log_le_iff_le_exp, Real.exp_one_gt_d9/_lt_d9, Real.exp_nat_mul : exp (n*x) = (exp x)^n — all as expected.
• norm_natCast is RCLike.norm_natCast (not Complex.*).
• mem_sphere_iff_norm is root-namespace (not Metric.*).
• rw [← mul_one]/[← div_one] rewrites ALL occurrences of the pattern — for one-sided division comparisons use div_le_iff₀ + explicit mul_nonneg hints to nlinarith instead.
• field_simp sometimes closes the goal entirely (trailing ring then errors "no goals") — check before appending ring.
• deriv-computation chain that worked: funext-reorder to (f + const) form → deriv_add_const → show with id w (defeq) → deriv_const_mul _ differentiableAt_id → deriv_id' → simp. (differentiableAt_id'/deriv_id'' pointwise forms do NOT exist as stated; deriv_id' : deriv id = fun _ => 1, deriv_id'' for (fun x=>x).)

Status / next

ii′-5c COMPLETE. Next per D-067 §6: ii′-5d (FE-reflection to σ ∈ [−5/2, 1/2] + the left-plane uniform digamma bound |ψ(w) − log w| ≤ C away from poles), then ii′-5e (partial-fraction identity; needs zeroMult(−2n) = 1 for ALL n — generalize ii′-4c's zeroMult_neg_two), ii′-5f (tight analysis → 10.5/48), ii′-3b (moments), ii′-3c (crux), ii′-6, ii′-7.