Session 038 (2026-08-24) — ii′-3b COMPLETE

Goal

Finish ii′-3b (the contour moments (M): sigmaP k = −gFun^{(k−1)}(0)/(k−1)!, D-070 route — from 5e's partialFraction_identity by pure algebra + series calculus, no contours). Session 037 banked §1–§4 + the k = 1 capstone; this session built §5 (termwise iterated derivation at 0, k ≥ 2) and §6 (the unified capstone), root-imported LiTightR + LiMoments, full build + audit.

What was done

LiMoments.lean §5 (~190 lines):

• iteratedDeriv_zpow_neg_one — the positive form of the zpow iterated derivative from LiDigamma's iteratedDeriv_neg_zpow_neg_one_add via iteratedDeriv_neg (neg_neg needed .symm in the funext; the final sign normalization needed simp only [neg_mul, neg_neg] — the neg is buried inside the product, bare neg_neg can't fire).
• iteratedDeriv_seriesTerm — (d/ds)^j [mult·(1/(s−ρ)+1/ρ)] = mult·(−1)^j·j!·(s−ρ)^{−j−1} (j ≥ 1). Via the zpow rewrite (funext + simp only [one_div, zpow_neg_one, sub_eq_add_neg]), iteratedDeriv_const_mul (ContDiffAt from AnalyticAt.contDiffAt), the Pi.add hsplit := rfl bridge before iteratedDeriv_add, iteratedDeriv_const + if_neg, and a sub_eq_add_neg bridge to the (s + −ρ) form of the zpow lemma.
• seriesTerm_deriv_summableLocallyUniformlyOn — the M-test on ball(0, δ/2): dominator C_j·(mult/‖ρ‖²) with C_j = j!·2^{j+1}·(1/δ)^{j−1} (‖s−ρ‖ ≥ ‖ρ‖/2 from the avoiding ball; 1/‖ρ‖^{j−1} ≤ (1/δ)^{j−1}; the h1/h2/h3 chain: one_div comparison, div_pow+inv_div for the (‖ρ‖/2)-power, pow_add+mul_inv for the j+1 = (j−1)+2 split). The norm chain is the LiDigamma:735–746 pattern (3× norm_mul + RCLike.norm_natCast ×2 + hsign + norm_zpow + the exponent rewrite), then a 3-step calc (mul_assoc bridge, the hkey multiplication, closing ring).
• iteratedDeriv_seriesFun_zero — the LiDigamma:749–785 iteratedDerivWithin_tsum call pattern verbatim on ball(0, δ/2): seriesSummable everywhere; the M-test per derivative order; the side differentiability by cases (k = 0: analyticAt const·(1/(z−σ)+1/σ); k ≥ 1: eventuallyEq with the closed form + hasDerivAt_zpow ∘ rfl). Local pole_free (‖σ‖ − ‖t‖ ≤ ‖t−σ‖ via norm_sub_norm_le + norm_sub_rev + linarith).

LiMoments.lean §6 (~100 lines):

• gFun_eventuallyEq_zero — (G) upgraded from 𝓝[≠] 0 to 𝓝 0 via eventually_nhdsWithin_iff + by_cases (at 0: gFun_zero + seriesFun_zero).
• sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC : ZeroCountProp) — THE CAPSTONE: sigmaP k = −(iteratedDeriv (k−1) gFun 0)/(k−1)!, all k ≥ 1. k = 1 branch: Nat.add_sub_cancel + iteratedDeriv_zero + the 0! = 1 fold + sigmaP_one_eq_neg_gFun_zero. k ≥ 2 branch: iteratedDeriv_congr_of_eventuallyEq → the Pi.add hsplit → iteratedDeriv_add → iteratedDeriv_const if_neg → iteratedDeriv_seriesFun_zero → the per-term sign algebra (e1: (0−ρ)^{−k−1} = (−1)^{k+1}(1/ρ)^{k+1} via zpow_neg/zpow_natCast/ neg_pow/mul_inv + inv_eq_of_mul_eq_one_right + ← inv_pow + one_div; hsign: (−1)^k·(−1)^{k+1} = −1 via pow_add/pow_mul; e2 ring regroup) → tsum_congr + tsum_neg + neg_neg + tsum_mul_left + ← sigmaP_eq_unpaired → field_simp with k! ≠ 0. FIRST-PASS GREEN.

