Session 037 (2026-08-24) — ii′-3b STARTED: capstone dependency audit + LiMoments §1–§4 COMPLETE (k=1 moment PROVED)

What happened

1. User-requested dependency audit of the ii′-5f capstone (pre-ii′-3b). New file AuditSession037.lean + output audit-session037-axioms.txt: - #print axioms logDeriv_riemannZeta_sub_nearZeros_le_tight → [propext, Classical.choice, Quot.sound] only (no sorryAx, nothing else). - The exact perimeter recorded verbatim from the elaborator: ZeroCountProp (unit window, mult-weighted, ≤ C0hat(t+1), t ≥ 2; C0hat t = 0.433·log(t+2) + 0.886·log log(t+2) + 2.9), ZeroCountProp2 (two-unit window, ≤ 0.6·L + 0.886·LL + 2.7, t ≥ 10), NoLowZeros (∀ ρ nontrivial, 14 ≤ |Im ρ|); plus the statement-level constructs nearZerosSub, Zeta23.zeroMult (= analyticOrderAt.toNat), zeroAbsWindow. One fix during the audit: zeroMult is Zeta23.zeroMult (not NguyenRH1) — the first script run caught it.

2. ii′-3b LAUNCHED with a route revision (D-070). D-066 §3's plan was rectangle contours (zero-avoiding T, horizontal decay from the R-bound, vertical push-off). But 5e's partialFraction_identity (hZC) IS the contour work done once: with gFun := logDeriv xiL, xiL := (s(s−1)/2)·Λ, the identity (G) gFun s = B + seriesFun s at every good point is pure logDeriv algebra, and the moments (M) sigmaP k = −gFun^{(k−1)}(0)/(k−1)! follow by termwise series calculus. Perimeter carried: ZeroCountProp ONLY (the 5f tight bound's hZC2/hNLZ are NOT needed for the moments). D-070 filed with the full argument + sanity gate (σ₁ = −gFun(0) = −B = 1 + γ/2 − ½log 4π ≈ 0.0230957, the Davenport value; B = log 2π − 1 − (log π)/2 − γ/2 ≈ −0.0230957 numerically).

3. LiMoments.lean §1–§4 COMPLETE, build GREEN (~730 lines, new file, not yet root-imported; imports NguyenRH1.LiTightR + LiSwaps + LiResidue + LiDigamma + LiReflect): - §1: xiL entire via the CLOSED FORM xiL s := (s(s−1)/2)·Λ₀(s) − (s−1)/2

   • s/2 (Mathlib completedRiemannZeta_eq: Λ = Λ₀ − 1/s − 1/(1−s), Λ₀ entire — sidesteps removable-singularity proofs; D-066's "Λ₀ wrong object" warning is about Λ₀'s ZEROS, never used). xiL_eq_mul (off {0,1}), xiL_zero/xiL_one (= 1/2), xiL_one_sub (FE, by cases), xiL_ne_zero (via RvM.completedRiemannZeta_eq_zero_iff), isNontrivialZero_one_sub (conj then Zeta23 zeta_reflect_zero), conjZeroEquiv/oneSubZeroEquiv (the two subtype involutions).
   • §2: momentB (Classical.choose of partialFraction_identity) + gFun_eq_momentB — (G) at good points: logDeriv_mul chains (xiL = (s(s−1)/2)·Λ eventuallyEq; Λ = ΓR·ζ eventuallyEq; logDeriv ΓR via logDeriv_Gammaℝ_eq_of_not_neg_nat; the good-set half-shift good_half_ne_neg_nat); final collapse by ring.
   • §3: eq_of_eventuallyEq_nhd_ne (punctured-continuity bridge, tendsto_nhds_unique), gFun_continuousAt, the good-eventually sets at 0 (ζ(0) = −1/2 continuity) and 1 (zetaA factor), seriesFun_zero (= 0 termwise), seriesFun_one (= Σ mult/(ρ(1−ρ))), gFun_zero (gFun 0 = B), gFun_one (gFun 1 = B + seriesFun 1), gFun_one_eq_neg (FE sign: xiL(1−s) = xiL(s) + deriv_comp chain rule + EventuallEq.of_eq.deriv_eq).
   • §4: the summability budget + the k=1 rearrangement: summable_mult_div_norm_sq (master, the ii′-2 (9/4)-comparison skeleton cloned), exists_norm_lower_bound (δ-ball at 0), summable_mult_inv_pow (k ≥ 2), tsum_mult_inv_pow_conj + summable_mult_inv_pow_conj (conjEquiv reindex, zeroMult_conj), sigmaP_eq_unpaired (k ≥ 2: sigmaP k = ½(S+S) = S), summable_mult_div_norm_sq_one_sub (oneSubEquiv transfer), mult_div_norm_mul_norm_le (AM-GM: 1/(‖ρ‖‖1−ρ‖) ≤ ½(‖ρ‖⁻²+‖1−ρ‖⁻²), via (1/a−1/b)² ≥ 0 — NO im-lower-bound needed), summable_mult_one_div_mul_one_sub, summable_mult_vTerm (the 1/ρ̄−1/(1−ρ) = (1−2re)/(ρ̄(1−ρ)) identity; |1−2re| ≤ 1), vTerm_tsum_eq_zero (V = W by conj reindex, W = −V by reflect reindex, so 2V = 0), summable_mult_fst/snd, two_mul_sigmaP_one (2σ₁ = Σ mult/(ρ(1−ρ)) = seriesFun 1), and the k=1 capstone sigmaP_one_eq_neg_gFun_zero (2σ₁ = seriesFun 1 = gFun 1 − B = −2·gFun 0 by the FE sign; linear_combination combo (h2 − hg1 + hg0 + hfe)/2). NO re/conj-of-tsum bridges anywhere — all reality arguments are subtype-equiv reindexes.

REMAINING for ii′-3b (§5/§6) — full skeleton (design verified against Mathlib)

§5 (termwise iterated derivation at 0, k ≥ 2):

• iteratedDeriv_zpow_neg_one (k c) (hs : s+c ≠ 0): iteratedDeriv k (fun s => (s+c)^(−1:ℤ)) s = (−1)^k·k!·(s+c)^(−k−1) — from LiDigamma's iteratedDeriv_neg_zpow_neg_one_add via e : f = −(−f) + iteratedDeriv_neg (EXISTS, explicit args (n f a), probed). (iteratedDeriv_const_mul (c) (hf : ContDiffAt) also exists, Lemmas.lean:368.)
• iteratedDeriv_seriesTerm (j ≥ 1) ρ (hs : s−ρ ≠ 0): seriesTerm s ρ = mult·((s+(−ρ))^(−1:ℤ) + 1/ρ); rw [e, iteratedDeriv_const_mul, iteratedDeriv_add hF1 hF2, iteratedDeriv_const, if_neg j≠0, add_zero, zpow lemma]. ContDiffAt proofs via AnalyticAt → AnalyticAt.contDiffAt (EXISTS, probed); constant via contDiff_const.contDiffAt.
• seriesTerm_deriv_summableLocallyUniformlyOn (j ≥ 1) hδ hball: on u := ball 0 (δ/2) via SummableLocallyUniformlyOn_of_locally_bounded (probed: (IsOpen s) → (∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ n k ∈ K, ‖f n k‖ ≤ u n)). Bound: ‖s−ρ‖ ≥ ‖ρ‖/2 (‖s‖ < δ/2 ≤ ‖ρ‖/2), term ≤ mult·j!·2^{j+1}·(1/δ)^{j−1}·‖ρ‖⁻² =: C_j·(mult/‖ρ‖²) (master lemma mul_left). Norm chain: 3× norm_mul + RCLike.norm_natCast ×2 + hsign (‖(−1)^j‖=1) + norm_zpow + exponent rewrite (−(j:ℤ)−1 = −((j+1:ℕ):ℤ), zpow_neg, zpow_natCast) — the LiDigamma:735–746 pattern EXACTLY. one_div_le_one_div_of_le (probed: 0<a → a≤b → 1/b ≤ 1/a).
• iteratedDeriv_seriesFun_zero (j ≥ 1): obtain δ from exists_ball_avoid_nontrivialZeros 0; iteratedDerivWithin_tsum (probed signature: (m) (IsOpen s) (x∈s) (∀ t∈s, Summable) (∀ k, 1≤k→k≤m → SummableLocallyUniformlyOn ...) (∀ n k r, k≤m→r∈s → DifferentiableAt (iteratedDerivWithin k (f n) s) r)) — the LiDigamma:749–785 call pattern verbatim (side condition: j'=0 → seriesTerm differentiable (s−ρ≠0 on the ball); j'≥1 → eventuallyEq with the closed form, zpow differentiability via hasDerivAt_zpow + rfl-bridge on ∘). Then iteratedDerivWithin_of_isOpen conversions + per-term iteratedDeriv_seriesTerm at 0.

§6 (capstone):

• gFun_eventuallyEq_zero (hZC): gFun =ᶠ[𝓝 0] (B + seriesFun) — upgrade the punctured version via eventually_nhdsWithin_iff (probed ✓) + gFun_zero/seriesFun_zero at the point.
• sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC) (hk : 1 ≤ k): k=1: show (1−1)≡0 defeq; sigmaP_one_eq_neg_gFun_zero. k≥2: iteratedDeriv_congr_of_eventuallyEq (LiDigamma:568) → (fun _ => B) + seriesFun via funext/Pi.add bridge → iteratedDeriv_add hcf hcg (ContDiffAt: const + seriesFun analytic) → iteratedDeriv_const if_neg (k−1≠0) → iteratedDeriv_seriesFun_zero (k−1) → per-term at 0: (0−ρ)^(−k:ℤ) = (−1)^k·(1/ρ)^k (zero_sub, zpow_neg, zpow_natCast, neg_pow, mul_inv, ((−1)^k)⁻¹ = (−1)^k via inv_eq_of_mul_eq_one_right + (−1)^{2k}=1, one_div/inv_pow) → sign (−1)^{k−1}·(−1)^k = −1 (pow_add, 2k−1 = 2(k−1)+1, pow_mul, (−1)²=1) → tsum = −(k−1)!·sigmaP k (tsum_congr, tsum_mul_left, sigmaP_eq_unpaired) → field_simp with (k−1)! ≠ 0 (Nat.cast_eq_zero, Nat.factorial_ne_zero).
• Then: root-import LiTightR + LiMoments in NguyenRH1.lean (STATE.md plan), full build, axiom audit (expect 3 standard axioms; hZC-only dependency), journal/db/STATE/NGUYEN updates, commit. ii′-3b → done; next is ii′-3c ((4.10-a) assembly, D-066 §2: needs also the FE derivative relation gFun^{(k−1)}(0) = (−1)^k·gFun^{(k−1)}(1) — new but small from xiL_one_sub
• iteratedDeriv comp machinery).

