← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (2011 chars)
RectangleBorderIntegrable's components ARE IntervalIntegrable — hf1 : IntervalIntegrable (fun x => f (x + z.im * I)) volume z.re w.re ✓. So my RectangleIntegral_add just needs the right destructuring: hf is a 4-tuple (and structure): `obtain ⟨hf1, hf2, hf3, hf4⟩ := hf` (it's a 4-way ∧, not nested pairs — ∧ ∧ ∧: obtain ⟨hf1, hf2, hf3, hf4⟩ works for right-nested ∧? The def: A ∧ B ∧ C ∧ D = A ∧ (B ∧ (C ∧ D)) — obtain ⟨a, b, c, d⟩ handles nested ✓).
But wait — there's ALREADY `RectangleBorderIntegrable.add` (line 157) in the vendored file! It proves exactly RectangleIntegral (f+g) = RectangleIntegral f + RectangleIntegral g. So I don't need my own HIntegral_add/VIntegral_add/RectangleIntegral_add — use the vendored one. And for RectangleIntegral' additivity: derive from it. Let me check if there's a primed version... and just use it:
```
lemma RectangleIntegral'_add (f g : ℂ → ℂ) (z w : ℂ)
(hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :
RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by
rw [RectangleIntegral', RectangleBorderIntegrable.add hf hg, RectangleIntegral', RectangleIntegral', smul_add]
```
Delete my HIntegral_add/VIntegral_add/RectangleIntegral_add entirely. Also fix the hmap/uIcc mess in HIntegral_deriv/VIntegral_deriv — the `Set.uIcc_of_le (by simp [Set.uIcc]) hx |>.elim ...` hack — let me think: hx : x ∈ Set.uIcc z.re w.re — need z.re ≤ w.re? uIcc a b = Icc (min) (max) — membership gives min ≤ x ≤ max. The MapsTo needs x ∈ [[z.re, w.re]] = uIcc — same set ✓ so `hmap hx` works directly if [[z.re, w.re]] unfolds to uIcc — `[[a,b]]` notation IS uIcc ✓ so `hmap hx` directly! Let me simplify:
```
have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=
(hG _ (hmap hx)).hasDerivAt
```
Wait — MapsTo f s t x hx : f x ∈ t for x ∈ s ✓ so `hmap hx : (x + y * I) ∈ RectangleBorder z w` ✓ directly (since [[z.re, w.re]] = uIcc z.re w.re defeq ✓).
Let me rewrite the whole file cleanly.
The vendored `RectangleBorderIntegrable.add` already exists — simplifying. Also fixing the MapsTo application (uIcc is definitionally `[[·,·]]`).
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiPrincipal.lean",
"content": "/-\nNguyenRH1/LiPrincipal.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b(ii) (D-064 \u00a74 R1):\nthe principal-part integral. For the explicit principal part\n P(w) = \u03a3_{i=1}^{n+1} A_i/(w\u22121)^i, A_i = F^{(n+1\u2212i)}(1)/(n+1\u2212i)!,\nwith F(w) = (w\u207f\u2212(w\u22121)\u207f)\u00b7hLi(w), on any rectangle with 1 in its interior:\n RectangleIntegral' P z w = A_1 = ResW1 n.\n\nMethod: P = A_1/(w\u22121) + (\u03a3_{i\u22652} A_i/(w\u22121)^i). The first term is handled\nby the vendored `ResidueTheoremInRectangle`; the tail has the explicit\nglobal primitive G(w) = \u2212\u03a3_{i\u22652} A_i/((i\u22121)(w\u22121)^{i\u22121}), 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. Additivity of the primed rectangle integral -/\n\nlemma RectangleIntegral'_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\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', RectangleBorderIntegrable.add hf hg, RectangleIntegral', RectangleIntegral',\n smul_add]\n\n/-! ## 2. Parametrized side derivatives and integrability -/\n\nlemma hasDerivAt_add_const_I (y : \u211d) (x : \u211d) :\n HasDerivAt (fun t => t + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun _ => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n\nlemma hasDerivAt_const_add_I (x y : \u211d) :\n HasDerivAt (fun t => x + t * I) I y := by\n have h1 : HasDerivAt (fun t => t * I) I y := by\n have := (hasDerivAt_id y).mul_const I\n simpa using this\n have hconst : HasDerivAt (fun _ => x) 0 y := hasDerivAt_const y x\n convert hconst.add h1 using 1\n simp\n\n/-- FTC on a horizontal side: \u222b_{x\u2081}^{x\u2082} (deriv G)(x + yI) dx\n= G(x\u2082 + yI) \u2212 G(x\u2081 + yI). -/\nlemma HIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (y : \u211d)\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun x : \u211d => \u2191x + y * I) [[z.re, w.re]] (RectangleBorder z w)) :\n \u222b x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by\n have hd : \u2200 x \u2208 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 _ (hmap hx)).hasDerivAt\n have h2 : HasDerivAt (fun x => x + y * I) 1 x := hasDerivAt_add_const_I y x\n have hcomp := h1.comp x h2\n convert hcomp 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\n intro x hx\n exact (hGc _ (hmap hx)).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n convert hftc using 1\n \u00b7 simp\n \u00b7 simp\n\n/-- FTC on a vertical side: \u222b_{y\u2081}^{y\u2082} (deriv G)(x + yI) dy\n= \u2212I\u00b7(G(x + y\u2082I) \u2212 G(x + y\u2081I)). -/\nlemma VIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (x : \u211d)\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun y : \u211d => \u2191x + \u2191y * I) [[z.im, w.im]] (RectangleBorder z w)) :\n \u222b y in z.im..w.im, deriv G (x + y * I) =\n -I * (G (x + w.im * I) - G (x + z.im * I)) := by\n have hd : \u2200 y \u2208 Set.uIcc z.im w.im,\n HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by\n intro y hy\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap hy)).hasDerivAt\n have h2 : HasDerivAt (fun y => x + y * I) I y := hasDerivAt_const_add_I x y\n have hcomp := h1.comp y h2\n convert hcomp using 1\n ring\n have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume z.im w.im := by\n apply ContinuousOn.intervalIntegrable\n intro y hy\n exact ContinuousWithinAt.mul continuousWithinAt_const\n ((hGc _ (hmap hy)).continuousWithinAt)\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n rw [\u2190 hftc, integral_smul]\n field_simp [Complex.I_ne_zero]\n\n/-- If `G : \u2102 \u2192 \u2102` 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 : \u2102 \u2192 \u2102} {z w : \u2102}\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s) :\n RectangleIntegral (fun s => deriv G s) z w = 0 := by\n rw [RectangleIntegral]\n rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),\n HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]\n have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)\n have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)\n rw [VIntegral, VIntegral, hVr, hVl]\n simp [Complex.I_mul_I]\n ring\n\nend NguyenRH1\n"
}
result 2026-08-21 21:31:49Z → 2026-08-29 00:21:55Z
{
"type": "update",
"filePath": "D:\\Python\\quantum-deploy\\docroot\\app.cgi",
"content": "#!/opt/alt/python311/bin/python3.11\n\"\"\"WSGI->CGI adapter \u2014 runs the RH-WEBSITE Django app on Apache shared hosting.\n\nApache rewrites every non-file request to /app.cgi/<path> (see .htaccess).\nwsgiref's CGIHandler bridges the CGI environment onto Django's WSGI app.\n\"\"\"\nimport os\nimport sys\n\nDOCROOT = os.path.dirname(os.path.abspath(__file__))\nAPP = os.path.join(DOCROOT, \"app\")\n\n# Vendored pure-Python deps (Django 5.2, markdown) + the project package.\nsys.path.insert(0, os.path.join(APP, \"vendor\"))\nsys.path.insert(0, os.path.join(APP, \"web\"))\n\nos.environ.setdefault(\"DJANGO_SETTINGS_MODULE\", \"rhweb.settings\")\n# Apache mounts us at /app.cgi/<path>; present clean root URLs to Django.\nos.environ[\"SCRIPT_NAME\"] = \"\"\n\nfrom wsgiref.handlers import CGIHandler\n\nfrom rhweb.wsgi import application\n\n\ndef _script_url_fix(environ, start_response):\n \"\"\"PEP 3333 fix for non-ASCII URLs (e.g. resources files with Greek\n letters/dashes in their names).\n\n wsgiref's read_environ() already latin-1-mangles PATH_INFO (and any\n REDIRECT_* var that is itself transcodable) so Django can re-decode\n it \u2014 do NOT touch PATH_INFO here (a second mangle breaks routing,\n 404s). But SCRIPT_URL and REDIRECT_URL pass through read_environ\n UNCHANGED as proper unicode, and Django's get_script_name() then\n crashes encoding them as iso-8859-1 (UnicodeEncodeError -> 500).\n Mangle exactly those two.\"\"\"\n for key in (\"SCRIPT_URL\", \"REDIRECT_URL\"):\n v = environ.get(key)\n if v:\n environ[key] = v.encode(\"utf-8\", \"surrogateescape\") \\\n .decode(\"latin-1\")\n return application(environ, start_response)\n\n\nCGIHandler().run(_script_url_fix)\n",
"structuredPatch": [
{
"oldStart": 9,
"oldLines": 17,
"newStart": 9,
"newLines": 6,
"lines": [
" ",
" DOCROOT = os.path.dirname(os.path.abspath(__file__))",
" APP = os.path.join(DOCROOT, \"app\")",
"-",
"-",
"-def _dbg(msg):",
"- if \"resources\" in (os.environ.get(\"PATH_INFO\") or \"\"):",
"- with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",",
"- encoding=\"utf-8\") as fh:",
"- fh.write(msg + \"\\n\")",
"-",
"-",
"-_dbg(\"TOP fsenc=\" + sys.getfilesystemencoding()",
"- + \" PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))",
" ",
" # Vendored pure-Python deps (Django 5.2, markdown) + the project package.",
" sys.path.insert(0, os.path.join(APP, \"vendor\"))"
]
},
{
"oldStart": 33,
"oldLines": 56,
"newStart": 22,
"newLines": 25,
"lines": [
" ",
" from rhweb.wsgi import application",
" ",
"-_dbg(\"AFTER-IMPORT PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))",
" ",
"-from urllib.parse import unquote_to_bytes",
"+def _script_url_fix(environ, start_response):",
"+ \"\"\"PEP 3333 fix for non-ASCII URLs (e.g. resources files with Greek",
"+ letters/dashes in their names).",
" ",
"-",
"-def _pep3333_paths(environ, start_response):",
"- \"\"\"Normalize Apache's path vars to the PEP 3333 form Django needs.",
"-",
"- Apache hands these vars either percent-encoded (mod_rewrite path)",
"- or UTF-8-decoded (direct CGI path). Django (a) crashes with",
"- UnicodeEncodeError on any non-latin-1 char (500) and (b) needs the",
"- decoded path for URL resolution (else the resolver sees %XX and 404s).",
"- So: bytes -> unquote -> re-mangle as latin-1. SCRIPT_URL/REDIRECT_URL",
"- (set by mod_rewrite) are consulted by get_script_name BEFORE",
"- PATH_INFO \u2014 all three must be normalized.\"\"\"",
"- if \"resources\" in (environ.get(\"PATH_INFO\") or \"\"):",
"- with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",",
"- encoding=\"utf-8\") as fh:",
"- fh.write(\"ENTRY PATH_INFO=\" + repr(environ.get(\"PATH_INFO\"))",
"- + \" SCRIPT_URL=\" + repr(environ.get(\"SCRIPT_URL\")) + \"\\n\")",
"- for key in (\"PATH_INFO\", \"SCRIPT_URL\", \"REDIRECT_URL\"):",
"+ wsgiref's read_environ() already latin-1-mangles PATH_INFO (and any",
"+ REDIRECT_* var that is itself transcodable) so Django can re-decode",
"+ it \u2014 do NOT touch PATH_INFO here (a second mangle breaks routing,",
"+ 404s). But SCRIPT_URL and REDIRECT_URL pass through read_environ",
"+ UNCHANGED as proper unicode, and Django's get_script_name() then",
"+ crashes encoding them as iso-8859-1 (UnicodeEncodeError -> 500).",
"+ Mangle exactly those two.\"\"\"",
"+ for key in (\"SCRIPT_URL\", \"REDIRECT_URL\"):",
" v = environ.get(key)",
" if v:",
"- raw = unquote_to_bytes(v) # %XX-decodes; utf-8-encodes str first",
"- environ[key] = raw.decode(\"latin-1\")",
"- if \"resources\" in (environ.get(\"PATH_INFO\") or \"\"):",
"- with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",",
"- encoding=\"utf-8\") as fh:",
"- fh.write(repr({k: environ.get(k) for k in",
"- (\"PATH_INFO\", \"SCRIPT_NAME\", \"SCRIPT_URL\",",
"- \"REDIRECT_URL\", \"REQUEST_METHOD\", \"HTTP_HOST\")})",
"- + \"\\n\")",
"- try:",
"- from django.core.handlers.wsgi import WSGIRequest",
"- req = WSGIRequest(dict(environ))",
"- fh.write(\"path_info=\" + repr(req.path_info) + \"\\n\")",
"- from django.urls import resolve",
"- m = resolve(req.path_info)",
"- fh.write(\"match=\" + repr(m.kwargs) + \"\\n\")",
"- except Exception as e: # noqa: BLE001",
"- fh.write(\"ERR \" + repr(e) + \"\\n\")",
"- try:",
"- raw = open(\"/proc/self/environ\", \"rb\").read()",
"- for entry in raw.split(b\"\\x00\"):",
"- if entry.startswith((b\"PATH_INFO=\", b\"SCRIPT_URL=\")):",
"- fh.write(\"ENVBYTES \" + repr(entry) + \"\\n\")",
"- except Exception as e: # noqa: BLE001",
"- fh.write(\"ENVBYTES ERR \" + repr(e) + \"\\n\")",
"+ environ[key] = v.encode(\"utf-8\", \"surrogateescape\") \\",
"+ .decode(\"latin-1\")",
" return application(environ, start_response)",
" ",
" ",
"-CGIHandler().run(_pep3333_paths)",
"+CGIHandler().run(_script_url_fix)",
" "
]
}
],
"originalFile": "#!/opt/alt/python311/bin/python3.11\n\"\"\"WSGI->CGI adapter \u2014 runs the RH-WEBSITE Django app on Apache shared hosting.\n\nApache rewrites every non-file request to /app.cgi/<path> (see .htaccess).\nwsgiref's CGIHandler bridges the CGI environment onto Django's WSGI app.\n\"\"\"\nimport os\nimport sys\n\nDOCROOT = os.path.dirname(os.path.abspath(__file__))\nAPP = os.path.join(DOCROOT, \"app\")\n\n\ndef _dbg(msg):\n if \"resources\" in (os.environ.get(\"PATH_INFO\") or \"\"):\n with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",\n encoding=\"utf-8\") as fh:\n fh.write(msg + \"\\n\")\n\n\n_dbg(\"TOP fsenc=\" + sys.getfilesystemencoding()\n + \" PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))\n\n# Vendored pure-Python deps (Django 5.2, markdown) + the project package.\nsys.path.insert(0, os.path.join(APP, \"vendor\"))\nsys.path.insert(0, os.path.join(APP, \"web\"))\n\nos.environ.setdefault(\"DJANGO_SETTINGS_MODULE\", \"rhweb.settings\")\n# Apache mounts us at /app.cgi/<path>; present clean root URLs to Django.\nos.environ[\"SCRIPT_NAME\"] = \"\"\n\nfrom wsgiref.handlers import CGIHandler\n\nfrom rhweb.wsgi import application\n\n_dbg(\"AFTER-IMPORT PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))\n\nfrom urllib.parse import unquote_to_bytes\n\n\ndef _pep3333_paths(environ, start_response):\n \"\"\"Normalize Apache's path vars to the PEP 3333 form Django needs.\n\n Apache hands these vars either percent-encoded (mod_rewrite path)\n or UTF-8-decoded (direct CGI path). Django (a) crashes with\n UnicodeEncodeError on any non-latin-1 char (500) and (b) needs the\n decoded path for URL resolution (else the resolver sees %XX and 404s).\n So: bytes -> unquote -> re-mangle as latin-1. SCRIPT_URL/REDIRECT_URL\n (set by mod_rewrite) are consulted by get_script_name BEFORE\n PATH_INFO \u2014 all three must be normalized.\"\"\"\n if \"resources\" in (environ.get(\"PATH_INFO\") or \"\"):\n with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",\n encoding=\"utf-8\") as fh:\n fh.write(\"ENTRY PATH_INFO=\" + repr(environ.get(\"PATH_INFO\"))\n + \" SCRIPT_URL=\" + repr(environ.get(\"SCRIPT_URL\")) + \"\\n\")\n for key in (\"PATH_INFO\", \"SCRIPT_URL\", \"REDIRECT_URL\"):\n v = environ.get(key)\n if v:\n raw = unquote_to_bytes(v) # %XX-decodes; utf-8-encodes str first\n environ[key] = raw.decode(\"latin-1\")\n if \"resources\" in (environ.get(\"PATH_INFO\") or \"\"):\n with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",\n encoding=\"utf-8\") as fh:\n fh.write(repr({k: environ.get(k) for k in\n (\"PATH_INFO\", \"SCRIPT_NAME\", \"SCRIPT_URL\",\n \"REDIRECT_URL\", \"REQUEST_METHOD\", \"HTTP_HOST\")})\n + \"\\n\")\n try:\n from django.core.handlers.wsgi import WSGIRequest\n req = WSGIRequest(dict(environ))\n fh.write(\"path_info=\" + repr(req.path_info) + \"\\n\")\n from django.urls import resolve\n m = resolve(req.path_info)\n fh.write(\"match=\" + repr(m.kwargs) + \"\\n\")\n except Exception as e: # noqa: BLE001\n fh.write(\"ERR \" + repr(e) + \"\\n\")\n try:\n raw = open(\"/proc/self/environ\", \"rb\").read()\n for entry in raw.split(b\"\\x00\"):\n if entry.startswith((b\"PATH_INFO=\", b\"SCRIPT_URL=\")):\n fh.write(\"ENVBYTES \" + repr(entry) + \"\\n\")\n except Exception as e: # noqa: BLE001\n fh.write(\"ENVBYTES ERR \" + repr(e) + \"\\n\")\n return application(environ, start_response)\n\n\nCGIHandler().run(_pep3333_paths)\n",
"autoRead": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"RectangleBorderIntegrable's components ARE IntervalIntegrable — hf1 : IntervalIntegrable (fun x => f (x + z.im * I)) volume z.re w.re ✓. So my RectangleIntegral_add just needs the right destructuring: hf is a 4-tuple (and structure): `obtain ⟨hf1, hf2, hf3, hf4⟩ := hf` (it's a 4-way ∧, not nested pairs — ∧ ∧ ∧: obtain ⟨hf1, hf2, hf3, hf4⟩ works for right-nested ∧? The def: A ∧ B ∧ C ∧ D = A ∧ (B ∧ (C ∧ D)) — obtain ⟨a, b, c, d⟩ handles nested ✓).\n\nBut wait — there's ALREADY `RectangleBorderIntegrable.add` (line 157) in the vendored file! It proves exactly RectangleIntegral (f+g) = RectangleIntegral f + RectangleIntegral g. So I don't need my own HIntegral_add/VIntegral_add/RectangleIntegral_add — use the vendored one. And for RectangleIntegral' additivity: derive from it. Let me check if there's a primed version... and just use it:\n\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', RectangleBorderIntegrable.add hf hg, RectangleIntegral', RectangleIntegral', smul_add]\n```\n\nDelete my HIntegral_add/VIntegral_add/RectangleIntegral_add entirely. Also fix the hmap/uIcc mess in HIntegral_deriv/VIntegral_deriv — the `Set.uIcc_of_le (by simp [Set.uIcc]) hx |>.elim ...` hack — let me think: hx : x ∈ Set.uIcc z.re w.re — need z.re ≤ w.re? uIcc a b = Icc (min) (max) — membership gives min ≤ x ≤ max. The MapsTo needs x ∈ [[z.re, w.re]] = uIcc — same set ✓ so `hmap hx` works directly if [[z.re, w.re]] unfolds to uIcc — `[[a,b]]` notation IS uIcc ✓ so `hmap hx` directly! Let me simplify:\n```\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap hx)).hasDerivAt\n```\nWait — MapsTo f s t x hx : f x ∈ t for x ∈ s ✓ so `hmap hx : (x + y * I) ∈ RectangleBorder z w` ✓ directly (since [[z.re, w.re]] = uIcc z.re w.re defeq ✓).\n\nLet me rewrite the whole file cleanly.","signature":""},{"type":"text","text":"The vendored `RectangleBorderIntegrable.add` already exists — simplifying. Also fixing the MapsTo application (uIcc is definitionally `[[·,·]]`)."},{"type":"tool_use","id":"Write_226","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. Additivity of the primed rectangle integral -/\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', RectangleBorderIntegrable.add hf hg, RectangleIntegral', RectangleIntegral',\n smul_add]\n\n/-! ## 2. Parametrized side derivatives and integrability -/\n\nlemma hasDerivAt_add_const_I (y : ℝ) (x : ℝ) :\n HasDerivAt (fun t => t + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun _ => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n\nlemma hasDerivAt_const_add_I (x y : ℝ) :\n HasDerivAt (fun t => x + t * I) I y := by\n have h1 : HasDerivAt (fun t => t * I) I y := by\n have := (hasDerivAt_id y).mul_const I\n simpa using this\n have hconst : HasDerivAt (fun _ => x) 0 y := hasDerivAt_const y x\n convert hconst.add h1 using 1\n simp\n\n/-- FTC on a horizontal side: ∫_{x₁}^{x₂} (deriv G)(x + yI) dx\n= G(x₂ + yI) − G(x₁ + yI). -/\nlemma HIntegral_deriv {G : ℂ → ℂ} {z w : ℂ} (y : ℝ)\n (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)\n (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun x : ℝ => ↑x + y * I) [[z.re, w.re]] (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 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 _ (hmap hx)).hasDerivAt\n have h2 : HasDerivAt (fun x => x + y * I) 1 x := hasDerivAt_add_const_I y x\n have hcomp := h1.comp x h2\n convert hcomp 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\n intro x hx\n exact (hGc _ (hmap hx)).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n convert hftc using 1\n · simp\n · simp\n\n/-- FTC on a vertical side: ∫_{y₁}^{y₂} (deriv G)(x + yI) dy\n= −I·(G(x + y₂I) − G(x + y₁I)). -/\nlemma VIntegral_deriv {G : ℂ → ℂ} {z w : ℂ} (x : ℝ)\n (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)\n (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun y : ℝ => ↑x + ↑y * I) [[z.im, w.im]] (RectangleBorder z w)) :\n ∫ y in z.im..w.im, deriv G (x + y * I) =\n -I * (G (x + w.im * I) - G (x + z.im * I)) := by\n have hd : ∀ y ∈ Set.uIcc z.im w.im,\n HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by\n intro y hy\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap hy)).hasDerivAt\n have h2 : HasDerivAt (fun y => x + y * I) I y := hasDerivAt_const_add_I x y\n have hcomp := h1.comp y h2\n convert hcomp using 1\n ring\n have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume z.im w.im := by\n apply ContinuousOn.intervalIntegrable\n intro y hy\n exact ContinuousWithinAt.mul continuousWithinAt_const\n ((hGc _ (hmap hy)).continuousWithinAt)\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n rw [← hftc, integral_smul]\n field_simp [Complex.I_ne_zero]\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 rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),\n HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]\n have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)\n have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)\n rw [VIntegral, VIntegral, hVr, hVl]\n simp [Complex.I_mul_I]\n ring\n\nend NguyenRH1\n"},"extra_content":null}]