[{"type":"thinking","thinking":"All APIs confirmed:\n- `Real.one_sub_inv_le_log_of_pos : 0 < x → 1 - x⁻¹ ≤ log x` ✓ (for log(33/32) ≥ 1 − 32/33 = 1/33)\n- `Set.Finite.toFinset_inj : hs.toFinset = ht.toFinset ↔ s = t` ✓\n- `Real.le_log_iff_exp_le` ✓ (for log(9/4) ≤ 1 ⟺ 9/4 ≤ e, and log 4100 ≤ 9 ⟺ 4100 ≤ e⁹)\n\nNow update todos and write the code. Plan of the file addition (append to LiDisc.lean before `end NguyenRH1`):\n\n§5. `norm_scaledZeta_le` — the (9/4)|t|² bound (extracted, duplicated proof).\n§6. `scaledZeta_order_ne_top` + `one_le_analyticOrderNatAt_of_zero`.\n§7. `scaledZeroFinset` (r-parameterized) + mem lemma.\n§8. Jensen count monotonicity: M_c over any r ≤ 24/25 ≤ J-bound; card ≤ M.\n§9. `exists_collection_radius` — R_c gap via ×10 rescale of exists_avoiding_midpoint.\n§10. With R_c chosen (use Classical choice via `choose` or just work inside the main theorem's proof with obtain) — hmm. Design decision: make r_c etc. FUNCTIONS via choice, or carry the existential into each lemma? Cleaner: one big theorem with `obtain ⟨R_c, ...⟩ := exists_collection_radius ht` at the top and everything inside. But that makes a monster proof. Better: define a structure/bundle? Standard Lean approach: noncomputable defs using Classical.choose:\n\n```lean\ndef collRadius (t : ℝ) (ht : 10 ≤ |t|) : ℝ := (exists_collection_radius ht).choose\n```\nThen lemmas about collRadius via .choose_spec. But ht : 10 ≤ |t| as an argument to a def is fine (Prop arg).\n\nHmm — but then every lemma needs ht. That's OK — they all have ht anyway.\n\nLet me define (all inside namespace, with t, ht):\n- `collRadius t ht` (R_c), spec: 23/10 ≤ R_c ≤ 24/10 ∧ gap.\n- `rC t ht := collRadius t ht * (2/5)` — scaled radius ∈ [23/25, 24/25].\n- `collCard t : ℕ` — card of the 24/25-scaled-zero finset (no ht needed).\n- `δw t := 1/(50*(collCard t + 1))`.\n- `logRad t ht := rC t ht` — wait I decided R_log = r_c exactly. ✓ so no separate logRad.\n- `scaledZerosRC t ht := scaledZeroFinset t (rC t ht) (r_c < 1 proof)` — hmm the def needs the proof r_c < 1 which needs ht. Messy but OK: scaledZeroFinset t r hr with hr : r < 1. For rC: rC t ht < 1 needs ht (via R_c ≤ 24/10 from choose_spec). So the def `scaledZerosRC t ht := scaledZeroFinset t (rC t ht) (rC_lt_one ht)`.\n\nAlternatively — simplify! Note finiteSetOfZeros_mono only needs r < 1 for the FINSET to make sense, but SetOfZeros r F is finite for ANY r ≤ 1 (subset of SetOfZeros 1). Actually even simpler: scaledZeroFinset could take (hr : r ≤ 1) and use Set.Finite.subset directly of scaledZeta_zeros_finite... but finiteSetOfZeros_mono needs r < 1; for r = 1 it's scaledZeta_zeros_finite itself. Let me just define:\n\n```lean\ndef scaledZeroFinset (t : ℝ) (r : ℝ) : Finset ℂ :=\n  if hr : r < 1 then\n    (finiteSetOfZeros_mono (f := scaledZeta t) hr (scaledZeta_zeros_finite)).toFinset\n  else (scaledZeta_zeros_finite (t := t)).toFinset\n```\nUgly. Better: use subset-direct:\n```lean\ndef scaledZeroFinset (t : ℝ) (r : ℝ) (hr : r ≤ 1) : Finset ℂ :=\n  (scaledZeta_zeros_finite.subset (fun w hw => ⟨hw.1.trans hr, hw.2⟩)).toFinset\n```\nWait scaledZeta_zeros_finite : (SetOfZeros 1 (scaledZeta t)).Finite. SetOfZeros r ⊆ SetOfZeros 1 for r ≤ 1: `Set.Finite.subset` gives (SetOfZeros r).Finite, then toFinset. This handles all r ≤ 1 uniformly without dite. But then membership: ρ ∈ scaledZeroFinset t r hr ↔ ‖ρ‖ ≤ r ∧ scaledZeta t ρ = 0 via mem_toFinset ✓. \n\nBUT: the Jensen count `scaledZeta_jensen_count` is stated over `(finiteSetOfZeros_mono (r := 24/25) ...).toFinset` — a DIFFERENTLY-DEFINED finset (same underlying set though). For monotonicity I need: Σ over scaledZeroFinset t (24/25) ≤ log-bound. The two finsets are equal as sets (both = SetOfZeros (24/25) F) — equal as finsets by Set.Finite.toFinset_inj (sets equal by rfl). So:\n\n```lean\ntheorem scaledZeroFinset_eq_jensenFinset : scaledZeroFinset t (24/25) (by norm_num) = (finiteSetOfZeros_mono (f := scaledZeta t) (r := 24/25) (by norm_num) scaledZeta_zeros_finite).toFinset := by\n  apply Set.Finite.toFinset_inj.mpr ... \n```\nhmm toFinset_inj : hs.toFinset = ht.toFinset ↔ s = t. The sets: SetOfZeros (24/25) F = SetOfZeros (24/25) F — rfl. But wait my subset-derived finite: `scaledZeta_zeros_finite.subset (...)` : (SetOfZeros (24/25) F).Finite — the SET is SetOfZeros (24/25) F? `Set.Finite.subset hs hsub : t.Finite` where hsub : t ⊆ s — so yes the resulting .Finite is OF SetOfZeros (24/25) F. toFinset_inj.mpr rfl gives the finset equality. ✓\n\nHmm — but actually, for the Cf function the internal finset is `finite_zeros_mono.toFinset` where the proof is chosen by the dite's Classical decidability — I can't control which proof. But toFinset_inj.mpr rfl handles ANY proof. So the Cf-unfold lemma:\n\n```lean\ntheorem Cf_eq_div_prod {t : ℝ} {r : ℝ} (hr : r ≤ 1) {w : ℂ}\n    (hw : w ∉ SetOfZeros r (scaledZeta t)) :\n    Cf r (scaledZeta t) w = scaledZeta t w / ∏ ρ ∈ scaledZeroFinset t r hr, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ := by\n  unfold Cf scaledZeroFinset\n  by_cases hfin : (SetOfZeros r (scaledZeta t)).Finite\n  · simp only [hfin, ↓reduceDIte, hw, if_true]\n    congr 2  -- or rw to equate finsets\n    exact Set.Finite.toFinset_inj.mpr rfl  -- (up to the subset-derived proof)\n  · exact absurd (the finiteness) hfin\n```\n\nThe subset-derived finiteness: `scaledZeta_zeros_finite.subset (fun w hw => ⟨hw.1.trans hr, hw.2⟩)` — as a term. OK.\n\nAnd:\n```lean\ntheorem Cf_eq_zeroFactor_div {t : ℝ} {r : ℝ} (hr : r ≤ 1) {w : ℂ}\n    (hw : w ∈ SetOfZeros r (scaledZeta t)) :\n    Cf r (scaledZeta t) w = ZeroFactor (scaledZeta t) w /\n      ∏ ρ ∈ (scaledZeroFinset t r hr) \\ {w}, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ\n```\n\nNow — for `B_nonzero` at a zero w: ZeroFactorization gives `ZeroFactor F w = h_w w` with `h_w w ≠ 0` — requires w ∈ SetOfZeros R F with R < 1 and F analytic on closedBall(0,1) and F 0 ≠ 0. All ✓ (r_c ≤ 24/25 < 1; scaledZeta_analytic ht; scaledZeta_zero t : F 0 = 1 ≠ 0).\n\nAnd the product over ZW \\ {w}: each factor (w − ρ)^m ≠ 0 ⟸ w ≠ ρ ⟸ ρ ∈ ZW\\{w} ✓.\n\nFor w ∉ zeros (‖w‖ ≤ r_c): B w = F w/prod, F w ≠ 0, prod ≠ 0 (w ≠ ρ for ρ ∈ ZW: w = ρ would give w ∈ zeros). ✓\n\nSphere bound: w with ‖w‖ = r_c. First: w ∉ SetOfZeros r_c F: if w ∈ zeros, then w ∈ ZW96 (‖w‖ = r_c ≤ 24/25), gap: |‖w‖ − r_c| ≥ δw > 0, contradiction with ‖w‖ = r_c. ✓ So B w = F w/prod. ‖F w‖ ≤ (9/4)|t|² (norm_scaledZeta_le, r_c ≤ 24/25 ≤ 99/100). ∏: for ρ ∈ ZW: ‖ρ‖ ≤ r_c − δw (gap-below lemma) ⟹ ‖w − ρ‖ ≥ ‖w‖ − ‖ρ‖ ≥ δw ⟹ ∏ ≥ δw^{M_c} (M_c = Σ over ZW). So ‖B w‖ ≤ (9/4)|t|² / δw^{M_c} = (9/4)|t|² · (50(k+1))^{M_c} — with 1/δw = 50(k+1): (1/δw)^{M_c}: write as ((50*(k+1)):ℝ)^{M_c} nat pow. Div bound: ‖F w‖/‖P‖ ≤ B/B' with div_le_div hFtop (prod lower) (prod pos)... div_le_div (a≤b, 0<c, c≤d → a/d ≤ b/c)? The form: ‖F‖/‖P‖ ≤ ((9/4)|t|²)/(δw^{M_c}) via div_le_div_of_nonneg... `div_le_div (hac : a ≤ b) (hc : c ≤ d) (c pos) (b nonneg)??` — signature: div_le_div (h₁ : a ≤ b) (h₂ : c ≤ d) (h₃ : 0 < c) (h₄ : 0 ≤ a) : a / d ≤ b / c? I always mix up. There's `div_le_div_of_nonneg_left/right`, `div_le_div` variants. At build time, use: ‖F‖/‖P‖ ≤ ‖F‖/δw^{M_c} (div_le_div_of_nonneg_left... numerator fixed, denominator smaller (both pos) ⟹ quotient bigger: div_le_div_of_nonneg_left (h : 0 < a)?? hmm — `div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (hbc : c ≤ b) : a / b ≤ a / c`. Then ≤ ((9/4)|t|²)/δw^{M_c} via div_le_div_of_nonneg_right (hFtop) hmm — `div_le_div_of_nonneg_right (h : a ≤ b) (hc : 0 < c) : a / c ≤ b / c`. These names shifted in recent Mathlib (session 023 gotcha: div_le_div_iff_of_pos_right/left renames). I'll adapt at build time. Alternatively just use `div_le_div hFtop hprod_le (pow_pos ...) (norm_nonneg _)` — the 4-arg div_le_div: `div_le_div (hbc : b ≤ c)??`. I'll sort it with exact?/apply? at build.\n\nMax-modulus then gives the bound on closedBall(0, r_c) — note norm_le_of_norm_le_on_sphere's analytic arg: AnalyticOn ℂ B (closedBall 0 R) with r = r_c ≤ R. Take R := (1 + r_c)/2... need r_c < 1: r_c ≤ 24/25 ✓. CfAnalytic (r_lt_R : r_c < R) (R_lt_one) gives AnalyticOnNhd on closedBall(0, R); .analyticOn : AnalyticOn on closedBall(0, R). But WAIT — AnalyticOnNhd.analyticOn: AnalyticOnNhd ℂ f s → AnalyticOn ℂ f s? AnalyticOnNhd means analytic at a neighborhood of each point of s; AnalyticOn means analytic within... there's `AnalyticOnNhd.analyticOn` ✓ (used in DiskBound). ✓ And norm_le_of_norm_le_on_sphere (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (closedBall 0 R)) (cond on sphere 0 r) (w ∈ closedBall 0 r). With r = r_c, R = (1+r_c)/2. ✓\n\nB 0 value: 0 ∉ zeros (F 0 = 1 ≠ 0) ⟹ B 0 = F 0/∏(0−ρ)^m = 1/∏(−ρ)^m. ‖B 0‖ = 1/∏‖ρ‖^m (norm_prod, norm_pow, norm_neg... ∏‖0−ρ‖^m = ∏‖ρ‖^m). log‖B 0‖ = −Σ m log‖ρ‖... via Real.log_div (numerator 1 ≠ 0, denom ≠ 0), log_one, Real.log_prod (each factor ≠ 0: `Real.log_prod : (∀ i ∈ s, f i ≠ 0) → log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)` ✓), Real.log_pow. Each ‖ρ‖ ≤ r_c − δw ≤ 24/25 < 1 ⟹ log‖ρ‖ ≤ log(24/25) < 0... just need log‖ρ‖ ≤ 0 (Real.log_nonpos (norm_nonneg) (‖ρ‖ ≤ 1)) ⟹ −m·log‖ρ‖ ≥ 0 ⟹ log‖B 0‖ = 0 − Σ m log‖ρ‖ ≥ 0 ✓ (Finset.sum_nonpos of m·log‖ρ‖).\n\nThen LogOfAnalyticFunction (r := 3/5) (R := r_c) — B analytic on closedBall(0, r_c) (mono from R'), B nonzero on closedBall(0, r_c):\nJ_B analytic on ball(0, r_c), J_B 0 = 0, deriv J_B = B'/B on closedBall(0, 3/5), Re J_B = log‖B‖ − log‖B 0‖ on ball(0, r_c).\n\nRe bound: w ∈ ball(0, r_c) ⟹ w ∈ closedBall ✓ ⟹ ‖B w‖ ≤ Bbound ⟹ (B w ≠ 0 ⟹ ‖B w‖ > 0) log‖B w‖ ≤ log Bbound (Real.log_le_log (norm_pos_iff.mpr (B w ≠ 0)) (ball bound)) ⟹ Re J_B(w) = log‖B w‖ − log‖B 0‖ ≤ log‖B w‖ ≤ log Bbound.\n\nlog Bbound ≤ (1 + 2L) + M_c·log(50(k+1)): Bbound = (9/4)·|t|²·(50(k+1))^{M_c}; log = log(9/4) + log(|t|²) + log((50(k+1))^{M_c}) via log_mul (positivity), log_pow: = log(9/4) + 2L + M_c·log(50(k+1)) hmm log(|t|²) = 2 log|t| via Real.log_pow (|t| ≠ 0... log (x^2) = 2 log x needs x > 0 — |t| ≥ 10 ✓). log(9/4) ≤ 1. So M_bound := 1 + 2L + M_c * log(50(k+1))... actually cleaner: define M_bound := Real.log Bbound and separately prove M_bound ≤ (1 + 2L) + M_c·log(50(k+1)) ≤ 361L². BC needs Mpos: 0 < M_bound: log Bbound ≥ log‖B w‖... hmm simpler: Bbound ≥ (9/4)·100·1 = 225 ⟹ log Bbound ≥ log 225 > 0 ✓.\n\nBC: w₀ ∈ closedBall(0, 3/5) ⟹ ‖deriv J_B w₀‖ ≤ 16·M_bound·r_c²/(r_c−3/5)³. With r_c ∈ [23/25, 24/25]: ≤ 16·M_bound·(24/25)²/(8/25)³ = 450·M_bound.\n\nDeriv identity at w₀ — as planned (Steps A–F).\n\nThen the main theorem assembles. The final numeric: \n‖...‖ ≤ (2/5)·450·M_bound + M_c ≤ 180·(361L²) + 35L² ≤ 66000L².\nWait: M_c ≤ J = 33 + 66L ≤ 35L² (need: 33 + 66L ≤ 35L² at L ≥ 2.302585: 35L² ≥ 35·5.3019 = 185.6 ≥ 33+66·2.302585+... hmm no: 33 + 66L ≤ 35L² ⟺ at L = 2.3026: LHS = 185.0, RHS = 185.57 ✓ barely; increasing L: derivative 66 vs 70L ≥ 161 ✓ increasing gap. For Lean: nlinarith with L ≥ 2.302585? Better: use L ≥ 23/10 = 2.3 (log 10 ≥ 2.3 ⟸ e^{2.3} ≤ 10? e^{2.3} = 9.974 ≤ 10 ✓ — provable? Real.exp 2.3 ≤ 10... hmm. Standard trick: log 10 ≥ 9/4? e^{9/4} = 9.4877 ≤ 10 ✓. e^{9/4} ≤ 10 in Lean: exp(9/4) ≤ 10... these exp bounds are painful. What do the base-point files use? LiBasePoints has exp ≤ (1−x/16)⁻¹⁶ tricks. For log 10 lower bound: `Real.log 10 ≥ 2.3`? There might be `Real.log_two_lt_d9` (log 2 < 0.6931471808) and `Real.log_two_gt_d9` (0.6931471803 < log 2). log 10 = log 2 + log 5... Alternatively just use L ≥ 2: from |t| ≥ 10 > e² = 7.389 ⟹ L ≥ 2 ✓ trivially via le_log_iff_exp_le: 2 ≤ log|t| ⟸ exp 2 ≤ 10 ⟸ exp 2 ≤ e^{2.3}-ish... exp 2 ≤ 10: `Real.exp_one_lt_d9` gives e < 2.719, so e² < 2.719² = 7.393 ≤ 10 ✓ norm_num-friendly: exp 2 = (exp 1)² via Real.exp_nat_mul (2 = 2*1: exp (2*1) = (exp 1)^2). Then 2.719² = 7.392... ≤ 10 ✓. So L ≥ 2.\n\nRedo the fold with L ≥ 2 (slightly worse margins, recheck):\n- 563L ≤ (563/2)L² = 281.5L²; 265 ≤ 66.25L²; M_bound ≤ (66 + 281.5 + 66.25)L² = 413.75L² ≤ 414L².\n- 180·414 = 74520; M_c ≤ 33+66L ≤ (33/4 + 33)L² = 41.25L² ≤ 42L². Total ≤ 74562L².\n- The log(50(k+1)) bound: 50(J+1) = 50(34+66L) = 1700+3300L ≤ (850+3300)L = 4150L (L ≥ 2). log(4150L) = log 4150 + log L ≤ 9 + (L − 1)?? log 4150 ≤ 9 ⟺ 4150 ≤ e⁹; e⁹ ≥ 2.718²...⁹: 2.718⁹ = 2.718·(2.718⁴)²; 2.718² = 7.387524; ⁴ = 54.57557; ⁸ = 2978.48; ⁹ = 8095.6 ≥ 4150 ✓. So log(4150L) ≤ 9 + log L. And log L ≤ L − 1 hmm that's log L ≤ L−1 (Real.log_le_sub_one_of_pos, L > 0) ✓. So ≤ L + 8 ✓ same as before.\n- 66L² + 563L + 265 ≤ 414L² at L ≥ 2 ✓ (check at 2: 264+1126+265 = 1655 ≤ 1656 ✓ barely! 66·4 = 264, 563·2 = 1126, +265 = 1655 vs 414·4 = 1656 ✓ 1 unit of slack — TOO TIGHT for comfort with real-number arithmetic... use 420L²: at 2: 1680 vs 1655 ✓ margin 25. And nlinarith should prove (66L² + 563L + 265 ≤ 420L²) from L ≥ 2: 354L² − 563L − 265 ≥ 0; at 2: 1416−1126−265 = 25 ≥ 0 ✓; roots: (563 + √(563² + 4·354·265))/(2·354) = (563 + √(316969+375540))/708 = (563+832.2)/708 = 1.97 < 2 ✓ so holds for L ≥ 2. nlinarith with the product form: (L−2)(354L + 132.5)... 354L²−563L−265 = (L−2)(354L+? ): (L−2)(354L + 132.5) = 354L² + 132.5L − 708L − 265 = 354L² − 575.5L − 265 — not exact. (L−2)(354L + 281.5·...). Let me just factor: 354L² − 563L − 265; divide by (L−2): 354L² − 563L − 265 = (L − 2)(354L + 131) + ( −265 + 262)= (L−2)(354L+131) − 3. Hmm −3: not clean. (L−2)(354L+131) = 354L² + 131L − 708L − 262 = 354L² − 577L − 262. Subtract from target: (−563L + 577L) + (−265 + 262) = 14L − 3 ≥ 0 for L ≥ 2 ✓. So 354L² − 563L − 265 = (L−2)(354L+131) + (14L − 3) — nlinarith [hL] should find this. OK.)\n\n- Total: 180·420 = 75600 + 42 = 75642 → C := 76000. Round: 80000 for headroom. Actually let me reconsider M_bound ≤ 420L²... to reduce nlinarith pain, take C := 100000? The fold: ‖R‖ ≤ (2/5)·450·M_bound + M_c = 180·M_bound + M_c ≤ 180·420L² + 42L² = 75642L² ≤ 100000L². Use 100000 for a nice round number with slack. It's a loose growth constant — bigger rounder is better for downstream manipulation. Hmm — 5e will use this as \"O((log R)²)\" — any constant works. 10⁵. \n\nActually — wait. Let me reconsider the Mpos side: BC needs 0 < M_bound where M_bound := Real.log Bbound. Bbound = (9/4)·|t|²·(50(k+1))^{M_c} ≥ (9/4)·100·1 = 225 (pow ≥ 1 since base 50(k+1) ≥ 50 > 1 and exponent... M_c could be 0! (50(k+1))^0 = 1 ✓ ≥ 1 via one_le_pow₀). So Bbound ≥ 225 > 1 ⟹ log > 0 ✓ (Real.log_pos). ✓\n\nAlso — one more subtlety in the sphere bound: ∏_{ρ∈ZW} ‖w−ρ‖^{m_ρ} ≥ δw^{M_c}: if ZW is EMPTY (M_c = 0), prod = 1 = δw^0 ✓ fine.\n\nAnd in the deriv-identity Step A: w₀ ∉ ZW — w₀ = (2/5)(s−s₀); if w₀ ∈ ZW then F w₀ = 0, but F w₀ = ζ(s)/ζ(s₀) ≠ 0 ✓.\n\nAlso need: w₀ ∈ closedBall(0, 3/5) — ‖w₀‖ = (2/5)|σ−2|, σ ∈ [1/2, 7/2] ⟹ |σ−2| ≤ 3/2 ⟹ ‖w₀‖ ≤ 3/5 ✓.\n\nAlso s.im = t used in: extras ‖s−ρ‖ ≥ |im(s−ρ)| = |t − ρ.im| ≥ 1. ✓\n\nNow — about `nearZeros`: define and prove membership + the two key properties (nontrivial ⟹ re ∈ (0,1); |im − t| < 1 ⟹ ‖ρ − s₀‖ ≤ √5 ≤ R_c for the image-subset argument).\n\n‖ρ − s₀‖² = (β−2)² + (γ−t)² ≤ 4 + 1 = 5 ⟹ ‖ρ−s₀‖ ≤ √5. Need √5 ≤ R_c: R_c ≥ 2.3; √5 ≤ 2.3 ⟺ 5 ≤ 5.29 ✓ (Real.sqrt_le_iff / sq). In Lean: ‖ρ−s₀‖ ≤ √5 via normSq: Complex.normSq (ρ − s₀) = (β−2)² + (γ−t)² ≤ 5, then ‖x‖ = √(normSq x) (Complex.norm_eq_sqrt_normSq? there's `Complex.normSq_eq_norm_sq : normSq z = ‖z‖^2`). So ‖ρ−s₀‖² ≤ 5 ⟹ ‖ρ−s₀‖ ≤ √5 via sq_le_sq₀/Real.sqrt. Then √5 ≤ 23/10: (23/10)² = 529/100 = 5.29 ≥ 5 ✓ via Real.sqrt_le_iff... `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y^2`? something like that. Fine.\n\nThen w := (ρ − s₀)/(5/2)... the affine inverse: w = (2/5)(ρ − s₀), aff w = ρ. ‖w‖ = (2/5)‖ρ−s₀‖ ≤ (2/5)(23/10) = 23/25 ≤ r_c ✓ (r_c = (2/5)R_c ≥ 23/25). And F w = ζ(ρ)/ζ(s₀) = 0 ✓. So w ∈ SetOfZeros r_c F ⟹ w ∈ ZW ⟹ ρ = aff w ∈ ZW.image aff ✓.\n\nFinset.sum_image needs `Set.InjOn aff ZW`: aff w = s₀ + (5/2)w injective globally: mul_left_cancel₀ (5/2 ≠ 0) + add_left_cancel ✓ (same as scaledZeta_zeros_finite's preimage inj).\n\nNow the sum-split: ZW.image aff ⊇ nearZeros t. Σ_{image} g = Σ_{near} g + Σ_{image\\near} g (Finset.sum_sdiff (h : near ⊆ image) : ∑ in (image \\ near) + ∑ in near = ∑ in image — the form `Finset.sum_sdiff : s₁ ⊆ s₂ → (∑ i in s₂ \\ s₁, f i) + (∑ i in s₁, f i) = ∑ i in s₂, f i` ✓).\n\nExtras bound: ρ ∈ image \\ near ⟹ (a) ρ ∈ image: ρ = aff w, zeroMult ρ = m_w; (b) ρ ∉ near: ρ ∈ zeroDiscFinset? Need that to conclude |im−t| ≥ 1: ρ = aff w with w ∈ ZW ⟹ F w = 0 ⟹ ζ(aff w) = 0 (F w = ζ(aff w)/ζ(s₀)) and ‖ρ − s₀‖ = (5/2)‖w‖ ≤ (5/2)r_c = R_c ≤ 2.4 ≤ 2.5 ⟹ ρ ∈ zeroDiscFinset ✓ (mem_zeroDiscFinset). So ρ ∉ near ⟹ ¬|ρ.im − t| < 1 ⟹ 1 ≤ |ρ.im − t|. Then ‖(m:ℂ)/(s−ρ)‖ = m/‖s−ρ‖ ≤ m/1 = m: ‖s−ρ‖ ≥ |im(s−ρ)| = |s.im − ρ.im| = |t − ρ.im| = |ρ.im − t| ≥ 1 (abs_sub_comm). ✓\n\nΣ_{extras} m ≤ Σ_{image} m = M_c... hmm M_c := Σ_{w ∈ ZW} analyticOrderNatAt F w. Σ_{ρ ∈ image} zeroMult ρ = M_c via sum_image + order-invariance ✓. And Σ over subset ≤ Σ over all (nonneg terms): Finset.sum_le_sum_of_subset_of_nonneg ✓ (subset: extras ⊆ image ✓). So extras ≤ M_c ≤ J.\n\nThe order-invariance: analyticOrderNatAt_scaledZeta ht (hw : ‖w‖ ≤ 1) : analyticOrderNatAt (scaledZeta t) w = analyticOrderNatAt riemannZeta (s₀ + (5/2)w). And zeroMult (aff w) = analyticOrderNatAt ζ (aff w) — def: zeroMult ρ := (analyticOrderAt riemannZeta ρ).toNat and analyticOrderNatAt f z₀ := (analyticOrderAt f z₀).toNat. So `zeroMult (aff w) = analyticOrderNatAt riemannZeta (aff w)` should be rfl after `unfold zeroMult analyticOrderNatAt`? or just `rfl`. Let me define a tiny lemma `zeroMult_eq : zeroMult ρ = analyticOrderNatAt riemannZeta ρ := rfl`. (Test at build; if not rfl, rw the defs.)\n\nOK — also the deriv-translation for logDeriv F: F = fun w => ζ(s₀ + (5/2)w)/ζ(s₀). logDeriv F w₀ where F w₀ ≠ 0:\nF = fun w => (ζ ∘ aff) w / c with c = ζ(s₀). Hmm scaledZeta def: riemannZeta (...) / riemannZeta (discCenter t). logDeriv (fun w => g w / c) w₀: logDeriv_div with g w₀ ≠ 0, c ≠ 0: = logDeriv g w₀ − logDeriv (fun _ => c) w₀ = logDeriv g − 0 (logDeriv_const: deriv const = 0, so logDeriv const = 0/c = 0 — `logDeriv_const` simp lemma exists? likely `logDeriv_const (c) : logDeriv (fun _ => c) = 0`? probably simp-able). Then logDeriv g w₀ with g = ζ ∘ aff: logDeriv_comp (diff ζ at aff w₀: analytic ⟹ differentiableAt — need aff w₀ = s ≠ 1: s ≠ 1 since s.im = t, |t| ≥ 10 ⟹ s ≠ 1 ✓; diff aff ✓): = logDeriv ζ (aff w₀) · deriv aff w₀. deriv aff w₀ = 5/2: aff = fun w => s₀ + (5/2)*w = const + const*w: deriv_const_add + deriv_const_mul (differentiableAt_id) + deriv_id''. Result: (5/2)·logDeriv ζ s ✓ (aff w₀ = s by ring-ish: s₀ + (5/2)·(2/5)(s−s₀) = s — needs field_simp/ring with ℂ... (5/2 : ℂ)*(2/5 : ℂ) = 1 by norm_num; so s₀ + 1·(s − s₀) = s by ring. Use `show` + ring? ring should handle: s₀ + (5/2)*((2/5)*(s − s₀)) = s as a ring identity in variables s₀, s ✓.)\n\nOne concern: `logDeriv_comp` needs `DifferentiableAt ℂ ζ (aff w₀)` — from analyticAt_riemannZeta_of_ne_one (s ≠ 1) .differentiableAt ✓.\n\nNow, an important check in Step B: `Filter.EventuallyEq.deriv : f =ᶠ[𝓝 x] g → deriv f x = deriv g x` — signature `EventuallyEq.deriv (h : f₁ =ᶠ[𝓝 x] f₂) : deriv f₁ x = deriv f₂ x` ✓ exists in Mathlib.\n\nAnd logDeriv (F/P) at w₀: F/P means fun w => F w / P w. logDeriv_div x (hf : f x ≠ 0) (hg : g x ≠ 0) (hdf : DifferentiableAt) (hdg) ✓.\n\nDifferentiableAt F w₀: scaledZeta_analytic ht gives AnalyticOnNhd on closedBall(0,1); w₀ ∈ closedBall(0, 3/5) ⊆ closedBall(0,1) ⟹ AnalyticAt ⟹ differentiableAt ✓.\n\nDifferentiableAt P w₀: analyticAt_finset_prod_sub_pow (Zeta23) ✓ .differentiableAt.\n\nP w₀ ≠ 0: Finset.prod_ne_zero_iff; each (w₀ − ρ)^{m} ≠ 0: w₀ ≠ ρ (w₀ ∉ ZW ∋ ρ) ✓.\n\nlogDeriv P w₀ = Σ logDeriv (each) w₀ (logDeriv_prod: each factor ≠ 0 at w₀ ✓, differentiable ✓) = Σ m_ρ * logDeriv (· − ρ) w₀ (logDeriv_fun_pow (diff) m) = Σ m_ρ * (1/(w₀ − ρ))... logDeriv (fun w => w − ρ) w₀ = deriv(...)/(...) = 1/(w₀−ρ): deriv (fun w => w − ρ) w₀ = 1: `deriv_sub_const`? hmm: fun w => w − ρ = id − const: deriv_sub (differentiableAt_id) (differentiableAt_const ρ) : deriv (id − fun _ => ρ) w₀ = deriv id w₀ − deriv (fun _ => ρ) w₀ = 1 − 0. But the lambda form: (fun w => w − ρ) — simp with deriv_id'' hmm. There are simp lemmas `deriv_add_const`, `deriv_sub_const`... I think `deriv_sub_const : deriv (fun x => f x − c) x = deriv f x` requires the function form f x − c ✓ that's our form! `deriv_sub_const (c : 𝕜) : deriv (fun x => f x − c) x = deriv f x`? Hmm the actual name might be `deriv_sub_const (hc : DifferentiableAt...)`. Recent Mathlib: `deriv_sub_const (c : F) : deriv (fun x => f x - c) x = deriv f x`? not sure if needs differentiability hypothesis. And then deriv (fun w => w) w₀ = 1: `deriv_id''`? or `deriv_id'`. There's `deriv_id' : deriv id x = 1`? Hmm — `deriv_id'` might be for `deriv id = fun _ => 1`. Or `deriv_id''`. I'll use `hasDerivAt_id` + `.deriv` as fallback: (hasDerivAt_id w₀).sub (hasDerivAt_const w₀ ρ) : HasDerivAt (fun w => w − ρ) (1 − 0) w₀ → .deriv gives deriv = 1 − 0 = 1. Safe. Then logDeriv = deriv/f = 1/(w₀−ρ) (logDeriv_apply? logDeriv f x = deriv f x / f x — `logDeriv_apply` simp). So the factor's logDeriv = 1/(w₀−ρ), and after logDeriv_fun_pow: m * (1/(w₀−ρ)) = m/(w₀−ρ) (mul_one_div m _). ✓\n\nThen: (5/2)·logDeriv ζ s = deriv J_B w₀ + Σ_{ZW} m/(w₀−ρ)?? Wait let me recompute: deriv J_B w₀ = deriv B w₀/B w₀ = logDeriv (F/P) w₀ = logDeriv F w₀ − logDeriv P w₀ = (5/2)·logDeriv ζ s − Σ m/(w₀−ρ).\nSo (5/2)·logDeriv ζ s = deriv J_B w₀ + Σ m/(w₀−ρ).\nlogDeriv ζ s = (2/5)·deriv J_B w₀ + (2/5)·Σ m/(w₀−ρ) = (2/5)·deriv J_B w₀ + Σ (2/5)·m/(w₀−ρ).\n(2/5)·m/(w₀−ρ) = m/((5/2)(w₀−ρ)) = m/(s − aff ρ): (5/2)(w₀−ρ) = (5/2)w₀ − (5/2)ρ = (s−s₀) − (aff ρ − s₀) = s − aff ρ ✓. So term = (m:ℂ)/(s − aff ρ). Field manipulation: (2/5)*m/(w₀−ρ) = m/(s−affρ): mul_div_assoc + congr on denominator. In Lean: prove `(2/5 : ℂ) * (m : ℂ)/(w₀ − ρ) = (m : ℂ)/(s − aff ρ)` by `rw [mul_div_assoc]; congr 1; field_simp; ring`? (5/2)(w₀−ρ) = s − aff ρ as complex identity: (5/2)*(w₀ − ρ) = s − (s₀ + (5/2)*ρ) where w₀ = (2/5)*(s − s₀): expand: (5/2)*(2/5)*(s−s₀) − (5/2)ρ = (s−s₀) − (5/2)ρ = s − s₀ − (5/2)ρ ✓ ring proves it. Then m/(X) = m/Y via congr_arg (HDIV) — need X ≠ 0? No: congr of the denominator is just congr_arg (·) — m/X = m/Y follows from X = Y by rw. So: rw [mul_div_assoc, show (5/2:ℂ)*(w₀−ρ) = s − aff ρ from by ring]... but the LHS after mul_div_assoc is ((2/5)*m)/(w₀−ρ), and I want m/(s − aff ρ). ((2/5)*m)/(w₀−ρ) = m/((5/2)(w₀−ρ))? a/b = (c·a)/(c·b) for c ≠ 0 — mul_div_mul_right? hmm: m/Y = (2/5·m)/((2/5)·Y) hmm. Easiest: field_simp [hw₀ρ ≠ 0, hsρ ≠ 0] then ring. The identity (2/5)*m/(w₀−ρ) = m/(s−affρ) is a field identity valid when denominators ≠ 0: field_simp clears: (2/5)*m*(s−affρ) = m*(w₀−ρ) — after substituting the relations... but field_simp needs to know (s−affρ) = (5/2)(w₀−ρ) — that's a ring identity that field_simp+ring might close: goal after field_simp: (2/5)*m*(s − (s₀+(5/2)*ρ)) = m*(w₀−ρ); with w₀ := (2/5)*(s−s₀) — if w₀ is a `let`/local def, ring needs it unfolded. I'll set w₀ via `set w₀ := (2/5 : ℂ)*(s − discCenter t) with hw₀def` then the ring identity needs w₀'s def — provide `have hws : (5/2:ℂ)*(w₀ − ρ) = s − (s₀ + (5/2)*ρ) := by rw [hw₀def]; ring`. Then: (2/5)*m/(w₀−ρ) = m/(s − affρ): rw [mul_div_assoc, ← hws]?? goal: (2/5)*m/(w₀−ρ) = m/(s−affρ). Rewrite RHS denom via hws.symm: s − affρ = (5/2)(w₀−ρ). Then RHS = m/((5/2)(w₀−ρ)). And m/((5/2)(w₀−ρ)) = (2/5)·(m/(w₀−ρ)): div_mul_eq_mul_div... m/((5/2)·X) = (m/(5/2))/X = m·(2/5)/X ✓ via div_div... m/((5/2)*X) = m/(5/2)/X (div_mul_eq_div_div) = m·(2/5)/X hmm (m/(5/2) = m·(2/5) via div_eq_mul_inv + inv... (5/2)⁻¹ = 2/5 by norm_num). Then (m·(2/5))/X = (2/5·m)/X (mul_comm). OK — chain of rws; fine.\n\nSo final: logDeriv ζ s = (2/5)·deriv J_B w₀ + Σ_{w∈ZW} (m_w:ℂ)/(s − aff w) = (2/5)·deriv J_B w₀ + Σ_{ρ∈image} (zeroMult ρ:ℂ)/(s−ρ).\n\nThen target: logDeriv ζ s − Σ_{near} ... = (2/5)·deriv J_B w₀ + Σ_{extras} ... \n‖·‖ ≤ (2/5)‖deriv J_B w₀‖ + Σ_extras ‖(m:ℂ)/(s−ρ)‖ ≤ (2/5)·450·M_bound + M_c(ℝ) ≤ 180·M_bound + J ≤ 180·420L² + 42L² = 75642L² ≤ 100000L².\n\nHmm wait — the M_bound in BC is the SYMBOLIC one (Real.log Bbound), and I separately show M_bound ≤ 420L². And extras ≤ M_c ≤ J = 33+66L ≤ 42L² (at L ≥ 2: 33+66L ≤ 42L² ⟺ 42L²−66L−33 ≥ 0; at 2: 168−132−33 = 3 ≥ 0 ✓; (L−2)(42L+?): 42L²−66L−33 = (L−2)(42L+16.5)... 42L²+16.5L−84L−33 = 42L²−67.5L−33. remainder 1.5L ≥ 0 ✓ nlinarith).\n\nM_c ≤ J: M_c = Σ_{ZW} order ≤ Σ_{ZW96} order (subset + nonneg) = (the Jensen finset sum) ≤ log((9/4)|t|²)/log(33/32) (scaledZeta_jensen_count) ≤ (1+2L)/(1/33) = 33(1+2L) = 33+66L = J. The last step: a/b ≤ c/d-form: log((9/4)|t|²) ≤ 1+2L ≥ 0? need 0 ≤ numerator ✓ (log((9/4)·100) ≥ log 225 > 0 ✓... log((9/4)|t|²) ≥ 0 since (9/4)|t|² ≥ 1) and log(33/32) ≥ 1/33 > 0: div_le_div (num ≤ num') (denom ≥ denom') (denom' pos) (num nonneg) — `div_le_div (hac : a ≤ b) (hbd : c ≤ d)...` the precise 4-arg: `div_le_div (h₁ : a ≤ b) (h₂ : c ≤ d) (h₃ : 0 < c) (h₄ : 0 ≤ a) : a / d ≤ b / c`? I think that's right: a/d ≤ b/c when a ≤ b, c ≤ d, 0 < c, 0 ≤ a. Let me double check direction: bigger numerator, smaller denominator ⟹ bigger. a/d vs b/c: a ≤ b and d ≥ c > 0 ⟹ a/d ≤ b/d ≤ b/c ✓. Signature in Mathlib (ordered field): `div_le_div (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 < c) (ha : 0 ≤ a) : a / d ≤ b / c` ✓ yes.\n\nAnd card ZW96 ≤ Σ_{ZW96} order: each order ≥ 1 (one_le for zeros — need: w ∈ ZW96 ⟹ F w = 0, ‖w‖ ≤ 24/25 ≤ 1 ⟹ order ≥ 1 via my helper). Finset.card_le_sum: card s = Σ 1 ≤ Σ order: `Finset.card_le_sum`? doesn't exist probably; do: s.card = ∑ _ ∈ s, 1 (Finset.card_eq_sum_ones) ≤ ∑ order (Finset.sum_le_sum, each 1 ≤ order) ✓.\n\nk+1 vs J: k = card ZW96 ≤ M96 ≤ J ⟹ k+1 ≤ J+1 (real cast: (k+1 : ℝ) ≤ J+1... k ≤ J from (k:ℝ) ≤ M96 ≤ J where M96 : ℕ cast — hmm M96 = Σ of ℕ orders: (M96 : ℝ)... the Jensen bound compares Σ (nat-valued orders) with a real: `∑ ρ ∈ ..., analyticOrderNatAt F ρ ≤ Real.log ... / Real.log ...` — the LHS is ℕ ≤ ℝ?? In the committed statement: `∑ ρ ∈ ..., analyticOrderNatAt (scaledZeta t) ρ ≤ Real.log (...) / Real.log (...)` — type: the sum is ℕ, RHS ℝ — so it's (↑sum) ≤ ℝ via Nat.cast_le. ✓. So (k:ℝ) ≤ (M96:ℝ) ≤ J. Then 50(k+1) ≤ 50(J+1): cast k+1: ((k+1:ℕ):ℝ) = k+1 ✓ push_cast.\n\nAlso for Bbound's definition, M_c appears as a NATURAL exponent: (50*(k+1))^{M_c} where M_c : ℕ. And log of it: log((50(k+1))^{M_c}) = M_c·log(50(k+1)) (Real.log_pow : log (x^n) = n*log x with n : ℕ cast ✓).\n\nAnd M_c ≤ J ⟹ (50(k+1))^{M_c} ≤ ... hmm — I bound log Bbound DIRECTLY: log Bbound = log(9/4) + 2L + M_c·log(50(k+1)) ≤ 1 + 2L + J·log(50(J+1)) ≤ ... For the fold I need: M_c·log(50(k+1)) ≤ J·(L+8): M_c ≤ J ✓, log(50(k+1)) ≤ L+8 ✓ (shown: 50(k+1) ≤ 4150L ⟹ log ≤ log 4150 + log L ≤ 9 + (L−1) = L+8), both nonneg (M_c ≥ 0 nat cast ✓; log(50(k+1)) ≥ log 50 > 0 ✓) ⟹ mul_le_mul ✓. Then M_bound ≤ 1+2L + J(L+8) = 1+2L+(33+66L)(L+8) = 66L²+563L+265 ≤ 420L² ✓ (the nlinarith bit).\n\nWait — one more check on the (2/5)·450 factor: BC gives 16·M·r_c²/(r_c−3/5)³. r_c² ≤ (24/25)² — r_c ≤ 24/25 ✓ (r_c ≥ 0 for pow_le_pow_left₀). (r_c−3/5)³ ≥ (8/25)³: r_c−3/5 ≥ 23/25−3/5 = 23/25−15/25 = 8/25 ✓ > 0. So 16·M·r_c²/(r_c−3/5)³ ≤ 16·M·(24/25)²/(8/25)³ = 450M. Steps: div_le_div (16Mr_c² ≤ 16M(24/25)²) ((8/25)³ ≤ (r_c−3/5)³) (pos) (nonneg) ✓ then = 450M by norm_num/ring: 16·(24/25)²/(8/25)³ = 16·576/625·15625/512 = 16·576·25/512 = 16·360000/... 576·25 = 14400; 14400/512 = 28.125; ×16 = 450 ✓ exact.\n\nThen (2/5)·450 = 180 ✓. 180·420 = 75600. 75600 + 42 = 75642 ≤ 100000 ✓.\n\nFinal statement:\n```lean\ntheorem logDeriv_riemannZeta_sub_nearZeros_le {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}\n    (hsim : s.im = t) (hσlo : 1 / 2 ≤ s.re) (hσhi : s.re ≤ 7 / 2)\n    (hs0 : riemannZeta s ≠ 0) :\n    ‖logDeriv riemannZeta s − ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖\n      ≤ 100000 * (Real.log |t|) ^ 2\n```\n\nHmm — should the constant be there or should I use ∃? D-067 says loose; explicit 100000 is honest and loose. But hmm, wait — actually let me reconsider: is there any chance 5e needs this in a different shape (e.g. on a circle of radius R with s varying)? The 5e circle argument: for s on a big circle, apply 5c at height t = im s (if |im s| ≥ 10) with the nearZeros of t... The growth bound C·(log|t|)² with |t| ≤ R+1 gives C·(log(R+1))² hmm ≤ C'·(log R)² for R ≥ ... fine, downstream can convert. The stated form is the D-067 target shape. Good.\n\nAlso — do I want `‖·‖ ≤ 100000 * (Real.log |t|)^2` or with (log(|t|))^2 vs log|t| ^ 2 — fine.\n\nNow about proof structure size: this is big. Let me organize the new code as a sequence of lemmas appended to LiDisc.lean:\n\n1. `norm_scaledZeta_le` (t, ht, z, ‖z‖ ≤ 99/100 → bound) — duplicated from jensen proof.\n2. `scaledZeta_order_ne_top_of_norm_le` (ht, ‖w‖ ≤ 1 → analyticOrderAt F w ≠ ⊤).\n3. `one_le_analyticOrderNatAt_scaledZeta` (ht, ‖w‖ ≤ 1, F w = 0 → 1 ≤ analyticOrderNatAt F w).\n4. `scaledZeroFinset t r (hr : r ≤ 1)` + `mem_scaledZeroFinset`.\n5. `scaledZeroFinset_mono` (r₁ ≤ r₂ → subset as finsets).\n6. `card_le_sum_order` (ht: card (scaledZeroFinset t r hr) ≤ Σ order) — needs orders ≥ 1: ht for ‖w‖ ≤ 1 (r ≤ 1 ✓).\n7. `sum_order_le_jensen` (ht, r ≤ 24/25: Σ order over scaledZeroFinset t r hr ≤ log((9/4)|t|²)/log(33/32)) — via mono to 24/25-finset + toFinset_inj-equality with the Jensen finset + scaledZeta_jensen_count.\n8. `exists_collection_radius` (ht → ∃ R_c ∈ [23/10, 24/10], gap) via the ×10 trick on exists_avoiding_midpoint with S := (scaledZeroFinset t (24/25) _).image (fun w => (5/2)*‖w‖)... hmm wait: exists_avoiding_midpoint needs S : Finset ℝ with card S ≤ k. S := image; k := card (scaledZeroFinset 24/25). card image ≤ card ✓. Then S10 := S.image (fun x => x*10): card ≤ card S ≤ k ✓. Apply with a := 23. T ∈ [23,24], ∀ y ∈ S10, 1/(2(k+1)) ≤ |y − T|. R_c := T/10. For w ∈ ZW96: y := 10·((5/2)‖w‖) = 25‖w‖ ∈ S10 (mem_image of mem_image). |25‖w‖ − T| ≥ 1/(2(k+1)) ⟹ |(5/2)‖w‖ − R_c| = |25‖w‖ − T|/10 ≥ 1/(20(k+1)). ✓ (|25‖w‖ − T| = 10·|(5/2)‖w‖ − T/10| via abs_mul, |10| = 10.)\n9. Bundle: `collRadius t ht := (exists_collection_radius ht).choose` + spec lemmas `collRadius_mem : 23/10 ≤ collRadius t ht ∧ collRadius t ht ≤ 24/10`, `collRadius_gap : ∀ w ∈ scaledZeroFinset t (24/25) _, 1/(20*(card+1)) ≤ |(5/2)*‖w‖ − collRadius t ht|`.\n   Hmm — with choose: `(exists_collection_radius ht).choose_spec` gives the ∃-body. ✓\n10. `rC t ht := collRadius t ht * (2/5)`; `rC_mem : 23/25 ≤ rC t ht ∧ rC t ht ≤ 24/25`; `rC_gap : ∀ w ∈ ZW96, δw ≤ |‖w‖ − rC|` where δw := 1/(50*(card+1)): from gap: |(5/2)‖w‖ − R_c| = (5/2)|‖w‖ − rC| (factor: (5/2)‖w‖ − R_c = (5/2)(‖w‖ − R_c·(2/5)) = (5/2)(‖w‖ − rC) ✓ ring; abs_mul; |5/2| = 5/2) ⟹ (5/2)|‖w‖−rC| ≥ 1/(20(k+1)) ⟹ |‖w‖−rC| ≥ (2/5)·1/(20(k+1)) = 1/(50(k+1)) ✓.\n11. `ZW` := scaledZeroFinset t (rC t ht) (rC ≤ 24/25 ≤ 1). `ZW_gap_below : w ∈ ZW → ‖w‖ ≤ rC − δw` (w ∈ ZW ⟹ w ∈ ZW96 (mono, rC ≤ 24/25) ⟹ gap; ‖w‖ ≤ rC + ... cases: |‖w‖ − rC| ≥ δw and ‖w‖ ≤ rC ⟹ ‖w‖ ≤ rC − δw ✓).\n12. `Cf` characterizations + `B_analytic` (AnalyticOnNhd on closedBall(0, (1+rC)/2)), `B_nonzero` (on closedBall(0, rC)), `B_bound_center` (log‖B 0‖ ≥ 0), `B_sphere_bound` (‖w‖ = rC → ‖B w‖ ≤ Bbound), `B_ball_bound` (closedBall(0, rC) via max-modulus).\n13. `J_B` obtain + `M_bound` def + Re-bound + BC bound: package as a lemma:\n    `∃ J_B : ℂ → ℂ, J_B 0 = 0 ∧ (∀ w ∈ closedBall 0 (3/5), deriv J_B w = deriv B w / B w) ∧ (∀ w ∈ ball 0 rC, (J_B w).re = log‖B w‖ − log‖B 0‖) ∧ (∀ w ∈ closedBall 0 (3/5), ‖deriv J_B w‖ ≤ 450 * M_bound) ∧ AnalyticOnNhd J_B (ball 0 rC)` — or just inline the obtain in the main theorem. Inline might be fine: obtain at the top of the main theorem, all facts local.\n14. Main theorem.\n\nAlso the w₀-side deriv identity could be a standalone lemma:\n`deriv_JB_eq : deriv J_B w₀ = (5/2)*logDeriv riemannZeta s − Σ_{w∈ZW} (m_w:ℂ)/(w₀−w)` — inside main proof.\n\nLet me think about what could be painful:\n(a) The Cf dite unfolding — the Classical instance: `open Classical` is at the top of StrongPNTPrefix (line 206 `open Classical`). The def Cf uses `if finite_zeros_mono : ...`. When I unfold Cf in NguyenRH1 (no `open Classical` in LiDisc?) — the instance is baked into the TERM (dite with the Classical.propDecidable instance — wait, `open Classical` makes `Classical.propDecidable` available as an instance during ELABORATION of Cf, so the dite's instance is Classical.propDecidable. When I unfold and want ↓reduceDIte to fire with my `hfin` proof, simp's ↓reduceDIte works regardless of instance (it matches `dite c ...` where c decides True-ish...). In Zeta23's own proofs they do `by_cases finite_zeros_mono : (SetOfZeros r f).Finite; simp only [finite_zeros_mono, ↓reduceDIte]` — and this works. I'll mirror exactly.\n\n(b) `analyticOrderNatAt` vs Zeta23's `ZeroFactor` — ZeroFactorization gives the factorization at zeros; I only need ZeroFactor F w ≠ 0 (from h_ρ ρ ≠ 0 + ZeroFactor F ρ = h_ρ ρ). ✓ ZeroFactorization's hypotheses: R < 1, F analytic on closedBall(0,1), F 0 ≠ 0, ρ ∈ SetOfZeros R F. With R := rC... wait it needs RleOne : R < 1 where hρ : ρ ∈ SetOfZeros R F. w ∈ ZW ⟹ w ∈ SetOfZeros (rC) F and rC < 1 ✓ (rC ≤ 24/25). But actually ZeroFactorization's signature: (RleOne : R < 1) (hfAnalytic) (hf_neq_zero_at_zero) (hρ : ρ ∈ SetOfZeros R f). Use R := rC ✓.\n\n(c) For B_nonzero at w with F w = 0 but ‖w‖ ∈ (rC, rC]... — wait closedBall(0, rC), F w = 0: is w ∈ SetOfZeros rC F? Need ‖w‖ ≤ rC ✓ and F w = 0 ✓ ⟹ yes! Oh nice — I don't even need the gap for nonvanishing ON closedBall(0, rC): F w = 0 ∧ ‖w‖ ≤ rC ⟹ w ∈ SetOfZeros directly. The GAP is needed only for: (i) sphere identity (no zeros ON the sphere for the else-branch... actually no — the else-branch needs w ∉ SetOfZeros rC F; on the sphere ‖w‖ = rC, if F w = 0 then w ∈ SetOfZeros (‖w‖ ≤ rC ✓). So sphere zeros ARE in the zero set, and Cf at them uses the if-branch. Hmm! So on the sphere, B w = ZeroFactor/prod_{≠w}, NOT F w/prod! Then ‖B w‖ = ‖ZeroFactor w‖/∏_{ρ≠w}‖w−ρ‖^m — the factor (w−w)^m is removed, but ZeroFactor w = h_w(w) with h_w(w) ≠ 0 — bounding ‖h_w(w)‖ above is NOT directly available!\n\n    Ugh. Wait — but the gap says: no zeros ON the sphere at all (zeros with ‖w‖ ≤ rC have ‖w‖ ≤ rC − δw). So on the sphere, F w ≠ 0, else-branch applies. ✓ The gap is exactly what kills this. Good — the sphere bound proceeds as planned: ∀ w, ‖w‖ = rC → F w ≠ 0 (via gap), hence B w = F w/prod, etc.\n\n    Hmm wait, one more: for the else-branch I need w ∉ SetOfZeros rC F — F w ≠ 0 suffices ✓.\n\n(d) For B_nonzero's zero-case: w ∈ SetOfZeros rC F ⟹ Cf w = ZeroFactor F w / ∏_{ρ ∈ ZW\\{w}} (w−ρ)^m. ZeroFactor ≠ 0 ✓; product: ρ ∈ ZW\\{w} ⟹ ρ ≠ w ⟹ factor ≠ 0 ✓. ✓\n\n(e) The max-modulus application: `AnalyticOn.norm_le_of_norm_le_on_sphere (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (closedBall 0 R)) (cond : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ closedBall 0 r)`. Take r := rC, R := (1+rC)/2 (need rC ≤ R ✓ since rC < 1), analytic: AnalyticOn on closedBall(0, R) from CfAnalytic (r_lt_R : rC < R ✓) (R < 1: (1+rC)/2 < 1 ⟸ rC < 1 ✓).analyticOn. cond: sphere(0, rC) = {‖z‖ = rC} (Metric.sphere 0 rC: dist z 0 = rC ⟺ ‖z‖ = rC via mem_sphere_iff_norm/sub_zero — diskBound used `rw[mem_sphere_iff_norm, sub_zero]`). ✓\n\n(f) BorelCaratheodoryDeriv needs AnalyticOn ℂ J_B (ball 0 R) — from AnalyticOnNhd J_B (ball 0 rC) .analyticOn ✓.\n\n(g) `Real.log Bbound` where Bbound := (9/4)*|t|^2*(50*(k+1))^{M_c}: log Bbound = log((9/4)*|t|²) + log((50(k+1))^{M_c}) via Real.log_mul ((9/4)|t|² ≠ 0, pow ≠ 0). log((9/4)|t|²) = log(9/4) + 2·log|t| — hmm log((9/4)·|t|²) = log(9/4) + log(|t|²) (log_mul) and log(|t|²) = 2·log|t|: Real.log_pow gives log(|t|^{2:ℕ}) = 2·log|t|... but |t|² could be written |t|^2 nat-pow ✓ (use |t|^2 with Nat pow everywhere; the Jensen bound has |t| ^ 2 — check the committed form: `Real.log ((9 / 4) * |t| ^ 2)` — |t| ^ 2 with ℕ exponent inferred ✓, and norm_riemannZeta_le_disc gives (3/4)*|t|^2. So |t|^2 nat pow ✓, Real.log_pow applies.)\n\nNow — nearZeros def and its lemmas. And `zeroMult` cast to ℂ in sums: (zeroMult ρ : ℂ).\n\nThe final sum identity chain in the main proof:\n```\nlogDeriv ζ s = (2/5)·deriv J_B w₀ + Σ_{w∈ZW} (m_w : ℂ)/(s − aff w)     (★)\nΣ_{w∈ZW} (m_w:ℂ)/(s−aff w) = Σ_{ρ∈ZW.image aff} (zeroMult ρ:ℂ)/(s−ρ)   (sum_image + order-inv)\nΣ_image = Σ_near + Σ_extras                                              (sum_sdiff)\n```\nFor (★): from deriv J_B w₀ = (5/2)·logDeriv ζ s − Σ_{w∈ZW} m_w/(w₀−w):\n(5/2)·logDeriv ζ s = deriv J_B w₀ + Σ m/(w₀−w); multiply by 2/5: logDeriv ζ s = (2/5)deriv J_B + (2/5)Σ m/(w₀−w) = (2/5)deriv J_B + Σ (2/5)·m/(w₀−w) (Finset.mul_sum) and per-term (2/5)·m/(w₀−w) = m/(s−aff w) (hws identity). ✓\n\nThen ‖logDeriv ζ s − Σ_near‖ = ‖(2/5)deriv J_B + Σ_extras‖ ≤ (2/5)‖deriv J_B‖ + ‖Σ_extras‖ ≤ (2/5)·450·M_bound + Σ_extras ‖(m:ℂ)/(s−ρ)‖ ≤ 180·M_bound + Σ_extras m.\n\nΣ_extras m (as ℝ): Σ_{ρ∈extras} (zeroMult ρ : ℝ) ≤ Σ_{ρ∈image} (zeroMult ρ : ℝ) = (M_c : ℝ)?? hmm: Σ_{ρ∈image} zeroMult ρ = Σ_{w∈ZW} zeroMult (aff w) = Σ_{w∈ZW} m_w = M_c ✓ (sum_image with g := fun ρ => (zeroMult ρ : ℝ)). Then ≤ J. Careful with nat vs real casts: keep sums in ℝ via casts and push_cast where needed. Actually simpler: do everything with (zeroMult ρ : ℂ) terms; the extras bound: ‖(m:ℂ)/(s−ρ)‖ = m/‖s−ρ‖ ≤ m (as real: (m:ℝ)/‖s−ρ‖ ≤ m since ‖s−ρ‖ ≥ 1: div_le_of_le_mul? m/‖s−ρ‖ ≤ m/1 = m via div_le_div_of_nonneg_left (m nonneg) (‖s−ρ‖ ≥ 1 > 0) (1 ≤ ‖s−ρ‖): `div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a / c ≤ a / b` — with b := 1: a/‖s−ρ‖ ≤ a/1 = a ✓). Then Σ ≤ Σ m (norm cast: ‖(m:ℂ)‖ = m since m ≥ 0: Complex.norm_natCast? `Complex.norm_natCast : ‖(n : ℂ)‖ = n` ✓ (RCLike.norm_natCast)). \n\nOK — I'm confident in the plan. One more piece: the FINAL fold nlinarith chains. To minimize pain, structure the fold as a standalone real-number lemma:\n\n```lean\ntheorem loose_fold {L M k : ℝ}... \n```\nHmm — variables entangled (M_c ≤ J, k ≤ J...). Let me instead do the fold stepwise with explicit haves inside the main proof. The non-linear parts:\n(i) log(33/32) ≥ 1/33: from Real.one_sub_inv_le_log_of_pos (33/32 > 0): 1 − (33/32)⁻¹ = 1 − 32/33 = 1/33 ✓ (norm_num).\n(ii) J := 33+66L bound: log((9/4)|t|²) ≤ 1+2L: log((9/4)|t|²) = log(9/4) + 2L; log(9/4) ≤ 1 ⟸ 9/4 ≤ exp 1 ⟸ (exp_one_gt_d9: 2.7182818283 < e?) — check the name used in LiContour: `Real.exp_one_lt_d9.le` — exp_one_lt_d9 : exp 1 < 2.7182818286? and exp_one_gt_d9 : 2.7182818283 < exp 1. LiContour used exp_one_lt_d9 for e < 2.7182818286... they wrote `Real.exp_one_lt_d9.le` in context: `he := Real.exp_one_lt_d9.le; linarith` where they needed 3 ≤ e? Their hlog needed t+2 ≥ 3 > e... they used exp_one_lt_d9.le : e ≤ 2.7182818286 then linarith with 3... wait that gives e < 3 ⟹ log 3 > ... hmm whatever — both directions exist as _gt_d9/_lt_d9. For 9/4 ≤ e: 9/4 = 2.25 ≤ 2.7182818283 ≤ e via exp_one_gt_d9. Then log(9/4) ≤ log e = 1: Real.log_le_log (0 < 9/4) (9/4 ≤ exp 1) gives log(9/4) ≤ log (exp 1) = 1 (Real.log_exp 1 hmm Real.exp_log... `Real.log_exp : log (exp x) = x` ✓).\n(iii) div: M96(ℝ) ≤ log((9/4)|t|²)/log(33/32) ≤ (1+2L)/(1/33) = 33(1+2L): div_le_div (num ≤ 1+2L) (1/33 ≤ log(33/32)) (1/33 > 0) (0 ≤ num): num = log((9/4)|t|²) ≥ 0 ⟸ (9/4)|t|² ≥ 1 ⟸ |t|² ≥ 100 ≥ 4/9 ⟸ |t| ≥ 10 ✓ (Real.log_nonneg: 1 ≤ x → 0 ≤ log x ✓). (1+2L)/(1/33) = 33+66L by field_simp/ring. So J-bound: (M96:ℝ) ≤ 33+66L.\n(iv) k+1 ≤ J+1: k ≤ M96 (nat ≤, cast) ⟹ (k:ℝ)+1 ≤ J+1.\n(v) 50(k+1) ≤ 4150L: 50(J+1) = 50(34+66L) = 1700+3300L ≤ 4150L ⟺ 1700 ≤ 850L ⟺ L ≥ 2 ✓. nlinarith.\n(vi) log(50(k+1)) ≤ L+8: 50(k+1) > 0; 50(k+1) ≤ 4150L; log(4150L) = log 4150 + log L (log_mul, L > 0); log 4150 ≤ 9: 4150 ≤ exp 9: exp 9 = (exp 1)^9 (Real.exp_nat_mul: exp (n*x) = (exp x)^n — exp 9 = exp (9*1); 9*1: norm_num; = (exp 1)^9 ≥ 2.7182818283^9 ≥ 4150: norm_num computes 2.7182818283^9 — big rational but norm_num should… 2.7182818283^9: numerator ~2.7e9...^9 — the integers involved: 27182818283^9 ≈ 10^94. norm_num can do this but might be slow. Alternative: 4150 ≤ 3^9 = 19683? No wait — need exp 9 ≥ 4150, and exp 9 ≥ (2.7)^9? 2.7^9 = 3325.3 < 4150 ✗. 2.71^9 = 7883.8 ≥ 4150 ✓ — 2.71^9: 271^9 ≈ 7.8e21 — norm_num fine. Use exp_one_gt_d9 (2.7182818283 < e): then e^9 > 2.7182818283^9 — even bigger rational (11-digit). Hmm. To be safe, derive a coarser decimal: e ≥ 2.71 via exp_one_gt_d9 (2.718... > 2.71 by norm_num) — then e^9 ≥ 2.71^9 via pow_le_pow_left₀ (2.71 ≥ 0). 2.71^9 as rational (271/100)^9 — norm_num: (271/100)^9 = 271^9/100^9; 271^9 = ? 271² = 73441; 271³ = 19,902,511; 271⁴ = 5.393e9; 271⁹ = 271·(271⁴)² = 271·2.909e19 = 7.883e21. 100^9 = 1e18. Ratio ≈ 7883.7 ≥ 4150 ✓ norm_num can verify. OK.\n   Then log(4150L) ≤ 9 + log L ≤ 9 + (L − 1) = L + 8 — log L ≤ L−1: Real.log_le_sub_one_of_pos (L > 0): log L ≤ L − 1 ✓.\n(vii) M_bound ≤ 420L²: M_bound = log Bbound ≤ (1+2L) + J·(L+8): need J ≥ 0 (33+66L, L ≥ 2 ✓) and log(50(k+1)) ≤ L+8, M_c ≤ J... M_c·log(50(k+1)) ≤ J·(L+8) via mul_le_mul (M_c ≤ J) (log ≤ L+8) (log ≥ 0) (J ≥ 0) ✓. Then 1+2L+(33+66L)(L+8) ≤ 420L²: expand: 1+2L+33L+264+66L²+528L = 66L²+563L+265 ≤ 420L² ⟺ 354L²−563L−265 ≥ 0, at L ≥ 2. nlinarith [hL: 2 ≤ L]: witness (L−2)(354L+131) + (14L−3)... earlier computed = 354L²−577L−262+(14L−3) hmm: (L−2)(354L+131) = 354L²+131L−708L−262 = 354L²−577L−262. Target minus this: (354L²−563L−265) − (354L²−577L−262) = 14L−3 ≥ 0 since L ≥ 2 ⟹ 14·2−3 = 25 ≥ 0 ✓. So target = (L−2)(354L+131) + (14L−3) ≥ 0 + 25 > 0. nlinarith [hL] with products (L−2)(354L+131) — nlinarith multiplies hypotheses pairwise: needs (L−2) ≥ 0 and (354L+131) ≥ 0: nlinarith [hL, mul_nonneg (sub_nonneg.mpr hL) (by linarith : (0:ℝ) ≤ 354*L+131)]... provide the product as a hint. ✓\n(viii) BC factor ≤ 450: 16·M·r_c²/(r_c−3/5)³ ≤ 450·M ⟸ r_c² ≤ (24/25)² (r_c ≥ 0, ≤ 24/25, pow_le_pow_left₀), (r_c−3/5)³ ≥ (8/25)³ (r_c−3/5 ≥ 8/25 > 0, pow_le_pow_left₀), M > 0: div_le_div (16·M·r_c² ≤ 16·M·(24/25)²: mul_le_mul_of_nonneg_left (pow) (16M ≥ 0)) ((8/25)³ ≤ (r_c−3/5)³) (pos (8/25)³) (nonneg 16Mr_c²) : gives 16Mr_c²/(r_c−3/5)³ ≤ 16M(24/25)²/(8/25)³ = 450M: norm_num: 16·(24/25)²/(8/25)³ = 450 ✓ then mul_assoc massaging.\n(ix) final: 180·M_bound + J ≤ 100000L²: 180·420L² = 75600L²; J ≤ 42L² (33+66L ≤ 42L² ⟺ 42L²−66L−33 ≥ 0 at L ≥ 2: = (L−2)(42L+16.5)+1.5L... check: (L−2)(42L+17) = 42L²+17L−84L−34 = 42L²−67L−34; target minus = (42L²−66L−33)−(42L²−67L−34) = L+1 ≥ 0 ✓). So 75600L²+42L² = 75642L² ≤ 100000L² (L² ≥ 0: mul_le_mul_of_nonneg_right) ✓.\n\nAlright. Also `abs_im_le_norm` : |z.im| ≤ ‖z‖ ✓ used already in file.\n\nOne more consideration: `nearZeros t` def + API:\n```lean\ndef nearZeros (t : ℝ) : Finset ℂ := (zeroDiscFinset t).filter fun ρ => |ρ.im - t| < 1\ntheorem mem_nearZeros {t : ℝ} {ρ : ℂ} : ρ ∈ nearZeros t ↔ ρ ∈ zeroDiscFinset t ∧ |ρ.im − t| < 1 := Finset.mem_filter\n```\n✓ trivial.\n\nAnd the application: ρ ∈ nearZeros t ⟹ ρ ∈ ZW.image aff: needs ‖ρ − s₀‖ ≤ √5 etc. Steps: ρ ∈ zeroDiscFinset ⟹ zeroDisc_isNontrivial ⟹ re ∈ (0,1) (IsNontrivialZero fields: ⟨ζ ρ = 0, 0 < re, re < 1⟩? check IsNontrivialZero def — from zeroDisc_isNontrivial's construction: exact ⟨h2, hpos, hnot1⟩ — three components: ζ ρ = 0, 0 < ρ.re, ρ.re < 1 ✓). ‖ρ − s₀‖² = (ρ.re−2)² + (ρ.im−t)²: compute via normSq: Complex.normSq (ρ − s₀) = (ρ.re−2)² + (ρ.im−t)² (sub_re, s₀ re = 2, im = t: discCenter t = 2 + t·I: add_re, mul_re... simp [discCenter]). Then ≤ 4+1 = 5: |ρ.re−2| ≤ 2 ⟸ ρ.re ∈ (0,1); (ρ.re−2)² ≤ 4 (sq_le_sq₀... or nlinarith with abs bounds); (ρ.im−t)² ≤ 1 ⟸ |ρ.im−t| < 1 (sq_le... abs_lt ⟹ −1 < .. < 1 ⟹ sq ≤ 1: nlinarith or sq_le_one_of_abs... use nlinarith [abs_lt.mp h]). Then ‖ρ−s₀‖ = √(normSq) ≤ √5: Complex.norm_eq_sqrt_normSq? hmm — `Complex.normSq_eq_norm_sq : normSq z = ‖z‖ ^ 2` so ‖z‖² ≤ 5 ⟹ ‖z‖ ≤ √5 via (sq_le_sq₀ nonneg (√5 ≥ 0)).mp: ‖z‖² ≤ (√5)² = 5 (Real.sq_sqrt 5 ≥ 0) ⟹ ‖z‖ ≤ √5. ✓ Then √5 ≤ 23/10: Real.sqrt_le_iff or sq: (√5)² = 5 ≤ (23/10)² = 529/100 ✓ norm_num; via Real.sqrt_le_left? `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2`? I think `Real.sqrt_le_iff : Real.sqrt x ≤ y ↔ 0 ≤ y ∧ x ≤ y^2` exists (with hy?) — there are several variants: Real.sqrt_le_iff (hy : 0 ≤ y)? no wait. `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2`?? Hmm, in recent Mathlib: `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2` — I'll try; fallback `Real.sqrt_le_sqrt` + show √5 = ... no. Or: sq_le_sq₀: √5 ≤ 23/10 ⟺ (√5)² ≤ (23/10)² via (sq_le_sq₀ (Real.sqrt_nonneg) (by norm_num)).mpr? hmm sq_le_sq₀ : 0 ≤ a → 0 ≤ b → (a² ≤ b² ↔ a ≤ b)? `sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b` ✓ (used already in LiContour). Then 5 ≤ 529/100 by Real.sq_sqrt + norm_num. ✓\n\nThen w_ρ := (2/5)·(ρ − s₀): aff w_ρ = ρ (ring ✓), ‖w_ρ‖ = (2/5)‖ρ−s₀‖ ≤ (2/5)(23/10) = 23/25 ≤ rC ✓. F w_ρ = ζ(ρ)/ζ(s₀) = 0 ✓ (num zero). So w_ρ ∈ SetOfZeros (rC) F ⟹ w_ρ ∈ ZW. ρ = aff w_ρ ∈ image: Finset.mem_image.mpr ⟨w_ρ, mem, aff w_ρ = ρ⟩ ✓.\n\nHmm wait — nearZeros ⊆ image requires ht only through... the gap/B machinery? No: nearZeros ⊆ ZW.image aff needs: ζ(ρ) = 0 (from zeroDiscFinset ✓ no ht), ζ(s₀) ≠ 0 (F w = 0 conclusion — zeta_lower_bound_two, no ht ✓), ‖w_ρ‖ ≤ rC — via √5 ≤ 23/10... wait rC ≥ 23/25 and ‖w_ρ‖ ≤ 23/25 ✓ — but rC's lower bound 23/25 comes from collRadius spec which needs... exists_collection_radius ht — hmm does the gap construction need ht? The gap exists for ANY t (combinatorial); ht only entered via... exists_avoiding_midpoint is unconditional; S/card fine. So exists_collection_radius doesn't need ht! Only the Jensen-related numeric bounds (card ≤ J etc.) need ht. But keeping ht uniformly is simpler — the final theorem has ht anyway. Fine, keep ht in the def bundle.\n\nWait, actually — there IS a subtlety: scaledZeroFinset t r hr uses scaledZeta_zeros_finite which needs... nothing (proved for all t ✓). Good.\n\nBut — one thing: ZW and the gap lemmas need rC > 0? For ZW ⊆ ZW96 need rC ≤ 24/25 ✓. Fine.\n\nAlso B's analyticity needs rC < R' < 1 with R' := (1+rC)/2: rC < (1+rC)/2 ⟺ rC < 1 ✓; (1+rC)/2 < 1 ✓.\n\nAlright — also the deriv identity needs F's differentiability at w₀: from scaledZeta_analytic ht (AnalyticOnNhd on closedBall(0,1)): w₀ ∈ closedBall(0, 3/5) ⊆ closedBall(0,1) ⟹ AnalyticAt F w₀ ⟹ .differentiableAt ✓.\n\nAnd logDeriv_div for F/P at w₀ needs DifferentiableAt F w₀ ✓ and DifferentiableAt P w₀ (analyticAt_finset_prod_sub_pow .differentiableAt ✓).\n\nThe EventuallyEq for B = F/P near w₀: \n```lean\nhave hB_eq : B =ᶠ[𝓝 w₀] fun w => scaledZeta t w / P w\n```\nproof: w₀ ∉ SetOfZeros rC F (F w₀ ≠ 0) ⟹ complement open? SetOfZeros rC F = {‖ρ‖ ≤ rC ∧ F ρ = 0} — is it closed? F restricted to closedBall(0,1) is continuous (analytic), so {F = 0} ∩ closedBall(0, rC) is closed: isClosed (closedBall) ∩ (preimage of {0} under continuous-on...). Simpler: SetOfZeros rC F ⊆ ZW-carrier?? No — SetOfZeros rC F = ZW.carrier as SETS (ZW := finite.toFinset, mem ⟺ ∈). ZW.carrier = ↑ZW is closed (Finset carrier finite ⟹ closed: `Finite.isClosed` with (ZW : Set ℂ) finite — `Finset.finite_toSet` then `.isClosed` ✓). And SetOfZeros rC F = ↑ZW: ext: x ∈ SetOfZeros ⟺ x ∈ ZW (mem_scaledZeroFinset) ⟺ x ∈ ↑ZW (Finset.mem_coe). ✓ So complement of SetOfZeros = complement of ↑ZW is open, contains w₀: gives ∀ᶠ z, z ∉ SetOfZeros rC F (isOpen_compl.mem_nhds... `IsOpen.mem_nhds : IsOpen s → a ∈ s → s ∈ 𝓝 a` then eventually). Combined with F z ≠ 0 eventually (F.continuousAt w₀ .eventually_ne (F w₀ ≠ 0)). For z with both: Cf rC F z = F z / P z — by the else-characterization lemma (Cf_eq_div_prod) ✓. So EventuallyEq via Filter.Eventually.of_forall... wait need eventually: filter_upwards [compl_eventually, F_eventually_ne] with z hz1 hz2; exact Cf_eq_div_prod rC_le_1 hz1. ✓\n\nwhere P := fun w => ∏ ρ ∈ ZW, (w − ρ) ^ analyticOrderNatAt (scaledZeta t) ρ.\n\nThen deriv J_B w₀ = deriv B w₀ / B w₀ (hJderiv w₀ mem) — and deriv B w₀ = deriv (F/P) w₀ (hB_eq.deriv), B w₀ = (F/P) w₀ (hB_eq.eq_of_nhds — check name: `Filter.EventuallyEq.eq_of_nhds : f =ᶠ[𝓝 x] g → f x = g x`? I believe it's `Filter.EventuallyEq.eq_of_nhds` ✓).\n\nderiv (F/P) w₀ / (F/P) w₀ = logDeriv (fun w => F w / P w) w₀ (logDeriv def: logDeriv f x = deriv f x / f x — `logDeriv_apply`? logDeriv f = fun x => deriv f x / f x by def — rfl after `rw [logDeriv_apply]`? The def: `logDeriv f := fun x ↦ deriv f x / f x` hmm might be `deriv f x / f x` directly — `logDeriv_apply : logDeriv f x = deriv f x / f x` simp lemma ✓).\n\nSo deriv J_B w₀ = logDeriv (F/P) w₀ = logDeriv F w₀ − logDeriv P w₀ (logDeriv_div w₀ (F w₀ ≠ 0) (P w₀ ≠ 0) (diffF) (diffP)) = (5/2)·logDeriv ζ s − Σ m/(w₀−·). \n\nlogDeriv F w₀: F = scaledZeta t = fun w => ζ(aff w)/c. logDeriv_div w₀ (g w₀ ≠ 0: ζ(s) ≠ 0 ✓) (c ≠ 0 ✓) (diff g: comp) (diff const): = logDeriv (ζ∘aff) w₀ − logDeriv (fun _ => c) w₀. logDeriv of const: deriv const = 0 ⟹ logDeriv = 0/c = 0: `logDeriv_const`? If exists: simp. Else: rw [logDeriv_apply, deriv_const, zero_div, sub_zero]. Then logDeriv (ζ ∘ aff) w₀: logDeriv_comp (diff ζ at aff w₀) (diff aff): logDeriv ζ (aff w₀) * deriv aff w₀. Hmm — but careful: (fun w => riemannZeta (aff w)) vs (riemannZeta ∘ aff): logDeriv_comp is stated for f ∘ g; (fun w => ζ (aff w)) is defeq to ζ ∘ aff — may need `show` conversion. deriv aff w₀ = 5/2: aff w = s₀ + (5/2)*w: deriv_const_add + deriv_const_mul (c) (hd : DifferentiableAt _ id) hmm `deriv_const_mul (c : 𝕜) (hd : DifferentiableAt 𝕜 f x) : deriv (fun x => c * f x) x = c * deriv f x` ✓ + deriv_id'' (deriv id x = 1: `deriv_id'`? Actually `deriv_id''`? I recall `deriv_id' : deriv id = fun _ => 1`... hmm deriv_id' might be `deriv id x = 1`? There are `deriv_id'` and `deriv_id''` variants. Fallback: (hasDerivAt_id x).deriv : deriv id x = 1 via HasDerivAt.deriv (hasDerivAt_id'?) — `hasDerivAt_id : HasDerivAt id 1 x`? hmm `hasDerivAt_id (x) : HasDerivAt id 1 x` hmm maybe `hasDerivAt_id'`... I know `HasDerivAt.deriv : HasDerivAt f f' x → deriv f x = f'` ✓. And (hasDerivAt_id w₀) — the name `hasDerivAt_id` exists? `hasDerivAt_id'`? Both exist in some form; simp can close `deriv (fun w : ℂ => w) w₀ = 1`? `deriv_id'` simp. I'll use simp [deriv_const_add, deriv_const_mul, deriv_id'']-style and fix at build.)\n\nOK. This is a huge but well-understood build. Let me also decide the ordering: lemmas first, main theorem last. Also, since LiDisc.lean already ends with `end NguyenRH1 / end`, I'll append before those.\n\nLet me also double-check `Finset.sum_image` signature: `Finset.sum_image (h : ∀ x ∈ s, ∀ y ∈ s, f x = f y → g x = g y)` : ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x) — the hypothesis form is InjOn-style. journal-011 gotcha: \"Finset.sum_image takes Set.InjOn, map = g, summand = f\" — hmm that suggests this Mathlib version's sum_image takes Set.InjOn. Fine, provide Set.InjOn.\n\nCheck: does `Finset.sum_image` in current Mathlib have signature `(h : Set.InjOn f s) : ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x)`? In recent Mathlib yes: `Finset.sum_image (h : Set.InjOn f s) : (∑ x ∈ s.image f, g x) = ∑ x ∈ s, g (f x)`. I'll adapt.\n\nNow — one more design point for the fold: the M_c (exponent in Bbound) is Σ over ZW of analyticOrderNatAt F — a natural. In the sphere bound I'll write Bbound := (9/4)*|t|^2 * (50*(k+1))^(M_c) with M_c := ∑ ρ ∈ ZW, analyticOrderNatAt (scaledZeta t) ρ (ℕ). Then log: log(Bbound) = log(9/4) + 2L + (M_c : ℝ)·log(50(k+1)) (Real.log_pow gives ↑(M_c) * log ✓).\n\nk := (scaledZeroFinset t (24/25) _).card. But note: scaledZeroFinset t (24/25) _ has a PROOF argument (hr : 24/25 ≤ 1) — proof irrelevance makes card independent ✓ but definitional equalities across different proof terms are fine (Subsingleton elimination — proof args are irrelevant definitionally for Prop). OK.\n\nWait, one issue — `scaledZeroFinset t r (hr : r ≤ 1)` with hr a proof: `scaledZeroFinset t (24/25) (by norm_num)` and inside Cf-unfolds I get `finite_zeros_mono.toFinset` where the proof is the dite-introduced one. My Cf_eq lemma will use toFinset_inj.mpr rfl to equate. Then the product over my finset. ✓\n\nActually hold on, let me reconsider: rather than a proof-carrying def, maybe define scaledZeroFinset via Set.Finite.toFinset of a direct finiteness proof without the r ≤ 1 hypothesis... The issue: SetOfZeros r F for r > 1 is NOT known finite (analyticity only on closedBall(0,1)). Keep the hypothesis. All my uses have r ≤ 24/25 or rC ≤ 24/25. OK.\n\nAlso `Finset.card_image_le` for card S ≤ card ZW96 — image under (fun w => (5/2)*‖w‖): card_image_le : (s.image f).card ≤ s.card ✓.\n\nNow write the code. I'll write it in chunks and compile iteratively. Given the size, let me write §5 (norm_scaledZeta_le through the gap machinery) first, compile, then §6 (Cf char + B lemmas), compile, then §7 (main theorem).\n\nActually, let me reconsider ONE more time whether there's a shortcut for the whole B-nonvanishing/bound complex... The alternative \"blended\" approach: skip Cf entirely and use BlaschkeB?? No — BlaschkeB includes the Blaschke factors whose log-deriv is messier. The Cf approach is the Davenport one per design. Proceed.\n\nAlso — STATE.md says \"g := ζ/∏(s−ρₖ)^{mₖ}\" and my approach uses Cf r_c F in scaled coords. deriv log of Cf at w₀ = (5/2)logDeriv ζ(s) − Σ m/(w₀−ρ). The unscaled g's log deriv at s would be logDeriv ζ s − Σ m/(s−ρ). Consistent ✓.\n\nLet me now also double-check the definition `SetOfZeros r f = {ρ | ‖ρ‖ ≤ r ∧ f ρ = 0}` ✓ (line 194). And `finiteSetOfZeros_mono` needs r < 1 — for ZW96 I use r = 24/25 < 1 ✓ in scaledZeta_jensen_count's statement. For my scaledZeroFinset with hr : r ≤ 1 — defined via subset of SetOfZeros 1 — fine. But for consistency with the Jensen finset equality (step 7), scaledZeroFinset t (24/25) (by norm_num) vs (finiteSetOfZeros_mono (by norm_num : (24/25:ℝ) < 1) scaledZeta_zeros_finite).toFinset — toFinset_inj.mpr rfl where the SETS: my subset-derived finite's underlying set: SetOfZeros (24/25) F (the .subset proof: `scaledZeta_zeros_finite.subset (fun w hw => ⟨hw.1.trans hr, hw.2⟩)` : (SetOfZeros (24/25) F).Finite — hmm Set.Finite.subset (hs : s.Finite) (hts : t ⊆ s) : t.Finite — so `.subset` on scaledZeta_zeros_finite : (SetOfZeros 1 F).Finite with subset proof SetOfZeros (24/25) ⊆ SetOfZeros 1 gives (SetOfZeros (24/25) F).Finite ✓ set is right. rfl : SetOfZeros (24/25) F = SetOfZeros (24/25) F ✓. toFinset_inj : hs.toFinset = ht.toFinset ↔ s = t — with s = t = SetOfZeros (24/25) F: mpr rfl : hs.toFinset = ht.toFinset ✓.\n\nGreat. Now the scaledZeta_jensen_count statement: the sum is over `(finiteSetOfZeros_mono (f := scaledZeta t) (r := 24 / 25) (by norm_num) (scaledZeta_zeros_finite)).toFinset` — note the implicit (r_lt_one : 24/25 < 1)? finiteSetOfZeros_mono {r} {f} (r_lt_one : r < 1) (finiteZeros : (SetOfZeros 1 f).Finite) : (SetOfZeros r f).Finite. In the committed code: `finiteSetOfZeros_mono (f := scaledZeta t) (r := 24 / 25) (by norm_num) (scaledZeta_zeros_finite)` ✓.\n\nSo Jensen-finset equality:\n```lean\ntheorem scaledZeroFinset_24_25_eq (t : ℝ) :\n    scaledZeroFinset t (24/25) (by norm_num) =\n      (finiteSetOfZeros_mono (f := scaledZeta t) (r := 24/25) (by norm_num)\n        scaledZeta_zeros_finite).toFinset :=\n  Set.Finite.toFinset_inj.mpr rfl\n```\n✓ (probably needs the def unfolded — toFinset_inj.mpr rfl : hs.toFinset = ht.toFinset where hs, ht are the two finiteness proofs — the LHS def: (scaledZeta_zeros_finite.subset ...).toFinset — matches scaledZeroFinset t (24/25) _ by rfl of the def ✓ hopefully direct).\n\nNow sum monotonicity: for r ≤ 24/25: scaledZeroFinset t r hr ⊆ scaledZeroFinset t (24/25) _ as finsets: Finset.subset via mem ⟹ mem: w ∈ ZW(r) ⟹ ‖w‖ ≤ r ≤ 24/25 ∧ F w = 0 ⟹ w ∈ ZW96 ✓. `Finset.sum_le_sum_of_subset_of_nonneg (hsub : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 0 ≤ f i)` : ∑ i in s, f i ≤ ∑ i in t, f i ✓ — orders nonneg (Nat.cast_nonneg or zero_le for ℕ: the sum is in ℕ? Σ of analyticOrderNatAt is ℕ — Jensen RHS is ℝ: committed statement: `∑ ρ ∈ ..., analyticOrderNatAt (scaledZeta t) ρ ≤ Real.log (...) / Real.log (...)` — so ℕ ≤ ℝ via Nat.cast_le? The ≤ there is... LHS : ℕ, RHS : ℝ — hmm, is there a coercion? In the committed line 352-355: `∑ ρ ∈ (...).toFinset, analyticOrderNatAt (scaledZeta t) ρ ≤ Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32)` — for this to typecheck, the sum must be coerced: there's likely a Nat.cast inserted (ℕ literal ≤ ℝ ⟹ Lean inserts ↑). And ZerosBound's conclusion: `∑ ... analyticOrderNatAt f ρ ≤ 1 / Real.log (R/r) * Real.log B` — same coercion. So the comparison is in ℝ with Nat.cast. ✓ So sum_le_sum_of_subset in ℕ then cast, or directly in ℝ with cast sums. I'll do ℕ-side: (Σ_{ZW} order : ℕ) ≤ (Σ_{ZW96} order : ℕ) then Nat.cast_le.trans jensen. Finset.sum_le_sum_of_subset_of_nonneg in ℕ: hf : 0 ≤ order ✓ (zero_le). ✓\n\nCard ≤ sum: (ZW.card : ℕ) = Σ_{w∈ZW} 1 ≤ Σ order (Finset.sum_le_sum: each 1 ≤ order — needs the one_le lemma with ht and ‖w‖ ≤ r ≤ 1 ✓). Then (k:ℝ) ≤ (Σ96 : ℝ) ≤ J.\n\nLet me now write all the code. I'll write it in one big chunk but compile in stages — actually, given the size, let me write §A–§C (through exists_collection_radius) first.\n\nNote the file's existing header imports: `import Mathlib / import Zeta23.FromPNTPlus.StrongPNTPrefix / import NguyenRH1.LiRBound`. Need to add `import NguyenRH1.LiContour` (for exists_avoiding_midpoint + ZeroCountProp not needed... just exists_avoiding_midpoint). LiContour imports Zeta23.Statement (zeroMult) ✓ and LiSides etc. And zeroMult comes via Zeta23.Statement — LiContour re-exports? Import chain: LiContour imports Zeta23.Statement — importing LiContour gives access to its imports' decls ✓.\n\nAlso `logDeriv` needs... Mathlib's LogDeriv is in Mathlib.Analysis.Calculus.LogDeriv — included in `import Mathlib` ✓.\n\nWrite chunk 1 now: helpers + gap.\n\n```lean\n/-! ## 5. The (9/4)|t|² bound as a standalone lemma, order helpers -/\n\n/-- The ii′-5b disc bound transferred to the scaled function (extracted\nfrom the Jensen-count proof for reuse in the |g| outer-circle bound). -/\ntheorem norm_scaledZeta_le {t : ℝ} (ht : 10 ≤ |t|) {z : ℂ} (hz : ‖z‖ ≤ 99 / 100) :\n    ‖scaledZeta t z‖ ≤ (9 / 4) * |t| ^ 2 := by\n  ... (copy of hB body)\n```\n\nThen order helpers:\n\n```lean\ntheorem scaledZeta_order_ne_top {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ} (hw : ‖w‖ ≤ 1) :\n    analyticOrderAt (scaledZeta t) w ≠ ⊤ := by\n  have hfAn := scaledZeta_analytic ht\n  have h0mem : (0 : ℂ) ∈ Metric.closedBall 0 1 := by\n    rw [Metric.mem_closedBall, dist_zero_right, norm_zero]; norm_num\n  have hwmem : w ∈ Metric.closedBall 0 1 := by\n    rwa [Metric.mem_closedBall, dist_zero_right]\n  have hord0 : analyticOrderAt (scaledZeta t) 0 = 0 := by\n    rw [analyticOrderAt_eq_zero]\n    exact Or.inr (Or.inr ...)  -- hmm: analyticOrderAt_eq_zero : order = 0 ↔ ¬AnalyticAt ∨ f z₀ ≠ 0\n```\nanalyticOrderAt_eq_zero : analyticOrderAt f z₀ = 0 ↔ ¬ AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0. F 0 = 1 ≠ 0: Or.inr (by rw [scaledZeta_zero]; exact one_ne_zero). Then:\n```lean\n  exact hfAn.analyticOrderAt_ne_top_of_isPreconnected Metric.isPreconnected_closedBall h0mem hwmem (by rw [hord0]; exact ENat.top_pos ... )\n```\nZeroFactorization used: `(lt_top_iff_ne_top.mp ?_); rw[orderAtZeroIsZero]; exact ENat.top_pos` — the arg is `analyticOrderAt f 0 < ⊤`... signature: AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected (hf : AnalyticOnNhd ℂ f s) (hs : IsPreconnected s) (hz₀ : z₀ ∈ s) (hz : z ∈ s) (h : analyticOrderAt f z₀ < ⊤) : analyticOrderAt f z ≠ ⊤. In ZeroFactorization they passed `(lt_top_iff_ne_top.mp ?_)` — hmm that's converting ne_top to lt_top... wait: they want to produce the hypothesis `analyticOrderAt f 0 < ⊤`: `lt_top_iff_ne_top.mp ?_` where ?_ : analyticOrderAt f 0 ≠ ⊤ — and they proved ≠ ⊤ by rw[orderAtZeroIsZero]; ENat.top_pos?? Hmm ENat.top_pos : 0 < ⊤... that's lt not ne. Confusing; probably: after rw [orderAtZeroIsZero], goal analyticOrderAt... wait they rewrote the GOAL (which was inside lt_top_iff_ne_top.mp ?_ so ?_ : analyticOrderAt f 0 ≠ ⊤)... rw turns it into (0 : ℕ∞) ≠ ⊤, and `ENat.top_pos`?? that doesn't match. Probably they used `ENat.top_pos` loosely and it elaborated via zero_ne_top or something. Let me just use: after rw [hord0]: goal (0:ℕ∞) ≠ ⊤ → `ENat.zero_ne_top`? hmm that's for... In ENat, (0 : ℕ∞) ≠ ⊤: `ENat.zero_ne_top`? exists? There's `ENat.natCast_ne_top`, `ENat.top_ne_zero`... For 0 ≠ ⊤: `ne_of_lt (ENat.top_pos ...)`? whatever — `ENat.zero_ne_top` might not exist; use `ENat.top_ne_zero.symm`? Hmm: `ENat.top_ne_zero : ⊤ ≠ 0`? then .symm? ≠ is symmetric: `Ne.symm`. Or `by simp`? At build time: try `exact ENat.natCast_ne_top 0` after showing (0:ℕ∞) = ((0:ℕ):ℕ∞) hmm. Simplest robust: `intro hcon; rw [hord0] at hcon; exact ENat.top_ne_zero ...`. I'll write `by rw [hord0]; exact fun h => ENat.zero_ne_top h`... let me check: does ENat.zero_ne_top exist? Hmm. There's `ENat.top_ne_zero : (⊤ : ℕ∞) ≠ 0`?? I don't remember. Safe: `Ne.symm ENat.top_ne_zero`? Ugh. Simplest bulletproof: after rw [hord0], `simp` should close (0 : ℕ∞) ≠ ⊤. Or `decide`? ℕ∞ has DecidableEq? Classical. `exact WithTop.zero_ne_top`? ℕ∞ = WithTop ℕ! `WithTop.zero_ne_top : (0 : WithTop ℕ) ≠ ⊤`? I believe `WithTop.zero_ne_top` exists ✓ (needs Zero). And ℕ∞ is defeq WithTop ℕ. ZeroFactorization actually used ENat.top_pos... whatever, I'll try WithTop.zero_ne_top first, fallback simp.\n\nThen one_le:\n```lean\ntheorem one_le_analyticOrderNatAt_scaledZeta {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n    (hw : ‖w‖ ≤ 1) (hw0 : scaledZeta t w = 0) :\n    1 ≤ analyticOrderNatAt (scaledZeta t) w := by\n  have htop := scaledZeta_order_ne_top ht hw\n  have hne : analyticOrderAt (scaledZeta t) w ≠ 0 := by\n    have han : AnalyticAt ℂ (scaledZeta t) w :=\n      scaledZeta_analytic ht w (by rwa [Metric.mem_closedBall, dist_zero_right])\n    rwa [han.analyticOrderAt_ne_zero]\n  -- analyticOrderNatAt = (analyticOrderAt).toNat, positive\n  have h := ENat.toNat_pos hne htop\n  -- analyticOrderNatAt f w = (analyticOrderAt f w).toNat by def\n  exact h\n```\nwith analyticOrderNatAt def: `analyticOrderNatAt f z₀ = (analyticOrderAt f z₀).toNat` — is it def? journal-023 says \"by DEF\". So the goal 1 ≤ analyticOrderNatAt F w unfolds to 1 ≤ (analyticOrderAt F w).toNat — and h : 0 < (analyticOrderAt F w).toNat ⟹ 1 ≤ it (Nat: 0 < n ↔ 1 ≤ n — same in ℕ). `exact h` might work (0 < n is 1 ≤ n definitionally in ℕ? 0 < n unfolds to 0+1 ≤ n = 1 ≤ n ✓ Nat.lt is defeq succ le). ✓\n\n§B finsets:\n\n```lean\n/-- Zeros of the scaled function with norm ≤ r, as a finset (r ≤ 1). -/\ndef scaledZeroFinset (t : ℝ) (r : ℝ) (hr : r ≤ 1) : Finset ℂ :=\n  (scaledZeta_zeros_finite.subset (fun w hw => ⟨hw.1.trans hr, hw.2⟩)).toFinset\n\ntheorem mem_scaledZeroFinset {t : ℝ} {r : ℝ} {hr : r ≤ 1} {w : ℂ} :\n    w ∈ scaledZeroFinset t r hr ↔ ‖w‖ ≤ r ∧ scaledZeta t w = 0 := by\n  unfold scaledZeroFinset\n  rw [Set.Finite.mem_toFinset]\n  -- goal: w ∈ SetOfZeros r (scaledZeta t) ↔ ...: SetOfZeros is a setOf: mem ⟺ ∧: rfl?\n  exact Iff.rfl  -- maybe\n```\nSetOfZeros r f = {ρ | ‖ρ‖ ≤ r ∧ f ρ = 0} — membership defeq ✓ (maybe needs `Set.mem_setOf_eq`... it's a def with setOf; Iff.rfl or `exact id`).\n\nWait — `Set.Finite.subset` signature: `Set.Finite.subset (hs : s.Finite) (hts : t ⊆ s) : t.Finite`. So `scaledZeta_zeros_finite.subset (hsub)` where hsub : SetOfZeros r F ⊆ SetOfZeros 1 F: `fun w hw => ⟨hw.1.trans hr, hw.2⟩` — hw : w ∈ SetOfZeros r F i.e. ‖w‖ ≤ r ∧ F w = 0; produces ‖w‖ ≤ 1 ∧ F w = 0 ✓. The resulting .Finite : (SetOfZeros r F).Finite ✓. toFinset membership ⟺ ∈ SetOfZeros r F ✓.\n\nHmm — hw.1 : ‖w‖ ≤ r — from hw : w ∈ {ρ | ‖ρ‖ ≤ r ∧ ...}, hw is the ∧ directly (setOf membership is the predicate application ✓).\n\n§C gap:\n\n```lean\n/-- The distance finset for the gap: (5/2)-scaled norms of the 24/25-zeros. -/\ndef zeroNormFinset (t : ℝ) : Finset ℝ :=\n  (scaledZeroFinset t (24/25) (by norm_num)).image fun w => (5/2) * ‖w‖\n```\n\nexists_collection_radius:\n```lean\ntheorem exists_collection_radius {t : ℝ} (ht : 10 ≤ |t|) :\n    ∃ R_c : ℝ, 23 / 10 ≤ R_c ∧ R_c ≤ 24 / 10 ∧\n      ∀ w ∈ scaledZeroFinset t (24/25) (by norm_num),\n        1 / (20 * (((scaledZeroFinset t (24/25) (by norm_num)).card : ℝ) + 1)) ≤\n          |(5 / 2) * ‖w‖ - R_c| := by\n  classical\n  set Z96 := scaledZeroFinset t (24/25) (by norm_num : (24/25:ℝ) ≤ 1) with hZ96\n  set S := Z96.image fun w => (5/2) * ‖w‖ with hS\n  set S10 := S.image fun x => x * 10 with hS10\n  have hcard : S10.card ≤ Z96.card := (Finset.card_image_le).trans Finset.card_image_le\n  obtain ⟨T, hT1, hT2, hT3⟩ := exists_avoiding_midpoint 23 S10 hcard\n  refine ⟨T / 10, by linarith, by linarith, fun w hw => ?_⟩\n  have hwS : (5/2) * ‖w‖ ∈ S := Finset.mem_image.mpr ⟨w, hw, rfl⟩\n  have hwS10 : (5/2) * ‖w‖ * 10 ∈ S10 := Finset.mem_image.mpr ⟨_, hwS, rfl⟩\n  have h := hT3 ((5/2) * ‖w‖ * 10) hwS10\n  -- |25‖w‖ − T| ≥ 1/(2(k+1)) ⟹ |(5/2)‖w‖ − T/10| ≥ 1/(20(k+1))\n  have hscale : |(5/2) * ‖w‖ * 10 - T| = 10 * |(5/2) * ‖w‖ - T / 10| := by\n    rw [← abs_mul]\n    congr 1\n    ring\n  rw [hscale] at h\n  -- h : 1/(2(k+1)) ≤ 10 * |(5/2)‖w‖ − T/10|\n  ...\n```\nhmm the final: 1/(2(k+1)) ≤ 10·X ⟹ 1/(20(k+1)) ≤ X: div/linarith with positivity of (k:ℝ)+1: h : 1/(2*(k+1)) ≤ 10*X; want 1/(20*(k+1)) ≤ X. 1/(20(k+1)) = (1/(2(k+1)))/10 hmm: 20(k+1) = 10·(2(k+1)): 1/(20(k+1)) = (1/10)·(1/(2(k+1)))... field_simp or: have hpos : (0:ℝ) < 2*(k+1); rw [div_le_iff] ... simplest: \n```\nhave hpos : (0:ℝ) < 20 * ((k : ℝ) + 1) := by positivity  -- needs k+1 > 0: k ≥ 0 ✓ positivity handles cast+add?\nhave hpos2 : (0:ℝ) < 2 * ((k : ℝ) + 1) := by positivity\nrw [le_div_iff₀ hpos]  -- goal: 1 ≤ X * (20(k+1))\n...\n```\nfrom h: 1/(2(k+1)) ≤ 10X ⟹ 1 ≤ 10X·2(k+1) (le_div_iff₀ at h) ⟹ 1 ≤ X·(20(k+1)) by ring_nf... Let me do: \n```\nhave h1 : (1:ℝ) ≤ |(5/2)*‖w‖*10 - T| * (2 * ((k:ℝ)+1)) := (le_div_iff₀ hpos2).mp ... \n```\nhmm h : 1/(2*(k+1)) ≤ |...|; (le_div_iff₀ hpos2).mp? le_div_iff₀ : a ≤ b / c ↔ a * c ≤ b (c > 0). h is div ≤ abs: 1/(2(k+1)) ≤ Y: (div_le_iff₀ hpos2).mp h : 1 ≤ Y * (2(k+1)). Then 1 ≤ Y·2(k+1) = X·10·2·(k+1) = X·(20(k+1)): rw hscale already done so Y = 10X: 1 ≤ 10X·2(k+1); want 1 ≤ X·(20(k+1)): 10X·2(k+1) = X·20(k+1) ✓ ring_nf or linarith can't (nonlinear products of X·k... these are products of X (a real expr) and (k:ℝ)+1 — linarith treats X·(k+1) as nonlinear atom... provide: have h2 : 10 * |(5/2)*‖w‖ − T/10| * (2*((k:ℝ)+1)) = |(5/2)*‖w‖ − T/10| * (20*((k:ℝ)+1)) := by ring. Then linarith. Then (le_div_iff₀ hpos).mpr. ✓ manageable.\n\nNote: `exists_avoiding_midpoint 23 S10 hcard` — signature: {k : ℕ} (a : ℝ) (S : Finset ℝ) (hcard : S.card ≤ k) — k implicit from hcard : S10.card ≤ Z96.card ⟹ k := Z96.card ✓. Returns T ∈ [23, 24] with clearance 1/(2(k+1)) where k = Z96.card ✓ matches the target form 1/(20*(card+1)).\n\nAlso `classical` needed for image decidability? Finset.image needs DecidableEq on target — ℝ has Classical. Add `classical` ✓ (done in the proof).\n\nThen the bundle:\n```lean\n/-- The chosen collection radius. -/\nnoncomputable def collRadius (t : ℝ) (ht : 10 ≤ |t|) : ℝ := (exists_collection_radius ht).choose\ntheorem collRadius_ge ... := ((exists_collection_radius ht).choose_spec).1\n...\n```\n\nThen rC, δw, ZW and their facts.\n\nOK — I've spent enough planning; let me start writing. I'll write the whole addition in one go but compile after each §. Also add `import NguyenRH1.LiContour` at top.\n\nActually — one more API check before writing: `Finset.card_image_le`: name? `Finset.card_image_le : (s.image f).card ≤ s.card` ✓ exists. And Finset.mem_image ✓. `Set.InjOn` for sum_image.\n\nAnd `Filter.EventuallyEq.eq_of_nhds`: hmm — I recall `Filter.EventuallyEq.eq_of_nhds : f =ᶠ[𝓝 x] g → f x = g x` ✓ exists.\n\n`Filter.EventuallyEq.deriv : f =ᶠ[𝓝 x] g → deriv f x = deriv g x` ✓ (EventuallyEq.deriv).\n\nLet me write chunk 1 now (§5–§9: helpers + gap + radius bundle + ZW facts). Then compile. Then chunk 2 (Cf characterizations + B lemmas). Then chunk 3 (main theorem + fold).","signature":""},{"type":"text","text":"Full API picture confirmed. Marking context done and starting the build."},{"type":"tool_use","id":"TodoWrite_33","name":"TodoWrite","input":{"todos":[{"content":"Read D-067 §6 + journal-023 + LiDisc.lean + LiContour.lean (context)","status":"completed","activeForm":"Reading context files"},{"content":"R-gap selection: scaled exists_avoiding_midpoint on [2.3, 2.4]","status":"in_progress","activeForm":"Building R-gap selection"},{"content":"g := ζ/∏(s−ρₖ)^mₖ analytic + nonvanishing on closed ball","status":"pending","activeForm":"Building g analytic/nonvanishing"},{"content":"Bounds: |g| outer circle + −log|g(s₀)|","status":"pending","activeForm":"Proving g bounds"},{"content":"BC assembly → loose R-bound theorem","status":"pending","activeForm":"Assembling Borel–Carathéodory"},{"content":"Build green + axiom audit + commit sub-stage","status":"pending","activeForm":"Building and auditing"}]},"extra_content":null}]