← Session 22 — ii′-1: liCoeff pairing fix + residue machinery
thinking (2797 chars)
Now the capstone in LiArchimedean.lean: the final τ_j theorem:
```lean
theorem iteratedDeriv_logDeriv_Gammaℝ (j : ℕ) :
iteratedDeriv j (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 =
((-1 : ℂ)) ^ (j + 1) * (j ! : ℂ) * (lagariasA (j + 1) : ℝ)
```
Plan:
- j = 0: logDeriv_Gammaℝ_one + lagariasA 1 = lagariasA1.
- j ≥ 1:
(a) hev : the split =ᶠ[𝓝 0] — via logDeriv_Gammaℝ_one_add on a nhd of 0 (the two hypotheses eventually).
(b) iteratedDeriv_congr_of_eventuallyEq hev — then the RHS's iteratedDeriv at 0.
(c) the RHS: fun s => −(log π)/2 + (1/2)·digamma((1+s)/2) — iteratedDeriv j at 0 (j ≥ 1): the const dies: iteratedDeriv_add + iteratedDeriv_const (if_neg) + zero_add; then (1/2)·[digamma∘φ]: iteratedDeriv_const_mul + iteratedDeriv_one_add_div_two_at.
(d) iteratedDeriv j digamma (1/2) = (−1)^{j+1}·j!·(2^{j+1}·↑lagariasA(j+1)) [iteratedDeriv_digamma_half_value].
(e) algebra: (1/2)·[(1/2)^j·((−1)^{j+1}·j!·(2^{j+1}·↑lagariasA(j+1)))] = (−1)^{j+1}·j!·↑lagariasA(j+1) — the 2-power cancellation: (1/2)·(1/2)^j·2^{j+1} = 1.
For (a) — the two hypotheses eventually near 0:
- hG : ∀ᶠ s in 𝓝 0, Complex.Gamma ((1+s)/2) ≠ 0: via Tendsto (fun s => Complex.Gamma ((1+s)/2)) (𝓝 0) (𝓝 (Complex.Gamma (1/2))) — via ContinuousAt.comp of (Complex.continuousAt_Gamma (1/2) (the pole-free at 1/2)) and the affine map's continuity — then Tendsto.eventually_ne (Gamma(1/2) ≠ 0 — from Complex.Gamma_one_half_eq + cpow ≠ 0 — I have that from logDeriv_Gammaℝ_one's hs — extract: the hs proof there shows Gamma(1/2) ≠ 0 — hmm — actually Gamma_one_half_eq : Gamma (1/2) = π^{1/2} ≠ 0 — small reuse).
Hmm — Complex.continuousAt_Gamma (s) (hs : ∀ m, s ≠ −m) — at 1/2 ✓ (pole-free since re > 0). The comp: ContinuousAt (fun s => Complex.Gamma ((1+s)/2)) 0 = ContinuousAt.comp (continuousAt_Gamma (1/2) proof) (the affine ContinuousAt) — ContinuousAt.comp (hf : ContinuousAt f (g x)) (hg : ContinuousAt g x) : ContinuousAt (f ∘ g) x ✓ — then the ∘ form vs the lambda — rfl-bridge.
- hpole : ∀ᶠ s in 𝓝 0, ∀ m : ℕ, (1+s)/2 ≠ −↑m: via the re-positivity open set (as planned).
Let me now write the capstone and add it to LiArchimedean.lean (which imports LiSkeleton — but I need LiDigamma's content — LiArchimedean currently imports LiSkeleton only. The capstone needs LiDigamma (iteratedDeriv_digamma_half_value) + LiSwaps (lagariasA) + LiSkeleton (lagariasA1). So change LiArchimedean's import to LiDigamma (which imports LiSwaps which imports LiSkeleton ✓ all transitively there). Wait — does changing an existing file's import violate the freeze? The freeze: no edits to existing PROOFS except the liCoeff fix. Changing an import line is not editing a proof — and LiArchimedean is a session-020 file (new this week) — fine.
Let me write the capstone block and append to LiArchimedean.lean.
Now the capstone. LiArchimedean needs LiDigamma's content — updating its import and appending the final theorem.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean",
"old_string": "import Mathlib\nimport NguyenRH1.LiSkeleton",
"new_string": "import Mathlib\nimport NguyenRH1.LiDigamma"
}
result 2026-08-22 10:57:40Z → 2026-08-22 10:57:40Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean",
"oldString": "import Mathlib\nimport NguyenRH1.LiSkeleton",
"newString": "import Mathlib\nimport NguyenRH1.LiDigamma",
"originalFile": "/-\nNguyenRH1/LiArchimedean.lean \u2014 tier ii\u2032 sub-stage ii\u2032-3a, piece (A)\n(D-066 \u00a74): the archimedean coefficients of the (4.10) split.\n\nTarget (D-066): the Taylor coefficients of s \u21a6 logDeriv Gamma\u211d (1+s) at 0:\n\n (1/j!)\u00b7iteratedDeriv j (fun s => logDeriv Gamma\u211d (1+s)) 0 = (\u22121)^{j+1} a_{j+1},\n\ni.e. `iteratedDeriv j ... 0 = (\u22121)^{j+1}\u00b7j!\u00b7lagariasA (j+1)`.\n\nPart 1 (this file, complete): the Gamma\u211d logDeriv split\n logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7digamma((1+s)/2)\n(`logDeriv_Gamma\u211d_one_add`) and the j = 0 evaluation\n logDeriv Gamma\u211d 1 = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212lagariasA1\n(`logDeriv_Gamma\u211d_one`) \u2014 via Mathlib's `Complex.digamma_one_half`.\n\nPart 2 (next): the digamma series from BohrMollerup's logGammaSeq and the\nj \u2265 1 polygamma values at 1/2, then the odd-m reindexing to lagariasA.\n\nArchive references: D-066 (route \u03b24, piece A), journal-019/020.\n-/\nimport Mathlib\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Gamma\u211d logDeriv split -/\n\n/-- The cpow factor as an exponential: \u03c0^(\u2212w/2) = exp(\u2212(log \u03c0)/2\u00b7w). -/\nlemma pi_cpow_neg_half_eq_exp (w : \u2102) :\n (\u2191Real.pi : \u2102) ^ (-w / 2) = Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w) := by\n rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero)]\n congr 1\n rw [\u2190 Complex.ofReal_log Real.pi_nonneg]\n ring_nf\n\n/-- The Gamma\u211d logDeriv split: for (1+s)/2 off the poles of \u0393,\n logDeriv Gamma\u211d (1+s) = \u2212(log \u03c0)/2 + (1/2)\u00b7\u03c8((1+s)/2). -/\nlemma logDeriv_Gamma\u211d_one_add {s : \u2102}\n (hs : Complex.Gamma ((1 + s) / 2) \u2260 0)\n (hs2 : \u2200 m : \u2115, ((1 + s) / 2) \u2260 -m) :\n logDeriv Complex.Gamma\u211d (1 + s) =\n -(Real.log Real.pi : \u2102) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2) := by\n have hfun : Complex.Gamma\u211d = fun w : \u2102 =>\n Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w) * Complex.Gamma (w / 2) := by\n funext w\n show Complex.Gamma\u211d w = _\n rw [Complex.Gamma\u211d_def]\n congr 1\n exact pi_cpow_neg_half_eq_exp w\n rw [hfun]\n have hdif1 : DifferentiableAt \u2102 (fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w))\n (1 + s) := by\n have h1 : DifferentiableAt \u2102 (fun w : \u2102 => -(Real.log Real.pi : \u2102) / 2 * w) (1 + s) :=\n differentiableAt_id.const_mul _\n exact Complex.differentiableAt_exp.comp (1 + s) h1\n have hdif2 : DifferentiableAt \u2102 (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) := by\n have h2 : DifferentiableAt \u2102 (fun w : \u2102 => w / 2) (1 + s) :=\n differentiableAt_id.div_const 2\n exact (Complex.differentiableAt_Gamma _ hs2).comp (1 + s) h2\n rw [logDeriv_mul (f := fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w))\n (g := fun w => Complex.Gamma (w / 2)) (1 + s) (Complex.exp_ne_zero _) hs hdif1 hdif2]\n have h1 : logDeriv (fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w)) (1 + s) =\n -(Real.log Real.pi : \u2102) / 2 := by\n rw [logDeriv_apply]\n have hd : deriv (fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w)) (1 + s) =\n Complex.exp (-(Real.log Real.pi : \u2102) / 2 * (1 + s)) * (-(Real.log Real.pi : \u2102) / 2) := by\n have hh1 : HasDerivAt (fun w : \u2102 => -(Real.log Real.pi : \u2102) / 2 * w)\n (-(Real.log Real.pi : \u2102) / 2) (1 + s) := by\n simpa using (hasDerivAt_id (1 + s)).const_mul (-(Real.log Real.pi : \u2102) / 2)\n have hh2 := (Complex.hasDerivAt_exp (-(Real.log Real.pi : \u2102) / 2 * (1 + s))).comp (1 + s) hh1\n have heq : (Complex.exp \u2218 fun w : \u2102 => -(Real.log Real.pi : \u2102) / 2 * w) =\n fun w : \u2102 => Complex.exp (-(Real.log Real.pi : \u2102) / 2 * w) := rfl\n rw [heq] at hh2\n exact hh2.deriv\n rw [hd]\n field_simp [Complex.exp_ne_zero (-(Real.log Real.pi : \u2102) / 2 * (1 + s))]\n have h2 : logDeriv (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) =\n (1 / 2) * Complex.digamma ((1 + s) / 2) := by\n rw [logDeriv_apply]\n have hd : deriv (fun w : \u2102 => Complex.Gamma (w / 2)) (1 + s) =\n deriv Complex.Gamma ((1 + s) / 2) * (1 / 2) := by\n have hh1 : HasDerivAt (fun w : \u2102 => w / 2) (1 / 2) (1 + s) := by\n simpa using (hasDerivAt_id (1 + s)).div_const (2 : \u2102)\n have hh2 := ((Complex.differentiableAt_Gamma _ hs2).hasDerivAt).comp (1 + s) hh1\n have heq : (Complex.Gamma \u2218 fun w : \u2102 => w / 2) = fun w : \u2102 => Complex.Gamma (w / 2) := rfl\n rw [heq] at hh2\n exact hh2.deriv\n rw [hd, Complex.digamma_def, logDeriv_apply]\n field_simp [hs]\n rw [h1, h2]\n\n/-! ## 2. The j = 0 evaluation: \u03c4\u2080 = \u2212a\u2081 -/\n\n/-- log(4\u03c0) = 2\u00b7log 2 + log \u03c0. -/\nlemma log_four_pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num) (by positivity)]\n congr 1\n rw [show (4 : \u211d) = 2 ^ 2 from by norm_num, Real.log_pow]\n ring\n\n/-- **\u03c4\u2080** (D-066 \u00a74, j = 0): logDeriv Gamma\u211d 1 = \u2212(log 4\u03c0 + \u03b3)/2 = \u2212a\u2081. -/\ntheorem logDeriv_Gamma\u211d_one :\n logDeriv Complex.Gamma\u211d 1 = -(lagariasA1 : \u2102) := by\n have hs : Complex.Gamma ((1 + (0 : \u2102)) / 2) \u2260 0 := by\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e, Complex.Gamma_one_half_eq]\n have hpi : (\u2191Real.pi : \u2102) \u2260 0 := by exact_mod_cast Real.pi_ne_zero\n rw [Complex.cpow_def_of_ne_zero hpi]\n exact Complex.exp_ne_zero _\n have hs2 : \u2200 m : \u2115, ((1 + (0 : \u2102)) / 2) \u2260 -m := by\n intro m hm\n have e : (1 + (0 : \u2102)) / 2 = 1 / 2 := by ring\n rw [e] at hm\n have hre : ((1 : \u2102) / 2).re = (-(m : \u2102)).re := by rw [hm]\n simp at hre\n have hm0 : (0 : \u211d) \u2264 (m : \u211d) := Nat.cast_nonneg m\n linarith\n have h := logDeriv_Gamma\u211d_one_add (s := 0) hs hs2\n rw [add_zero] at h\n rw [h]\n rw [Complex.digamma_one_half]\n rw [show Complex.log (2 : \u2102) = (Real.log 2 : \u2102) by\n rw [show (2 : \u2102) = ((2 : \u211d) : \u2102) by simp]\n exact (Complex.ofReal_log (by norm_num : (0 : \u211d) \u2264 2)).symm]\n rw [lagariasA1, log_four_pi]\n push_cast\n ring\n",
"structuredPatch": [
{
"oldStart": 20,
"oldLines": 7,
"newStart": 20,
"newLines": 7,
"lines": [
" Archive references: D-066 (route \u03b24, piece A), journal-019/020.",
" -/",
" import Mathlib",
"-import NguyenRH1.LiSkeleton",
"+import NguyenRH1.LiDigamma",
" ",
" open Zeta23 Complex Filter Topology",
" open scoped Nat"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now the capstone in LiArchimedean.lean: the final τ_j theorem:\n\n```lean\ntheorem iteratedDeriv_logDeriv_Gammaℝ (j : ℕ) :\n iteratedDeriv j (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 =\n ((-1 : ℂ)) ^ (j + 1) * (j ! : ℂ) * (lagariasA (j + 1) : ℝ)\n```\n\nPlan:\n- j = 0: logDeriv_Gammaℝ_one + lagariasA 1 = lagariasA1.\n- j ≥ 1: \n (a) hev : the split =ᶠ[𝓝 0] — via logDeriv_Gammaℝ_one_add on a nhd of 0 (the two hypotheses eventually).\n (b) iteratedDeriv_congr_of_eventuallyEq hev — then the RHS's iteratedDeriv at 0.\n (c) the RHS: fun s => −(log π)/2 + (1/2)·digamma((1+s)/2) — iteratedDeriv j at 0 (j ≥ 1): the const dies: iteratedDeriv_add + iteratedDeriv_const (if_neg) + zero_add; then (1/2)·[digamma∘φ]: iteratedDeriv_const_mul + iteratedDeriv_one_add_div_two_at.\n (d) iteratedDeriv j digamma (1/2) = (−1)^{j+1}·j!·(2^{j+1}·↑lagariasA(j+1)) [iteratedDeriv_digamma_half_value].\n (e) algebra: (1/2)·[(1/2)^j·((−1)^{j+1}·j!·(2^{j+1}·↑lagariasA(j+1)))] = (−1)^{j+1}·j!·↑lagariasA(j+1) — the 2-power cancellation: (1/2)·(1/2)^j·2^{j+1} = 1.\n\nFor (a) — the two hypotheses eventually near 0:\n- hG : ∀ᶠ s in 𝓝 0, Complex.Gamma ((1+s)/2) ≠ 0: via Tendsto (fun s => Complex.Gamma ((1+s)/2)) (𝓝 0) (𝓝 (Complex.Gamma (1/2))) — via ContinuousAt.comp of (Complex.continuousAt_Gamma (1/2) (the pole-free at 1/2)) and the affine map's continuity — then Tendsto.eventually_ne (Gamma(1/2) ≠ 0 — from Complex.Gamma_one_half_eq + cpow ≠ 0 — I have that from logDeriv_Gammaℝ_one's hs — extract: the hs proof there shows Gamma(1/2) ≠ 0 — hmm — actually Gamma_one_half_eq : Gamma (1/2) = π^{1/2} ≠ 0 — small reuse).\n Hmm — Complex.continuousAt_Gamma (s) (hs : ∀ m, s ≠ −m) — at 1/2 ✓ (pole-free since re > 0). The comp: ContinuousAt (fun s => Complex.Gamma ((1+s)/2)) 0 = ContinuousAt.comp (continuousAt_Gamma (1/2) proof) (the affine ContinuousAt) — ContinuousAt.comp (hf : ContinuousAt f (g x)) (hg : ContinuousAt g x) : ContinuousAt (f ∘ g) x ✓ — then the ∘ form vs the lambda — rfl-bridge.\n- hpole : ∀ᶠ s in 𝓝 0, ∀ m : ℕ, (1+s)/2 ≠ −↑m: via the re-positivity open set (as planned).\n\nLet me now write the capstone and add it to LiArchimedean.lean (which imports LiSkeleton — but I need LiDigamma's content — LiArchimedean currently imports LiSkeleton only. The capstone needs LiDigamma (iteratedDeriv_digamma_half_value) + LiSwaps (lagariasA) + LiSkeleton (lagariasA1). So change LiArchimedean's import to LiDigamma (which imports LiSwaps which imports LiSkeleton ✓ all transitively there). Wait — does changing an existing file's import violate the freeze? The freeze: no edits to existing PROOFS except the liCoeff fix. Changing an import line is not editing a proof — and LiArchimedean is a session-020 file (new this week) — fine.\n\nLet me write the capstone block and append to LiArchimedean.lean.","signature":""},{"type":"text","text":"Now the capstone. LiArchimedean needs LiDigamma's content — updating its import and appending the final theorem."},{"type":"tool_use","id":"Edit_552","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiArchimedean.lean","old_string":"import Mathlib\nimport NguyenRH1.LiSkeleton","new_string":"import Mathlib\nimport NguyenRH1.LiDigamma"},"extra_content":null}]