Banked gotchas (this session)

• SummationFilter refactor: tsum lemmas are SummationFilter-parameterized in this Mathlib; tsum_add/tsum_sub exist ONLY as method forms Summable.tsum_add hf hg / Summable.tsum_sub (plain tsum_add is UNKNOWN); tsum_neg, tsum_zero, tsum_congr, tsum_mul_left are plain.
• eq_zero_of_neg_eq needs LinearOrder — N/A for ℂ; use 2V = 0 via linear_combination + mul_eq_zero.resolve_left.
• Complex.norm_conj : ‖(starRingEnd ℂ) z‖ = ‖z‖ — takes the starRingEnd form DIRECTLY (don't rw [starRingEnd_apply] first; the star form breaks rw matching).
• iteratedDeriv_neg (n) (f) (a) EXISTS (explicit args); iteratedDeriv_const_mul (c) (hf : ContDiffAt 𝕜 n f x); AnalyticAt.contDiffAt exists (CompleteSpace needed).
• Equiv.tsum_eq e f : ∑' a, f (e a) = ∑' b, f b; Equiv.summable_iff e : Summable (f ∘ e) ↔ Summable f (f implicit — NO second argument; state the family equation with ∘ and funext).
• Beta-redex goals (families applied to equiv images): show-before-rw (state the beta-reduced form with show, then rw) — plain rw can't find the cast patterns inside redexes. (Recurred 5×.)
• Ascribe every tsum binder: ∑' ρ, ... (zeroMult ρ : ℂ) ... elaborates ρ : ℂ (zeroMult expects ℂ) — silently produces a tsum over the WRONG domain. Always ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, ....
• field_simp closes goals outright (trailing ring then errors "no goals" — 3× this session); but field_simp given ‖x‖ ≠ 0 instead of x ≠ 0 normalizes without clearing — pass the COMPLEX nonzeros (x ≠ 0, 1−x ≠ 0, conj x ≠ 0).
• convert h using 1; ring on HasDerivAt values: convert can produce non-equality goals ("ring_nf made no progress") — instead ASCRIBE the derivative value in the HasDerivAt statement and rw [h.deriv]; ring.
• deriv.comp / deriv_comp: point arg x is EXPLICIT first (deriv_comp 0 h1 h2); numeral-as-function error otherwise.
• ContinuousAt.add on continuousAt_const: produces Pi.add functions — the defeq assignment have hG : ContinuousAt (fun s => c + f s) x := hG0 works (simpa [Pi.add_apply] does NOT).
• linear_combination works over ℂ (use it for ℂ equalities; linarith does NOT).
• Housekeeping: Scratch.lean (previously the session-029 audit script) was overwritten with this session's lemma probe — the session-029 audit RESULTS are preserved in audit-session029-axioms.txt (script re-derivable from the AuditSession03X pattern).

Files

• research/lean/NguyenRH1/NguyenRH1/LiMoments.lean (NEW, ~730 lines, GREEN)
• research/lean/NguyenRH1/AuditSession037.lean + audit-session037-axioms.txt
• research/lean/NguyenRH1/Scratch.lean (lemma probe; see housekeeping)
• research/derivations/D-070-ii-prime-3b-route-revision.md (NEW)