[{"type":"thinking","thinking":"The user approves DL-1 (Lean). Per the directive §13:\n\nii′-6-DL-1: Dog-leg region analyticity. Exact contour deformation identity.\n\nDeliverables (from D-074 §3.1/3.2 and the directive §4–5):\n1. **Analyticity lemma**: Jlag analytic on a neighborhood of the dog-leg rectangle [3, X_R]×[T_cut, U] — or more precisely in a form the rectangle-integral API needs. Looking at the existing machinery: the residue theorem used was `rectInt'_Jlag` (LiSides) which needs: hre, him, 1 interior, ζ ≠ 0 on border, Sz. For the dog-leg we want the EMPTY residue sum — i.e., RectangleIntegral' (Jlag n) (3+iT) (X_R+iU) = 0. \n\nHow to prove ∮ = 0 in the existing API? Options:\n(a) Use `rectInt'_Jlag` itself with Sz = ∅: it states RectangleIntegral' (Jlag n) z w = ResW1 n + Σ_{ρ∈Sz} ... — but that has ResW1 built in (requires 1 interior) — wrong shape for the dog-leg (1 is NOT in the dog-leg rectangle: re ∈ [3, X_R], so 1 ∉).\n(b) The underlying Zeta23 machinery: `residueTheorem_finset` (vendored, used in LiSides) — RectangleIntegral' f z w = Σ residues for f with principal parts. With S = ∅ and f analytic inside+border: integral = 0. Let me look at what LiSides.lean's rectInt'_Jlag is built on: the vendored `residueTheorem_finset` (from Zeta23.FromPNTPlus.ResidueCalcOnRectangles, seen earlier: \"f − A p/(s − p) bounded near each p ∈ S ⟹ RectangleIntegral' f z w = Σ_{p∈S} A p\" — line 36: `RectangleIntegral' f z w = ∑ p ∈ S, A p`). With S = ∅: the hypothesis \"f − 0 bounded near each p ∈ ∅\" vacuous, but the theorem likely also needs analyticity inside except S and border integrability — with S = ∅ that's exactly \"f analytic on the rectangle + border-integrable\" ⟹ integral = 0.\n\nLet me check the vendored residue theorem's exact signature to see the S = ∅ specialization. Actually simpler: look at how rectInt'_ppart or the residue theorem is applied; there may be a direct \"RectangleIntegral'_eq_zero_of_analytic\" — but likely not; we'll instantiate residueTheorem_finset with S = ∅ and A = 0.\n\nAlternatively (c): Cauchy's theorem for rectangles directly — Zeta23 might have `RectangleIntegral'_eq_zero` of some form. Let me grep.\n\n2. **The exact identity** `upper_right_horizontal_eq_dogleg`: from ∮ = 0, expand the four sides (H/V forms), solve for −H(3→X_R, T): \n   H(3→X_R, T) = H(3→X_R, U) − V(X_R, T→U) + V(3, T→U).\n   In Lean: HIntegral (Jlag n) 3 X_R T = HIntegral (Jlag n) 3 X_R U − VIntegral (Jlag n) X_R T U + VIntegral (Jlag n) 3 T U. From RectangleIntegral' = 0 ⟹ RectangleIntegral = 0 (smul by nonzero) ⟹ expand the def.\n\n3. **Jlag conj identity**: Jlag n (conj s) = conj (Jlag n s) — for the lower side later (DL-5).\n\nThe analyticity needs: for s in the rectangle region (re ∈ [3, X_R], im ∈ [T, U]) and a neighborhood: s ≠ 1 (im > 0 ✓ since T ≥ ... for the identity we need T_cut ≥ something — actually the theorem should be stated for 0 < T and 3 ≤ re: s ≠ 1 since im = T > 0 ✓) and ζ s ≠ 0 (re s > 1 ⟹ nonvanishing — the Mathlib lemma: let me find the exact name. In LiDisc it was \"re ≥ 1 via Mathlib's one_le_re nonvanishing\" — `riemannZeta_ne_zero_of_one_le_re`? Hmm — for re > 1: there's `riemannZeta_ne_zero_of_one_lt_re`? or via the Euler product: `riemannZeta_eulerProduct`... In session-033 banked: \"riemannZeta_ne_zero_of_one_le_re takes ONLY re\". So Mathlib has `riemannZeta_ne_zero_of_one_le_re : 1 ≤ s.re → riemannZeta s ≠ 0`? That seems too strong (ζ(1) is a pole — but at re = 1, s ≠ 1 with im ≠ 0: nonvanishing at re = 1 is the de la Vallée-Poussin theorem — Mathlib has that? Actually the banked note says it exists and takes only re — presumably : 1 ≤ s.re → s ≠ 1 → ζ s ≠ 0 or similar. For our use re ≥ 3: whatever its exact form, re ≥ 3 satisfies it.)\n\nThe plan for DL-1 (one Lean file, say `LiDogLeg.lean`):\n1. `doglegJlagAnalytic`: ∀ s ∈ Rectangle (3+iT) (X_R+iU) ∪ border... — actually the cleanest form for the residue theorem: ∀ s ∈ RectangleBorder, DifferentiableAt; plus interior analyticity except ∅. Let me look at the vendored residue theorem signature first.\n2. `rectangleIntegral'_Jlag_dogleg_eq_zero`.\n3. `upper_right_horizontal_eq_dogleg` (the H/V expansion solved).\n4. `Jlag_conj`.\n\nLet me first look at the vendored residue theorem (ResidueCalcOnRectangles.lean line 30–50) for its exact signature, and check what RectangleBorderIntegrable needs. Also check LiSides.lean's use of it (the vendored residueTheorem_finset call) to clone the pattern.","signature":""},{"type":"text","text":"DL-1 approved. First, inspecting the vendored residue theorem's exact signature (the analyticity→∮ = 0 route) and how LiSides instantiates it."},{"type":"tool_use","id":"TodoWrite_161","name":"TodoWrite","input":{"todos":[{"content":"DL-1: inspect vendored residue theorem + RectangleBorderIntegrable API; design LiDogLeg.lean","status":"in_progress","activeForm":"Inspecting the residue-theorem API"},{"content":"DL-1a: dog-leg analyticity lemma (Jlag analytic at Re ≥ 3, no perimeter)","status":"pending","activeForm":"Proving dog-leg analyticity"},{"content":"DL-1b: ∮ = 0 on the dog-leg rectangle (S = ∅ residue theorem)","status":"pending","activeForm":"Proving the dog-leg rectangle integral vanishes"},{"content":"DL-1c: upper_right_horizontal_eq_dogleg (H/V expansion solved, orientations)","status":"pending","activeForm":"Proving the deformation identity"},{"content":"DL-1d: Jlag_conj identity (for the lower side)","status":"pending","activeForm":"Proving the Jlag conjugation identity"},{"content":"Build green + axiom audit + D-074 log/STATE update + commit DL-1","status":"pending","activeForm":"Building and committing DL-1"}]},"extra_content":null},{"type":"tool_use","id":"Read_162","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\zeta-23-lean\\Zeta23\\FromPNTPlus\\ResidueCalcOnRectangles.lean","offset":28,"limit":45},"extra_content":null}]