Session 016 — 2026-08-21 — Tier ii′ sub-stage ii′-1b (i)+(ii) COMPLETE

Directive

Continue tier ii′ per D-064: sub-stage ii′-1b (R1 residue machinery).

Work done

ii′-1b(i) COMPLETE (commit 1c35d31) — LiResidue.lean:

• zetaA = (w−1)·ζ(w) extended by 1 at 1: analytic (removable singularity via Mathlib riemannZeta_residue_one + RemovableSingularity.lean's differentiableOn_update_limUnder_of_bddAbove).
• hLi = 1 − (w−1)·(zetaA′/zetaA): analytic at 1, value 1, agrees with (w−1)(−ζ′/ζ) on a punctured neighborhood of 1 (hLi_eq_near_one, via riemannZeta_residue_one.eventually_ne).
• lcoeff k := iteratedDeriv (k+1) hLi 1 / (k+1)! — operational Laurent coefficients of −ζ′/ζ at 1.
• A_iter: iterated derivatives of A(w) = wⁿ−(w−1)ⁿ at 1 (descFactorial for i < n, 0 for i = n; via iteratedDeriv_pow + iteratedDeriv_comp_sub_const).
• ResW1_eq_sum: the w=1 residue of the Lagarias-kernel integrand equals Σ_{j=1}^n C(n,j)·lcoeff(j−1) — via iteratedDeriv_mul (Leibniz), as designed (D-064 R1) and verified numerically (session 014).

ii′-1b(ii) COMPLETE (commit 973fe66) — LiPrincipal.lean:

• rectInt_deriv_eq_zero: RectangleIntegral (deriv G) = 0 when G is differentiable on the border — per-side FTC with the mixed-field chain rule (HasDerivAt.comp in the ℝ→ℂ→ℂ algebra tower), border MapsTo from vendored Rectangle.lean.
• RectangleIntegral'_add linearity.
• Acoeff/ppart/Gprim; deriv_Gprim (termwise: hasDerivAt_zpow + comp); tail_continuousAt (Finset induction); ppart_eq_deriv_add.
• rectInt'_ppart: RectangleIntegral' (ppart n) z w = ResW1 n on any rectangle with 1 interior — A_1 term by the vendored ResidueTheoremInRectangle, i ≥ 2 tail vanishes by the primitive FTC.

Both axiom-audited: 3 standard axioms only.

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

• Factorial n ! is SCOPED notation — needs open scoped Nat.
• conj is scope-locked (ComplexConjugate) — use starRingEnd ℂ.
• Parametrized lambdas over ℝ into ℂ need explicit (x : ℝ) annotations (else x elaborates at ℂ and every downstream unify fails).
• HasDerivAt.comp handles mixed fields via NormedAlgebra/IsScalarTower.
• ContinuousLinearMap.hasDerivAt : HasDerivAt e (e 1) x (ofRealCLM).
• intervalIntegral.integral_eq_sub_of_hasDerivAt (FTC-2) with explicit (f := ...) (f' := ...) args — unification is brittle otherwise.
• ContinuousAt of expressions containing the point variable: write the fun w => lambda EXPLICITLY (Lean's eta-unification misfires).
• Finset.sum_apply / funext for sum-of-functions ↔ lambda-of-sums.
• Finset.sum_bij arg order: (i, hi, i_inj, i_surj, h).
• differentiableOn_update_limUnder_of_bddAbove (removable singularity); Tendsto.eventually_ne; DifferentiableOn.deriv (CauchyIntegral.lean).

State at stop

ii′-1b(i)+(ii) complete. Remaining for ii′-1b: (iii) the full rectangle residue theorem for J — R = J − P holomorphic off {zeros ∪ {−2}} (order ≥ 0 at 1 via Taylor-remainder), simple poles at zeros (residue mult·(1−(ρ/(ρ−1))ⁿ)) and at −2 (residue 1−(2/3)ⁿ), via vendored residueTheorem_finset (Zeta23.Analytic.RectangleLogDeriv), then assemble sides = ResW1 + Σ + triv. Next session: ii′-1b(iii).