Session 017 — 2026-08-21 — Tier ii′ sub-stage ii′-1b(iii) COMPLETE (ii′-1b now fully done)

Directive

Continue tier ii′ per D-064: finish ii′-1b — (iii) the rectangle residue theorem for the Lagarias-kernel integrand J (STATE.md NEXT ACTION).

Work done

ii′-1b(iii) COMPLETE (commit f3d7244) — LiSides.lean (~460 lines, 19 new declarations, single-file check clean, full lake build GREEN 8745 jobs — first build covering LiResidue/LiPrincipal, which session 016 had left out of the package root; root NguyenRH1.lean now imports all three):

• kFun n w = (w/(w−1))ⁿ−1, Jlag n w = kFun n w·(−ζ′/ζ(w)), Rfun n = Jlag n − ppart n + differentiability/continuity kits (kFun_differentiableAt, ppart_differentiableAt, Jlag_differentiableAt, Rfun_differentiableAt, ppart_continuousAt).
• zeta_order_ne_top_of_ne : analyticOrderAt ζ ρ ≠ ⊤ for all ρ ≠ 1 — identity principle through the ENTIRE zetaA (avoids punctured-plane connectedness): analyticOrderAt_ne_top_of_isPreconnected on univ with zetaA 1 = 1 ≠ 0, then order(zetaA) = order((w−1)·ζ) = 0 + order(ζ) via analyticOrderAt_congr + analyticOrderAt_mul. NOTE: zetaA's value-1-at-1 also makes riemannZeta 1's junk value irrelevant everywhere — no ζ(1) ≠ 0 lemma needed.
• rectangle_mem_nhds_of_mem_not_border — interior from border avoidance (extracted from the vendored hZint argument).
• Removable singularity at 1 (Rfun_bounded_near_one): on 𝓝[≠] 1, R = (Ffun n − TaylP n)/(w−1)^{n+1} (Rfun_eq_sub_div_near_one, from Jlag_mul_pow + ppart_mul_pow); Ffun_sub_TaylP_order: order ≥ n+1 via natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero — iteratedDeriv_TaylP (the i-th deriv of the Taylor poly matches Ffun's: descFactorial/0^{j−i} split, Finset.sum_eq_single); then Rfun_tendsto_one by cases on order = ⊤ (R → 0) or factorization g = (w−1)^m·h with m ≥ n+1 (R → 0^{m−n−1}·h(1)). Residue at 1 is 0 for R — exactly what residueTheorem_finset needs with 1 ∈ S.
• Residue at a zero (Rfun_residue_at): for ANY ρ ≠ 1, R − mult(ρ)·(1−(ρ/(ρ−1))ⁿ)/(w−ρ) is bounded on 𝓝[≠] ρ — logDeriv normal form ζ = (w−ρ)^m·h, h(ρ) ≠ 0 (from zeta_order_ne_top_of_ne + AnalyticAt.analyticOrderAt_ne_top), so −ζ′/ζ = −m/(w−ρ) − h′/h; the kFun slope → kFun′(ρ), h′/h and ppart continuous. Multiple zeros OK (logDeriv poles are simple). Sign check: residue = −m·kFun n ρ = m·(1−(ρ/(ρ−1))ⁿ) ✓ matches D-064.
• rectInt'_Jlag (the deliverable): rectangle with 1 interior, no zeros of ζ on the border, Sz any finset with s ∈ Sz ↔ s ∈ Rectangle ∧ zetaA s = 0 (supplied form, like the vendored rectangleIntegral'_mul_logDeriv; downstream produces Sz from finite_zeros_rectangle — zetaA is entire so it applies across w = 1): RectangleIntegral' (Jlag n) z w = ResW1 n + Σ_{ρ ∈ Sz} (zeroMult ρ)·(1 − (ρ/(ρ−1))ⁿ). Proof: residueTheorem_finset on R with S = insert 1 Sz, A 1 = 0, A ρ = mult·(1−(ρ/(ρ−1))ⁿ); then Jlag = Rfun + ppart, RectangleIntegral'_add, rectInt'_ppart (session 016).

Axiom audit (PrintAxioms.lean): all 19 declarations — propext, Classical.choice, Quot.sound ONLY. No sorryAx.

Deferred (documented in file header): zeroMult(−2) = 1 (trivial-zero simplicity — not in Mathlib/Zeta23; would need the functional-equation deriv computation). The sum keeps zeroMult symbolic; the Sz = {nontrivial} ∪ {−2} split on the D-064 rectangle is ii′-4 territory.

Lean notes (hard-won this session, additions to the handoff list)

• analyticOrderAt_ne_top_of_isPreconnected is AnalyticOnNhd-namespaced (AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected).
• mul_div_cancel_left₀ (b) (ha : a ≠ 0) : a * b / a = b — the EXPLICIT arg is b (the kept factor); pass _.
• Tendsto.congr' needs an EventuallyEq — a raw ∀ᶠ s, f s = c has no .symm; ascribe the have as f =ᶠ[l] g explicitly.
• mem_nhdsWithin_of_mem_nhds yields the raw set-membership form ({x | p x} ∈ 𝓝 s); coerce to f =ᶠ[𝓝 s] g by type ascription before .deriv_eq / .self_of_nhds dot-projection works.
• analyticOrderAt_mul in a rw needs (f := ...) (g := ...) named — analyticAt_id.sub analyticAt_const elaborates to id − const, not the fun w => w − 1 lambda; show-bridge for the defeq.
• field_simp sometimes closes the cleared goal itself — a trailing ring then errors "no goals". Remove on recompile error.
• Nat.cast_analyticOrderNatAt (h : order ≠ ⊤) : ↑orderNat = order — rewrite direction ← ... at h to turn an order bound into a nat bound (ENat.natCast_le_natCast.mp).
• riemannZeta 1 = (γ − log 4π)/2 (Mathlib ZetaAsymp) — junk value but nonzero; routing everything through zetaA avoids needing it.

State at stop

ii′-1b (R1 residue machinery) FULLY COMPLETE: (i) ResW1_eq_sum, (ii) rectInt'ppart, (iii) rectInt'_Jlag. The sides identity sides(T) = ResW1 n + Σ{ρ ∈ Sz} mult·(1−(ρ/(ρ−1))ⁿ) is now a Lean theorem. Next: ii′-2 — R2(i)/(ii) elementary swaps: λ_n = Σ_j (−1)^{j+1}C(n,j)σ_j (binomial + paired swap) and S_∞ = Σ_j C(n,j)τ_{j−1} (D-064 §4 R2).