Closure: LiTightR + LiMoments root-imported (root header updated); full build GREEN (8770 jobs, LiMoments 20 s); AuditSession038.lean + audit-session038-axioms.txt — 23 declarations, ALL: [propext, Classical.choice, Quot.sound] only, 0 sorryAx.

ii′-3b → COMPLETE. Perimeter of the capstone: ZeroCountProp ONLY (5f's hZC2/hNLZ not needed for the moments, per D-070).

Banked gotchas (this session)

• Factorial ! notation is scoped notation in namespace Nat — needs open scoped Nat (LiDigamma has it; LiMoments didn't; the parse error "unexpected token ':'; expected no space before or term" points at the ! and looks like a spacing problem but is a MISSING OPEN).
• Summable.mul_left unification loop: the dominator MUST be written C * (D ρ) (constant first) to match fun i => a * f i syntactically; D ρ * C sends the anonymous-constructor refine into an 800k-heartbeat whnf loop (the mismatch only shows up when u and the mul_left proof are elaborated together — bisect with dominator-only/mulleft-only sorries).
• rw [seriesFun] FAILS when seriesFun appears UNAPPLIED (e.g. inside iteratedDeriv j seriesFun 0) — equation-theorem matching needs the applied form; use a show with the beta-expanded lambda instead (defeq unfolds the def).
• norm_sub_norm_le (a) (b) : ‖a‖ − ‖b‖ ≤ ‖a − b‖ in this Mathlib — NO abs on the LHS (the abs_le.mp detour errors; use it directly).
• Don't rw [Metric.mem_ball, ...] at h a membership hypothesis you still need as membership — derive a separate norm hypothesis with simpa only [Metric.mem_ball, dist_zero_right] using h.
• (neg_neg _).symm for the funext direction (goal f = -(-f)).
• Buried-neg normalization: simp only [neg_mul, neg_neg] (bare neg_neg can't fire when the inner neg is a factor of a product).
• iteratedDeriv_add needs the Pi.add form — bridge with have hsplit : (fun s => F s + G s) = (fun s => F s) + (fun s => G s) := rfl before the rw (the pointwise lambda doesn't match the lemma's f + g pattern).
• The calc-step 2^(j+1) * ((δ^(j−1))⁻¹ * X) = 2^(j+1) * (1/δ)^(j−1) * X closes by rw [div_pow, one_pow, one_div, mul_assoc] (the trailing mul_assoc fixes the reassociation; rw auto-closes by rfl).

Files

• research/lean/NguyenRH1/NguyenRH1/LiMoments.lean (§5/§6 added; file now ~1020 lines, GREEN)
• research/lean/NguyenRH1/NguyenRH1.lean (LiTightR + LiMoments root-imported; header updated)
• research/lean/NguyenRH1/AuditSession038.lean + audit-session038-axioms.txt (23 decls, 3 standard axioms only)
• research/lean/NguyenRH1/Scratch.lean (lemma probes; session-037 results preserved in audit-session037-axioms.txt)

ii′-3c COMPLETE (same session, continuation)

LiCrux.lean NEW (~430 lines, GREEN, root-imported): the (4.10-a) assembly + the crux identity. Chain (D-066 §2):

• gFun_one_sub_fun — the FE as a function identity gFun(1−s) = −gFun everywhere (xiL entire; xiL_one_sub + deriv_comp chain rule; the simp at hcomp beta-normalization + linear_combination -h2).
• iteratedDeriv_gFun_zero — gFun^{(m)}(0) = (−1)^{m+1}·gFun^{(m)}(1) via the UNCONDITIONAL iteratedDeriv_comp_const_sub (function-level equality, junk-free!) + iteratedDeriv_neg. No induction needed.
• gFun_one_add_punctured — the shift expansion gFun(1+s) = 1/(1+s) + hLiExt s + ΓR′/ΓR(1+s) on 𝓝[≠] 0 (the gFun_eq_momentB logDeriv-algebra pattern at 1+s; the hLiExt identity via zetaA's deriv_mul + mul_div_cancel_left₀).
• gFun_one_add_eventuallyEq — upgraded to full 𝓝 0 (continuity of both sides + eq_of_eventuallyEq_nhd_ne; the Gammaℝ-piece ContDiffAt via ContDiffAt.congr_of_eventuallyEq with the digamma form — NO AnalyticAt-Gammaℝ detour needed).
• iteratedDeriv_gFun_one — coefficient extraction: gFun^{(m)}(1) = (−1)^m·m! − m!·lcoeff m + (−1)^{m+1}·m!·a_{m+1} (iteratedDeriv_comp_add_const + congr + two add splits + the three pieces: iteratedDeriv_one_div_one_add (zpow lemma), iteratedDeriv_hLiExt, iteratedDeriv_logDeriv_Gammaℝ).
• lagarias_4_10_a (hZC) — (4.10-a) PROVED: lcoeff (k−1) = (−1)^k·(lagariasA k + sigmaP k) + (−1)^{k−1}, all k ≥ 1. The multiplied-out linear_combination ((−t)·hM2 + t·hFE + t²·hExp + (−F·c + t·F·a + s·F)·ht_sq with F = m!, s = (−1)^m, t = (−1)^{m+1})
• mul_left_cancel₀ (m! ≠ 0).
• sf_eq_resW1 (hZC) — THE CRUX PROVED: (ResW1 n).re = Sf n for n ≥ 1. ResW1_eq_sum + (4.10-a) per-term + the two ii′-2 swaps (sInfty_eq_sum cast by push_cast; liCoeff_eq_sum_sigma with the (−1)^j = −(−1)^{j+1} per-term ring) + the binomial sum Σ_{j=1}^n (−1)^{j−1}C(n,j) = 1 (add_pow (−1) 1 n + insert-0 peel + hsign (−1)^{j−1} = −(−1)^j) + the ℂ identity hid + .re.

Closure: LiCrux root-imported; full build GREEN (8771 jobs); AuditSession038b.lean + audit-session038b-axioms.txt — 8 declarations, ALL: [propext, Classical.choice, Quot.sound] only, 0 sorryAx.

ii′-3 (ALL of (4.10)) → COMPLETE. Perimeter of both capstones: ZeroCountProp ONLY.

Banked gotchas (ii′-3c)

• iteratedDeriv_comp_const_sub/add_const are UNCONDITIONAL function-level equalities — no differentiability hypotheses, no induction (the whole FE relation is 4 lines).
• ContDiffAt.congr_of_eventuallyEq (hf : ContDiffAt n f x) (h : f₁ =ᶠ[𝓝 x] f) — the h goes FROM the target TO the proved-smooth function (pass hev, NOT hev.symm).
• Finset.sum_add is RENAMED Finset.sum_add_distrib (SummationFilter refactor); Finset.sum_sub also gone.
• Nat.exists_eq_succ_of_ne_zero gives m.SUCC form — normalize with rw [Nat.succ_eq_add_one, Nat.add_sub_cancel] (Nat.add_sub_cancel doesn't match m.succ − 1).
• simp using X.deriv SILENTLY derailed the tactic block (rw [h1] then can't fire; error reported at the have statement) — use the direct .deriv term: ((hasDerivAt_id' x).sub_const 1).deriv : deriv (fun w => w − 1) x = 1 (sub_const's value is ALREADY 1, not 1−0 — the ascription (1 − 0) fails).
• ContinuousAt.comp/Tendsto.comp numerals: (1:ℂ)+0 is NOT kernel-defeq to 1 — rw [show (1 : ℂ) = 1 + 0 from (add_zero 1).symm] at hg BEFORE the comp so the points match syntactically; dot-notation hg.comp hc elaborates f := const-ofNat unless pinned.
• show with U+2212 minus (−1) breaks the parser ("(↥) must have a function type") — the file's (−1)-forms are ASCII (-1 : ℂ); keep show-statements ASCII.
• rw [hS] vs rw [← hS]: when hS : cast = Σ and the goal has the Σ (from a previous sum-split rewrite), the direction is ← hS.
• mul_div_cancel_left₀ (b) (ha : a ≠ 0) : a * b / a = b — kills (s·X)/s goals field_simp leaves behind.
• Fraction-equality pattern that ALWAYS works: div_add_div to merge the RHS + div_eq_div_iff (both denominators ≠ 0) + ring — avoids field_simp's s⁻¹ leftovers (s·ζ·s⁻¹ is not a ring identity).

Files (ii′-3c)

• research/lean/NguyenRH1/NguyenRH1/LiCrux.lean (NEW, ~430 lines, GREEN)
• research/lean/NguyenRH1/NguyenRH1.lean (LiCrux root-imported)
• research/lean/NguyenRH1/AuditSession038b.lean + audit-session038b-axioms.txt (8 decls, 3 standard axioms only)

Next

ii′-6 (L0 assembly, D-064 R4/R5): the sides identity |sides| bound via the tight R-bound (5f) + the bridge |λ_n(T)| ≤ 2·FAlt(T) (hRH) + |Sf n| ≤ Bn FAlt n on [10⁵, N₁]; D-069 Finding 2's H(T) near-sum repair map (honest ≈ 7·Ĉ₀² vs baked 3·Ĉ₀²; margin survives via E-028's 26× slack) lives here. Then ii′-7 (closure).

ii′-6-0 DESIGN COMPLETE (same session, second continuation)

D-071 design doc + E-030 validation (ALL CHECKS PASS) + two user approvals. The fold analysis found THREE findings:

• F-A (bridge factor-2): λ_n(T) sums over BOTH signs of γ ⟹ honest bridge |λ_n(T)| ≤ 4·FAlt; D-036/D-037/E-023's B(n) charges 2·FAlt (one-sign N(T) with a both-signs sum) — factor-2 accounting slip, harmless to R-004 (≪ margins), paper erratum at ii′-7 (user protocol step 7).
• F-B (I_III two-unit count): the near-sum on the left vertical honestly needs (2/3)·Z2 (ZeroCountProp2 form), not (2/3)Ĉ₀ — D-069 Finding 2's "(4/3)-ish" made exact.
• F-C (baked Bn unprovable beyond ~5×10⁷, E-030 V1): the killers (+2F, +(2/3)(Z2−Ĉ₀)·4T) grow like T·log T and outgrow the horizontal slack (log T)²: assembly/baked-Bn = 0.656 (10⁵) → 0.980 (10⁸) → 1.012 (10¹²) → 1.015 (N₁). RESOLUTION (user-approved, 8-step protocol): redefine Bn honestly (4F, (2/3)Z2) — fold then works everywhere (V4), margin > 0 on the grid (V2, IMPROVED near 10⁵), horizontal segment-integral ≤ 0.40 of its share (V3).
• Perimeter additions approved: ZeroCountGlobalProp (global Trudgian N(T) ≤ FAlt, one-sign) + MZeroProp (‖ζ′/ζ(−5/2+it)‖ ≤ 1.3352, |t| ≤ 10) — D-062 §4 trust classes.
• Sub-stage map: ii′-6-a (Bn redefinition + convexity re-proof + base-point re-certification) → 6-b (perimeter Props + extended pigeonhole + sides identity + bridge) → 6-c (four side bounds; horizontals = the segment-integral machine, long pole) → 6-d (fold ⟹ sfBoundProp) → ii′-7 (closure + paper correction note).
• E-030 registered (script + CSV/JSON + db; V4 initially failed on a 6-digit string-precision artifact in the check itself — fixed to full-precision comparison; the fold was never in doubt).

ii′-6-a COMPLETE (same session, third continuation) — the honest-Bn redefinition

User protocol steps 1–5 ALL DONE (D-071 §5):

1. Bn redefined (LiSkeleton.lean): bridge 2F → 4F, I_III (2/3)Ĉ₀ → (2/3)Z2hat (new def Z2hat with the D-071 doc comment); marginTilde in lockstep.
2. Corrected definitions carry explicit D-071 correction comments (identifier retained; audit history preserved via git + E-030).
3. marginTilde_convex RE-PROVED (builds green): the block constants mFblock (−2→−4), mTL1b ((8/3)·0.433→(8/3)·0.6), mIdb ((8/3)·2.9→(8/3)·2.7) + the ψ-row literals (vF/vTL1/vId, hnn1/hnn2/hnn4) — the sign haves' by norm_num handled the new constants mechanically; marginTilde_eq_expanded needed Z2hat added to the simp only unfold list; continuousOn_marginExpanded had a hardcoded const_mul (−2) → (−4).
4. Base points RE-CERTIFIED (LiBasePoints.lean): the upper bounds Bn_FAlt_80000_le 328,000 → 329,000 and Bn_FAlt_100000_le 347,000 → 350,000 (the old ones FAIL for the corrected Bn — 4F + (2/3)Z2 raise the totals by ~1.1–2.2k); new Z2hat interval bounds (7.6705/7.7483 upper, 6.06 lower); the _ge lower-bound proofs' brackets converted to Z2hat; one 3×10⁻⁵ rounding slip (114.0655 → 114.0656) caught by linarith. Downstream margins: marginTilde_FAlt_80000_pos (≥ 7,001 > 0 ✓), marginTilde_FAlt_80000_lt_100000 (65,001 < 82,501 ✓) — statements otherwise unchanged.
5. Endpoint margins re-run (dps 60): margiñ(8×10⁴) = 14,681.84 (was 15,763.68); margiñ(10⁵) = 90,652.75 (was 91,887.77); margin(N₁) = 2.457962406×10²⁶ (unchanged to leading digits).

Closure: full build GREEN (8771 jobs — first background attempt killed by the wrapper timeout; restarted detached per the long-run protocol); AuditSession038c.lean + audit-session038c-axioms.txt — lambda_pos_finite_height_verified + marginTilde_convex + the eq-lemmas + both base-point certificates: ALL 3 standard axioms only, 0 sorryAx; the corrected Bn printed verbatim (4F, (2/3)Z2hat ✓).

Banked: lake env lean FILE type-checks against the STALE olean of its imports — after editing a file's dependencies, lake build NguyenRH1.X FIRST (the LiBasePoints "clean build" against the old Bn was an artifact); certified-constant arithmetic must be re-checked by hand at 1e-4 (the (2/3)·7.7483 + 60.9 + 48 = 114.06553 vs certified 114.0655 slip).

Files (ii′-6-a)

• research/lean/NguyenRH1/NguyenRH1/LiSkeleton.lean (Z2hat + corrected Bn/marginTilde + block constants + ψ-row literals)
• research/lean/NguyenRH1/NguyenRH1/LiBasePoints.lean (base points re-certified at 329,000/350,000)
• research/lean/NguyenRH1/AuditSession038c.lean + audit-session038c-axioms.txt

Next

ii′-6-b (D-071 §6): perimeter Props (ZeroCountGlobalProp — global Trudgian N(T) ≤ FAlt one-sign; MZeroProp — M₀ ≤ 1.3352), the extended pigeonhole exists_zero_avoiding_T_wide (3-unit window, clearance 1/(9·C0hat(a+2))), the sides identity (rectInt'_Jlag on the variant-B rectangle ⟹ |Sf n| ≤ ‖RectInt‖ + |λ_n(T)| + |triv|), and the bridge |λ_n(T)| ≤ 4·FAlt (hRH + conj symmetry + ZeroCountGlobalProp).

ii′-6-b COMPLETE (same session, fourth continuation) — the assembly pieces

LiContour.lean additions (builds green): the two user-approved perimeter Props — ZeroCountGlobalProp (∀ T ≥ 2, mult-weighted one-sign count with 0 < γ ≤ T ≤ FAlt T; zeroGlobalWindow + zeroGlobalWindow_finite) and MZeroProp (∀ |t| ≤ 10, ‖logDeriv ζ (−5/2 + t·I)‖ ≤ 1.3352) — plus the wide pigeonhole exists_zero_avoiding_T_wide (T ∈ [a, a+1], clearance 1/(9·C0hat(a+2)) against ALL zeros with im ∈ (a−1, a+2); zeroWindowWide + the 3-unit count ≤ 3·C0hat(a+2) via three unit windows + inline log-monotonicity; the exists_avoiding_midpoint machine reused verbatim).

LiAssembly.lean NEW (~460 lines, builds green, root-imported):

• §1 sf_abs_le_rectInt_add_zeroSum (hZC): the sides identity — rectInt'_Jlag on the variant-B rectangle (rectZ T = −5/2 − iT, rectW n T = 2√n + iT) with 1 interior and the border zero-free (zeta_zero_classification: nontrivial → the wide-pigeonhole contradiction on im = ±T (conj for the bottom); re = −5/2 excluded by the strip; re = 2√n ≥ 2 by one_le_re; s = 0 / −2n by direct re/im computation) ⟹ |Sf n| = |(ResW1 n).re| ≤ ‖RectInt‖ + ‖Σ‖ (sf_eq_resW1 + abs_re_le_norm + norm_sub_le). Sz = zeroBothWindow ∪ {−2} with the full ↔ characterization (backward: zetaA s = 0 ∧ inside ⟹ classification, with −2n inside ⟹ m = 1).
• §2 zeroSum_norm_le_four_FAlt_add_one (hRH) (hZCG) (hNLZ): the bridge — zeroTerm_norm_le_two (|ρ| = |1−ρ| at re = 1/2 via normSq, hence |1−(ρ/(ρ−1))ⁿ| ≤ 2·mult), zeroSum_nontriv_norm_le (norm_sum_le
• per-term), zeroBothWindow_sum_eq_two_mul (both-signs = 2× one-sign: NoLowZeros ⟹ im ≠ 0; the conj-image reindex with zeroMult_conj; Finset.image PLAIN-function + Set.InjOn form in this Mathlib), trivTerm_norm_le_one (zeroMult_neg_two + |1−(2/3)ⁿ| ≤ 1) ⟹ ‖Σ‖ ≤ 4·FAlt T + 1.

Closure: LiAssembly root-imported; full build GREEN (8772 jobs); AuditSession038d.lean + audit-session038d-axioms.txt — 12 decls, ALL 3 standard axioms only, 0 sorryAx; both perimeter Props printed verbatim.

Banked gotchas (ii′-6-b)

• The RectangleBorder rcases trap: rcases hs with hb | hb | hb | hb on a RectangleBorder membership CASES the singleton-Eq inside the ×ℂ pieces ("dependent elimination failed ... at case Eq.refl" — the sides are non-defeq by design). ROUTE THAT WORKS: rw [RectangleBorder]
• simp only [Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff] at hs + tauto to a flat 4-way Eq-disjunction, then rcases THAT (Eqs stay as hypotheses).
• Finset.image in this Mathlib takes a PLAIN function + Set.InjOn (Finset.sum_image signature), NOT an embedding (the ⟨f, inj⟩ anonymous constructor errors "not an inductive type").
• set x := toFinset breaks mem_toFinset rewrite patterns (the goal keeps the local variable; rw [hX] at the goal first or avoid set). Finset-ext goals use the SetLike coe (displays as the set); Set.Finite.mem_toFinset rewrites need the Finset-membership form — simp only [mem_toFinset] is more robust than rw.
• ne_of_gt/ne_of_lt directions: ne_of_gt (b < a) : a ≠ b — for 0 ≠ −T use ne_of_lt (−T < 0)?? NO — use by linarith : (0:ℝ) ≠ -T (linarith proves ≠ directly, no direction bugs).
• rw [hre] at hnt FAILS on IsNontrivialZero (structure opacity) — use the projections: hre ▸ hnt.2.1.
• sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _) |>.mp h : ‖a‖ = ‖b‖ for the |ρ| = |1−ρ| equality at re = 1/2 (normSq expansion + simp only [sub_re, one_re, sub_im] + rw [hre] AFTER the simp, then ring).
• pow_le_one₀ (h1 : 0 ≤ a) (h2 : a ≤ 1) : a ^ n ≤ 1 — n IMPLICIT (don't pass it; ascribe).
• Finset.sum_union takes a Disjoint proof (build via Finset.disjoint_left for the singleton).
• riemannZeta_neg_two_mul (hn : 1 ≤ n) : riemannZeta (-2·n) = 0 (LiFEntire) + zeroMult_neg_two : zeroMult (-2) = 1 (LiContour).

Files (ii′-6-b)

• research/lean/NguyenRH1/NguyenRH1/LiContour.lean (perimeter Props + wide pigeonhole)
• research/lean/NguyenRH1/NguyenRH1/LiAssembly.lean (NEW, ~460 lines)
• research/lean/NguyenRH1/NguyenRH1.lean (LiAssembly root-imported)
• research/lean/NguyenRH1/AuditSession038d.lean + audit-session038d-axioms.txt

Next

ii′-6-c (D-071 §4.4, the long pole): the four side bounds — I_III (left vertical: kFun_norm_le_two × [tight R-bound + (2/3)·Z2 near + MZeroProp short piece]), I_II/I_IV (horizontals: the segment-integral machine — per-zero ∫ dx/|w−ρ| ≤ 2·log(16.5/c) via asinh, the extended pigeonhole's clearance, Z2 count, 5.5·(10.5 log + 48) R-part, the Dirichlet stepping tail 3.3), I_I (right vertical: Dirichlet stepping 2^{−(σ₁−2)}·dirichletC2 × kFun_shift ≤ e^{√n/2}+1 ⟹ IIMaj), triv (done in §2). Then ii′-6-d (the fold ⟹ sfBoundProp).

FINDING F-D (session end — user paused to think) — the (6.12) stepping is broken

While designing ii′-6-c (the horizontal side bounds), a fold analysis uncovered a broken stepping argument in Lagarias's Thm 6.1 proof ((6.12)): the claim that |k_n(s)·L′/L(s)| "decreases geometrically" per unit step right from σ = 3 is false at T = √n — the per-step product ratio is e/2 ≈ 1.36 > 1 (zeta halves, kernel ratio ≤ e), so the product GROWS from σ = 3 to σ ≈ 0.36√n, peaking at ~e^{0.066√n}. Direct numeric confirmation (E-031, ALL CHECKS PASS): the right-tail envelope integral is ~5.9×10¹⁰ at n = 10⁵ (peak 1.6×10⁹ at σ = 111); |k_n(100+317i)| = 4.4×10³⁹ and |ζ′/ζ(101+317i)| ≈ 1.8×10⁻³¹ measured directly. D-036/D-037/R-004 inherit the bug verbatim (the right-tail charge "3.3" is off by ~10⁷×); the honest B(n) collapses for n ≳ 3×10⁴ (margin negative).

What survives: the theorem statement (λ_n > 0, verified to 5×10⁵; measured |Sf| ~ 13; the closed contour identity is exact — the sides cancel by conjugation + phase winding), and ALL Lean work to date (the bug is in the horizontal piece ii′-6-c, not yet built). Repair path (R) verified numerically: T = c√n with c > 1.2012 (kernel ratio ≤ e^{1/c²} < 2 ⟹ the stepping works; monotone decrease confirmed at c = 1.5 and c = 2). Costs: N₁ → (T₀/c)² (2.25×10²⁴ at c = 2, 4×10²⁴ at c = 1.5), bridge ~c×, I_III length doubles, horizontal kernel charge drops (e^{4/c²}+1). Literature: no erratum found (arXiv v4 notes, web search) — possibly undocumented.

D-072 filed (the full finding: claim, mechanism, evidence, inheritance, survival, repair path, literature status, open questions). User decision: pause here and think. The session ends at a clean, committed, resumable boundary with the direction OPEN (repair vs oscillation-salvage vs deeper literature check vs pause).