[{"type":"thinking","thinking":"Committed (222d65d). Now 3c-iii: the critical shell + final assembly.\n\n**shell_crit** (R−2 < ‖ρ‖ < R+2): needs the arc analysis (uniform ‖s−ρ‖ ≥ 1/(32Ĉ)) + the brick count (single window).\n\nThe hypotheses needed beyond hs/hsz/hR: the gap property hgap and k with R ≥ 4k+5/2 (for the threshold 416Ĉ ≤ R). Signature:\n\n```lean\nlemma shell_crit {k : ℕ} (hk : 4000 ≤ k) {R : ℝ} (hRlo : 4*(k:ℝ)+5/2 ≤ R)\n    (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n      1/(16*C0hat(4*(k:ℝ)+9/2)) ≤ |ρ.im − R| ∨ 1 ≤ |ρ.im − R|)\n    {s : ℂ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s) :\n    ∑ ρ ∈ (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        ¬ ‖(ρ : ℂ)‖ ≤ R - 2 ∧ ‖(ρ : ℂ)‖ < R + 2), ‖seriesTerm s ρ‖\n      ≤ 2688 * C0hat (4*(k:ℝ)+9/2) * A0count * Real.log R\n```\n\nProof structure:\n- hth := gapCircle_threshold hk : 416·Ĉ ≤ 4k+5/2 ≤ R.\n- hĈ2 : 2 ≤ Ĉ (two_le_C0hat).\n- hR : 16002 ≤ R (linarith from hk/hRlo).\n- **hsep : ∀ ρ ∈ FS, (1/(32*Ĉ)) ≤ ‖s − (ρ:ℂ)‖** — the arc analysis:\n  per ρ ∈ FS: ‖ρ‖ ∈ (R−2, R+2). Set γ := (ρ:ℂ).im, t := s.im.\n  Case split on |s.re| ≤ Real.sqrt 13?? — hmm, √13 requires Real.sqrt: |s.re| ≤ √13 ⟺ s.re² ≤ 13 (sq_le_sq-ish). Use s.re^2 ≤ 13 as the case condition (avoids sqrt): by_cases hre13 : s.re^2 ≤ 13.\n  \n  Case 1 (s.re² ≤ 13): \n  - hRt : R − |t| ≤ 13/R: from 3a's computation: R−|t| = s.re²/(R+|t|) ≤ s.re²/R ≤ 13/R. (Re-derive: hnormSq, ht2 etc. — factor out a helper lemma? The 3a proof has this inline. Let me factor a tiny helper: `norm_circle_re_sq_le {s : ℂ} {R B : ℝ} (hs : ‖s‖ = R) (hR1 : 0 < R) (hre : s.re^2 ≤ B) : R − |s.im| ≤ B / R`. Used twice (3a could use it too but it's proved inline there — leave 3a as is, add the helper now for the crit shell.) Actually — simpler to inline again (~15 lines). But a helper is cleaner. Let me add the helper lemma.\n  - |t−γ| ≥ 1/(32Ĉ): \n    have hgap' := hgap (ρ:ℂ) ρ.2: 1/(16Ĉ) ≤ |γ−R| ∨ 1 ≤ |γ−R|.\n    have habs : |(|t| − |γ|)| ≥ |(|γ| − R)| − |(|t| − R)| — via the abs_sub chain: |(|γ|−R)| ≤ |(|γ|−|t|)| + |(|t|−R)| (abs_sub_le: |x−z| ≤ |x−y|+|y−z| with x := |γ|, y := |t|, z := R: |(|γ|−R)| ≤ |(|γ|−|t|)|+|(|t|−R)| ✓) and |(|γ|−|t|)| = |(|t|−|γ|)| (abs_sub_comm).\n    Then: ||t|−|γ|| ≥ ||γ|−R| − ||t|−R|: ||t|−R| = R−|t| (|t| ≤ R: abs_im_le_norm + hs: abs_of_nonpos...) hmm: ||t|−R|: |t| ≤ R ⟹ |t|−R ≤ 0 ⟹ ||t|−R| = R−|t| ✓ abs_of_nonpos.\n    And |t−γ| ≥ ||t|−|γ|| (abs_abs_sub_abs_le_abs_sub : |(|a|−|b|)| ≤ |a−b| — need the name. `abs_abs_sub_abs_le_abs_sub` — I used this name in design; check: in Mathlib it's `abs_abs_sub_abs_le_abs_sub : |(|a| − |b|)| ≤ |a − b|` ✓ I believe.)\n    And ||γ|−R| ≥ 1/(16Ĉ): from hgap': \n      case 1/(16Ĉ) ≤ |γ−R|: |γ−R| = ||γ|−R|?? γ could be negative: |γ−R| vs ||γ|−R|: if γ ≥ 0: equal. If γ < 0: |γ−R| = |γ|+R (γ−R < 0: |γ−R| = R−γ = R+|γ|) and ||γ|−R| = ||γ|−R| = |γ|+R... wait |γ|−R: |γ| ≥ 0, could be < R: ||γ|−R| = R−|γ| if |γ| ≤ R or |γ|−R if |γ| > R. For γ < 0: |γ−R| = R+|γ| (since γ−R < 0, |γ−R| = −(γ−R) = R−γ = R+|γ| ✓). And ||γ|−R|: hmm these differ: |γ−R| = R+|γ| vs ||γ|−R| = |R−|γ||. NOT equal in general! E.g. γ = −1, R = 100: |γ−R| = 101, ||γ|−R| = 99.\n      So hgap's bound on |γ−R| doesn't directly bound ||γ|−R| for negative γ. BUT for γ < 0: ||γ|−R| = |R−|γ|| — is that large? |γ| ≥ ‖ρ‖−1 ≥ R−3 (the crit shell zeros) ⟹ ||γ|−R| ≤ 3 possibly small! E.g. γ = −R+1: ||γ|−R| = 1. Hmm — but that's the distance of |γ| from R, and |γ| ∈ (R−3, R+3): ||γ|−R| ≤ 3: the gap property hgap gives |γ−R| ≥ 1/(16Ĉ) or ≥ 1 — for γ < 0, |γ−R| = |γ|+R ≥ R ≥ 1 ✓ second disjunct — tells us nothing about ||γ|−R|.\n      WAIT — but for the crit arc bound, I need |t−γ| large where t = s.im can have EITHER sign. If γ < 0 and t < 0: |t−γ| = ||t|−|γ|| could be small if both ≈ −R... but then ρ' = conj ρ has im = −γ > 0 with ||γ|−R| small... The hgap property applied to CONJ ρ! hgap is universal over all nontrivial zeros: apply it to (starRingEnd ℂ) ρ (nontrivial via isNontrivialZero_conj): |−γ−R| = |γ+R| ≥ 1/(16Ĉ) or ≥ 1. For γ < 0: |γ+R| = ||γ|−R|·... γ+R: if γ ∈ (−R−3, −R+3): γ+R ∈ (−3, 3): |γ+R| = |γ−(−R)| hmm |γ+R| = ||γ|... γ = −|γ|: γ+R = R−|γ|: |γ+R| = |R−|γ|| = ||γ|−R|·... |R−|γ|| = ||γ|−R| ✓ (abs_sub_comm). So for γ < 0: hgap (conj ρ) gives ||γ|−R| ≥ 1/(16Ĉ) or ≥ 1 ✓. For γ ≥ 0: hgap ρ directly: |γ−R| = ||γ|−R| (γ = |γ|) ✓.\n      So in BOTH cases: ||γ|−R| ≥ min(1/(16Ĉ), 1) = 1/(16Ĉ) (Ĉ ≥ 2 ⟹ 1/(16Ĉ) ≤ 1/32 < 1): uniformly ||γ|−R| ≥ 1/(16Ĉ).\n    - Then |t−γ| ≥ ||t|−|γ|| ≥ ||γ|−R| − ||t|−R| = ||γ|−R| − (R−|t|) ≥ 1/(16Ĉ) − 13/R ≥ 1/(32Ĉ) ⟸ 13/R ≤ 1/(32Ĉ) ⟺ 13·32·Ĉ ≤ R ⟺ 416·Ĉ ≤ R ✓ hth.\n    - Finally ‖s−ρ‖ ≥ |im(s−ρ)| = |t−γ| ✓ (abs_im_le_norm (s−ρ); im(s−ρ) = t−γ: Complex.sub_im).\n  Case 2 (s.re² > 13): ‖s−ρ‖ ≥ |re(s−ρ)| = |s.re − ρ.re| ≥ |s.re|−|ρ.re| ≥ |s.re|−1 > √13−1: |s.re| > √13 ⟸ s.re² > 13, |s.re| ≥ 0: |s.re| > √13: sq_lt_sq-ish: (√13)² = 13 < s.re² = |s.re|² ⟹ √13 < |s.re| (sq_lt_sq (|√13| = √13, √13 ≥ 0): Real.lt_sqrt (|s.re| ≥ 0) (h : 13 < s.re²): |s.re| > √13 ⟺ 13 < |s.re|²: Real.lt_sqrt (hx : 0 ≤ x) : y < √x ↔ y² < x... let me recall: Real.lt_sqrt (hx : 0 ≤ x) : y < Real.sqrt x ↔ y ^ 2 < x. With x := s.re^2, y := √13?? no: want √13 < |s.re|: Real.lt_sqrt: y < sqrt x ↔ y² < x: |s.re| vs sqrt 13: use Real.sqrt_lt (hx : 0 ≤ x)... `Real.sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : √x < y ↔ x < y^2`. x := 13, y := |s.re|: √13 < |s.re| ↔ 13 < |s.re|² ✓ (|s.re|² = s.re² via sq_abs). \n    Then |s.re|−1 > √13−1 ≥ 2: √13 ≥ 3 (9 ≤ 13: Real.sqrt_le_sqrt): |s.re|−1 > 2: and 1/(32Ĉ) ≤ 1/64 ≤ 2 ✓ (Ĉ ≥ 2). So ‖s−ρ‖ ≥ 2 ≥ 1/(32Ĉ) ✓... wait strictly: ‖s−ρ‖ ≥ |re(s−ρ)| ≥ |s.re|−|ρ.re| > √13−1−... |s.re|−|ρ.re| ≥ |s.re|−1 (|ρ.re| ≤ 1 hmm ρ.re ∈ (0,1): |ρ.re| < 1 ✓): > √13−1 ≥ 2 — but I need ≥ 1/(32Ĉ) (non-strict fine): √13−1 ≥ 2 ⟺ √13 ≥ 3 ⟺ 13 ≥ 9 ✓ Real.sqrt_le_sqrt (by norm_num : (9:ℝ) ≤ 13) + Real.sqrt_9? hmm √9 = 3: Real.sqrt_eq_cases... `Real.sqrt_eq_iff_eq_sq`? There's `Real.sqrt_eq_iff_mul_self_eq`... simpler: 3 = √9 ≤ √13: rw [show (3:ℝ) = Real.sqrt 9 from by rw [Real.sqrt_eq_cases]; norm_num]... there's `Real.sqrt_natCast_eq_iff`... Let me use: (3:ℝ) = Real.sqrt (3^2) (Real.sqrt_sq (by norm_num)) then Real.sqrt_le_sqrt (by norm_num : (3:ℝ)^2 ≤ 13). ✓\n  So hsep holds.\n  \n- Then per-element term bound: g ρ ≤ 64·Ĉ·m: g = m·R/(‖ρ‖‖s−ρ‖): ‖ρ‖ > R−2 > 0, ‖s−ρ‖ ≥ 1/(32Ĉ) > 0: ‖ρ‖·‖s−ρ‖ ≥ (R−2)/(32Ĉ) (mul_le_mul (‖ρ‖ ≥ R−2... ‖ρ‖ > R−2 ⟹ ≥) (hsep) (1/(32Ĉ) ≥ 0) (‖ρ‖... hmm mul_le_mul (hab : ‖ρ‖... wait the factors: (R−2) ≤ ‖ρ‖ and (1/(32Ĉ)) ≤ ‖s−ρ‖: mul_le_mul hab hcd (0 ≤ 1/(32Ĉ)) (0 ≤ R−2) : (R−2)·(1/(32Ĉ)) ≤ ‖ρ‖·‖s−ρ‖ ✓.\n  m·R/(‖ρ‖‖s−ρ‖) ≤ m·R/((R−2)/(32Ĉ)) = m·R·32Ĉ/(R−2) ≤ m·2·32Ĉ = 64Ĉm (R/(R−2) ≤ 2 ⟺ R ≥ 4).\n  Via div_le_div_of_nonneg_left (m·R ≥ 0) (denominator pos) (product bound)... then the algebra: R/((R−2)/(32Ĉ)) = 32Ĉ·R/(R−2) (field_simp) and R/(R−2) ≤ 2 (div_le_iff₀).\n  \n- Count: brick with a := R−3, b := R+2, c := R−3: hM1 : 1 ≤ max (R−3)(R−3) = R−3 ✓ (R ≥ 4); hMb : R−3 ≤ R+2 ✓. hsub: |γ| ≥ ‖ρ‖−1 > R−3 = a ⟹ a ≤ |γ| ✓; |γ| ≤ ‖ρ‖ < R+2 ⟹ |γ| ≤ b ✓; c = a ✓.\n  brick: ≤ 3A₀·(b−a+2)·log(3·max|a||b|+5) = 3A₀·7·log(3·max|R−3||R+2|+5): max|R−3||R+2| = R+2 (both positive, R−3 < R+2): log(3(R+2)+5) ≤ 2L: 3(R+2)+5 = 3R+11 ≤ 4R (11 ≤ R) ⟹ log ≤ log(4R) = log4+L: log4 = 2log2 ≤ 2 ≤ L·... 2 ≤ L ⟸ L ≥ 9 ✓: ≤ 2L ✓ — hmm via log_three_le_two_log (x := R+2 ≤ 3R ✓): direct ✓.\n  count ≤ 3A₀·7·(2L) = 42A₀L.\n- Sum ≤ Σ 64Ĉ·m = 64Ĉ·(Σ m) ≤ 64Ĉ·42A₀L = 2688ĈA₀L ✓.\n\nWait — one subtlety in the hsep case 1: I need t := s.im and γ — and the uniform ||γ|−R| ≥ 1/(16Ĉ). The conj application: hgap ((starRingEnd ℂ) ρ) (isNontrivialZero_conj ρ.2): gives 1/(16Ĉ) ≤ |(conj ρ).im − R| ∨ 1 ≤ |(conj ρ).im − R|: (conj ρ).im = −γ (Complex.conj_im): |−γ−R|: for γ < 0: −γ = |γ|: |−γ−R| = ||γ|−R| ✓. So:\n```\nhave hγR : 1/(16*Ĉ) ≤ |(|γ|) - R| ∨ 1 ≤ |(|γ|) - R| ... \n```\nHmm — unify: want ||γ|−R| ≥ 1/(16Ĉ) in all cases. Split on hγ : 0 ≤ γ:\n- γ ≥ 0: hgap ρ.2: |γ−R| ≥ 1/(16Ĉ) ∨ ≥ 1: γ = |γ| (abs_of_nonneg): |γ−R| = ||γ|−R| ✓: so ||γ|−R| ≥ 1/(16Ĉ) or ≥ 1: either way ≥ 1/(16Ĉ) (1 ≥ 1/(16Ĉ) ⟸ 16Ĉ ≥ 1 ✓).\n- γ < 0: hgap (conj ρ): |(−γ)−R| ≥ 1/(16Ĉ) ∨ ≥ 1: −γ = |γ| (abs_of_neg): same ✓.\nSo hγR : (1/(16*Ĉ)) ≤ |(|(ρ:ℂ).im|) - R|... careful with the abs nesting: ||γ| − R| — the outer bars: |(|γ| − R)|. In Lean: `|(|(ρ:ℂ).im| - R)|`. Hmm hgap gives |γ−R| with γ = ρ.im: rewrite γ = |γ| (when γ ≥ 0): |(|γ|)−R| — hmm the rewriting: hgap ρ : ... |ρ.im − R| ∨ ...: with hγ : 0 ≤ ρ.im: ρ.im = |ρ.im| (abs_of_nonneg hγ).symm: rw ← in hgap. The term becomes |(|ρ.im| − R)| — wait |ρ.im − R| with ρ.im := |ρ.im|: |(|ρ.im|) − R|: the abs_of_nonneg gives |ρ.im| = ρ.im: rw [← abs_of_nonneg hγ] at hgap' : turns ρ.im into |ρ.im| inside the abs — rw would rewrite ALL occurrences of ρ.im — there's only the one. ✓\n\nThen |t−γ| ≥ ||t|−|γ||: abs_abs_sub_abs_le_abs_sub s.im ρ.im : |(|s.im| − |ρ.im|)| ≤ |s.im − ρ.im| ✓.\nThe chain: ||t|−|γ|| ≥ ||γ|−R| − ||t|−R| where ||t|−R| = R−|t|: abs_sub_le (|γ|) (|t|) R : ||γ|−R| ≤ ||γ|−|t|| + ||t|−R|: abs_sub_le : |a − c| ≤ |a − b| + |b − c| ✓ with a := |γ|, b := |t|, c := R. And ||γ|−|t|| = ||t|−|γ|| (abs_sub_comm). ||t|−R| = R−|t| (|t| ≤ R: abs_of_nonpos (|t|−R ≤ 0) : |(|t|−R)| = −(|t|−R) = R−|t| ✓).\nSo |t−γ| ≥ ||t|−|γ|| ≥ ||γ|−R| − (R−|t|) ≥ 1/(16Ĉ) − 13/R ✓.\nAnd 13/R ≤ 1/(32Ĉ): from hth : 416·Ĉ ≤ 4k+5/2 ≤ R: 13·32·Ĉ = 416·Ĉ ≤ R ⟹ 13/R ≤ 13/(416Ĉ) = 1/(32Ĉ): 13·32·Ĉ ≤ R ⟹ 13 ≤ R/(32Ĉ)·... formal: 13/R ≤ 1/(32·Ĉ) ⟺ 13·(32·Ĉ) ≤ R·1 (div_le_div_iff₀ (R > 0) (32Ĉ > 0)): 13·32·Ĉ ≤ R ✓ = 416·Ĉ ≤ R: linarith with hth and the ring-normal form: 13*(32*Ĉ) = 416*Ĉ by ring — linarith handles linear: 13·32·Ĉ = 416·Ĉ ✓ linarith can match (constant multiple).\n\nThen |t−γ| ≥ 1/(16Ĉ) − 1/(32Ĉ) = 1/(32Ĉ) ✓ linarith.\nThen ‖s−ρ‖ ≥ |im(s−ρ)|: abs_im_le_norm (s − ρ) : |(s−ρ).im| ≤ ‖s−ρ‖ ✓; (s−ρ).im = s.im − ρ.im (Complex.sub_im) ✓.\n\nThe sqrt-13 case: \n- Real.sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : Real.sqrt x < y ↔ x < y ^ 2 — check name/signature. `Real.sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : √(x) < y ↔ x < y ^ 2`? I think `Real.sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : Real.sqrt x < y ↔ x < y ^ 2` ✓.\n- √13 < |s.re| ⟸ 13 < |s.re|²: |s.re|² = s.re² (sq_abs) > 13 (case hypothesis).\n- 3 ≤ √13: rw [show (3:ℝ) = Real.sqrt (3^2) from (Real.sqrt_sq (by norm_num)).symm] hmm: Real.sqrt_sq (h : 0 ≤ x) : √(x^2) = x: (Real.sqrt_sq (show (0:ℝ) ≤ 3 by norm_num)).symm : 3 = √(3^2): then Real.sqrt_le_sqrt (by norm_num : (3:ℝ)^2 ≤ 13) : √(3^2) ≤ √13 ✓.\n- |re(s−ρ)| ≤ ‖s−ρ‖: abs_re_le_norm (s−ρ) ✓; re(s−ρ) = s.re − ρ.re (Complex.sub_re) ✓; |s.re − ρ.re| ≥ |s.re| − |ρ.re| (abs_sub_abs_le_abs_sub... : |s.re|−|ρ.re| ≤ |s.re−ρ.re| — hmm that's `abs_sub_abs_le_abs_sub : |a| − |b| ≤ |a − b|` ✓).\n\nNow the helper lemma for R−|t| ≤ B/R:\n```\nlemma norm_circle_sub_abs_im_le {s : ℂ} {R B : ℝ} (hs : ‖s‖ = R) (hR0 : (0:ℝ) < R)\n    (hre : s.re ^ 2 ≤ B) : R - |s.im| ≤ B / R := by\n  have hnormSq : ‖s‖ ^ 2 = s.re ^ 2 + s.im ^ 2 := by\n    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    ring\n  have ht2 : |s.im| ^ 2 = R ^ 2 - s.re ^ 2 := by\n    have h1 : s.im ^ 2 = R ^ 2 - s.re ^ 2 := by\n      have h2 : s.re ^ 2 + s.im ^ 2 = R ^ 2 := by rw [← hnormSq, hs]\n      linarith\n    rw [sq_abs]\n    linarith [h1]\n  have hRt : R - |s.im| = s.re ^ 2 / (R + |s.im|) := by\n    have hne : R + |s.im| ≠ 0 := by positivity\n    field_simp\n    have h1 : (R - |s.im|) * (R + |s.im|) = R ^ 2 - |s.im| ^ 2 := by ring\n    rw [h1, ht2]\n    ring\n  rw [hRt]\n  have h1 : s.re ^ 2 / (R + |s.im|) ≤ s.re ^ 2 / R := by\n    apply div_le_div_of_nonneg_left (sq_nonneg _) hR0\n    have h2 : (0 : ℝ) ≤ |s.im| := abs_nonneg _\n    linarith\n  have h3 : s.re ^ 2 / R ≤ B / R :=\n    div_le_div_of_nonneg_right hre hR0.le\n  exact h1.trans h3\n```\nHmm — 3a's inline version had this; now the helper. (3a stays as is — freeze protocol concerns only EXISTING proofs in OTHER files; LiCircleBound is this session's file, fine to add helpers, but no need to refactor 3a.)\n\nWait — h1's div_le_div_of_nonneg_left (ha : 0 ≤ a) (hc : 0 < c) (hcd : c ≤ d) : a / d ≤ a / c: so s.re²/(R+|t|) ≤ s.re²/R needs R ≤ R+|t|: div_le_div_of_nonneg_left (sq_nonneg _) hR0 (by linarith : R ≤ R+|s.im|) : s.re²/(R+|t|) ≤ s.re²/R ✓ — as I wrote: `apply div_le_div_of_nonneg_left (sq_nonneg _) hR0; linarith [abs_nonneg _]` — the third arg: R ≤ R+|s.im| ✓.\n\n- h3 : div_le_div_of_nonneg_right? For s.re²/R ≤ B/R with s.re² ≤ B, R > 0: `div_le_div_of_nonneg_right hre hR0.le`?? div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a/c ≤ b/c ✓ (just found it exists). ✓\n\nAlso — crit count: brick b−a+2 = (R+2)−(R−3)+2 = 7 ✓ ring.\n\nAssembly theorem:\n```lean\ntheorem seriesFun_norm_le_gapCircle {k : ℕ} (hk : 4000 ≤ k)\n    {R : ℝ} (hRlo : 4*(k:ℝ)+5/2 ≤ R) (hRhi : R ≤ 4*(k:ℝ)+3)\n    (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n      1/(16*C0hat(4*(k:ℝ)+9/2)) ≤ |ρ.im − R| ∨ 1 ≤ |ρ.im − R|)\n    {s : ℂ} (hs : ‖s‖ = R) :\n    ‖seriesFun s‖ ≤ 2 * lowZeroConst +\n      2900 * A0count * C0hat (4*(k:ℝ)+9/2) * (Real.log R)^2\n```\nProof:\n- hsz := not_isNontrivialZero_on_gapCircle hk hRlo hgap hs.\n- hR : 16002 ≤ R.\n- hlogR : 9 ≤ log R; hĈ2 : 2 ≤ Ĉ.\n- hsplit := seriesFun_norm_le_split (s := s) (R := R) : ‖seriesFun s‖ ≤ Σ_F g + tail.\n- The iterated filter split of Σ_F g into the 5 shells:\n  F := circleZeros R. P1 := (‖·‖ ≤ 3), P2 := (‖·‖ ≤ R/2), P3 := (‖·‖ ≤ R−2), P4 := (‖·‖ < R+2).\n  Σ_F g = Σ_{F.filter P1} g + Σ_{F.filter ¬P1} g (Finset.sum_filter_add_sum_filter_not F P1 g).\n  Σ_{F.filter ¬P1} g = Σ_{(F.filter ¬P1).filter P2} g + Σ_{(F.filter ¬P1).filter ¬P2} g.\n  (F.filter ¬P1).filter P2 = F.filter (¬P1 ∧ P2) (Finset.filter_filter — the conjunction form: filter P2 (filter ¬P1 F) = filter (fun a => ¬P1 a ∧ P2 a) F ✓ — that's shell_inlo's finset ✓ (my shell_inlo used `¬ ‖ρ‖ ≤ 3 ∧ ‖ρ‖ ≤ R/2` ✓ matches).\n  Continue: (F.filter ¬P1).filter ¬P2 → filter P3: ((F.filter ¬P1).filter ¬P2).filter P3 = F.filter (¬P1 ∧ ¬P2 ∧ P3)... hmm filter_filter iterated: filter P3 (filter ¬P2 (filter ¬P1 F)) = filter (fun a => ¬P1 a ∧ ¬P2 a ∧ P3 a)?? Finset.filter_filter : filter p (filter q s) = filter (fun a => q a ∧ p a) s. Inner first: filter ¬P2 (filter ¬P1 F) = filter (¬P1 ∧ ¬P2) F. Then filter P3 of that: filter (fun a => (¬P1 ∧ ¬P2) a ∧ P3 a) = filter (¬P1 ∧ ¬P2 ∧ P3) — but shell_inhi's finset is F.filter (¬P2 ∧ P3)! — i.e., shell_inhi = F.filter (fun ρ => ¬‖ρ‖ ≤ R/2 ∧ ‖ρ‖ ≤ R−2) — the iterated split's third piece is F.filter (¬P1 ∧ ¬P2 ∧ P3) — has the extra ¬P1 conjunct! MISMATCH. Hmm — the pieces from the iterated split: piece1 = filter P1; piece2 = filter (¬P1 ∧ P2); piece3 = filter (¬P1 ∧ ¬P2 ∧ P3); piece4 = filter (¬P1 ∧ ¬P2 ∧ ¬P3 ∧ P4); piece5 = filter (¬P1 ∧ ¬P2 ∧ ¬P3 ∧ ¬P4).\n  But my shell lemmas are stated on: inlo: (¬P1 ∧ P2) ✓ matches piece2; inhi: (¬P2 ∧ P3) — piece3 has extra ¬P1 — but on P3's range (‖ρ‖ ≤ R−2), ¬P2 ⟹ ‖ρ‖ > R/2 > 3 ⟹ ¬P1 automatic! So the filters are EQUAL as sets: filter (¬P1 ∧ ¬P2 ∧ P3) F = filter (¬P2 ∧ P3) F: ext ρ: ↔: forward: drop ¬P1 ✓; backward: ¬P2 ∧ P3 ⟹ ‖ρ‖ > R/2 ≥ 8001 > 3 ⟹ ¬P1 ✓. Similarly piece4 = filter (¬P3 ∧ P4) (¬P1, ¬P2 automatic: ¬P3 ⟹ ‖ρ‖ > R−2 > R/2 > 3 ✓) = shell_crit's finset ✓ (mine: ¬‖ρ‖ ≤ R−2 ∧ ‖ρ‖ < R+2 ✓). Piece5 = filter ¬P4 = shell_up's ✓ (¬P1..¬P3 automatic: ¬P4 ⟹ ‖ρ‖ ≥ R+2 > R−2 > R/2 > 3 ✓).\n  So the assembly: iterated sum_filter_add_sum_filter_not 4 times, then rewrite each piece's filter to the shell-normal form via Finset.filter_congr (decidable) or ext + simp + tauto with the R-bounds. Each piece congruence ~6 lines. Total assembly ~60-80 lines.\n  \n  Alternatively — cleaner: prove the partition as a single `Finset.sum` identity via... the iterated approach is fine.\n\n- Then: Σ_F g ≤ 2·lowZeroConst + 60A₀L² + 60A₀L² + 2688ĈA₀L + 45A₀L² and tail ≤ 91A₀L.\n  Total: 2·lowZeroConst + 165A₀L² + 2688ĈA₀L + 91A₀L ≤ 2·lowZeroConst + 2900·A₀·Ĉ·L²:\n  165A₀L² ≤ (165/2)ĈA₀L² (Ĉ ≥ 2) = 82.5ĈA₀L²; 91A₀L ≤ 91A₀L² (L ≥ 1) ≤ 45.5ĈA₀L² (Ĉ ≥ 2); 2688+82.5+45.5 = 2816 ≤ 2900 ✓.\n  With the Ĉ-coefficient: 2688 + 165/2 + 91/2 = 2688 + 82.5 + 45.5 = 2816. Fine.\n  linarith with: hĈ2 (2 ≤ Ĉ), hlogR (9 ≤ L ⟹ 1 ≤ L, L ≤ L²... need L ≤ L²: from L ≥ 9: L² ≥ 9L ≥ L... linarith can't multiply: give nlinarith or explicit hLL : L ≤ L^2: `by nlinarith [hlogR]` or have hLL : Real.log R ≤ (Real.log R)^2 := by nlinarith [hlogR]. And products A₀·Ĉ·L² nonneg: the final: 165A₀L² + 2688ĈA₀L + 91A₀L ≤ 2900A₀ĈL²: nlinarith [hĈ2, hlogR, A0count_pos, hLL]? nlinarith with products of three unknowns (A₀·Ĉ·L²) — nlinarith multiplies PAIRS of hypotheses: (Ĉ−2)·(A₀·L²) etc. Might work: 2900A₀ĈL² − 2688ĈA₀L − 165A₀L² − 91A₀L = A₀L·(2900ĈL − 2688Ĉ − 165L − 91) = A₀L·(Ĉ(2900L−2688) − (165L+91)): 2900L−2688 ≥ 2900·9−2688 > 0 and Ĉ ≥ 2: Ĉ(2900L−2688) ≥ 2(2900L−2688) = 5800L−5376 ≥ 165L+91 ⟺ 5635L ≥ 5467 ✓ L ≥ 9. So = A₀L·(...) ≥ 0: needs Ĉ(2900L−2688) ≥ 2(2900L−2688) (Ĉ ≥ 2, 2900L−2688 ≥ 0): nlinarith can find: product (Ĉ−2)·(2900L−2688) ≥ 0 hmm nlinarith [hĈ2, hlogR, A0count_pos.le, hLL] with hints — it multiplies pairs: (Ĉ−2) and L: ĈL ≥ 2L ✓; A₀·(...) — nlinarith should manage with A0count_pos.le, hlogR, hĈ2, hLL. Let me structure it manually to be safe:\n  ```\n  have hA0 := A0count_pos.le\n  have hL2 : Real.log R ≤ (Real.log R)^2 := by nlinarith [hlogR]\n  have h1 : 165 * A0count * (Real.log R)^2 ≤ (165/2) * A0count * C0hat(4*(k:ℝ)+9/2) * (Real.log R)^2 := by\n    ... (Ĉ ≥ 2: 165 ≤ 165/2·Ĉ: mul_le_mul_of_nonneg... )\n  ```\n  Manual: \n  ĈA₀L² ≥ 2A₀L² ⟹ 165A₀L² ≤ 82.5·ĈA₀L² — wait 165A₀L² vs 82.5ĈA₀L²: 82.5Ĉ ≥ 165 ⟸ Ĉ ≥ 2 ✓. And 91A₀L ≤ 91A₀L² ≤ 45.5ĈA₀L² ✓.\n  So total ≤ (82.5+2688+45.5)ĈA₀L² = 2816ĈA₀L² ≤ 2900A₀ĈL² ✓.\n  As one nlinarith: goal after summing shells: `2*lowZeroConst + 165*A₀*L² + 2688*Ĉ*A₀*L + 91*A₀*L ≤ 2*lowZeroConst + 2900*A₀*Ĉ*L²`: cancel 2·lowZeroConst (nonneg? lowZeroConst_nonneg ✓ — the LHS has +2·lowZeroConst and RHS too: linarith subtracts). Remaining: 165A₀L²+2688ĈA₀L+91A₀L ≤ 2900A₀ĈL²: nlinarith [hĈ2, hlogR, hA0, hL2, lowZeroConst_nonneg] — nlinarith needs to find: Ĉ ≥ 2 ⟹ Ĉ·X ≥ 2X for X = A₀L² ≥ 0: that's mul_le_mul_of_nonneg_right — nonlinear: nlinarith multiplies hypothesis pairs: (Ĉ − 2)·(A₀·L²) ≥ 0 ⟸ both nonneg ✓ nlinarith CAN do this (it considers products of pairs). (Ĉ−2)·(A₀·L²) ≥ 0 gives ĈA₀L² ≥ 2A₀L² ✓; (L²−L)·(A₀·... ) hmm 91A₀L ≤ 91A₀L² from L ≤ L² ✓ then ≤ 45.5·(2A₀L²) ≤ 45.5ĈA₀L². The combination: 165A₀L²+91A₀L ≤ 165A₀L²+91A₀L² = (256)A₀L²·... wait 165+91 = 256: 256A₀L²·... hmm: 165A₀L² + 91A₀L ≤ 165A₀L² + 91A₀L² = 256A₀L² (using 91A₀L ≤ 91A₀L²). Then 256A₀L² ≤ 128·(2A₀L²) ≤ 128·ĈA₀L². Total: 2688+128 = 2816 ✓. nlinarith with [hĈ2, hlogR, hA0, hL2]: pairs: (Ĉ−2)·(A₀·L²) ≥ 0: needs A₀·L² ≥ 0 (mul_nonneg hA0 (sq_nonneg·... (Real.log R)^2 ≥ 0: sq_nonneg... nlinarith considers squares: (L)² ≥ 0 automatic? pow_two_nonneg). Hmm — nlinarith proves goals of the form t ≤ 0 by trying products; feeding [hĈ2, hlogR, hA0, hL2, mul_nonneg hA0 (pow_two_nonneg (Real.log R) : 0 ≤ A0count*(Real.log R)^2)]... let me give it good hints:\n  ```\n  have hfin : 165 * A0count * (Real.log R)^2 + 2688 * C0hat (4*(k:ℝ)+9/2) * A0count * Real.log R + 91 * A0count * Real.log R\n      ≤ 2900 * A0count * C0hat (4*(k:ℝ)+9/2) * (Real.log R)^2 := by\n    have hnn : (0:ℝ) ≤ A0count * (Real.log R)^2 := mul_nonneg hA0 (pow_two_nonneg _)\n    nlinarith [hĈ2, hlogR, hA0, hL2, hnn, mul_nonneg hA0 hlogRnn]\n  ```\n  nlinarith: products to consider: (Ĉ−2)·hnn ≥ 0: ĈA₀L² − 2A₀L² ≥ 0 ✓; hL2·(91A₀): 91A₀L ≤ 91A₀L² (from L ≤ L2, 91A₀ ≥ 0): that's mul_le_mul_of_nonneg_right — a pair product (L²−L)·(91A₀)... nlinarith multiplies pairs of the PROVIDED facts/atoms — (L²−L) is from hL2 ✓ and 91A₀ from mul_nonneg hA0 hlogRnn·... hmm 91·A₀ vs A₀: (L²−L)·A₀ ≥ 0 ⟸ A₀ ≥ 0 ✓ pair. Then: 2900A₀ĈL² − 2688ĈA₀L − 256A₀L² = ĈA₀L·(2900L−2688) − 256A₀L²: hmm the ĈA₀L vs ĈA₀L² mismatch: 2688ĈA₀L ≤ 2688ĈA₀L² (L ≥ 1 ⟹ L ≤ L²: ĈA₀·(L²−L) ≥ 0 pair (ĈA₀ ≥ 0)·(L²−L ≥ 0) ✓). Then need 165A₀L²+91A₀L+2688ĈA₀L² ≤ 2900A₀ĈL² ⟸ (2900−2688)ĈA₀L² ≥ 165A₀L²+91A₀L ⟸ 212ĈA₀L² ≥ 256A₀L² ⟸ Ĉ ≥ 256/212 = 1.21 ⟸ Ĉ ≥ 2 ✓: 212·(ĈA₀L²−2A₀L²)·... 212·(Ĉ−2)A₀L² ≥ 0 ⟹ 212ĈA₀L² ≥ 424A₀L² ≥ 256A₀L² ✓. nlinarith should find with the hints. Fingers crossed; if nlinarith struggles, decompose manually.\n\nLet me also handle the filter-congruence lemmas for the assembly pieces. For piece3:\n```\nhave hpiece3 : (F.filter (fun ρ => ¬ ‖(ρ:ℂ)‖ ≤ 3)).filter (fun ρ => ¬ ‖(ρ:ℂ)‖ ≤ R/2) |>.filter ... \n```\nHmm — actually the cleanest: prove for each piece the filter EQUALITY via ext:\n```\nhave he3 : F.filter (fun ρ => ¬‖(ρ:ℂ)‖ ≤ 3 ∧ ¬‖(ρ:ℂ)‖ ≤ R/2 ∧ ‖(ρ:ℂ)‖ ≤ R−2)\n    = F.filter (fun ρ => ¬‖(ρ:ℂ)‖ ≤ R/2 ∧ ‖(ρ:ℂ)‖ ≤ R−2) := by\n  ext ρ\n  simp only [Finset.mem_filter]\n  constructor\n  · intro h; exact ⟨h.2⟩\n  · intro h\n    refine ⟨⟨?_, h.1⟩, h.2⟩... \n```\nwait — shell_inhi's finset: F.filter (fun ρ => ¬‖ρ‖ ≤ R/2 ∧ ‖ρ‖ ≤ R−2): mem ↔ ρ ∈ F ∧ (¬‖ρ‖ ≤ R/2 ∧ ‖ρ‖ ≤ R−2). The iterated piece: F.filter (¬P1 ∧ ¬P2 ∧ P3): mem ↔ ρ ∈ F ∧ (¬P1 ∧ ¬P2 ∧ P3)... hmm the AND-nesting from filter_filter: filter P3 (filter (¬P1 ∧ ¬P2) F)?? — the iterated: ((F.filter ¬P1).filter ¬P2).filter P3: filter_filter says filter p (filter q s) = filter (fun a => q a ∧ p a) s — applied twice: (F.filter ¬P1).filter ¬P2 = filter (¬P1 ∧ ¬P2) F; then filter P3 of THAT: = filter (fun a => (¬P1 a ∧ ¬P2 a) ∧ P3 a) F. So the predicate is (¬P1 ∧ ¬P2) ∧ P3 — the equality to shell_inhi's (¬P2 ∧ P3): ext + tauto with the bound: ¬P2 ∧ P3 ⟹ ¬P1 (‖ρ‖ > R/2 ≥ 8001 > 3 ⟹ ¬(‖ρ‖ ≤ 3) ✓ linarith).\n\nOK. Rather than perfect foresight, write it and iterate. Also — the `F.filter` lambdas must pin the binder type (banked gotcha) — the shell lemmas' finsets all have pinned lambdas; the assembly's filter predicates must be SYNTACTICALLY IDENTICAL for the congruence/sum_filter lemmas to rewrite. The iterated split produces predicates built from P1..P4 as I write them — I'll write the split with exactly the shell lambdas:\n- P1-lambda: (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ‖(ρ:ℂ)‖ ≤ 3) ✓ = shell_low's.\n- inlo: (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ¬‖(ρ:ℂ)‖ ≤ 3 ∧ ‖(ρ:ℂ)‖ ≤ R/2) ✓ shell_inlo's.\n- inhi: (¬‖·‖ ≤ R/2 ∧ ‖·‖ ≤ R−2) ✓.\n- crit: (¬‖·‖ ≤ R−2 ∧ ‖·‖ < R+2) ✓.\n- up: (¬‖·‖ < R+2) ✓.\n\nThe sum_filter_add_sum_filter_not with explicit (p := ...) — the decidability instance: with `classical` in scope, fine.\n\nThe five-way split chain: let me define the split as a have:\n```\nhave hsplit5 : ∑ ρ ∈ F, g ρ =\n    ∑ ρ ∈ F.filter q1, g ρ + (∑ ρ ∈ F.filter q2, g ρ +\n      (∑ ρ ∈ F.filter q3, g ρ + (∑ ρ ∈ F.filter q4, g ρ +\n        ∑ ρ ∈ F.filter q5, g ρ)))\n```\nwhere q1 = low-pred, q2 = inlo-pred (¬q1' ∧ ·), q3 = inhi-pred, q4 = crit-pred, q5 = up-pred, with q1' := (‖·‖ ≤ 3) etc. Hmm — the sum_filter_add_sum_filter_not splits by p = (‖·‖ ≤ 3): filter p + filter ¬p. ¬p as a lambda: (fun ρ => ¬‖ρ‖ ≤ 3) — then filter P2 on it = filter (fun ρ => ¬‖ρ‖ ≤ 3 ∧ ‖ρ‖ ≤ R/2) via filter_filter ✓ = q2 ✓ directly! Great — so piece2 IS q2 (shell_inlo's finset) with no congruence needed. piece3: (F.filter (¬p1)).filter (¬p2')... wait the split of filter ¬p1 by p2' := (‖·‖ ≤ R/2): = filter (¬p1 ∧ p2') + filter (¬p1 ∧ ¬p2') ✓ first = q2 ✓. Then split filter (¬p1 ∧ ¬p2') by p3' := (‖·‖ ≤ R−2): filter ((¬p1 ∧ ¬p2') ∧ p3') + filter ((¬p1 ∧ ¬p2') ∧ ¬p3'): first = filter (fun ρ => (¬‖ρ‖≤3 ∧ ¬‖ρ‖≤R/2) ∧ ‖ρ‖≤R−2) — vs shell_inhi's q3 = (¬‖ρ‖≤R/2 ∧ ‖ρ‖≤R−2): congruence needed (drop ¬p1, regroup). piece4: split by p4' := (‖·‖ < R+2): filter (((¬p1∧¬p2')∧¬p3') ∧ p4') + filter (((¬p1∧¬p2')∧¬p3')∧¬p4'): congr to q4 = (¬p3' ∧ p4') and q5 = ¬p4'. \n\nSo 3 congruences (piece3 → q3, piece4 → q4, piece5 → q5). Each ~8 lines (ext, simp [mem_filter], tauto with linarith for the drop).\n\nAlright — let me write shell_crit + the helper + assembly in one go. Actually, given the size, let me do shell_crit first (compile), then assembly.","signature":""},{"type":"text","text":"3c-ii committed. Now the critical shell with the arc analysis, plus a factored helper for the R−|im| bound."},{"type":"tool_use","id":"Edit_106","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 9. The critical shell and the assembly (5e-v-b chunk 3c-iii)\n\n`norm_circle_sub_abs_im_le`: on ‖s‖ = R, R−|im s| = re²/(R+|im|) ≤ B/R\nwhen re² ≤ B. `shell_crit`: the critical annulus (R−2 < ‖ρ‖ < R+2) —\nthe γ-gap arc analysis: |re s| ≤ √13 ⟹ |t| within 13/R of R ⟹\n|t−γ| ≥ 1/(32·Ĉ₀) (the γ-gap + threshold); |re s| > √13 ⟹\n‖s−ρ‖ ≥ √13−1 ≥ 2. Uniform separation ‖s−ρ‖ ≥ 1/(32·Ĉ₀), term ≤\n64·Ĉ₀·m, single-window count 42·A₀·log R ⟹ ≤ 2688·Ĉ₀·A₀·log R.\n`seriesFun_norm_le_gapCircle`: the assembly. -/\n\n/-- On the circle ‖s‖ = R: R − |im s| = re²/(R+|im s|) ≤ B/R when\nre² ≤ B. -/\nlemma norm_circle_sub_abs_im_le {s : ℂ} {R B : ℝ} (hs : ‖s‖ = R) (hR0 : (0 : ℝ) < R)\n    (hre : s.re ^ 2 ≤ B) : R - |s.im| ≤ B / R := by\n  have hnormSq : ‖s‖ ^ 2 = s.re ^ 2 + s.im ^ 2 := by\n    rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    ring\n  have ht2 : |s.im| ^ 2 = R ^ 2 - s.re ^ 2 := by\n    have h1 : s.im ^ 2 = R ^ 2 - s.re ^ 2 := by\n      have h2 : s.re ^ 2 + s.im ^ 2 = R ^ 2 := by rw [← hnormSq, hs]\n      linarith\n    rw [sq_abs]\n    linarith [h1]\n  have hRt : R - |s.im| = s.re ^ 2 / (R + |s.im|) := by\n    have hne : R + |s.im| ≠ 0 := by positivity\n    field_simp\n    have h1 : (R - |s.im|) * (R + |s.im|) = R ^ 2 - |s.im| ^ 2 := by ring\n    rw [h1, ht2]\n    ring\n  rw [hRt]\n  have h1 : s.re ^ 2 / (R + |s.im|) ≤ s.re ^ 2 / R := by\n    apply div_le_div_of_nonneg_left (sq_nonneg _) hR0\n    have h2 : (0 : ℝ) ≤ |s.im| := abs_nonneg _\n    linarith\n  have h3 : s.re ^ 2 / R ≤ B / R := div_le_div_of_nonneg_right hre hR0.le\n  exact h1.trans h3\n\n/-- **The critical shell** (R−2 < ‖ρ‖ < R+2): ≤ 2688·Ĉ₀·A₀·log R. -/\nlemma shell_crit {k : ℕ} (hk : 4000 ≤ k) {R : ℝ} (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R)\n    (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →\n      1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)\n    {s : ℂ} (hs : ‖s‖ = R) (hsz : ¬ IsNontrivialZero s) :\n    ∑ ρ ∈ (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        ¬ ‖(ρ : ℂ)‖ ≤ R - 2 ∧ ‖(ρ : ℂ)‖ < R + 2), ‖seriesTerm s ρ‖\n      ≤ 2688 * C0hat (4 * (k : ℝ) + 9 / 2) * A0count * Real.log R := by\n  classical\n  have hth := gapCircle_threshold hk\n  have hĈ2 : (2 : ℝ) ≤ C0hat (4 * (k : ℝ) + 9 / 2) := two_le_C0hat (by\n    have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast (by omega : 1 ≤ k)\n    linarith)\n  have hR : (16002 : ℝ) ≤ R := by\n    have hkR : (16000 : ℝ) ≤ 4 * (k : ℝ) := by\n      have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n      linarith\n    linarith [hRlo]\n  have hRpos : (0 : ℝ) < R := by linarith [hR]\n  have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR\n  have hlogRnn : (0 : ℝ) ≤ Real.log R := by linarith [hlogR]\n  have hĈpos : (0 : ℝ) < C0hat (4 * (k : ℝ) + 9 / 2) := by linarith [hĈ2]\n  set FS := (circleZeros R).filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n    ¬ ‖(ρ : ℂ)‖ ≤ R - 2 ∧ ‖(ρ : ℂ)‖ < R + 2) with hFS\n  -- the uniform separation 1/(32Ĉ₀) ≤ ‖s−ρ‖ on the critical shell\n  have hsep : ∀ ρ ∈ FS, 1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ ‖s - (ρ : ℂ)‖ := by\n    intro ρ hρ\n    rw [hFS, Finset.mem_filter] at hρ\n    obtain ⟨-, hρRm2, hρRp2⟩ := hρ\n    have hρRm2' : (R - 2 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_ge hρRm2\n    -- |γ| ≥ ‖ρ‖−1 ≥ R−3; the γ-gap for |γ| near R (conj if γ < 0)\n    have hγR : 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |(|(ρ : ℂ).im|) - R| := by\n      rcases le_or_gt 0 (ρ : ℂ).im with hγ | hγ\n      · have hgap' := hgap (ρ : ℂ) ρ.2\n        rw [← abs_of_nonneg hγ] at hgap'\n        rcases hgap' with h | h\n        · exact h\n        · have h1 : 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ 1 := by\n            rw [div_le_one (by positivity : (0 : ℝ) < 16 * C0hat (4 * (k : ℝ) + 9 / 2))]\n            linarith [hĈ2]\n          exact h1.trans h\n      · have hconj := hgap ((starRingEnd ℂ) (ρ : ℂ)) (isNontrivialZero_conj ρ.2)\n        rw [Complex.conj_im, ← abs_of_neg hγ] at hconj\n        rcases hconj with h | h\n        · exact h\n        · have h1 : 1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ 1 := by\n            rw [div_le_one (by positivity : (0 : ℝ) < 16 * C0hat (4 * (k : ℝ) + 9 / 2))]\n            linarith [hĈ2]\n          exact h1.trans h\n    by_cases hre13 : s.re ^ 2 ≤ 13\n    · -- the strip arcs: |t| within 13/R of R, |t−γ| ≥ 1/(32Ĉ₀)\n      have hRt : R - |s.im| ≤ 13 / R :=\n        norm_circle_sub_abs_im_le hs hRpos hre13\n      have ht_le : |s.im| ≤ R := by\n        have h := abs_im_le_norm s\n        rw [hs] at h\n        exact h\n      have h1 : |(|s.im| - |(ρ : ℂ).im|)| ≤ |s.im - (ρ : ℂ).im| :=\n        abs_abs_sub_abs_le_abs_sub _ _\n      have h2 : |(|(ρ : ℂ).im| - R)| ≤ |(|(ρ : ℂ).im| - |s.im|)| + |(|s.im| - R)| :=\n        abs_sub_le _ _ _\n      have h3 : |(|(ρ : ℂ).im| - |s.im|)| = |(|s.im| - |(ρ : ℂ).im|)| := abs_sub_comm _ _\n      have h4 : |(|s.im| - R)| = R - |s.im| := by\n        rw [abs_of_nonpos (by linarith [ht_le] : |s.im| - R ≤ 0)]\n        ring\n      -- the threshold: 13/R ≤ 1/(32Ĉ₀)\n      have hthr : 13 / R ≤ 1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)) := by\n        rw [div_le_div_iff₀ hRpos (by positivity : (0 : ℝ) < 32 * C0hat (4 * (k : ℝ) + 9 / 2))]\n        have h1 : 13 * (32 * C0hat (4 * (k : ℝ) + 9 / 2))\n            = 416 * C0hat (4 * (k : ℝ) + 9 / 2) := by ring\n        rw [h1]\n        linarith [hth, hRlo]\n      have h5 : 1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |s.im - (ρ : ℂ).im| := by\n        linarith [hγR, h1, h2, h3, h4, hRt, hthr]\n      have h6 : (s - (ρ : ℂ)).im = s.im - (ρ : ℂ).im := Complex.sub_im _ _\n      have h7 : |(s - (ρ : ℂ)).im| ≤ ‖s - (ρ : ℂ)‖ := abs_im_le_norm _\n      rw [h6] at h7\n      linarith [h5, h7]\n    · -- the near-axis arcs: |re s| > √13 ⟹ ‖s−ρ‖ ≥ √13−1 ≥ 2\n      push Not at hre13\n      have hsqrt : Real.sqrt 13 < |s.re| := by\n        rw [Real.sqrt_lt (by norm_num : (0 : ℝ) ≤ 13) (abs_nonneg _)]\n        rw [sq_abs]\n        exact hre13\n      have h3le : (3 : ℝ) ≤ Real.sqrt 13 := by\n        rw [show (3 : ℝ) = Real.sqrt (3 ^ 2) from (Real.sqrt_sq (by norm_num)).symm]\n        exact Real.sqrt_le_sqrt (by norm_num : (3 : ℝ) ^ 2 ≤ 13)\n      have h1 : |s.re| - |(ρ : ℂ).re| ≤ |s.re - (ρ : ℂ).re| := abs_sub_abs_le_abs_sub _ _\n      have hreρ : |(ρ : ℂ).re| ≤ 1 := by\n        rw [abs_le]\n        exact ⟨by linarith [ρ.2.2.1], by linarith [ρ.2.2.2]⟩\n      have h2 : (2 : ℝ) < |s.re - (ρ : ℂ).re| := by linarith [hsqrt, h3le, h1, hreρ]\n      have h3 : (s - (ρ : ℂ)).re = s.re - (ρ : ℂ).re := Complex.sub_re _ _\n      have h4 : |(s - (ρ : ℂ)).re| ≤ ‖s - (ρ : ℂ)‖ := abs_re_le_norm _\n      rw [h3] at h4\n      have h5 : 1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ 2 := by\n        rw [div_le_iff₀ (by positivity : (0 : ℝ) < 32 * C0hat (4 * (k : ℝ) + 9 / 2))]\n        linarith [hĈ2]\n      linarith [h2, h4, h5]\n  -- the per-element term bound g ρ ≤ 64·Ĉ₀·m\n  have hterm : ∀ ρ ∈ FS, ‖seriesTerm s ρ‖\n      ≤ 64 * C0hat (4 * (k : ℝ) + 9 / 2) * (zeroMult (ρ : ℂ) : ℝ) := by\n    intro ρ hρ\n    rw [hFS, Finset.mem_filter] at hρ\n    obtain ⟨-, hρRm2, hρRp2⟩ := hρ\n    have hρRm2' : (R - 2 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_ge hρRm2\n    have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := by linarith [hR]\n    have hsepρ := hsep ρ hρ\n    have hsepρpos : (0 : ℝ) < ‖s - (ρ : ℂ)‖ := by\n      have h1 : (0 : ℝ) < 1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)) := by positivity\n      linarith [hsepρ, h1]\n    have hid := seriesTerm_norm_eq_div hs hsz ρ\n    rw [hid]\n    have hm : (0 : ℝ) ≤ (zeroMult (ρ : ℂ) : ℝ) := Nat.cast_nonneg _\n    have hden : (R - 2) * (1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)))\n        ≤ ‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖ :=\n      mul_le_mul hρRm2'.le hsepρ (by positivity) (by linarith [hR])\n    have h1 : R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖)\n        ≤ R / ((R - 2) * (1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2)))) := by\n      apply div_le_div_of_nonneg_left hRpos.le (by positivity)\n      exact hden\n    have h2 : R / ((R - 2) * (1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2))))\n        = 32 * C0hat (4 * (k : ℝ) + 9 / 2) * (R / (R - 2)) := by\n      field_simp\n      ring\n    have h3 : R / (R - 2) ≤ 2 := by\n      rw [div_le_iff₀ (by linarith [hR] : (0 : ℝ) < R - 2)]\n      linarith [hR]\n    calc (zeroMult (ρ : ℂ) : ℝ) * (R / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖))\n        ≤ (zeroMult (ρ : ℂ) : ℝ) *\n            (R / ((R - 2) * (1 / (32 * C0hat (4 * (k : ℝ) + 9 / 2))))) :=\n          mul_le_mul_of_nonneg_left h1 hm\n      _ = (zeroMult (ρ : ℂ) : ℝ) * (32 * C0hat (4 * (k : ℝ) + 9 / 2) * (R / (R - 2))) := by\n          rw [h2]\n      _ ≤ (zeroMult (ρ : ℂ) : ℝ) * (32 * C0hat (4 * (k : ℝ) + 9 / 2) * 2) := by\n          apply mul_le_mul_of_nonneg_left _ hm\n          exact mul_le_mul_of_nonneg_left h3\n            (mul_nonneg (by norm_num : (0 : ℝ) ≤ 32) hĈpos.le)\n      _ = 64 * C0hat (4 * (k : ℝ) + 9 / 2) * (zeroMult (ρ : ℂ) : ℝ) := by ring\n  -- the single-window count\n  have hcount : ∑ ρ ∈ FS, (zeroMult (ρ : ℂ) : ℝ)\n      ≤ 3 * A0count * 7 * (2 * Real.log R) := by\n    have hM1 : (1 : ℝ) ≤ max (R - 3) (R - 3) := by rw [max_self]; linarith [hR]\n    have hMb : max (R - 3) (R - 3) ≤ R + 2 := by rw [max_self]; linarith [hR]\n    have hsub : ∀ ρ ∈ FS,\n        R - 3 ≤ |(ρ : ℂ).im| ∧ |(ρ : ℂ).im| ≤ R + 2 ∧ R - 3 ≤ |(ρ : ℂ).im| := by\n      intro ρ hρ\n      rw [hFS, Finset.mem_filter] at hρ\n      obtain ⟨-, hρRm2, hρRp2⟩ := hρ\n      have hρRm2' : (R - 2 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_not_ge hρRm2\n      have him1 := abs_im_ge_norm_sub_one ρ\n      have him2 : |(ρ : ℂ).im| ≤ ‖(ρ : ℂ)‖ := abs_im_le_norm _\n      exact ⟨by linarith [him1, hρRm2'], by linarith [him2, hρRp2],\n        by linarith [him1, hρRm2']⟩\n    have hbrick := sum_zeroMult_le_of_im_band FS hM1 hMb hsub\n    have hab : R + 2 - (R - 3) + 2 = 7 := by ring\n    have hmax : max |R - 3| |R + 2| = R + 2 := by\n      rw [abs_of_nonneg (by linarith [hR] : (0 : ℝ) ≤ R - 3),\n        abs_of_nonneg (by linarith [hR] : (0 : ℝ) ≤ R + 2)]\n      exact max_eq_right (by linarith [hR])\n    rw [hab, hmax] at hbrick\n    have hlogle : Real.log (3 * (R + 2) + 5) ≤ 2 * Real.log R := by\n      have h1 : Real.log (3 * (R + 2) + 5) ≤ Real.log (4 * R) := by\n        apply Real.log_le_log (by linarith [hRpos])\n        linarith [hR]\n      have h2 : Real.log (4 * R) = Real.log 4 + Real.log R :=\n        Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) (by linarith [hR] : R ≠ 0)\n      have h3 : Real.log 4 = 2 * Real.log 2 := by\n        rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]\n        push_cast\n        ring\n      have h4 := log_two_le_one\n      linarith [h1, h2, h3, h4, hlogR]\n    exact hbrick.trans (mul_le_mul_of_nonneg_left hlogle\n      (mul_nonneg (mul_nonneg (by norm_num : (0 : ℝ) ≤ 3) A0count_pos.le)\n        (by norm_num : (0 : ℝ) ≤ 7)))\n  -- assemble\n  have hsum : ∑ ρ ∈ FS, ‖seriesTerm s ρ‖\n      ≤ ∑ ρ ∈ FS, 64 * C0hat (4 * (k : ℝ) + 9 / 2) * (zeroMult (ρ : ℂ) : ℝ) :=\n    Finset.sum_le_sum hterm\n  have hfact : ∑ ρ ∈ FS, 64 * C0hat (4 * (k : ℝ) + 9 / 2) * (zeroMult (ρ : ℂ) : ℝ)\n      = (64 * C0hat (4 * (k : ℝ) + 9 / 2)) * ∑ ρ ∈ FS, (zeroMult (ρ : ℂ) : ℝ) := by\n    rw [Finset.mul_sum]\n  have hfin : (64 : ℝ) * C0hat (4 * (k : ℝ) + 9 / 2) * (3 * A0count * 7 * (2 * Real.log R))\n      = 2688 * C0hat (4 * (k : ℝ) + 9 / 2) * A0count * Real.log R := by ring\n  calc ∑ ρ ∈ FS, ‖seriesTerm s ρ‖\n      ≤ ∑ ρ ∈ FS, 64 * C0hat (4 * (k : ℝ) + 9 / 2) * (zeroMult (ρ : ℂ) : ℝ) := hsum\n    _ = (64 * C0hat (4 * (k : ℝ) + 9 / 2)) * ∑ ρ ∈ FS, (zeroMult (ρ : ℂ) : ℝ) := hfact\n    _ ≤ (64 * C0hat (4 * (k : ℝ) + 9 / 2)) * (3 * A0count * 7 * (2 * Real.log R)) :=\n        mul_le_mul_of_nonneg_left hcount\n          (mul_nonneg (by norm_num : (0 : ℝ) ≤ 64) hĈpos.le)\n    _ = 2688 * C0hat (4 * (k : ℝ) + 9 / 2) * A0count * Real.log R := hfin\n\nend NguyenRH1\n\nend"},"extra_content":null}]