← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (13482 chars)
Committed. Now Section 3: the complex series + the identity principle. Let me write it:
```lean
/-! ## 3. The complex series and the identity with Complex.digamma -/
/-- The complex digamma series summand. -/
def dpsiTermC (s : ℂ) (m : ℕ) : ℂ := 1 / ((m : ℂ) + 1) - 1 / (s + m + 1)
/-- The complex digamma series. -/
def DinfC (s : ℂ) : ℂ :=
-(Real.eulerMascheroniConstant : ℂ) - 1 / s + ∑' m : ℕ, dpsiTermC s m
```
The domain: U := Metric.ball (1/2 : ℂ) (1/2).
Lemmas:
(a) Summable (dpsiTermC s) for s ∈ U: ‖dpsiTermC s m‖ = ‖s‖/(‖↑m+1‖·‖s+↑m+1‖) — bounds: for s ∈ U: ‖s‖ < 1 (‖s‖ ≤ ‖s − 1/2‖ + ‖1/2‖ < 1 ✓); ‖s + ↑m + 1‖ ≥ |re(s + m + 1)| = re s + m + 1 > m (re s > 0 for s ∈ U: |re s − 1/2| ≤ |s − 1/2| < 1/2 ⟹ re s > 0 ✓) — hmm ‖s+m+1‖ ≥ re(s+m+1) = re s + m + 1 ≥ m + 1·(re s)... — use ‖z‖ ≥ |re z| (`Complex.abs_re_le_norm`? — `Complex.abs_re_le_norm z : |z.re| ≤ ‖z‖` ✓ used in LiSkeleton line 204). So ‖s+m+1‖ ≥ re s + m + 1 ≥ ... m + 1 (re s > 0)... ≥ (m+1)·(re s)?? no — ≥ m + re s·... let me just: ‖s+m+1‖ ≥ re s + m + 1. For the summability bound: ‖term‖ ≤ ‖s‖/((m+1)·(re s + m + 1)) ≤ ‖s‖/((m+1)·(m+1))·(1/re s)? — hmm: 1/(re s + m + 1) ≤ 1/(m+1) (re s > 0) — so ‖term‖ ≤ ‖s‖/(m+1)² ≤ 1/(m+1)²·(‖s‖) — with ‖s‖ < 1: ≤ 1/(m+1)² — but for the SUMMABILITY at a FIXED s, the bound u m := ‖s‖/(m+1)²·(1/...)... — let me use: ‖dpsiTermC s m‖ ≤ (‖s‖/re s)·(1/(m+1)²)·... hmm: ‖term‖ = ‖s‖/((m+1)‖s+m+1‖) ≤ ‖s‖/((m+1)(re s + m + 1)) — and (re s + m + 1) ≥ m + 1 gives ≤ ‖s‖/(m+1)² ✓ (no re s needed!) — wait: 1/(re s + m + 1) ≤ 1/(m+1) since re s ≥ 0 ✓ — so ‖term‖ ≤ ‖s‖/(m+1)² — and for s ∈ U, ‖s‖ < 1: ≤ 1/(m+1)². So summable via comparison with (‖s‖/(m+1)²) — the complex comparison: `Summable.of_norm_bounded (summable_div_add_one_sq ‖s‖)` — wait the dominator family fun m => ‖s‖/(m+1)² ✓ summable ✓ — and ‖dpsiTermC s m‖ ≤ ‖s‖/(m+1)² ✓ — via Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) — that worked in liSummable ✓.
The norm computation: ‖dpsiTermC s m‖ = ‖s / ((m+1)(s+m+1))‖: dpsiTermC s m = 1/(m+1) − 1/(s+m+1) = s/((m+1)(s+m+1)) — via field_simp + ring (need (m+1:ℂ) ≠ 0 ✓ and s+m+1 ≠ 0 — for s ∈ U: re(s+m+1) > 0 ⟹ ≠ 0 ✓).
So lemma dpsiTermC_eq : dpsiTermC s m = s / ((↑m + 1) * (s + ↑m + 1)) for s ∈ U (or for s+m+1 ≠ 0 — state with (hs : s + m + 1 ≠ 0)).
Then ‖dpsiTermC s m‖ = ‖s‖/(‖↑m+1‖·‖s+m+1‖) ≤ ‖s‖/((m+1)·(re s + m + 1)) ≤ ‖s‖/(m+1)² — for s ∈ U. Fine.
(b) HasSumUniformlyOn of dpsiTermC on U (the M-test with u m := 1/(m+1)² — wait the bound needs ‖s‖ ≤ 1: ‖term‖ ≤ ‖s‖/(m+1)² ≤ 1/(m+1)² for s ∈ U ✓): so HasSumUniformlyOn dpsiTermC (fun s => ∑' m, dpsiTermC s m) U via of_norm_le_summable (summable_div_add_one_sq 1) (bound) ✓. Then TendstoLocallyUniformlyOn of the partial sums (hasSumUniformlyOn... — HasSumUniformlyOn ⟹ TendstoLocallyUniformlyOn — via hasSumUniformlyOn_iff_tendstoUniformlyOn + locally — hmm — HasSumUniformlyOn on U (open) ⟹ TendstoUniformlyOn partial sums on U ⟹ TendstoLocallyUniformlyOn ✓ (TendstoUniformlyOn.tendstoLocallyUniformlyOn? — `TendstoUniformlyOn.tendstoLocallyUniformlyOn (hs : IsOpen s)`? — there's a lemma — or via the iff). Then TendstoLocallyUniformlyOn.differentiableOn (LocallyUniformLimit.lean:136) gives DifferentiableOn ℂ (fun s => ∑' m, dpsiTermC s m) U — then DinfC differentiableOn U (the −γ − 1/s pieces differentiable on U — 0 ∉ U ✓) — then AnalyticOnNhd via DifferentiableOn.analyticOnNhd isOpen_ball.
Wait — TendstoLocallyUniformlyOn.differentiableOn's exact signature (line 136): `_root_.TendstoLocallyUniformlyOn.differentiableOn [φ.NeBot] (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U)?` — let me check — from line 136-137: `theorem _root_.TendstoLocallyUniformlyOn.differentiableOn [φ.NeBot] (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) : DifferentiableOn ℂ f U`? — roughly. The F := partial sums (differentiable on U: finite sums of the terms ✓) — f := the tsum function ✓.
(c) The cast bridge: DinfC ↑x = ↑(DinfR x) for x ∈ (0,1):
DinfC ↑x = −γ − 1/↑x + ∑' m, dpsiTermC ↑x m; ↑(DinfR x) = ↑(−γ − 1/x + ∑' m, dpsiTermR x m) — push_cast (distributes ↑ over +, −, /, the constants: ↑(−γ) = −↑γ ✓ — and the tsum: ↑(∑' m, dpsiTermR x m) = ∑' m, ↑(dpsiTermR x m) via Complex.ofRealCLM.map_tsum (dpsiTermR_summable hx) — and ↑(dpsiTermR x m) = dpsiTermC ↑x m (push_cast per-term ✓). So:
```lean
lemma DinfC_ofReal {x : ℝ} (hx : 0 < x) : DinfC (↑x) = ↑(DinfR x) := by
rw [DinfC, DinfR]
push_cast
rw [show ((↑(∑' m : ℕ, dpsiTermR x m)) : ℂ) = ∑' m : ℕ, dpsiTermC (↑x) m from ?_] -- hmm
...
```
Let me structure:
```lean
lemma DinfC_ofReal {x : ℝ} (hx : 0 < x) : DinfC (↑x) = ↑(DinfR x) := by
have h1 : (↑(∑' m : ℕ, dpsiTermR x m) : ℂ) = ∑' m : ℕ, dpsiTermC (↑x) m := by
rw [Complex.ofRealCLM_apply ▸ ...] -- use map_tsum
have := Complex.ofRealCLM.map_tsum (dpsiTermR_summable hx)
-- this : ofRealCLM (∑' m, dpsiTermR x m) = ∑' m, ofRealCLM (dpsiTermR x m)
rw [Complex.ofRealCLM_apply] at this -- turns ofRealCLM into ↑
rw [this]
apply tsum_congr
intro m
rw [dpsiTermR, dpsiTermC]
push_cast
ring
rw [DinfC, DinfR]
push_cast
rw [h1]?? hmm — after push_cast the ↑(∑' ...) becomes ... push_cast might rewrite the cast-of-tsum via map_tsum itself? push_cast has `Complex.ofReal_tsum`? no. Let me do it stepwise:
rw [DinfC, DinfR]
push_cast
-- goal: −↑γ − 1/↑x + ↑(∑' m, dpsiTermR x m) = ... hmm the DinfC LHS: −↑γ − 1/↑x + ∑' m, dpsiTermC ↑x m — and RHS ↑(−γ − 1/x + ∑' ...) → push_cast → −↑γ − 1/↑x + ↑(∑' ...) — then rw [h1] and congr
```
Order: rw [DinfC, DinfR] unfolds both; push_cast normalizes the RHS's outer casts (keeping ↑(∑'...) as an atom hopefully — push_cast distributes over +/−/// but not over tsum ✓); then rw [h1] : ↑(∑' m, dpsiTermR x m) → ∑' m, dpsiTermC ↑x m ✓ then both sides −↑γ − 1/↑x + ∑' ... — wait the LHS (DinfC ↑x) has −(↑γ) − 1/↑x + ∑' dpsiTermC — hmm push_cast also normalizes the LHS's −(Real.eulerMascheroniConstant : ℂ) — it's already a cast — fine. Then ring/rfl. Manageable.
Hmm — `Complex.ofRealCLM.map_tsum` — the signature from Module.lean:134: `protected theorem ContinuousLinearMap.map_tsum [T2Space M₂] [L.NeBot] {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f L) : φ (∑'[L] z, f z) = ∑'[L] z, φ (f z)` — the ∑'[L] — the summation filter L — with `[L.NeBot]` — the plain ∑' uses the default filter — is the default `L` the universal filter ⊤? In current Mathlib, `∑' z, f z` = `∑'[⊤] z, f z`? or the default SummationFilter... There was a refactor (SummationFilter.lean exists) — plain ∑' is notation for ∑'[⊤] (the "universal" filter) I believe. So map_tsum with L := ⊤ — `[L.NeBot]` — ⊤ is NeBot ✓ instance. So Complex.ofRealCLM.map_tsum (hf : Summable f) : ofRealCLM (∑' z, f z) = ∑' z, ofRealCLM (f z) ✓ — with the plain ∑' ✓.
(d) digamma = DinfC on U via the identity principle:
- digamma AnalyticOnNhd U: digamma = logDeriv Complex.Gamma = fun s => deriv Complex.Gamma s / Complex.Gamma s — analytic on U since Gamma analytic & nonvanishing on U: for s ∈ U (ball (1/2)(1/2)): re s > 0 — Gamma differentiable at s (differentiableAt_Gamma — needs s ≠ −m: re s > 0 ⟹ s ≠ −(m:ℂ) since re(−m) = −m ≤ 0 < re s ✓) and Gamma s ≠ 0 (`Complex.Gamma_ne_zero (hs : ∀ m, s ≠ -↑m)`? — name: from digamma_apply_add_one's proof: `Gamma_ne_zero hs` with hs : ∀ m : ℕ, s ≠ -m ✓ exists as Complex.Gamma_ne_zero presumably).
AnalyticOnNhd ℂ digamma U: for s ∈ U: AnalyticAt ℂ digamma s: digamma = deriv Gamma / Gamma — deriv Gamma analytic at s: Gamma analytic at s (DifferentiableAt → AnalyticAt? — for ℂ: differentiable at a POINT doesn't imply analytic at the point — need differentiability on a nhd — `DifferentiableAt.analyticAt`? no. The right route: Gamma is analytic on ℂ minus poles — is there `Complex.analyticAt_Gamma`? hmm — differentiableAt_Gamma gives pointwise; for analyticity use: DifferentiableOn on an open nhd ⟹ analytic — the set ℂ ∖ {0, −1, ...} — or just on U directly: DifferentiableOn ℂ Gamma U (each point differentiable ✓) — U open ⟹ AnalyticOnNhd ℂ Gamma U (`DifferentiableOn.analyticOnNhd`? — hmm — the right name: `DifferentiableOn.analyticOnNhd (h : DifferentiableOn ℂ f s) (hs : IsOpen s) : AnalyticOnNhd ℂ f s` — I believe it exists — it was used in... zetaA's proof used `.analyticOnNhd Metric.isOpen_ball` on a DifferentiableOn — from LiResidue line 77: `h.analyticOnNhd Metric.isOpen_ball` — so DifferentiableOn.analyticOnNhd ✓ EXISTS).
Then AnalyticOnNhd ℂ (deriv Gamma) U := (AnalyticOnNhd Gamma U).deriv — `AnalyticOnNhd.deriv` ✓ (exists — used implicitly? AnalyticOnNhd.deriv : AnalyticOnNhd f s → AnalyticOnNhd (deriv f) s ✓ I believe).
Then the quotient: AnalyticOnNhd (deriv Gamma / Gamma) U: AnalyticOnNhd.div with Gamma ≠ 0 on U ✓ — `AnalyticOnNhd.div (hf : AnalyticOnNhd f s) (hg : AnalyticOnNhd g s) (hg0 : ∀ x ∈ s, g x ≠ 0)`? — hmm — AnalyticOnNhd.div might not exist with that exact form — there's `AnalyticAt.div` (used in LiResidue: hda.div ha hne ✓ pointwise) — so build pointwise: AnalyticOnNhd f U means ∀ x ∈ U, AnalyticAt f x — pointwise AnalyticAt.div ✓.
- DinfC AnalyticOnNhd U ✓ from (b).
- The frequently-eq at z₀ := ↑(1/2): ∃ᶠ z in 𝓝[≠] ↑(1/2), digamma z = DinfC z: from the real-segment agreement: for real x ∈ (0,1), x ≠ 1/2: digamma ↑x = ↑(DinfR x) [psiReal bridge + cast] = DinfC ↑x [cast bridge]. The frequently: the set S := {↑x : x ∈ (0,1)} ∋ points arbitrarily close to ↑(1/2) with x ≠ 1/2: formalize via a sequence: z_n := ↑(1/2 + 1/(n+2)) — z_n → ↑(1/2), z_n ≠ ↑(1/2), and digamma z_n = DinfC z_n (1/(n+2) ∈ (0,1) for n ≥ 1... 1/2 + 1/(n+2) ∈ (0,1) ⟺ 1/(n+2) < 1/2 ⟺ n ≥ 1 — take n ≥ 1 or use 1/(n+3)). Then `frequently` from the sequence: `Filter.frequently_atTop`... — the bridge: Tendsto z_n (𝓝 ↑(1/2)) with z_n ≠ point + P z_n ∀ n ⟹ ∃ᶠ z in 𝓝[≠] z₀, P z — there's `Filter.Tendsto.frequently_...`? — `Frequently` from a sequence: I recall `frequently_of_...`? — maybe easiest: ∃ᶠ z in 𝓝[≠] z₀, P z ⟺ ∀ U ∈ 𝓝[≠] z₀, ∃ z ∈ U, P z — `Filter.frequently_iff`? — `frequently_iff : (∃ᶠ x in l, P x) ↔ ∀ U ∈ l, ∃ x ∈ U, P x`? hmm — `Filter.frequently_iff` might be about ≤... Let me use: `Filter.Frequently` unfolds — `frequently_iff_exists_...`? Alternatively: the AccPt formulation: ∃ᶠ z in 𝓝[≠] z₀, P z ⟺ AccPt z₀ (𝓟 {z | P z})? no wait — there's `accPt_iff_frequently : AccPt x s ↔ ∃ᶠ y in 𝓝[≠] x, y ∈ s`? — hmm — actually simplest robust: prove ∃ᶠ via the sequence using `Filter.frequently_of_seq`?... Let me search for the right frequently-from-sequence lemma at build. Alternatively use a DIFFERENT identity principle form: `eqOn_of_preconnected_of_eventuallyEq` needs agreement on a whole nhd — I only have the segment. Hmm — there's also the zero-set-codiscrete route... Let me just do the frequently via: 𝓝[≠] z₀'s membership: every punctured-nhd set contains a point of the segment:
```lean
have hfreq : ∃ᶠ z in 𝓝[≠] (↑(1/2 : ℝ)), Complex.digamma z = DinfC z := by
rw [frequently_iff] -- hmm
...
```
Let me look up: `Filter.frequently_iff : (∃ᶠ x in l, P x) ↔ ∀ {U}, U ∈ l → ∃ x ∈ U, P x`? — there IS `frequently_iff : ...` in Mathlib/Order/Filter/Basic — `theorem Filter.frequently_iff {l : Filter α} {P : α → Prop} : (∃ᶠ x in l, P x) ↔ ∀ U ∈ l, ∃ x ∈ U, P x`? I believe so (frequently = the complement-free form). Then for U ∈ 𝓝[≠] ↑(1/2): U ⊇ (punctured ball) — pick a real point: U ∈ 𝓝[≠] z₀ means U ⊇ ball(z₀, δ) ∖ {z₀} for some δ > 0 (𝓝[≠] has such sets — `nhdsWithin` membership: U ∈ 𝓝[≠] z₀ ⟺ ∃ V ∈ 𝓝 z₀, V ∖ {z₀} ⊆ U — take V = ball — then ↑x with x real, 0 < |x − 1/2| < min(δ, 1/2) — e.g. x := 1/2 + (min δ (1/2))/2 — then ↑x ∈ U, x ∈ (0,1) ✓ and x ≠ 1/2 ✓ — the agreement holds there ✓.
This is doable but fiddly. Let me write it with frequently_iff and the ball membership extraction (`Metric.mem_nhdsWithin_iff`? — U ∈ 𝓝[≠] z₀: nhdsWithin — `Metric.nhdsWithin...`: there's `Metric.eventually_nhdsWithin...`? — use `mem_nhdsWithin_iff_exists...`? — I'll extract via: 𝓝[≠] z₀ = 𝓝[{z₀}ᶜ] z₀ — U ∈ it ⟺ ∃ V ∈ 𝓝 z₀, V ∩ {z₀}ᶜ ⊆ U (mem_nhdsWithin_iff... `mem_nhdsWithin_iff_exists_mem_nhds_inter`? hmm — `mem_nhdsWithin_iff : s ∈ 𝓝[t] a ↔ ∃ U ∈ 𝓝 a, U ∩ t ⊆ s`? — `mem_nhdsWithin_iff_exists...`? there's `mem_nhdsWithin_iff`? not sure — `Filter.mem_nhdsWithin_iff...` — I'll find it).
Hmm — this frequently argument is ~30 lines of filter fiddliness. Let me simplify by choosing a SMARTER identity-principle application: apply eqOn_of_preconnected_of_frequently_eq at a point where agreement is EASIER: is there a point where I get a full neighborhood of agreement? NO — the agreement is only on the real line. So the frequently route it is.
Actually — alternative: use the frequently via the IMAGE of the real interval under ofReal: the set S := Complex.ofReal '' Set.Ioo 0 1 — and 1/2 is an accumulation point of S: `AccPt (↑(1/2)) (𝓟 S)`? — there's `AccPt` API: `accPt_principal_iff_nhds`? — hmm. You know — let me just try frequently_iff + mem_nhdsWithin. Let me check the exact names:
- `Filter.frequently_iff`?
- `Set.mem_nhdsWithin_iff`? — there's `mem_nhdsWithin_iff_exists_mem_nhds_inter : s ∈ 𝓝[t] a ↔ ∃ U ∈ 𝓝 a, U ∩ t ⊆ s`? — I recall `mem_nhdsWithin_iff_exists_mem_nhds_inter` ✓ exists.
OK let me write Section 3 now (the complex series + analyticity + cast bridge), and leave the identity-principle for after a compile check of the base pieces. Given the hour, let me get as far as compiles cleanly tonight and commit.
Now Section 3 — the complex series, analyticity, and the cast bridge.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean",
"old_string": "end NguyenRH1",
"new_string": "/-! ## 3. The complex series: summability, analyticity, cast bridge -/\n\n/-- The complex digamma series summand. -/\ndef dpsiTermC (s : \u2102) (m : \u2115) : \u2102 := 1 / ((m : \u2102) + 1) - 1 / (s + m + 1)\n\n/-- The complex digamma series: \u2212\u03b3 \u2212 1/s + \u03a3_{m\u22650} dpsiTermC s m. -/\ndef DinfC (s : \u2102) : \u2102 :=\n -(Real.eulerMascheroniConstant : \u2102) - 1 / s + \u2211' m : \u2115, dpsiTermC s m\n\n/-- The domain: the ball of radius 1/2 around 1/2 (avoids 0, \u22121, \u22122, \u2026;\nconvex, contains the real segment (0,1)). -/\ndef dpsiDomain : Set \u2102 := Metric.ball ((1 : \u2102) / 2) (1 / 2)\n\nlemma dpsiDomain_convex : Convex \u211d dpsiDomain := convex_ball _ _\nlemma dpsiDomain_isOpen : IsOpen dpsiDomain := Metric.isOpen_ball\nlemma dpsiDomain_half : (1 : \u2102) / 2 \u2208 dpsiDomain :=\n Metric.mem_ball_self (by norm_num : (0 : \u211d) < 1 / 2)\n\nlemma dpsiTermC_pole_free {s : \u2102} (hs : s \u2208 dpsiDomain) (m : \u2115) : s + m + 1 \u2260 0 := by\n intro h\n have hre : 0 < s.re := by\n have h1 : |s.re - 1 / 2| < 1 / 2 := by\n have := hs\n rw [dpsiDomain, Metric.mem_ball] at this\n have h2 : |s.re - (1 / 2 : \u211d)| \u2264 \u2016s - (1 : \u2102) / 2\u2016 := by\n have e : s.re - 1 / 2 = (s - (1 : \u2102) / 2).re := by\n simp [Complex.sub_re, Complex.ofReal_re]\n rw [e]\n exact Complex.abs_re_le_norm _\n have h3 : dist s ((1 : \u2102) / 2) = \u2016s - (1 : \u2102) / 2\u2016 := dist_eq_norm _ _\n rw [h3] at this\n have h4 : (((1 : \u2102) / 2).re) = 1 / 2 := by simp\n linarith [this, h2]\n linarith [abs_lt.mp h1]\n have : s.re + m + 1 = 0 := by\n have h2 : (s + m + 1).re = 0 := by rw [h]; simp\n simp [Complex.add_re, Complex.ofReal_re, Complex.one_re] at this\n linarith\n linarith [Nat.cast_nonneg (\u03b1 := \u211d) m]\n\n/-- The summand in factored form: dpsiTermC s m = s/((m+1)(s+m+1)). -/\nlemma dpsiTermC_eq {s : \u2102} (hs : s + 1 \u2260 0) (m : \u2115) (hsm : s + m + 1 \u2260 0) :\n dpsiTermC s m = s / ((\u2191m + 1) * (s + \u2191m + 1)) := by\n have hm0 : ((m : \u2102) + 1) \u2260 0 := by\n intro h\n have hre : ((m : \u2102) + 1).re = 0 := by rw [h]; simp\n simp [Complex.add_re, Complex.ofReal_re, Complex.one_re] at hre\n have : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n rw [dpsiTermC]\n field_simp [hm0, hs, hsm]\n ring\n\n/-- The complex series is summable on dpsiDomain. -/\nlemma dpsiTermC_summable {s : \u2102} (hs : s \u2208 dpsiDomain) : Summable (dpsiTermC s) := by\n have hs1 : s + 1 \u2260 0 := by\n have h := dpsiTermC_pole_free hs 0\n simpa using h\n have hnorm : \u2200 m : \u2115, \u2016dpsiTermC s m\u2016 \u2264 \u2016s\u2016 / ((m : \u211d) + 1) ^ 2 := by\n intro m\n have hsm : s + m + 1 \u2260 0 := dpsiTermC_pole_free hs m\n rw [dpsiTermC_eq hs1 m hsm]\n rw [norm_div]\n have hden : \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2265 ((m : \u211d) + 1) * ((m : \u211d) + 1) := by\n rw [norm_mul]\n apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : \u211d) \u2264 \u2016(m : \u2102) + 1\u2016)\n \u00b7 -- \u2016s + m + 1\u2016 \u2265 m + 1 via the real part\n have hre : 0 < s.re := by\n have h1 : |s.re - 1 / 2| < 1 / 2 := by\n have h2 : |s.re - (1 / 2 : \u211d)| \u2264 \u2016s - (1 : \u2102) / 2\u2016 := by\n have e : s.re - 1 / 2 = (s - (1 : \u2102) / 2).re := by\n simp [Complex.sub_re]\n rw [e]\n exact Complex.abs_re_le_norm _\n have h3 : dist s ((1 : \u2102) / 2) = \u2016s - (1 : \u2102) / 2\u2016 := dist_eq_norm _ _\n have h4 := hs\n rw [dpsiDomain, Metric.mem_ball, h3] at h4\n exact lt_of_le_of_lt h2 h4\n linarith [abs_lt.mp h1]\n have h5 : \u2016s + \u2191m + 1\u2016 \u2265 s.re + m + 1 := by\n have h6 : (s + \u2191m + 1).re = s.re + m + 1 := by\n simp [Complex.add_re, Complex.one_re, Complex.ofReal_re]\n rw [\u2190 h6]\n exact Complex.re_le_norm _\n have h7 : s.re + m + 1 \u2265 (m : \u211d) + 1 := by linarith\n exact h5.trans h7\n -- \u2016\u2191m + 1\u2016 = m + 1\n have hnorm1 : \u2016((m : \u2102) + 1)\u2016 = (m : \u211d) + 1 := by\n rw [show ((m : \u2102) + 1) = ((m + 1 : \u211d) : \u2102) by push_cast; ring]\n rw [RCLike.norm_ofReal]\n exact abs_of_nonneg (by positivity)\n rw [hnorm1] at hden\n -- \u2016s\u2016/(\u2016m+1\u2016\u00b7\u2016s+m+1\u2016) \u2264 \u2016s\u2016/(m+1)\u00b2\n have hpos : (0 : \u211d) < ((m : \u211d) + 1) * ((m : \u211d) + 1) := by positivity\n calc \u2016s\u2016 / \u2016((m : \u2102) + 1) * (s + \u2191m + 1)\u2016 \u2264 \u2016s\u2016 / (((m : \u211d) + 1) * ((m : \u211d) + 1)) := by\n apply div_le_div_of_nonneg_left (norm_nonneg _) hpos hden\n _ = \u2016s\u2016 / ((m : \u211d) + 1) ^ 2 := by ring\n exact Summable.of_norm_bounded (summable_div_add_one_sq \u2016s\u2016) hnorm\n\nend NguyenRH1"
}
result 2026-08-22 07:31:44Z → 2026-08-23 18:31:06Z
{
"filePath": "D:\\Python\\Quantum\\STATE.md",
"oldString": "**Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8766 jobs);\nLiFEntire.lean root-imported (session 029). sorryAx remains ONLY on:\nR003_exact_factorization (tier iv) + 4 valley statements (tier iii).",
"newString": "**Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8766 jobs);\nLiFEntire.lean root-imported (session 029); LiCircleBound.lean\n(session 030, 5e-v IN PROGRESS \u2014 not yet root-imported). sorryAx\nremains ONLY on: R003_exact_factorization (tier iv) + 4 valley\nstatements (tier iii).",
"originalFile": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-23 | Session 030 COMPLETE \u2014 **ii\u2032-5e-v-a +\n5e-v-b chunk 1 COMPLETE** (LiCircleBound.lean: the count bridges\nA0count/Ncount windows + the Dirichlet bound + the tsum-split\nmachinery + lowZeroConst; clean elaboration; NOT yet root-imported \u2014\nthe file is mid-sub-stage; journal-030 has the full remaining design).\nTIER ii\u2032 in progress (user decision: option (a) \u2014 close SfBoundProp\nin Lean BEFORE submission; Paper A frozen/submittable throughout).\nDONE: ii\u2032-0 (D-064 design + liCoeff defect + crux Sf = Res\u2081 found),\nii\u2032-1a (liCoeff defect REPAIRED), ii\u2032-1b (R1 residue machinery:\nrectInt'_Jlag), ii\u2032-2 (elementary swaps), ii\u2032-3-DESIGN (D-066, \u03b24),\nii\u2032-3a (pieces A+B: LiZetaCoeff, LiArchimedean, LiDigamma), ii\u2032-4\n(LiContour.lean: L3 exists_zero_avoiding_T + L1 kernel bounds +\nzeroMult_neg_two), ii\u2032-5a (D-067 design), ii\u2032-5b (LiRBound.lean:\nlevel-2 \u03b6 representation + norm_riemannZeta_le_disc \u2016\u03b6\u2016 \u2264 (3/4)|t|\u00b2),\nii\u2032-5c (LiDisc.lean: the loose disc R-bound \u2264 100000\u00b7(log|t|)\u00b2 on\n\u03c3 \u2208 [1/2, 7/2] via R-gap + Blaschke + BC, Jensen count, NO perimeter),\n**ii\u2032-5d COMPLETE** (session 025, LiReflect.lean, ~640 lines, 26\ndecls): the FE logDeriv identity `logDeriv_zeta_fe` (logDeriv \u03b6 s =\n\u2212logDeriv \u03b6(1\u2212s) \u2212 [logDeriv \u0393R s + logDeriv \u0393R(1\u2212s)] at good points);\nthe EXACT zero-sum cancellation `sum_nearZeros_neg_reflect`\n(nearZeros(\u2212t) = image under \u03c1 \u21a6 1\u2212\u03c1, zeroMult invariant by\nanalyticOrderAt_zeta_one_sub, 1\u2212s\u2212(1\u2212\u03c1) = \u2212(s\u2212\u03c1)); the \u0393R-bracket\n\u2264 4(log|t|)\u00b2 (the +4 \u0393R shift `logDeriv_Gamma\u211d_shift` putting both\ndigamma arguments in re > 0 + StirlingVert digamma_stirling); capstone\n**logDeriv_riemannZeta_sub_nearZeros_le_left**: the loose R-bound\n\u2264 200000\u00b7(log|t|)\u00b2 on \u03c3 \u2208 [\u22125/2, 1/2], |t| \u2265 10; PLUS the 5e input\n**norm_digamma_sub_log_le_of_two_le_abs_im**: \u2016\u03c8(w) \u2212 log w\u2016 \u2264 3 for\n2 \u2264 |im w| (digamma_add_natCast shift + first-order EM comparison\n+ arctan-FTC integral bound \u2014 UNIFORM in the chain length).\nAll axiom-audited (26 decls, audit-session025-axioms.txt): 3 standard\naxioms only.\n**ii\u2032-5e-0 + DESIGN COMPLETE** (session 026): LiTrivialZeros.lean \u2014\n`gamma_mul_prod` (product-form \u0393 recurrence) + the `HfunT n` cofactor\n(analytic + nonzero at \u22122n) + **zeroMult_neg_two_mul**: zeroMult(\u22122n)\n= 1 for ALL n \u2265 1 (8 decls, audit-session026-axioms.txt clean); build\nGREEN (8762 jobs, root-imported). D-068 (5e design): F entire via\nprincipal-part splits (no removable-singularity theorem, no Hadamard);\nTWO CORRECTIONS to D-067 \u00a76 \u2014 (C1) the circle series bound is\nO((log R)\u00b3) via the RADIAL split (\u03b3-gap only in the critical annulus\n[R\u00b12]; the naive split gives O(R log R) \u2014 fatal), (C2) the near-axis\nleft-plane digamma bound is a SEPARATE build (recurrence + separated\nreciprocal sum \u03a3 1/|w+j| \u2264 C\u00b7log(m+1), dist(w,\u2212\u2115) \u2265 1/4).\n**ii\u2032-5e-i COMPLETE** (session 027, commit e28eff6): LiGapCircles.lean\n\u2014 `exists_gapCircle_radius`: R \u2208 [4k+5/2, 4k+3] with dist(R/2,\u2124) \u2265 1/4\nand every zero ordinate \u2265 1 away or at clearance \u2265 1/(16\u00b7C0hat(4k+9/2))\n(the \u00d72-rescaled midpoint pigeonhole + C0hat_mono; 2 decls clean).\n**ii\u2032-5e-ii COMPLETE** (session 027, commits 0e9336e + ec13029):\nLiDigammaLeft.lean \u2014 `tsum_one_div_sub_telescope` (1/N tail);\n**norm_digamma_le_of_two_le_re** (B): \u2016\u03c8(w)\u2016 \u2264 20\u00b7log(2+\u2016w\u2016) for\nre w \u2265 2, |im w| \u2264 5 (Weierstrass split: harmonic head + telescoping\ntail; integers via digamma_natCast_eq); **digamma_recip_sum_le** (C):\n\u03a3 \u2016(w+j)\u207b\u00b9\u2016 \u2264 2/c + 2 + 2\u00b7log m for dist(w,\u2212\u2115) \u2265 c (V-split);\n**norm_digamma_le_of_dist_nat** (A): \u2016\u03c8(w)\u2016 \u2264 (46 + 2/c) + 23\u00b7log(2+\u2016w\u2016)\nfor re w \u2264 2, dist(w,\u2212\u2115) \u2265 c (recurrence to re \u2208 [3,4) via\ndigamma_add_natCast\u2032 \u2014 pole-avoidance form, covers real points);\n**logDeriv_Gamma\u211d_eq** (G): logDeriv \u0393R s = \u2212(log \u03c0)/2 + \u00bd\u03c8(s/2) for\nim s \u2260 0 (the m-fold shift + 5d's EventuallyEq machinery). Build\nGREEN (8764 jobs); 15 decls audited clean.\n**ii\u2032-5e-iii COMPLETE** (session 028, LiSeries.lean, ~600 lines, 22\ndecls, audit-session028-axioms.txt clean): `seriesTerm s \u03c1 :=\n(zeroMult \u03c1 : \u2102)\u00b7(1/(s\u2212\u03c1) + 1/\u03c1)` over the nontrivial-zero subtype;\n`seriesFun s := \u2211' \u03c1, seriesTerm s \u03c1`. (i) **seriesSummable** at EVERY\ns (unconditional; the ii\u2032-1a D-trick: tail 2\u2016s\u2016/\u2016\u03c1\u2016\u00b2 via\none_div_sub_add_one_div + one_add_normSq_gammaOf_le (1+\u2016\u03b3\u2016\u00b2 \u2264\n(17/12)\u2016\u03c1\u2016\u00b2 for \u2016\u03c1\u2016 \u2265 2), dominator (17/6)(\u2016s\u2016+1)\u00b7mult/(1+\u2016\u03b3\u2016\u00b2) via\nWeilEF.zero_sum_inv_sq zetaSeam, finite head via\nfinite_subtype_norm_lt). (ii) **seriesFun_analyticAt /\nseriesFun_analyticOnNhd** on {\u00acIsNontrivialZero}: avoiding balls by\nthe three-case split (\u03b6\u22600 continuity; \u03b6=0,s\u2080\u22601 order normal form via\nzeta_order_ne_top_of_ne; s\u2080=1 zetaA factorization) + the Weierstrass\nM-test of_norm_le_summable_eventually + the journal-020/021\nTendstoLocallyUniformlyOn\u2192differentiableOn\u2192analyticOnNhd pattern.\n(iii) **nontrivialZero_isolated** (finite unit-ball min-distance) +\n**seriesFunSub_analyticAt** (the \u03c1\u2080-term-zeroed series analytic AT\n\u03c1\u2080) + **seriesFun_sub_term** (seriesFun = seriesFunSub + the \u03c1\u2080-term\neverywhere) + capstones **seriesFun_sub_self_term_analyticAt** and\n**seriesFun_sub_polar_analyticAt** (series \u2212 mult/(s\u2212\u03c1\u2080) analytic at\n\u03c1\u2080 \u2014 the 5e-iv residue-cancellation input). Build GREEN (8765 jobs,\nLiSeries root-imported).\n**ii\u2032-5e-iv COMPLETE** (session 029, commits 58e03e2 + closure;\nLiFEntire.lean, ~1130 lines, 30 decls, audit-session029-axioms.txt\nclean): F ENTIRE. `Fexpr s := logDeriv \u03b6 s \u2212 seriesFun s + 1/s +\n1/(s\u22121) \u2212 (log \u03c0)/2 + \u03c8(s/2)/2`; `badPoint s := nontrivial \u2228 s = 0 \u2228\ns = 1 \u2228 \u2203 n \u2265 1, s = \u22122n`. Since Mathlib lacks a general removable-\nsingularity theorem and Fexpr's values at bad points are junk, the\nextension is `Gentire s := limUnder (\ud835\udcdd[\u2260] s) Fexpr`: at good points\nFexpr analytic (`Fexpr_analyticAt_of_not_bad`, via\n`zeta_zero_classification` \u2014 every zero is nontrivial/0/\u22122n) \u27f9\nGentire = Fexpr (`gentire_eq_Fexpr`, limUnder uniqueness); at bad\npoints explicit analytic witnesses with punctured agreement:\nnontrivial \u03c1\u2080 (`logDeriv_zeta_sub_mult_div_eventually` NF witness +\n5e-iii's polar subtraction), s = 1 (logDeriv zetaA), s = 0 (\u03c8(s/2)/2\n+ 1/s = \u2212\u03b3/2 + \u00bd\u00b7digammaSeriesPart(s/2), M-test on ball(0,1/2)),\ns = \u22122n (NF + `zeroMult_neg_two_mul` via new `riemannZeta_neg_two_mul`\n+ the dropped-term series `digammaSeriesPartSub`/H_n, eventually\nM-test on ball(\u2212n,1/2)). Capstone **gentire_analyticAt_and_eq**:\n(\u2200 s, AnalyticAt \u2102 Gentire s) \u2227 (\u2200 s good, Gentire s = Fexpr s).\nBuild GREEN (8766 jobs, LiFEntire root-imported).\nROUTE (D-067 \u00a76 + D-068): loose disc bound (5c \u2714) + FE-reflection\n(5d \u2714) + the digamma/circle inputs (5e-i/ii \u2714) + the series (5e-iii\n\u2714) + F entire (5e-iv \u2714) feed the partial-fraction identity (5e-v:\ncircle bound + squeeze \u27f9 capstone \u2203 B identity); tight A = 10.5,\nB\u2080 = 48 from D-056's analysis of the identity (5f).\nRemaining map: ii\u2032-5e-v \u2192 ii\u2032-5f \u2192 ii\u2032-3b (moments) \u2192 ii\u2032-3c\n(crux) \u2192 ii\u2032-6 \u2192 ii\u2032-7.\n\n## CURRENT POSITION\n\u2714 PHASE 0, 1, 4 COMPLETE. PHASE 3 (Track C): 3.1\u20133.8 CLOSED (R-004,\nfull tag). PHASE 2 (Track B): mapped to exhaustion at current\ntechnology (2.6\u20132.13). PHASE 5: 5.3 \u2714, 5.4 \u2714, 5.2 \u2714 (live);\n5.1 skeleton \u2714 + tier (i) \u2714 (session 011) + **tier (ii) STEP 1 \u2714\n(session 012)**.\n\n**Theorem status (session 012 Lean upgrade):**\n- T-1 (R-004): [PROVED-CONDITIONAL(computational RH-to-T\u2080;\n computational finite verification)] \u2014 **Lean-verified modulo\n SfBoundProp + the declared computational perimeter only**:\n `lambda_pos_finite_height_verified` (LiBasePoints.lean) PROVED from\n (hRH : RHUpTo 3\u00d710\u00b9\u00b2) (hfinite : LiVerifiedUpTo 5\u00d710\u2075)\n (hSf : SfBoundProp). PrintAxioms = 3 standard axioms, no sorryAx.\n The two margin evaluations are discharged by certified interval\n bounds (margin\u0303(8\u00d710\u2074) \u2265 8001 certified / 15 764 true; margin\u0303(10\u2075)\n \u2265 85 501 certified). LiSkeleton + LiBasePoints both sorry-free.\n- T-2 (R-003 + D-041): factorization + (\u2605) \u27fa (1.12) [PROVED modulo\n Phase-5 formalities]; (1.12) \u27f9 spec(D) \u2282 \u211d [PROVED via Suzuki + D1];\n \u21d0 [SKELETON L3/L4].\n- T-3 (valley, D-049 + D-058): [PROVED-CONDITIONAL(RH)].\n\n**Paper:** research/paper/paperA.tex \u2014 Paper A (finite-height Li +\nmachine-verified assembly), 8 pp, compiles clean, zero undefined refs.\npaperB.tex \u2014 spectral-line research note (skeleton, standing items in\n\u00a70), 6 pp. draft.tex \u2014 FROZEN combined archive copy (12 pp). No\nfigures yet.\n\n**Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8766 jobs);\nLiFEntire.lean root-imported (session 029). sorryAx remains ONLY on:\nR003_exact_factorization (tier iv) + 4 valley statements (tier iii).\n`lambda_pos_finite_height` (tier ii step 1) PROVED with hypotheses:\n(_hRH : RHUpTo 3\u00d710\u00b9\u00b2) (hfinite : LiVerifiedUpTo 5\u00d710\u2075)\n(hbase : 0 < marginTilde FAlt 80000)\n(hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000)\n(hSf : SfBoundProp). Key session-012 constructs: FAlt (\u03c8-clean\nTrudgian-shape majorant \u2014 true F+S_b has \u03c8 > 0 on [5.47,~16], term\ndropped, cost 0.9\u221an), Bn, Sf (= SInfty + 1 \u2212 liCoeff.re, BL Thm 2 by\nconstruction), pos_of_convex_of_two_points (secant; derivative variant\npos_of_convex_of_base also proved), FAlt_psi_neg, contDiffOn_FAlt.\n\n## ACTIVE PLAN (tier ii\u2032, per D-064 \u00a76)\nFreeze protocol in force (user directive 2026-08-21): no edits to\npaperA.tex/paperB.tex/draft.tex/references.bib until ii\u2032-7; no edits\nto existing Lean proofs except the liCoeff correctness fix (ii\u2032-1a);\ncommit at every sub-stage. Fallback integrity: D-064 \u00a78.\nSub-stage map: ii\u2032-1a liCoeff pairing fix + summability (0.5\u20131 sess)\n\u2192 ii\u2032-1b residue machinery R1 (1\u20132) \u2192 ii\u2032-2 elementary swaps R2(i)(ii)\n(1\u20132) \u2192 ii\u2032-3 (4.10) R2(iii) \u2014 EF-reuse first, Hadamard fallback (2\u20134,\nlong pole) \u2192 ii\u2032-4 L3+L1 (1) \u2192 ii\u2032-5 R-bound local route R3 (2\u20133)\n\u2192 ii\u2032-6 L0 assembly (1\u20132) \u2192 ii\u2032-7 close + audit + paper Appendix B (1).\nDeprioritized: a=13+ push; adversary-ceiling LP; T4b; \u03bb-channel\n(G-004); \u03b8-channel (dead, E-024); Paper B Task 1 (R-003 bookkeeping)\nholds as queued after ii\u2032; user read-through of paperA.pdf still open\n(nothing blocks it); repo-publication prep still open.\n\n## NEXT ACTION\nSession 031: **ii\u2032-5e-v chunk 2** \u2014 the tail bound + the main series\ncircle bound (LiCircleBound.lean \u00a74\u2013\u00a75). FULL DESIGN in journal-030\n\u00a7\"Design state\" (all API verified session 030). Summary:\n1. `zero_tail_inv_sq_le` (X \u2265 4\u00b710\u00b3): \u03a3_{|\u03b3|>X} m/(1+\u03b3\u00b2) \u2264\n 16\u00b7A0count\u00b7log X / X \u2014 via ENNReal.tsum_fiberwise (free in \u211d\u22650\u221e)\n with the dyadic key j(\u03c1) := Nat.log 2 \u230a|\u03b3|/X\u230b, the window counts\n (Ncount_le_of_interval_gen), and the dyadic series\n \u03a3 (j+4)/2^j = 10 (tsum_geometric + tsum_coe_mul_geometric \u2014\n check exact names at build time).\n2. The main bound `seriesFun_norm_le_gapCircle` (k \u2265 4000, R the 5e-i\n radius, \u2016s\u2016 = R): ONE tsum_split_finset at F := {\u2016\u03c1\u2016 \u2264 2R}; the\n finite part by Finset.filter into low (\u2264 lowZeroConst), inner\n (dyadic in \u2016\u03c1\u2016 and in R\u2212\u2016\u03c1\u2016), critical (\u03b3-gap 1/(32\u0108\u2080) on strip\n arcs |t| \u2265 10 \u2014 needs 13/R \u2264 1/(32\u0108\u2080(4k+9/2)) i.e. k \u2265 4000 with\n the numerics in journal-030: \u0108\u2080(16006) \u2264 9.36 via log(16008) \u2264 10\n \u27f8 2.718281828^10 \u2265 22026 \u2014 vs near-axis arcs: \u2016s\u2212\u03c1\u2016 \u2265 \u221a(R\u00b2\u2212100)\u22121\n \u2265 R/2, no gap), upper band (dyadic in \u2016\u03c1\u2016\u2212R); the tail via chunk-2's\n zero_tail_inv_sq_le (term \u2264 (17R/6)\u00b7m/(1+\u03b3\u00b2) by 5e-iii's (17/12)\n comparison, \u2016s\u2212\u03c1\u2016 \u2265 \u2016\u03c1\u2016/2).\n3. THEN 5e-v-c: the logDeriv circle assembly (5c/5d near-sum \u2264\n 32\u0108\u2080\u00b72A\u2080\u00b7log(|t|+4); Dirichlet right; FE-reflect + \u0393R brackets\n left) + elems (\u03c8(s/2)/2 per arc via 5e-ii (A)/(B) + 5d's\n norm_digamma_sub_log; dist(s/2,\u2212\u2115) \u2265 1/8 on the left arc for\n R \u2265 208) \u27f9 \u2016Fexpr\u2016 \u2264 C(log R)\u00b3 on the circle (\u2016Gentire\u2016 same:\n circle points are good).\n4. THEN 5e-v-d: the squeeze via Mathlib's Schwarz\n `Complex.dist_le_div_mul_dist_of_mapsTo_ball` on Gentire with\n R\u2082(R_k) = C(log R_k)\u00b3 + \u2016Gentire 0\u2016 \u27f9 Gentire \u2261 Gentire 0 =: B\n (the ratio \u2192 0 via (log R)\u00b3 \u2264 64 R^{3/4} from Real.log_le_rpow-ish)\n \u27f9 capstone `partialFraction_identity (hZC : ZeroCountProp)`.\nTHEN ii\u2032-5f (D-056's tight analysis \u27f9 10.5/48) \u2192 ii\u2032-3b \u2192 ii\u2032-3c \u2192\nii\u2032-6 \u2192 ii\u2032-7.\nRead first: journal-030 gotchas (le_or_lt absent \u2014 use le_or_gt;\nfinsum_mem_union/finsum_mem_empty/tsum_eq_sum forms; bare\nNat.cast_nonneg needs ascription; pin Ncount_add_of_le's endpoints;\nno nested calc-:= by in deep case blocks; union membership rcases\ndirectly; positivity can't see Classical.choose defs; norm_num at\nwith norms can leak metavars; statement-level if needs [DecidableEq \u03b9];\n_root_.riemannZeta_conj for the unconditional conj) + journal-029\ngotchas.\n\n## COMPLETED (Sessions 001\u2013010)\n- [x] Phase 0, Phase 1 (Track A \u2192 monitoring mode, D-013).\n- [x] 2.6 V3 root-cause + repair (E-016b/c, D-025).\n- [x] 2.7 R-003 exact factorization (D-026, E-017/D-027, ledger #5).\n- [x] 2.8 a=12 no transition (E-018/D-028, backend v2, E-019/D-029).\n- [x] 1.6 \u03be\u2032-world saturated (E-020b/D-030); 1.7 T4b closed (D-031).\n- [x] 3.3 \u2192 G-003; 3.4 (Suzuki line spawned); 3.5 design (D-032/D-033).\n- [x] (\u2605) design (D-034/D-035); new tasks 2.9/2.10/2.11.\n- [x] 3.6 D-036 explicit contour constants (session 006 cont.9).\n- [x] 3.7 E-021 (session 007): S_\u221e exact + c\u2080, |S_f| curve, A/B\u2080\n measured; 6-bug saga documented.\n- [x] Session 008: regroup; R7 resources atlas registered; 3.8\n COMPLETE (D-037, E-023, R-004 ledger #6); 2.10 COMPLETE\n (E-022/E-022b + D-040, valley observable); 2.9-D1 COMPLETE\n (D-041); 2.11 COMPLETE (D-038); 2.12 COMPLETE (E-024 + D-042,\n \u03b8-independence); 2.13 COMPLETE (E-025 + D-043, discretization\n floor; quadratic locking correction).\n- [x] Session 009: PHASE 4 COMPLETE (D-052/D-053/D-054, E-027 + D-055,\n repairs 4.5a\u2013d: D-056\u2013D-059; R-004 tag restored).\n- [x] Session 010: 5.3 paper draft complete; 5.4 honesty audit (D-060);\n 5.1/5.2 skeleton stage (D-061).\n- [x] Session 011: Lean proof tier (i) COMPLETE \u2014 sInfty_lower_bound,\n marginTilde_convex, chain_rule_sqrt_shift PROVED (journal-011;\n 10 commits; D-061 \u00a75 updated).\n\n## OPEN CONJECTURES / THREADS\n- (\u2605) (R-003): central conjectural target (task 2.9).\n- Q-S1 (D-019 \u00a73): L\u00b2\u2192uniform lifting. Q-S2: \u210b(T_a) de Branges (2.4).\n \u03b8(a) theory: must explain both metrics (D-028 F3) + z\u2081\u00b7a\u22484.5 law.\n- Q6 (D-001); Q14 Gutzwiller (Phase 2); T2 Christoffel/CMS (D-006).\nCLOSED: T1, T3, T4, T4b (D-031), T5 (\u2192G-001), 3.4a/b/c, 3.3 (\u2192G-003),\n2.8 (D-029), 1.6 (D-030), 1.7 (D-031), 3.5-design (D-033), (\u2605)-design\n(D-035), 3.6 (D-036), 3.7 (E-021), 3.8 (D-037/R-004), 5.3, 5.4,\n5.1-tier-(i).\n\n## BLOCKERS\n(none)\n\n## HANDOFF NOTES\n- db.py add-derivation/log-experiment use INSERT OR REPLACE keyed by\n id \u2014 a mistyped re-register OVERWRITES the row.\n- db.py: init, log-experiment, add-result, add-derivation, add-graveyard,\n list. add-derivation signature: positional id, --title --task\n --status --file (NO --date flag). Session registration via direct\n sqlite3 insert (journal_file column).\n- venv: ./.venv/Scripts/python.exe. git: git -c user.name=\"NGUYEN-RH-1\"\n -c user.email=\"research@local\" commit (config NOT modified).\n- LONG RUNS: DETACHED + sandbox DISABLED + log file; poll. For lake:\n SINGLE command per detached spawn; short PrintAxioms in foreground.\n- LEAN: elan 4.2.3 at ~/.elan/bin (export PATH per shell); toolchain\n v4.33.0-rc2; zeta-23-lean fully built (9010 jobs) + cache ~7 GB;\n NguyenRH1 at research/lean/NguyenRH1 with path requires. Iterate\n single-file with `lake env lean NguyenRH1/LiSkeleton.lean` from the\n package dir (elan errors \"no default toolchain\" outside it).\n- LEAN 4 gotchas (session 011, hard-won \u2014 full list in journal-011):\n HasDerivAt.add_const adds to VALUE (use .comp for precomposition);\n Pi.mul_apply/Pi.add_apply/Pi.sub_apply simp after .mul/.add/.sub;\n convert leaves instance side-goals \u2192 `first | rfl | ring`;\n field_simp often closes goals (trailing ring errors);\n Finset.sum_image takes Set.InjOn, map = g, summand = f;\n deriv^[2] \u2260 deriv (deriv \u00b7) syntactically (show bridges);\n subtype coercions (m : \u211d) vs (m.1 : \u211d) can explode isDefEq \u2014 pin\n families explicitly; -a*b vs -(a*b) breaks Real.exp_neg rewrites;\n check norm_num digit-bounds by hand (two tight ones failed);\n set_option maxHeartbeats goes BEFORE the doc comment;\n iimaj_bracket_bound needs maxHeartbeats 800000.\n- flint for ALL \u03b6/Stieltjes >16 digits; mp.zetazero safe; mpmath\n complex-\u03b6 OK to ~1e-10; mpmath zeta (integer+Hurwitz)\n UNTRUSTWORTHY beyond ~57 digits at any dps.\n- PRECISION RULES (session 007): (1) mp.mp.dps = X BEFORE every\n mp.mpf(string) parse; (2) long decimal constants as STRINGS;\n (3) float64 zero ordinates insufficient for \u03c3_m; (4) Li binomial\n truncation boundary error ~C(n,M)\u00b714^{\u2212M} peaks at M = n/15.\n- prime_backend_v2: blockwise \u039b to e\u00b2\u2074, cache E-019-backend-cache.npz;\n monkeypatch E16.prime_sum_vec + E16._BUILD.clear().\n- Winding diagnostic: \u22654000 pts/edge near real zeros.\n- E-016/E-016b FROZEN; correct machinery: E-016c, E-017/E-018.\n- \u03b3-locking claim protocol: D-029 \u00a73.\n- Lagarias paper math/0404394 (research/paper/): \u00a75\u20136 read in full.\n- research/resources/: 43-note RH-equivalence atlas = R7.\n- E-021 caches: E-021-zeta-cache.json, E-021-zeros100-hi-cache.json,\n E-021-zeros-cache.npy (4624 zeros float64 \u2014 P1 use ONLY).\n- E-023: E-023-assembly.csv + .json (M\u2080, N\u2080, N\u2081, margins).\n- E-027: detector stress test; zeros cache E-027-zeros-cache.npy;\n rerun 16 s with cache (--force).\n- PAPER: build with pdflatex+bibtex in research/paper/ (MiKTeX);\n draft.pdf is gitignored. Audit rule (D-060 \u00a75): any edit to\n draft.tex re-opens the audit for the edited lines.\n",
"structuredPatch": [
{
"oldStart": 135,
"oldLines": 8,
"newStart": 135,
"newLines": 10,
"lines": [
" figures yet.",
" ",
" **Lean:** research/lean/NguyenRH1/ \u2014 full build GREEN (8766 jobs);",
"-LiFEntire.lean root-imported (session 029). sorryAx remains ONLY on:",
"-R003_exact_factorization (tier iv) + 4 valley statements (tier iii).",
"+LiFEntire.lean root-imported (session 029); LiCircleBound.lean",
"+(session 030, 5e-v IN PROGRESS \u2014 not yet root-imported). sorryAx",
"+remains ONLY on: R003_exact_factorization (tier iv) + 4 valley",
"+statements (tier iii).",
" `lambda_pos_finite_height` (tier ii step 1) PROVED with hypotheses:",
" (_hRH : RHUpTo 3\u00d710\u00b9\u00b2) (hfinite : LiVerifiedUpTo 5\u00d710\u2075)",
" (hbase : 0 < marginTilde FAlt 80000)"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Committed. Now Section 3: the complex series + the identity principle. Let me write it:\n\n```lean\n/-! ## 3. The complex series and the identity with Complex.digamma -/\n\n/-- The complex digamma series summand. -/\ndef dpsiTermC (s : ℂ) (m : ℕ) : ℂ := 1 / ((m : ℂ) + 1) - 1 / (s + m + 1)\n\n/-- The complex digamma series. -/\ndef DinfC (s : ℂ) : ℂ :=\n -(Real.eulerMascheroniConstant : ℂ) - 1 / s + ∑' m : ℕ, dpsiTermC s m\n```\n\nThe domain: U := Metric.ball (1/2 : ℂ) (1/2). \n\nLemmas:\n(a) Summable (dpsiTermC s) for s ∈ U: ‖dpsiTermC s m‖ = ‖s‖/(‖↑m+1‖·‖s+↑m+1‖) — bounds: for s ∈ U: ‖s‖ < 1 (‖s‖ ≤ ‖s − 1/2‖ + ‖1/2‖ < 1 ✓); ‖s + ↑m + 1‖ ≥ |re(s + m + 1)| = re s + m + 1 > m (re s > 0 for s ∈ U: |re s − 1/2| ≤ |s − 1/2| < 1/2 ⟹ re s > 0 ✓) — hmm ‖s+m+1‖ ≥ re(s+m+1) = re s + m + 1 ≥ m + 1·(re s)... — use ‖z‖ ≥ |re z| (`Complex.abs_re_le_norm`? — `Complex.abs_re_le_norm z : |z.re| ≤ ‖z‖` ✓ used in LiSkeleton line 204). So ‖s+m+1‖ ≥ re s + m + 1 ≥ ... m + 1 (re s > 0)... ≥ (m+1)·(re s)?? no — ≥ m + re s·... let me just: ‖s+m+1‖ ≥ re s + m + 1. For the summability bound: ‖term‖ ≤ ‖s‖/((m+1)·(re s + m + 1)) ≤ ‖s‖/((m+1)·(m+1))·(1/re s)? — hmm: 1/(re s + m + 1) ≤ 1/(m+1) (re s > 0) — so ‖term‖ ≤ ‖s‖/(m+1)² ≤ 1/(m+1)²·(‖s‖) — with ‖s‖ < 1: ≤ 1/(m+1)² — but for the SUMMABILITY at a FIXED s, the bound u m := ‖s‖/(m+1)²·(1/...)... — let me use: ‖dpsiTermC s m‖ ≤ (‖s‖/re s)·(1/(m+1)²)·... hmm: ‖term‖ = ‖s‖/((m+1)‖s+m+1‖) ≤ ‖s‖/((m+1)(re s + m + 1)) — and (re s + m + 1) ≥ m + 1 gives ≤ ‖s‖/(m+1)² ✓ (no re s needed!) — wait: 1/(re s + m + 1) ≤ 1/(m+1) since re s ≥ 0 ✓ — so ‖term‖ ≤ ‖s‖/(m+1)² — and for s ∈ U, ‖s‖ < 1: ≤ 1/(m+1)². So summable via comparison with (‖s‖/(m+1)²) — the complex comparison: `Summable.of_norm_bounded (summable_div_add_one_sq ‖s‖)` — wait the dominator family fun m => ‖s‖/(m+1)² ✓ summable ✓ — and ‖dpsiTermC s m‖ ≤ ‖s‖/(m+1)² ✓ — via Summable.of_norm_bounded (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) — that worked in liSummable ✓.\n The norm computation: ‖dpsiTermC s m‖ = ‖s / ((m+1)(s+m+1))‖: dpsiTermC s m = 1/(m+1) − 1/(s+m+1) = s/((m+1)(s+m+1)) — via field_simp + ring (need (m+1:ℂ) ≠ 0 ✓ and s+m+1 ≠ 0 — for s ∈ U: re(s+m+1) > 0 ⟹ ≠ 0 ✓).\n So lemma dpsiTermC_eq : dpsiTermC s m = s / ((↑m + 1) * (s + ↑m + 1)) for s ∈ U (or for s+m+1 ≠ 0 — state with (hs : s + m + 1 ≠ 0)).\n Then ‖dpsiTermC s m‖ = ‖s‖/(‖↑m+1‖·‖s+m+1‖) ≤ ‖s‖/((m+1)·(re s + m + 1)) ≤ ‖s‖/(m+1)² — for s ∈ U. Fine.\n\n(b) HasSumUniformlyOn of dpsiTermC on U (the M-test with u m := 1/(m+1)² — wait the bound needs ‖s‖ ≤ 1: ‖term‖ ≤ ‖s‖/(m+1)² ≤ 1/(m+1)² for s ∈ U ✓): so HasSumUniformlyOn dpsiTermC (fun s => ∑' m, dpsiTermC s m) U via of_norm_le_summable (summable_div_add_one_sq 1) (bound) ✓. Then TendstoLocallyUniformlyOn of the partial sums (hasSumUniformlyOn... — HasSumUniformlyOn ⟹ TendstoLocallyUniformlyOn — via hasSumUniformlyOn_iff_tendstoUniformlyOn + locally — hmm — HasSumUniformlyOn on U (open) ⟹ TendstoUniformlyOn partial sums on U ⟹ TendstoLocallyUniformlyOn ✓ (TendstoUniformlyOn.tendstoLocallyUniformlyOn? — `TendstoUniformlyOn.tendstoLocallyUniformlyOn (hs : IsOpen s)`? — there's a lemma — or via the iff). Then TendstoLocallyUniformlyOn.differentiableOn (LocallyUniformLimit.lean:136) gives DifferentiableOn ℂ (fun s => ∑' m, dpsiTermC s m) U — then DinfC differentiableOn U (the −γ − 1/s pieces differentiable on U — 0 ∉ U ✓) — then AnalyticOnNhd via DifferentiableOn.analyticOnNhd isOpen_ball.\n Wait — TendstoLocallyUniformlyOn.differentiableOn's exact signature (line 136): `_root_.TendstoLocallyUniformlyOn.differentiableOn [φ.NeBot] (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U)?` — let me check — from line 136-137: `theorem _root_.TendstoLocallyUniformlyOn.differentiableOn [φ.NeBot] (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) : DifferentiableOn ℂ f U`? — roughly. The F := partial sums (differentiable on U: finite sums of the terms ✓) — f := the tsum function ✓.\n\n(c) The cast bridge: DinfC ↑x = ↑(DinfR x) for x ∈ (0,1): \n DinfC ↑x = −γ − 1/↑x + ∑' m, dpsiTermC ↑x m; ↑(DinfR x) = ↑(−γ − 1/x + ∑' m, dpsiTermR x m) — push_cast (distributes ↑ over +, −, /, the constants: ↑(−γ) = −↑γ ✓ — and the tsum: ↑(∑' m, dpsiTermR x m) = ∑' m, ↑(dpsiTermR x m) via Complex.ofRealCLM.map_tsum (dpsiTermR_summable hx) — and ↑(dpsiTermR x m) = dpsiTermC ↑x m (push_cast per-term ✓). So:\n```lean\nlemma DinfC_ofReal {x : ℝ} (hx : 0 < x) : DinfC (↑x) = ↑(DinfR x) := by\n rw [DinfC, DinfR]\n push_cast\n rw [show ((↑(∑' m : ℕ, dpsiTermR x m)) : ℂ) = ∑' m : ℕ, dpsiTermC (↑x) m from ?_] -- hmm\n ...\n```\nLet me structure:\n```lean\nlemma DinfC_ofReal {x : ℝ} (hx : 0 < x) : DinfC (↑x) = ↑(DinfR x) := by\n have h1 : (↑(∑' m : ℕ, dpsiTermR x m) : ℂ) = ∑' m : ℕ, dpsiTermC (↑x) m := by\n rw [Complex.ofRealCLM_apply ▸ ...] -- use map_tsum\n have := Complex.ofRealCLM.map_tsum (dpsiTermR_summable hx)\n -- this : ofRealCLM (∑' m, dpsiTermR x m) = ∑' m, ofRealCLM (dpsiTermR x m)\n rw [Complex.ofRealCLM_apply] at this -- turns ofRealCLM into ↑\n rw [this]\n apply tsum_congr\n intro m\n rw [dpsiTermR, dpsiTermC]\n push_cast\n ring\n rw [DinfC, DinfR]\n push_cast\n rw [h1]?? hmm — after push_cast the ↑(∑' ...) becomes ... push_cast might rewrite the cast-of-tsum via map_tsum itself? push_cast has `Complex.ofReal_tsum`? no. Let me do it stepwise:\n rw [DinfC, DinfR]\n push_cast\n -- goal: −↑γ − 1/↑x + ↑(∑' m, dpsiTermR x m) = ... hmm the DinfC LHS: −↑γ − 1/↑x + ∑' m, dpsiTermC ↑x m — and RHS ↑(−γ − 1/x + ∑' ...) → push_cast → −↑γ − 1/↑x + ↑(∑' ...) — then rw [h1] and congr\n```\nOrder: rw [DinfC, DinfR] unfolds both; push_cast normalizes the RHS's outer casts (keeping ↑(∑'...) as an atom hopefully — push_cast distributes over +/−/// but not over tsum ✓); then rw [h1] : ↑(∑' m, dpsiTermR x m) → ∑' m, dpsiTermC ↑x m ✓ then both sides −↑γ − 1/↑x + ∑' ... — wait the LHS (DinfC ↑x) has −(↑γ) − 1/↑x + ∑' dpsiTermC — hmm push_cast also normalizes the LHS's −(Real.eulerMascheroniConstant : ℂ) — it's already a cast — fine. Then ring/rfl. Manageable.\n\nHmm — `Complex.ofRealCLM.map_tsum` — the signature from Module.lean:134: `protected theorem ContinuousLinearMap.map_tsum [T2Space M₂] [L.NeBot] {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f L) : φ (∑'[L] z, f z) = ∑'[L] z, φ (f z)` — the ∑'[L] — the summation filter L — with `[L.NeBot]` — the plain ∑' uses the default filter — is the default `L` the universal filter ⊤? In current Mathlib, `∑' z, f z` = `∑'[⊤] z, f z`? or the default SummationFilter... There was a refactor (SummationFilter.lean exists) — plain ∑' is notation for ∑'[⊤] (the \"universal\" filter) I believe. So map_tsum with L := ⊤ — `[L.NeBot]` — ⊤ is NeBot ✓ instance. So Complex.ofRealCLM.map_tsum (hf : Summable f) : ofRealCLM (∑' z, f z) = ∑' z, ofRealCLM (f z) ✓ — with the plain ∑' ✓.\n\n(d) digamma = DinfC on U via the identity principle:\n - digamma AnalyticOnNhd U: digamma = logDeriv Complex.Gamma = fun s => deriv Complex.Gamma s / Complex.Gamma s — analytic on U since Gamma analytic & nonvanishing on U: for s ∈ U (ball (1/2)(1/2)): re s > 0 — Gamma differentiable at s (differentiableAt_Gamma — needs s ≠ −m: re s > 0 ⟹ s ≠ −(m:ℂ) since re(−m) = −m ≤ 0 < re s ✓) and Gamma s ≠ 0 (`Complex.Gamma_ne_zero (hs : ∀ m, s ≠ -↑m)`? — name: from digamma_apply_add_one's proof: `Gamma_ne_zero hs` with hs : ∀ m : ℕ, s ≠ -m ✓ exists as Complex.Gamma_ne_zero presumably).\n AnalyticOnNhd ℂ digamma U: for s ∈ U: AnalyticAt ℂ digamma s: digamma = deriv Gamma / Gamma — deriv Gamma analytic at s: Gamma analytic at s (DifferentiableAt → AnalyticAt? — for ℂ: differentiable at a POINT doesn't imply analytic at the point — need differentiability on a nhd — `DifferentiableAt.analyticAt`? no. The right route: Gamma is analytic on ℂ minus poles — is there `Complex.analyticAt_Gamma`? hmm — differentiableAt_Gamma gives pointwise; for analyticity use: DifferentiableOn on an open nhd ⟹ analytic — the set ℂ ∖ {0, −1, ...} — or just on U directly: DifferentiableOn ℂ Gamma U (each point differentiable ✓) — U open ⟹ AnalyticOnNhd ℂ Gamma U (`DifferentiableOn.analyticOnNhd`? — hmm — the right name: `DifferentiableOn.analyticOnNhd (h : DifferentiableOn ℂ f s) (hs : IsOpen s) : AnalyticOnNhd ℂ f s` — I believe it exists — it was used in... zetaA's proof used `.analyticOnNhd Metric.isOpen_ball` on a DifferentiableOn — from LiResidue line 77: `h.analyticOnNhd Metric.isOpen_ball` — so DifferentiableOn.analyticOnNhd ✓ EXISTS).\n Then AnalyticOnNhd ℂ (deriv Gamma) U := (AnalyticOnNhd Gamma U).deriv — `AnalyticOnNhd.deriv` ✓ (exists — used implicitly? AnalyticOnNhd.deriv : AnalyticOnNhd f s → AnalyticOnNhd (deriv f) s ✓ I believe).\n Then the quotient: AnalyticOnNhd (deriv Gamma / Gamma) U: AnalyticOnNhd.div with Gamma ≠ 0 on U ✓ — `AnalyticOnNhd.div (hf : AnalyticOnNhd f s) (hg : AnalyticOnNhd g s) (hg0 : ∀ x ∈ s, g x ≠ 0)`? — hmm — AnalyticOnNhd.div might not exist with that exact form — there's `AnalyticAt.div` (used in LiResidue: hda.div ha hne ✓ pointwise) — so build pointwise: AnalyticOnNhd f U means ∀ x ∈ U, AnalyticAt f x — pointwise AnalyticAt.div ✓.\n - DinfC AnalyticOnNhd U ✓ from (b).\n - The frequently-eq at z₀ := ↑(1/2): ∃ᶠ z in 𝓝[≠] ↑(1/2), digamma z = DinfC z: from the real-segment agreement: for real x ∈ (0,1), x ≠ 1/2: digamma ↑x = ↑(DinfR x) [psiReal bridge + cast] = DinfC ↑x [cast bridge]. The frequently: the set S := {↑x : x ∈ (0,1)} ∋ points arbitrarily close to ↑(1/2) with x ≠ 1/2: formalize via a sequence: z_n := ↑(1/2 + 1/(n+2)) — z_n → ↑(1/2), z_n ≠ ↑(1/2), and digamma z_n = DinfC z_n (1/(n+2) ∈ (0,1) for n ≥ 1... 1/2 + 1/(n+2) ∈ (0,1) ⟺ 1/(n+2) < 1/2 ⟺ n ≥ 1 — take n ≥ 1 or use 1/(n+3)). Then `frequently` from the sequence: `Filter.frequently_atTop`... — the bridge: Tendsto z_n (𝓝 ↑(1/2)) with z_n ≠ point + P z_n ∀ n ⟹ ∃ᶠ z in 𝓝[≠] z₀, P z — there's `Filter.Tendsto.frequently_...`? — `Frequently` from a sequence: I recall `frequently_of_...`? — maybe easiest: ∃ᶠ z in 𝓝[≠] z₀, P z ⟺ ∀ U ∈ 𝓝[≠] z₀, ∃ z ∈ U, P z — `Filter.frequently_iff`? — `frequently_iff : (∃ᶠ x in l, P x) ↔ ∀ U ∈ l, ∃ x ∈ U, P x`? hmm — `Filter.frequently_iff` might be about ≤... Let me use: `Filter.Frequently` unfolds — `frequently_iff_exists_...`? Alternatively: the AccPt formulation: ∃ᶠ z in 𝓝[≠] z₀, P z ⟺ AccPt z₀ (𝓟 {z | P z})? no wait — there's `accPt_iff_frequently : AccPt x s ↔ ∃ᶠ y in 𝓝[≠] x, y ∈ s`? — hmm — actually simplest robust: prove ∃ᶠ via the sequence using `Filter.frequently_of_seq`?... Let me search for the right frequently-from-sequence lemma at build. Alternatively use a DIFFERENT identity principle form: `eqOn_of_preconnected_of_eventuallyEq` needs agreement on a whole nhd — I only have the segment. Hmm — there's also the zero-set-codiscrete route... Let me just do the frequently via: 𝓝[≠] z₀'s membership: every punctured-nhd set contains a point of the segment: \n ```lean\n have hfreq : ∃ᶠ z in 𝓝[≠] (↑(1/2 : ℝ)), Complex.digamma z = DinfC z := by\n rw [frequently_iff] -- hmm\n ...\n ```\n Let me look up: `Filter.frequently_iff : (∃ᶠ x in l, P x) ↔ ∀ {U}, U ∈ l → ∃ x ∈ U, P x`? — there IS `frequently_iff : ...` in Mathlib/Order/Filter/Basic — `theorem Filter.frequently_iff {l : Filter α} {P : α → Prop} : (∃ᶠ x in l, P x) ↔ ∀ U ∈ l, ∃ x ∈ U, P x`? I believe so (frequently = the complement-free form). Then for U ∈ 𝓝[≠] ↑(1/2): U ⊇ (punctured ball) — pick a real point: U ∈ 𝓝[≠] z₀ means U ⊇ ball(z₀, δ) ∖ {z₀} for some δ > 0 (𝓝[≠] has such sets — `nhdsWithin` membership: U ∈ 𝓝[≠] z₀ ⟺ ∃ V ∈ 𝓝 z₀, V ∖ {z₀} ⊆ U — take V = ball — then ↑x with x real, 0 < |x − 1/2| < min(δ, 1/2) — e.g. x := 1/2 + (min δ (1/2))/2 — then ↑x ∈ U, x ∈ (0,1) ✓ and x ≠ 1/2 ✓ — the agreement holds there ✓.\n This is doable but fiddly. Let me write it with frequently_iff and the ball membership extraction (`Metric.mem_nhdsWithin_iff`? — U ∈ 𝓝[≠] z₀: nhdsWithin — `Metric.nhdsWithin...`: there's `Metric.eventually_nhdsWithin...`? — use `mem_nhdsWithin_iff_exists...`? — I'll extract via: 𝓝[≠] z₀ = 𝓝[{z₀}ᶜ] z₀ — U ∈ it ⟺ ∃ V ∈ 𝓝 z₀, V ∩ {z₀}ᶜ ⊆ U (mem_nhdsWithin_iff... `mem_nhdsWithin_iff_exists_mem_nhds_inter`? hmm — `mem_nhdsWithin_iff : s ∈ 𝓝[t] a ↔ ∃ U ∈ 𝓝 a, U ∩ t ⊆ s`? — `mem_nhdsWithin_iff_exists...`? there's `mem_nhdsWithin_iff`? not sure — `Filter.mem_nhdsWithin_iff...` — I'll find it).\n\nHmm — this frequently argument is ~30 lines of filter fiddliness. Let me simplify by choosing a SMARTER identity-principle application: apply eqOn_of_preconnected_of_frequently_eq at a point where agreement is EASIER: is there a point where I get a full neighborhood of agreement? NO — the agreement is only on the real line. So the frequently route it is.\n\nActually — alternative: use the frequently via the IMAGE of the real interval under ofReal: the set S := Complex.ofReal '' Set.Ioo 0 1 — and 1/2 is an accumulation point of S: `AccPt (↑(1/2)) (𝓟 S)`? — there's `AccPt` API: `accPt_principal_iff_nhds`? — hmm. You know — let me just try frequently_iff + mem_nhdsWithin. Let me check the exact names:\n- `Filter.frequently_iff`? \n- `Set.mem_nhdsWithin_iff`? — there's `mem_nhdsWithin_iff_exists_mem_nhds_inter : s ∈ 𝓝[t] a ↔ ∃ U ∈ 𝓝 a, U ∩ t ⊆ s`? — I recall `mem_nhdsWithin_iff_exists_mem_nhds_inter` ✓ exists.\n\nOK let me write Section 3 now (the complex series + analyticity + cast bridge), and leave the identity-principle for after a compile check of the base pieces. Given the hour, let me get as far as compiles cleanly tonight and commit.","signature":""},{"type":"text","text":"Now Section 3 — the complex series, analyticity, and the cast bridge."},{"type":"tool_use","id":"Edit_342","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDigamma.lean","old_string":"end NguyenRH1","new_string":"/-! ## 3. The complex series: summability, analyticity, cast bridge -/\n\n/-- The complex digamma series summand. -/\ndef dpsiTermC (s : ℂ) (m : ℕ) : ℂ := 1 / ((m : ℂ) + 1) - 1 / (s + m + 1)\n\n/-- The complex digamma series: −γ − 1/s + Σ_{m≥0} dpsiTermC s m. -/\ndef DinfC (s : ℂ) : ℂ :=\n -(Real.eulerMascheroniConstant : ℂ) - 1 / s + ∑' m : ℕ, dpsiTermC s m\n\n/-- The domain: the ball of radius 1/2 around 1/2 (avoids 0, −1, −2, …;\nconvex, contains the real segment (0,1)). -/\ndef dpsiDomain : Set ℂ := Metric.ball ((1 : ℂ) / 2) (1 / 2)\n\nlemma dpsiDomain_convex : Convex ℝ dpsiDomain := convex_ball _ _\nlemma dpsiDomain_isOpen : IsOpen dpsiDomain := Metric.isOpen_ball\nlemma dpsiDomain_half : (1 : ℂ) / 2 ∈ dpsiDomain :=\n Metric.mem_ball_self (by norm_num : (0 : ℝ) < 1 / 2)\n\nlemma dpsiTermC_pole_free {s : ℂ} (hs : s ∈ dpsiDomain) (m : ℕ) : s + m + 1 ≠ 0 := by\n intro h\n have hre : 0 < s.re := by\n have h1 : |s.re - 1 / 2| < 1 / 2 := by\n have := hs\n rw [dpsiDomain, Metric.mem_ball] at this\n have h2 : |s.re - (1 / 2 : ℝ)| ≤ ‖s - (1 : ℂ) / 2‖ := by\n have e : s.re - 1 / 2 = (s - (1 : ℂ) / 2).re := by\n simp [Complex.sub_re, Complex.ofReal_re]\n rw [e]\n exact Complex.abs_re_le_norm _\n have h3 : dist s ((1 : ℂ) / 2) = ‖s - (1 : ℂ) / 2‖ := dist_eq_norm _ _\n rw [h3] at this\n have h4 : (((1 : ℂ) / 2).re) = 1 / 2 := by simp\n linarith [this, h2]\n linarith [abs_lt.mp h1]\n have : s.re + m + 1 = 0 := by\n have h2 : (s + m + 1).re = 0 := by rw [h]; simp\n simp [Complex.add_re, Complex.ofReal_re, Complex.one_re] at this\n linarith\n linarith [Nat.cast_nonneg (α := ℝ) m]\n\n/-- The summand in factored form: dpsiTermC s m = s/((m+1)(s+m+1)). -/\nlemma dpsiTermC_eq {s : ℂ} (hs : s + 1 ≠ 0) (m : ℕ) (hsm : s + m + 1 ≠ 0) :\n dpsiTermC s m = s / ((↑m + 1) * (s + ↑m + 1)) := by\n have hm0 : ((m : ℂ) + 1) ≠ 0 := by\n intro h\n have hre : ((m : ℂ) + 1).re = 0 := by rw [h]; simp\n simp [Complex.add_re, Complex.ofReal_re, Complex.one_re] at hre\n have : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n linarith\n rw [dpsiTermC]\n field_simp [hm0, hs, hsm]\n ring\n\n/-- The complex series is summable on dpsiDomain. -/\nlemma dpsiTermC_summable {s : ℂ} (hs : s ∈ dpsiDomain) : Summable (dpsiTermC s) := by\n have hs1 : s + 1 ≠ 0 := by\n have h := dpsiTermC_pole_free hs 0\n simpa using h\n have hnorm : ∀ m : ℕ, ‖dpsiTermC s m‖ ≤ ‖s‖ / ((m : ℝ) + 1) ^ 2 := by\n intro m\n have hsm : s + m + 1 ≠ 0 := dpsiTermC_pole_free hs m\n rw [dpsiTermC_eq hs1 m hsm]\n rw [norm_div]\n have hden : ‖((m : ℂ) + 1) * (s + ↑m + 1)‖ ≥ ((m : ℝ) + 1) * ((m : ℝ) + 1) := by\n rw [norm_mul]\n apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ ‖(m : ℂ) + 1‖)\n · -- ‖s + m + 1‖ ≥ m + 1 via the real part\n have hre : 0 < s.re := by\n have h1 : |s.re - 1 / 2| < 1 / 2 := by\n have h2 : |s.re - (1 / 2 : ℝ)| ≤ ‖s - (1 : ℂ) / 2‖ := by\n have e : s.re - 1 / 2 = (s - (1 : ℂ) / 2).re := by\n simp [Complex.sub_re]\n rw [e]\n exact Complex.abs_re_le_norm _\n have h3 : dist s ((1 : ℂ) / 2) = ‖s - (1 : ℂ) / 2‖ := dist_eq_norm _ _\n have h4 := hs\n rw [dpsiDomain, Metric.mem_ball, h3] at h4\n exact lt_of_le_of_lt h2 h4\n linarith [abs_lt.mp h1]\n have h5 : ‖s + ↑m + 1‖ ≥ s.re + m + 1 := by\n have h6 : (s + ↑m + 1).re = s.re + m + 1 := by\n simp [Complex.add_re, Complex.one_re, Complex.ofReal_re]\n rw [← h6]\n exact Complex.re_le_norm _\n have h7 : s.re + m + 1 ≥ (m : ℝ) + 1 := by linarith\n exact h5.trans h7\n -- ‖↑m + 1‖ = m + 1\n have hnorm1 : ‖((m : ℂ) + 1)‖ = (m : ℝ) + 1 := by\n rw [show ((m : ℂ) + 1) = ((m + 1 : ℝ) : ℂ) by push_cast; ring]\n rw [RCLike.norm_ofReal]\n exact abs_of_nonneg (by positivity)\n rw [hnorm1] at hden\n -- ‖s‖/(‖m+1‖·‖s+m+1‖) ≤ ‖s‖/(m+1)²\n have hpos : (0 : ℝ) < ((m : ℝ) + 1) * ((m : ℝ) + 1) := by positivity\n calc ‖s‖ / ‖((m : ℂ) + 1) * (s + ↑m + 1)‖ ≤ ‖s‖ / (((m : ℝ) + 1) * ((m : ℝ) + 1)) := by\n apply div_le_div_of_nonneg_left (norm_nonneg _) hpos hden\n _ = ‖s‖ / ((m : ℝ) + 1) ^ 2 := by ring\n exact Summable.of_norm_bounded (summable_div_add_one_sq ‖s‖) hnorm\n\nend NguyenRH1"},"extra_content":null}]