D-064 — Tier ii′ design: closing SfBoundProp in Lean

Date: 2026-08-21 | Session: 014 | Task: 5.1 tier ii′ sub-stage 0 (design + skeleton) Status: design COMPLETE (route decisions + lemma graph); two design-level discoveries (§1, §2) that reshape the whole tier; numerically verified identity chain (§3, all checks against E-015/E-021 certified data).

Origin: user directive 2026-08-21 — option (a): do tier ii′ BEFORE submission, with Paper A frozen/submittable at all times. Freeze protocol: no edits to paperA.tex/paperB.tex/draft.tex/references.bib until ii′-7; no edits to existing Lean proofs except the §1 correctness fix (flagged).

1. DISCOVERY 1 — the liCoeff encoding is defective (must fix first)

LiSkeleton.lean:39 defines

liCoeff n := tsum fun ρ : {ρ // IsNontrivialZero ρ} =>
               (zeroMult ρ : ℂ) * (1 - (1 - 1/ρ)^n)

The summand is ~ n/|γ| for |γ| ≫ n (for ANY zero: 1−1/ρ = 1+i/γ+O(γ⁻²), so 1−(1−1/ρ)ⁿ ≈ −n·i/γ to first order). Since Σ_ρ mult/|ρ| = ∞ (consequence of RvM, proved in Zeta23 as riemannVonMangoldt), the family is NOT Summable for any n ≥ 1 — hence tsum evaluates to the junk value 0. Consequences:

• LiVerifiedUpTo N (0 < (liCoeff n).re) is false under this def;
• SfBoundProp is false under this def (e.g. at n = 10⁵: |Sf| = SInfty + 1 ≥ 432 501 > 347 000 ≥ Bn, using the certified LiBasePoints bounds);
• lambda_pos_finite_height_verified is therefore vacuously true — logically valid, but its two hypotheses are unfulfillable. The paper's mathematics (D-037 chain) is untouched; this is purely a Lean-encoding defect, invisible to the session-013 audit (which checks axioms, not hypothesis truth). Found by the ii′-0 inventory.

Fix (design). Replace by the paired (absolutely summable) form — which is also the classical definition (Bombieri–Lagarias sum by symmetric pairs):

liCoeff n := ∑' ρ : {ρ // IsNontrivialZero ρ},
               (zeroMult ρ : ℂ)/2 * (f ρ + f (star ρ))    -- f ρ = 1−(1−1/ρ)ⁿ

• Real-valued summand (½(f ρ + conj(f ρ)) = Re f ρ), so .re downstream is cosmetic; no no-real-zeros lemma needed (the symmetrized form is correct regardless).
• Summability: |pair| = |2 − wⁿ − w̄ⁿ| ≤ C(n)·mult/|ρ|² for |ρ| ≥ 2n (w = 1−1/ρ; |wⁿ−1−n(w−1)| ≤ n²|w−1|²·e^{n/|ρ|}, and 2Re(w−1) = −2σ/|ρ|² ≤ 2/|ρ|²), then comparison with Zeta23's WeilEF.zero_sum_inv_sq (Σ mult/(1+‖γ_ρ‖²) < ∞, proved, axiom-clean (session-014 live check: 3 standard axioms only); mult/|ρ|² ≤ 4·mult/(1+‖γ_ρ‖²) for |ρ| ≥ 1 since re ∈ (0,1)).
• Conjugation invariance of the zero set with mult: needs riemannZeta (conj s) = conj (riemannZeta s) + mult preservation — check Mathlib for the conj lemma (Zeta23 has zeta_reflect_zero/ zeta_mult_reflect for reflect ρ = 1−ρ̄; the conj half to inventory).

Priority: FIRST executable sub-stage (ii′-1a). Small, isolated, recompiles the whole package unchanged downstream (liCoeff is only used abstractly in hypotheses). Makes LiVerifiedUpTo/SfBoundProp true statements; the session-012 theorems go from vacuous to meaningful.

2. DISCOVERY 2 — the crux identity: S_f(n) = Res₁(n) EXACTLY

(and the assembly is tail-free)

Settling the D-036/D-037 identity bookkeeping against the primary source (Lagarias math/0404394 §4–6, archived PDF) produced the exact chain — and it is simpler than D-062 feared.

Notation. c_k = Laurent coefficients of −ζ′/ζ at s = 1: −ζ′/ζ(1+u) = u⁻¹ + c₀ + c₁u + …; Res₁(n) := Σ_{j=1}^n C(n,j)·c_{j−1} (the residue at w = 1 of the Lagarias-kernel integrand J(w) = k_n(w−1)(−ζ′/ζ(w)), k_n(s) = (1+1/s)ⁿ−1 — pole of order n+1).

The crux identity. Sf(n) := S_∞(n) + 1 − λ_n = Res₁(n) for all n ≥ 1. Proof content: sum Lagarias's (4.10) [τ_j = η_j + (−1)ʲσ_{j+1} − (−1)ʲδ] against C(n,j); the σ_j = Σ_ρ ρ⁻ʲ are the zero power sums (paired), τ_j the archimedean coefficients (digamma/Hurwitz values), η_j = c_j. Binomial bookkeeping (verified in §3): S_∞ + 1 − λ_n = Σ_j C(n,j)[τ_{j−1} + (−1)ʲσ_j] + 1 = Σ_j C(n,j)[c_{j−1} + (−1)ʲ] + 1 = Res₁(n) + (−1) + 1. So the BL decomposition λ_n = S_∞ − S_f + 1 IS the binomial assembly of the Laurent-coefficient identity (4.10) — which is itself the coefficient-wise reading of the Hadamard product of ξ vs its Γ·ζ decomposition.

Residue theorem (exact, finite T). For T zero-avoiding in [√n, √n+1], rectangle σ ∈ [−5/2, 2√n], |Im| ≤ T: sides(T) := (1/2πi)∮ J = λ_n(T) + triv(n) + Res₁(n) where λ_n(T) = Σ_{|γ|<T} mult·[1−(1−1/ρ)ⁿ] (finite reindexing of the reflected residues via ρ ↦ 1−ρ, exact), triv(n) = 1−(2/3)ⁿ (the trivial zero at −2; only one inside).

The bound (tail-free). Solving for Res₁ and using the crux: |Sf(n)| ≤ |λ_n(T)| + |sides(T)| + |triv(n)| ≤ 2N(T) [bridge, hRH: |1−1/ρ| = 1 on the line ⟹ each ≤ 2] + [I_I..I_IV pieces, D-036/D-037] + 1 = B(n). NO tail term appears anywhere — D-037's B(n) has none, and now we know why: the identity lives at a single finite T; the full zero sum enters only through the crux identity (BL decomposition), not through the contour.

3. Numeric verification of the identity chain (this session, dps 40–50)

Also verified: D-037's line-63 compressed identity (S_f = −λ_n(T) + sides + triv(−2)) is correct ONLY when read as Sf = Res₁ = sides − λ_n(T) − triv with triv(−2) = −triv; the archive file itself should get an erratum pointer to this file (ii′-7 housekeeping).

4. Route decisions

R1 (LIFT-α): higher-order residue machinery — BUILD, bounded

The vendored RectangleIntegral'_eq_sumResiduesIn (FromPNTPlus, axiom- clean) carries the HasSimplePolesOn scaffold (placeholder residue valid only for simple poles). Our integrand J has simple poles at zeros and an order-(n+1) pole at w = 1. Plan:

• Define gresidue f p for finite-order poles via the meromorphic normal form (Mathlib MeromorphicAt/meromorphicOrderAt/ toMeromorphicNFAt): if order = −m, residue = (m−1)-th Taylor coefficient of the NF analytic part / (m−1)!.
• Prove the rectangle residue theorem for finite-order poles by principal-part decomposition: subtract Σ_p Σ_{j=1}^{m_p} c_{p,j}/(s−p)^j; j ≥ 2 terms integrate to 0 (global primitive); j = 1 terms via the vendored simple-pole theorem.
• Residue computations: zeros via vendored logDerivResidue family; w = 1 by the Leibniz computation (verified algebraically this session): with h(w) = (w−1)(−ζ′/ζ) analytic, h(1) = 1: (w−1)^{n+1}J = [wⁿ − (w−1)ⁿ]h(w), hence Res = (1/n!)(d/dw)ⁿ{[wⁿ−(w−1)ⁿ]h(w)}|₁ = Σ_{j=1}^n C(n,j)·h⁽ʲ⁾(1)/j! = Σ_j C(n,j)c_{j−1} = Res₁(n). Leibniz-rule formalization over iteratedDeriv — mechanical. Est. 1–2 sessions.

R2 (LIFT-β): the crux identity Sf = Res₁ — via (4.10); two candidate routes, decide at skeleton time

Needed components: (i) λ_n = Σ_j (−1)^{j+1}C(n,j)σ_j — binomial expansion of the summand

+ swap finite j-sum with paired zero sum (pair bound + zero_sum_inv_sq
comparison; j = 1 term needs the paired form — same machinery as the
§1 fix). ELEMENTARY-side.

(ii) S_∞(n) = Σ_j C(n,j)τ_{j−1} — identity between the Lean SInfty odd-m tsum and the binomial/τ form (Lagarias (4.11) ↔ (4.7) via digamma partial fractions (4.19)–(4.22); the double-sum swap is D-037 §3's absolute-convergence argument). ELEMENTARY-side (tier-(i)-class). (iii) (4.10) itself: τ_j = c_j + (−1)ʲσ_{j+1} − (−1)ʲ for all j ≥ 0. THE analytic heart. Two candidate routes: - (β1) Hadamard product of ξ. log ξ(s) = A + Bs − Σ_{k≥2} σ_k s^k/k near s = 0 (product over zeros; convergence from the perimeter zero count), differentiate, compare with ξ = π^{-s/2}Γ(s/2)·s(s−1)·ζ(s)/2-style decomposition. Mathlib has NO Weierstrass/Hadamard factorization; would be built from MeromorphicOn.extract_zeros_poles (FactorizedRational) + the order-1 estimate. Heavy but self-contained. - (β2) Reuse zeta-23-lean's proved explicit formula (EF_lit_zeta, axiom-clean per D-061 live audit). The σ_j are moments of the zero measure; (4.10) is a moment identity — an EF instance with coefficient-extracting test functions. The WeilEF/Contour.lean "weighted argument principle" may already contain a directly reusable Laurent/moment form. INVESTIGATE FIRST (1–2 days of reading); fallback (β1). Sanity gate (must hold in either route): the j = 0 case is the classical Σ 1/ρ = 1 + γ/2 − ½ log 4π (verified to 15 digits). Est. 2–4 sessions depending on route.

R3 (LIFT-γ): the R-bound (D-056, A = 10.5, B₀ = 48) — LOCAL route (no Hadamard)

D-056's proof uses partial fractions, but the same bound is provable by the Davenport-Ch.-15 local route, for which the machinery EXISTS: Mathlib Complex.borelCaratheodory, MeromorphicOn.circleAverage_log_norm (Jensen), and FromPNTPlus StrongPNTPrefix (BorelCaratheodoryDeriv, LogOfAnalyticFunction, Blaschke factors, ZerosBound). Sketch: on a disc around s₀ = 2+it of radius ~ 9/2, log ζ bounded via Borel– Carathéodory from |ζ| bounds (ZetaBounds' ZetaUpperBnd + functional- equation polynomial bound in the strip — the FE polynomial bound to be built from Mathlib riemannZeta_one_sub + Stirling bounds for Γ); zero extraction by Blaschke/Jensen with the perimeter C₀ count; Cauchy estimate for the derivative; digamma terms via Mathlib Complex.digamma (Lemma D already proved pen-and-paper in D-056 §1 — formalize the Binet bound or re-derive via the local route). Fallback if (β1) is built anyway: reuse the Hadamard partial fractions. Est. 2–3 sessions.

R4: the w=1 residue = Res₁ identification with S_∞ — RESOLVED by Discovery 2

No separate S_∞ ↔ Laurent identification is needed: the crux identity (§2) IS that identification, and it factors through (4.10) (R2) plus the elementary swaps (i)/(ii). This KILLS the sub-task D-062 feared most (the variable-order pole meeting the archimedean sum): the pole computation (R1) and the archimedean meeting (R2) are now separate, each bounded.

R5: perimeter — unchanged (D-062 §4)

Trudgian 2014 N(T)/S(T) (FAlt majorant already in Lean), Platt– Trudgian RHUpTo, LiVerifiedUpTo, M₀ (L6; E-023b acb optional).

5. Lemma dependency graph (skeleton blueprint)

Module: NguyenRH1/LiContour.lean (+ LiResidue.lean for R1 machinery, LiCrux.lean for R2, LiRBound.lean for R3).

[perimeter] RHUpTo, LiVerifiedUpTo, TrudgianN (FAlt form, named hyp)
[§1 fix]    liCoeff (paired) + liCoeff_summable            — ii′-1a
[R1]        gresidue + rect residue theorem (finite order)  — ii′-1b
[R1]        Res_zero (logDerivResidue reuse), Res_w1 (Leibniz)
[R2(i)]     lambda_eq_binom_sigma  (λ_n = Σ(−1)^{j+1}C(n,j)σ_j)
[R2(ii)]    sInfty_eq_binom_tau    (S_∞ = Σ C(n,j)τ_{j−1})
[R2(iii)]   laurent_relation_410   (τ_j = c_j + (−1)ʲσ_{j+1} − (−1)ʲ)
[R2]        CRUX: Sf n = Res1 n                             — ii′-2/3
[L3]        exists_zero_avoiding_T (pigeonhole on C₀/FAlt)  — ii′-4
[L1]        kernel bounds |k_n| ≤ 2, e⁴+1, e^{√n/2}+1      — ii′-4
[R3]        R_bound (D-056 constants)                       — ii′-5
[L6/perim]  M₀ ≤ 1.3352 (hypothesis-of-record; E-023b later)
[L0]        sides_identity: sides(T) = λ_n(T)+triv+Res₁    — ii′-6
[bridge]    |λ_n(T)| ≤ 2·FAlt(T) via hRH                    — ii′-6
[assemble]  |Sf n| ≤ Bn FAlt n  on [10⁵, N₁]                — ii′-6
[close]     theorem sfBoundProp : SfBoundProp               — ii′-7
            theorem lambda_pos_finite_height_closed
              := lambda_pos_finite_height_verified hRH hfinite sfBoundProp
            axiom audit (target: 3 standard + 0 sorryAx in Li chain)
            paper Appendix B + tag upgrade (D-062 §4 endpoint form)

6. Revised sub-stage map (supersedes the coarse ii′-1..ii′-7)

Order: 1a → 1b → 2 → 3 → 4 → 5 → 6 → 7 (1b/4/5 are independent and may be reordered for variety; 3 is the long pole).

Total: ~9–16 sessions. Biggest risks: (a) (4.10) route β2 may not fit EF's test-function class cleanly → β1 fallback (Hadamard build, +1–2 sessions); (b) R-bound local route's FE polynomial bound in the strip may need a Phragmén–Lindelöf we don't have → bounded build from Hadamard three-lines (Mathlib HAS HadamardThreeLines); (c) gresidue API friction → fall back to direct "subtract principal part" per-pole arguments without a general residue def.

7. What success yields (restated)

R-004 tag: [Lean-verified modulo published explicit N(T)/S(T) bounds (Trudgian 2014) + computational certificates (Platt–Trudgian RH to 3×10¹²; Li verification to 5×10⁵; M₀ acb certificate)] — no named analytic hypothesis remains. Paper A changes ONLY in Appendix B (final form paragraph) + possibly one abstract sentence; everything else frozen (ii′-7, with a D-060-rule mini-audit of the edited lines).

8. Fallback integrity statement

If ii′ stalls at any point: Paper A stands exactly as committed at session 013 (submission-ready), with the §1 liCoeff fix committed separately as a correctness improvement (it makes the declared hypotheses TRUE, strengthening the paper's formal claim even with SfBoundProp still open). No state is worse than today's.