← Session 29 — ii′-5e-v: circle bound (far-tail + series bounds)
thinking (2251 chars)
`HasDerivAt.const_cpow (hf) (h0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x`.
Now I have everything for 5e-v-c. Let me set up the build plan with sub-stages:
**c-i: the (G)-at-real-point + gapCircle_sep + nearZeros count.**
1. `differentiableAt_Gammaℝ_of_not_neg_nat {s : ℂ} (hs : ∀ m : ℕ, s / 2 ≠ -(m : ℂ)) : DifferentiableAt ℂ Complex.Gammaℝ s` — clone of the im≠0 proof.
2. `logDeriv_Gammaℝ_eq_of_not_neg_nat {s₀ : ℂ} (hs : ∀ m : ℕ, s₀ / 2 ≠ -(m : ℂ)) : logDeriv Gammaℝ s₀ = −(log π:ℂ)/2 + (1/2:ℂ)·digamma (s₀/2)` — via logDeriv_mul.
3. `gapCircle_sep` — the standalone separation 1/(32Ĉ₀) ≤ ‖s−ρ‖ for nontrivial ρ with ‖ρ‖ ∈ (R−2, R+2) (clone of shell_crit's hsep, ρ : ℂ).
4. `nearZeros_count_le {t : ℝ} (ht : 10 ≤ |t|) : ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℝ) ≤ 3·A0count·Real.log (3·max |t−1| |t+1| + 5)` — zerosIn(t−1, t+1] cover + Ncount_le_of_interval_gen.
5. `nearZeros_term_le` — per-ρ separation: for ρ ∈ nearZeros (s.im): 1/(32Ĉ₀) ≤ ‖s−ρ‖ (the ‖ρ‖ > R−2 vs ≤ R−2 split + gapCircle_sep).
**c-ii: digamma bounds.**
6. `digamma_right_le {w} (hwre : 1.75 ≤ w.re) : ‖digamma w‖ ≤ 48 + 23·log(2+‖w‖)`.
7. `digamma_circle_le {s} (hs : ‖s‖ = R) (hgapInt) (hR : 16002 ≤ R) : ‖digamma (s/2)‖ ≤ 62 + 23·log (2 + R/2)`.
8. Small elems: `norm_one_div_circle_le`, `log_pi_div_two_le`.
**c-iii: logDeriv_circle_le + Fexpr_circle_le.**
9. `logDeriv_circle_le` — the three regions. Includes: the near-sum bound (via nearZeros count + separation), the FE route for re < −5/2 (logDeriv_zeta_fe at all points — hypotheses discharged: s ≠ 0 (‖s‖=R>0), s ≠ 1 (re < −5/2), Gammaℝ s ≠ 0 (Gammaℝ_eq_zero_iff + pole avoidance: s/2 ∉ −ℕ — for im s ≠ 0: im(s/2) ≠ 0 ✓; for s = −R: dist(R/2,ℤ) ≥ 1/4 ✓ hgapInt), ζ s ≠ 0 (zeta_zero_classification + s ≠ −2n: s/2 ∉ −ℕ ⟹ s ≠ −2n ✓ same; s ≠ 0 ✓; not nontrivial: re < −5/2 vs (0,1) ✓), DifferentiableAt Gammaℝ s (via #1 with s/2 ∉ −ℕ ✓), and at 1−s: 1−s ≠ 0 ✓ (s≠1), 1−s ≠ 1 ✓ (s≠0), Gammaℝ(1−s) ≠ 0 ((1−s)/2 ∉ −ℕ: re((1−s)/2) > 0 ✓), ζ(1−s) ≠ 0 (re(1−s) > 1: Mathlib's riemannZeta_ne_zero_of_one_le_re? — check the name; used in 5c/5d — grep), DifferentiableAt ✓ ((1−s)/2 ∉ −ℕ ✓).
10. `Fexpr_circle_le` — the assembly.
Let me also check Gammaℝ_eq_zero_iff and the zeta nonvanishing names quickly.
All API pinned. Check the zero-vanishing facts needed for the FE route (`Gammaℝ_eq_zero_iff`, `Gamma_ne_zero`, zeta nonvanishing re ≥ 1).
tool: Grep ok
input
{
"pattern": "(Gamma\u211d_eq_zero_iff|Gamma_ne_zero|riemannZeta_ne_zero_of_one_le_re|zeta_ne_zero_of_one_le_re|zeta_zero_classification)",
"path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1",
"output_mode": "content",
"-n": true,
"head_limit": 20
}
result 2026-08-24 02:24:28Z → 2026-08-26 19:48:08Z
mode='content' num_files=0 filenames=[] content="research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean:76:theorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n)\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-77- {T: ℝ} (hT1 : 1 ≤ T) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1)\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-78- (hTwide: ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-79- ρ.im < Real.sqrt n + 2 → 1 \\ (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|):\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-80- |Sf n| ≤ ‖RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)‖ +\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-81- ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2: ℂ)}),\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-82- (zeroMult ρ: ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := by\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-83- set z:= rectZ T\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-84- set w:= rectW n T\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-85- have hn1sqrt: (1 : ℝ) ≤ Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-86- have hre: z.re ≤ w.re := by\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-87- rw [rectZ_re, rectW_re]\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-88- have h:= Real.sqrt_nonneg (n : ℝ)\n--\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean:443:theorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12))\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-444- (hZCG: ZeroCountGlobalProp) (hNLZ : NoLowZeros) {n : ℕ} {T : ℝ}\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-445- (hTle: T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-446- ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2: ℂ)}),\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-447- (zeroMult ρ: ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-448- have h2not: (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-449- intro h\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-450- have hnt:= (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-451- have h21: (0 : ℝ) < (-2 : ℂ).re := hnt.2.1\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-452- norm_num at h21\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-453- have hdisj2: Disjoint (zeroBothWindow_finite T).toFinset {(-2 : ℂ)} := by\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-454- rw [Finset.disjoint_left]\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiAssembly.lean-455- intro ρ hρ hρ2\n--\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean:404:theorem exists_zero_avoiding_T_wide (hZC : ZeroCountProp) {a : ℝ} (ha : 3 ≤ a) :\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-405- ∃ T: ℝ, a ≤ T ∧ T ≤ a + 1 ∧\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-406- ∀ ρ: ℂ, IsNontrivialZero ρ → a - 1 < ρ.im → ρ.im < a + 2 →\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-407- 1 \\ (9 * C0hat (a + 2)) ≤ |ρ.im - T|:= by\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-408- classical\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-409- have hfin:= zeroWindowWide_finite a\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-410- set WF: Finset ℂ := hfin.toFinset with hWF_def\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-411- have hWFmem: ∀ ρ : ℂ, ρ ∈ WF ↔ ρ ∈ zeroWindowWide a :=\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-412- fun ρ => Set.Finite.mem_toFinset hfin\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-413- set S: Finset ℝ := WF.image Complex.im with hS_def\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-414- have hScard: S.card ≤ WF.card := Finset.card_image_le\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-415- have hWFcard: (WF.card : ℝ) ≤ 3 * C0hat (a + 2) := zeroWindowWide_card_le hZC ha\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean-416- obtain ⟨T, hT1, hT2, hT3⟩:= exists_avoiding_midpoint a S hScard\n--\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean:2443:def FAlt (T : ℝ) : ℝ :=\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2444- (1 / (2 * Real.pi)) * (T * Real.log T) + 0.137 * Real.log T +\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2445- 0.443 * Real.log (Real.log T) + (7 / 8 + 1.588)\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2446-\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2447-/-- The explicit finite-part bound B(n) (D-037 (4.1) CORRECTED per D-071,\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2448-user-approved session 038; REPAIRED per D-074, session 040; constants\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2449-A = 10.5, B₀ = 48 from D-056; Ĉ₀/Ĥ/Z₂ closed forms; M₀ = 1.3352 from\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2450-E-023; IIMaj the I_I majorant), with the zero-count majorant F as a\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2451-parameter:\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2452-B(n) = 4F(T) + 4T[(2/3)Z₂(T) + 10.5·log(T+2) + 48] + 40·1.3352\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2453- + 2(e⁴+1)·7Ĥ(T) + 2·DogLegRight(n) + IIMaj(n) + 1, T = √n + 1.\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2454-The corrections: (D-071 F-A/F-B) the bridge is 4F (both-signs slip,\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2455-R-004 unaffected) and the I_III near-sum uses (2/3)Z₂ (D-069 Finding 2\n--\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean:2463:def Bn (F : ℝ → ℝ) (n : ℝ) : ℝ :=\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2464- let T:= Real.sqrt n + 1\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2465- 4 * F T + 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2466- 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T) +\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2467- 2 * DogLegRight n + IIMaj n + 1\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2468-\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2469-/-- [PROVED session 012] The margin IS sInftyLower − Bn + 1 (pure\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2470-bookkeeping; same constants as `marginTilde_eq_expanded`). -/\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2471-theorem marginTilde_eq_sub (F: ℝ → ℝ) (n : ℝ) :\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2472- marginTilde F n = sInftyLower n - Bn F n + 1:= by\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2473- simp only [marginTilde, Bn, sInftyLower]\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2474-\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2475-/-- The finite part S_f(n) of the Bombieri–Lagarias decomposition\n--\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean:2480:def Sf (n : ℕ) : ℝ := SInfty n + 1 - (liCoeff n).re\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2481-\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2482-\\-- ⭐ THE named analytic hypothesis of tier (ii): the finite part is\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2483-bounded by the explicit traced B(n) on the whole margin range\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2484-10⁵ ≤ n ≤ N₁ = (T₀−1)², T₀ = 3×10¹².\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2485-Proof content (triage D-062): the D-036/D-056 contour estimate — kernel\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2486-bounds + reference-point R-bound (Mathlib-tractable complex analysis),\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2487-Trudgian 2014 N(T)/S(T) (trusted-perimeter literature candidate), the\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2488-bridge via `RHUpTo` (perimeter), M₀ (E-023 grid; E-023b acb optional). -/\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean:2489:def SfBoundProp : Prop :=\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2490- ∀ n: ℕ, 100000 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2491- |Sf n| ≤ Bn FAlt (n: ℝ)\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2492-\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2493-/-! ### The ψ-blocks of FAlt (D-057 table rows #1/#3/#4) -/\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2494-\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2495-/-- [PROVED session 012] Per-point derivative of T·log T. -/\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2496-theorem hasDerivAt_T_mul_log (x: ℝ) (hx : 0 < x) :\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2497- HasDerivAt (fun t => t * Real.log t) (Real.log x + 1) x:= by\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2498- have h:= (hasDerivAt_id' x).mul (Real.hasDerivAt_log (ne_of_gt hx))\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2499- rwa [one_mul, mul_inv_cancel₀ (ne_of_gt hx)] at h\nD:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2500-\nresearch\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean-2501-\\-- [PROVED session 012] Block #1 (T·log T): ψ-formula. -/" num_lines=92 num_matches=None applied_limit=None applied_offset=None
raw content_json (database row)
[{"type":"thinking","thinking":"`HasDerivAt.const_cpow (hf) (h0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x`.\n\nNow I have everything for 5e-v-c. Let me set up the build plan with sub-stages:\n\n**c-i: the (G)-at-real-point + gapCircle_sep + nearZeros count.**\n1. `differentiableAt_Gammaℝ_of_not_neg_nat {s : ℂ} (hs : ∀ m : ℕ, s / 2 ≠ -(m : ℂ)) : DifferentiableAt ℂ Complex.Gammaℝ s` — clone of the im≠0 proof.\n2. `logDeriv_Gammaℝ_eq_of_not_neg_nat {s₀ : ℂ} (hs : ∀ m : ℕ, s₀ / 2 ≠ -(m : ℂ)) : logDeriv Gammaℝ s₀ = −(log π:ℂ)/2 + (1/2:ℂ)·digamma (s₀/2)` — via logDeriv_mul.\n3. `gapCircle_sep` — the standalone separation 1/(32Ĉ₀) ≤ ‖s−ρ‖ for nontrivial ρ with ‖ρ‖ ∈ (R−2, R+2) (clone of shell_crit's hsep, ρ : ℂ).\n4. `nearZeros_count_le {t : ℝ} (ht : 10 ≤ |t|) : ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℝ) ≤ 3·A0count·Real.log (3·max |t−1| |t+1| + 5)` — zerosIn(t−1, t+1] cover + Ncount_le_of_interval_gen.\n5. `nearZeros_term_le` — per-ρ separation: for ρ ∈ nearZeros (s.im): 1/(32Ĉ₀) ≤ ‖s−ρ‖ (the ‖ρ‖ > R−2 vs ≤ R−2 split + gapCircle_sep).\n\n**c-ii: digamma bounds.**\n6. `digamma_right_le {w} (hwre : 1.75 ≤ w.re) : ‖digamma w‖ ≤ 48 + 23·log(2+‖w‖)`.\n7. `digamma_circle_le {s} (hs : ‖s‖ = R) (hgapInt) (hR : 16002 ≤ R) : ‖digamma (s/2)‖ ≤ 62 + 23·log (2 + R/2)`.\n8. Small elems: `norm_one_div_circle_le`, `log_pi_div_two_le`.\n\n**c-iii: logDeriv_circle_le + Fexpr_circle_le.**\n9. `logDeriv_circle_le` — the three regions. Includes: the near-sum bound (via nearZeros count + separation), the FE route for re < −5/2 (logDeriv_zeta_fe at all points — hypotheses discharged: s ≠ 0 (‖s‖=R>0), s ≠ 1 (re < −5/2), Gammaℝ s ≠ 0 (Gammaℝ_eq_zero_iff + pole avoidance: s/2 ∉ −ℕ — for im s ≠ 0: im(s/2) ≠ 0 ✓; for s = −R: dist(R/2,ℤ) ≥ 1/4 ✓ hgapInt), ζ s ≠ 0 (zeta_zero_classification + s ≠ −2n: s/2 ∉ −ℕ ⟹ s ≠ −2n ✓ same; s ≠ 0 ✓; not nontrivial: re < −5/2 vs (0,1) ✓), DifferentiableAt Gammaℝ s (via #1 with s/2 ∉ −ℕ ✓), and at 1−s: 1−s ≠ 0 ✓ (s≠1), 1−s ≠ 1 ✓ (s≠0), Gammaℝ(1−s) ≠ 0 ((1−s)/2 ∉ −ℕ: re((1−s)/2) > 0 ✓), ζ(1−s) ≠ 0 (re(1−s) > 1: Mathlib's riemannZeta_ne_zero_of_one_le_re? — check the name; used in 5c/5d — grep), DifferentiableAt ✓ ((1−s)/2 ∉ −ℕ ✓).\n10. `Fexpr_circle_le` — the assembly.\n\nLet me also check Gammaℝ_eq_zero_iff and the zeta nonvanishing names quickly.","signature":""},{"type":"text","text":"All API pinned. Check the zero-vanishing facts needed for the FE route (`Gammaℝ_eq_zero_iff`, `Gamma_ne_zero`, zeta nonvanishing re ≥ 1)."},{"type":"tool_use","id":"Grep_158","name":"Grep","input":{"pattern":"(Gammaℝ_eq_zero_iff|Gamma_ne_zero|riemannZeta_ne_zero_of_one_le_re|zeta_ne_zero_of_one_le_re|zeta_zero_classification)","path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1","output_mode":"content","-n":true,"head_limit":20},"extra_content":null}]