[{"type":"thinking","thinking":"The definitions are plain interval integrals. The FTC approach: for a function G : ℂ → ℂ differentiable on a neighborhood of the border, with G' = deriv G:\n\nRectangleIntegral (deriv G) z w = \n  HIntegral G' z.re w.re z.im − HIntegral G' z.re w.re w.im + VIntegral G' w.re z.im w.im − VIntegral G' z.re z.im w.im\n\nHIntegral G' x₁ x₂ y = ∫_{x₁}^{x₂} G'(x + yI) dx = G(x₂ + yI) − G(x₁ + yI) via `intervalIntegral.integral_deriv_eq_sub`.\n\nThe relevant Mathlib lemma: `intervalIntegral.integral_deriv_eq_sub (h : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (h' : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b - f a` — need f' = deriv (fun x => G (x + y*I)). The chain rule: HasDerivAt (fun x => G (x + y*I)) (deriv G (x+y*I)) x? deriv (fun x => G (x + y*I)) x = deriv G (x+y*I) · 1 (the inner function x ↦ x + yI has derivative 1). So:\n```\nhave hside : ∫ x in x₁..x₂, deriv G (x + y*I) = G (x₂ + y*I) - G (x₁ + y*I) := by\n  have hd : ∀ x ∈ Set.uIcc x₁ x₂, HasDerivAt (fun x => G (x + y*I)) (deriv G (x + y*I)) x := by\n    intro x hx\n    have hG : HasDerivAt G (deriv G (x + y*I)) (x + y*I) := (hGd (x + y*I)).hasDerivAt  -- G differentiable at border points\n    have hc : HasDerivAt (fun x => x + y*I) 1 x := by\n      have := hasDerivAt_id x\n      -- x ↦ x + y*I has derivative 1\n      ...\n    convert hG.comp x hc using 1\n    simp\n  have hint : IntervalIntegrable (fun x => deriv G (x + y*I)) volume x₁ x₂ := by\n    apply ContinuousOn.intervalIntegrable ... -- deriv G continuous on border nhd (G analytic there ⟹ deriv continuous? G holomorphic ⟹ deriv G holomorphic? If G is differentiable on an OPEN set containing the border, deriv G is continuous? For complex functions, differentiability on open sets ⟹ analytic ⟹ deriv analytic/continuous ✓.)\n  have := intervalIntegral.integral_deriv_eq_sub hd hint\n  rw [this]\n```\nHmm wait — the FTC lemma's f is the parametrized function: integral_deriv_eq_sub (h : ∀ x ∈ uIcc, HasDerivAt f (f' x) x) : ∫ f' = f b − f a — with f := fun x => G (x + y*I), f' := fun x => deriv G (x + y*I)·1 = deriv G (x+y*I). ✓.\n\nThe differentiability of G at border points: G is meromorphic with pole only at 1; border avoids 1 ⟹ G differentiable at each border point ✓.\n\nThe integrability: deriv G continuous on the segment: G differentiable on an open nhd of the border ⟹ G analytic there ⟹ deriv G analytic ⟹ continuous ✓ (AnalyticOnNhd.continuousOn.deriv? or DifferentiableOn.continuousOn for deriv — deriv of a holomorphic function is holomorphic: `DifferentiableOn.deriv`? there's `DifferentiableOn.deriv (hd : DifferentiableOn ℂ f s) (ho : IsOpen s) : DifferentiableOn ℂ (deriv f) s`? I believe `DifferentiableOn.deriv` exists ✓ — and continuousOn from differentiableOn).\n\nFor G := our specific primitive (finite sum of (w−1)^{-k} terms) — differentiability at border points: each term (w−1)^{-k} differentiable off {1}; finite sum ✓. Even simpler than the abstract argument: G is a rational function with pole only at 1 — differentiable wherever w ≠ 1 ✓ directly (no analyticity machinery needed — `DifferentiableAt.div` etc.).\n\nAlso `deriv G = the i≥2 sum`: G(w) = −Σ_{i=2}^{n+1} A_i/((i−1)(w−1)^{i−1}): deriv G (w) = Σ_{i=2}^{n+1} A_i/(w−1)^i =: Ptail(w) — compute via deriv_sum + deriv of (w−1)^{-(i−1)}: d/dw [(w−1)^{-(i−1)}] = −(i−1)(w−1)^{-i} ✓ (deriv_zpow or deriv of (w−1)^(−(i−1) : ℤ)) — the terms: A_i/((i−1))·(w−1)^{-(i−1)} with negation: G = Σ_{i=2}^{n+1} −(A_i/((i−1):ℂ))·(w−1)^{-((i−1):ℤ)}: deriv = Σ −(A_i/(i−1))·(−(i−1))(w−1)^{-(i−1)−1} = Σ A_i (w−1)^{-i} ✓. With zpow: deriv_zpow (m : ℤ) — `deriv_zpow (m : ℤ) (x) : deriv (· ^ m) x = m * x ^ (m - 1)`? there's `deriv_zpow` ✓ I believe.\n\nOK — this is all standard. Estimate ~200 lines for part (ii). Let me write it as Part 2 of LiResidue.lean (appended, or a new file LiPrincipal.lean — separate file keeps compile times modular: new file `LiPrincipal.lean` importing LiResidue).\n\nStructure of LiPrincipal.lean:\n1. `Acoeff (n i : ℕ) : ℂ := iteratedDeriv (n + 1 - i) (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) 1 / (n + 1 - i)!`\n2. `ppart (n : ℕ) (w : ℂ) : ℂ := ∑ i ∈ Finset.Icc 1 (n+1), Acoeff n i / (w - 1)^i`\n3. `Gpart (n : ℕ) (w : ℂ) : ℂ := ∑ i ∈ Finset.Icc 2 (n+1), -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))`\n4. `deriv_Gpart : ∀ w ≠ 1, deriv (Gpart n) w = ∑ i ∈ Finset.Icc 2 (n+1), Acoeff n i / (w - 1)^i`\n5. `rectInt_deriv_eq_zero`: the generic FTC lemma — RectangleIntegral (fun s => deriv G s) z w = 0 for G differentiable at all border points (with G deriv continuous on the border).\n6. `RectangleIntegral'_add` / linearity (check if vendored: `RectangleBorderIntegrable.add` exists — but I need the integral-level additivity: RectangleIntegral (f+g) = RectangleIntegral f + RectangleIntegral g — from the HIntegral/VIntegral defs + intervalIntegral additivity: should be a short proof by unfolding + integral_add).\n7. `rectInt'_ppart`: 1 interior ⟹ RectangleIntegral' (ppart n) z w = ResW1 n.\n\nWait — one important detail: Acoeff n 1 = ResW1 n: Acoeff n 1 = iteratedDeriv (n+1−1) F 1/(n+1−1)! = iteratedDeriv n F 1/n! = ResW1 n ✓ (n+1−1 = n).\n\nLet me also double-check the decomposition: ppart n w = A_1/(w−1) + Σ_{i≥2} A_i/(w−1)^i = A_1/(w−1) + deriv Gpart n w ✓ (off {1}).\n\nFor the integral additivity: RectangleIntegral (f + g) = RectangleIntegral f + RectangleIntegral g — via HIntegral_add/VIntegral_add: each is intervalIntegral of (f+g) = integral f + integral g (IntervalIntegrable needed). Let me write HIntegral.add/VIntegral.add helpers.\n\nAlright — writing LiPrincipal.lean now. Given the length of this session already, I'll write the whole file then compile-iterate.","signature":""},{"type":"text","text":"Definitions confirmed. Writing `LiPrincipal.lean` (part ii: the principal-part integral via per-side FTC)."},{"type":"tool_use","id":"Write_220","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiPrincipal.lean","content":"/-\nNguyenRH1/LiPrincipal.lean — tier ii′ sub-stage ii′-1b(ii) (D-064 §4 R1):\nthe principal-part integral. For the explicit principal part\n  P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i,   A_i = F^{(n+1−i)}(1)/(n+1−i)!,\nwith F(w) = (wⁿ−(w−1)ⁿ)·hLi(w), on any rectangle with 1 in its interior:\n  RectangleIntegral' P z w = A_1 = ResW1 n.\n\nMethod: P = A_1/(w−1) + (Σ_{i≥2} A_i/(w−1)^i). The first term is handled\nby the vendored `ResidueTheoremInRectangle`; the tail has the explicit\nglobal primitive G(w) = −Σ_{i≥2} A_i/((i−1)(w−1)^{i−1}), differentiable\non the border (1 is interior, hence off the border), so its rectangle\nintegral vanishes by per-side FTC (`rectInt_deriv_eq_zero`).\n\nArchive references: D-036, D-064 (R1), journal-016.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ResidueCalcOnRectangles\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Linearity of rectangle integrals -/\n\nlemma HIntegral_add (f g : ℂ → ℂ) (x₁ x₂ y : ℝ)\n    (hf : IntervalIntegrable (fun x => f (x + y * I)) volume x₁ x₂)\n    (hg : IntervalIntegrable (fun x => g (x + y * I)) volume x₁ x₂) :\n    HIntegral (f + g) x₁ x₂ y = HIntegral f x₁ x₂ y + HIntegral g x₁ x₂ y := by\n  rw [HIntegral, HIntegral, HIntegral]\n  have e : (fun x => (f + g) (x + y * I)) = (fun x => f (x + y * I) + g (x + y * I)) := by\n    funext x\n    simp [Pi.add_apply]\n  rw [e, intervalIntegral.integral_add hf hg]\n\nlemma VIntegral_add (f g : ℂ → ℂ) (x y₁ y₂ : ℝ)\n    (hf : IntervalIntegrable (fun y => f (x + y * I)) volume y₁ y₂)\n    (hg : IntervalIntegrable (fun y => g (x + y * I)) volume y₁ y₂) :\n    VIntegral (f + g) x y₁ y₂ = VIntegral f x y₁ y₂ + VIntegral g x y₁ y₂ := by\n  rw [VIntegral, VIntegral, VIntegral]\n  have e : (fun y => (f + g) (x + y * I)) = (fun y => f (x + y * I) + g (x + y * I)) := by\n    funext y\n    simp [Pi.add_apply]\n  rw [e, intervalIntegral.integral_add hf hg, smul_add]\n\nlemma RectangleIntegral_add (f g : ℂ → ℂ) (z w : ℂ)\n    (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n    RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w := by\n  rw [RectangleIntegral, RectangleIntegral, RectangleIntegral]\n  obtain ⟨⟨hf1, hf2⟩, hf3, hf4⟩ := hf\n  obtain ⟨⟨hg1, hg2⟩, hg3, hg4⟩ := hg\n  rw [HIntegral_add f g _ _ _ hf1 hg1, HIntegral_add f g _ _ _ hf2 hg2,\n    VIntegral_add f g _ _ _ hf3 hg3, VIntegral_add f g _ _ _ hf4 hg4]\n  ring\n\nlemma RectangleIntegral'_add (f g : ℂ → ℂ) (z w : ℂ)\n    (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n    RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by\n  rw [RectangleIntegral', RectangleIntegral_add f g z w hf hg, RectangleIntegral', RectangleIntegral',\n    smul_add]\n\n/-! ## 2. The per-side FTC vanishing lemma -/\n\n/-- If `G : ℂ → ℂ` is differentiable at every point of the rectangle\nborder, then the rectangle integral of `deriv G` vanishes (each side\ntelescopes by FTC). -/\nlemma rectInt_deriv_eq_zero {G : ℂ → ℂ} {z w : ℂ}\n    (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)\n    (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s) :\n    RectangleIntegral (fun s => deriv G s) z w = 0 := by\n  rw [RectangleIntegral]\n  have hsideH : ∀ y : ℝ, (∀ x : ℝ, x ∈ Set.uIcc z.re w.re → (x + y * I) ∈ RectangleBorder z w) →\n      ∫ x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by\n    intro y hy\n    have hd : ∀ x ∈ Set.uIcc z.re w.re,\n        HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by\n      intro x hx\n      have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n        (hG _ (hy x hx)).hasDerivAt\n      have h2 : HasDerivAt (fun x => x + y * I) 1 x := by\n        have hid := hasDerivAt_id x\n        have hconst : HasDerivAt (fun x => y * I) 0 x := hasDerivAt_const x _\n        convert hid.add hconst using 1\n        simp\n      have := h1.comp x h2\n      convert this using 1\n      simp\n    have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by\n      apply ContinuousOn.intervalIntegrable_of_Icc (a := z.re) (b := w.re)\n      intro x hx\n      have hmem : (x + y * I) ∈ RectangleBorder z w := hy x (Set.uIcc_of_le ?_ hx |>.elim (fun h => h.1) )\n      · exact (hGc _ hmem).continuousWithinAt\n      · sorry\n    have := intervalIntegral.integral_deriv_eq_sub hd hint\n    convert this using 1\n  sorry\n\nend NguyenRH1\n"},"extra_content":null}]