Current task: —

Updated 08-26-2026

D-037 — Task 3.8: the explicit finite-height Li theorem — full assembly

Date: 2026-08-19 | Session: 008 | Task: 3.8 Status: complete (assembly + adversarial review). Result filed as R-004. Support computation: E-023 (ALL CHECKS PASS).

ERRATUM BLOCK (2026-08-26, session 041, tier ii′-7 closure). The B(n) account in this file is SUPERSEDED in exactly four places by the Lean-closed form; the theorem (N₁, positivity) is unchanged and is now FULLY MACHINE-PROVED (NguyenRH1 LiSideBounds.sfBoundProp + LiClosed.lambda_pos_finite_height_closed; axiom-audited on the full chain: the 3 standard axioms only, 0 sorryAx). The four corrections (all found during the machine closure; D-071/D-072/D-074 with E-031/E-032/E-034): - F-A (both-signs factor-2, D-071 §1): the bridge |λ_n(T)| ≤ 2N(T) under-counts by a factor 2 — the residue sum runs over BOTH signs of γ while N(T) counts one sign. Honest charge: 4F(T) (the global Trudgian majorant). Theorem unaffected. - F-B (two-unit count, D-071 §1 = D-069 Finding 2): the I_III near-sum window |γ−t| ≤ 1 spans TWO unit intervals — the honest count is (2/3)·Z₂(T) (the two-unit Trudgian form), not (2/3)·C₀(T). - F-D (the broken (6.12) stepping, D-072): Lagarias's Thm 6.1 right-tail stepping at T = √n has product ratio e/2 > 1 — the envelope GROWS like e^{0.066√n} (E-031: ~5.9×10¹⁰ at n = 10⁵); the charge "3.3" is off by ~10⁷× there and worsens. Repaired by the D-074 zero-free dog-leg at U = (3/2)√n (D-073's repaired stepping, q = e^{4/9}/2 < 1 certified); the dog-leg rectangle lies entirely in Re w ≥ 3 (zero-free UNCONDITIONALLY). T_cut = √n and the endpoint N₁ = (T₀−1)² are PRESERVED. (The per-side claim at T = √n is empirically TRUE by hidden cancellation — E-032, |I|/envelope down to 5.6×10⁻¹⁰ — parked as an open question, D-073 §8 D4.) - F-E (I_I kernel off-by-one, D-074 §9): the right-vertical kernel at re w = 2√n near t = 0 is e^{√n/2+1/8}, one eighth-power above the charged e^{√n/2}+1; charged honestly as e^{1/3}·IIMaj (uniform kernel e^{√n/2+1/3}+1, n ≥ 4), absorbed by the fold's free 2π normalization (e^{1/3} ≤ 1.4 ≤ 2π). The authoritative B(n) is the Lean Bn (LiSkeleton): 4F(T) + 4T[(2/3)Z₂(T) + 10.5 log(T+2) + 48] + 40·1.3352 + 2(e⁴+1)·7Ĥ(T) + 2·DogLegRight(n) + IIMaj(n) + 1, T = √n + 1. Paper A carries the same correction note (ii′-7c, footnote in §3 Step 2).

ERRATUM ADDENDUM (2026-08-26, session 042, user review — the fifth correction: the finite-verification certificate). This file's Step-5 citation "Misguich–Voros to 5×10⁵" is RETRACTED: Voros's 2020 paper (Exp. Math. 29(4):452–469) verifies a DEFORMED Keiper–Li sequence Λ_n (computed by G. Misguich, private communication 2017), NOT the ordinary λ_n, so the citation could not carry the finite splice. (User's instruction: check theorem-by-theorem before letting a citation carry the splice — confirmed against the paper's own text.) Replacement certificate: Johansson 2015 § 4.2 (Numer. Algor. 69:253–270) — rigorous interval-arithmetic computation of the ORDINARY Keiper–Li coefficients λ_0…λ_{100000}, all positive (λ_100000 certified to ~2900 digits; "shows agreement with Keiper's conjecture (and the Riemann hypothesis)") — covering the assembly's hfinite branch n < 10⁵ EXACTLY. The Lean perimeter LiVerifiedUpTo was reduced from (5·10⁵) to (10⁵) to match the checkable evidence (commit 79c96f2); the theorem and the overlap picture (N₀ = 8×10⁴ covered by 1.25×; the n = 10⁵ split met exactly) are unchanged. Related novelty note found during the same check: the finite-height STATEMENT has an unpublished precursor (Oesterlé 2000, prop. 2, cited in Voros 2020: RH-to-T₀ ⟹ λ_n ≥ 0 for n ≤ T₀²); the explicit, machine-verified assembly remains, to our knowledge, without a published predecessor.

1. Theorem (target of this file)

THEOREM (finite-height Li bound). Let λ_n = Σ′_ρ [1−(1−1/ρ)ⁿ] be the Li coefficients of ζ. Assume RH verified to height T₀ = 3×10¹² (Platt–Trudgian 2021, interval arithmetic). Then

λ_n > 0 for all 1 ≤ n ≤ N₁ := (T₀ − 1)² = 8 999 999 999 994 000 000 000 001.

Tag: [PROVED-CONDITIONAL(computational RH-to-height-T₀; computational finite verification; one numerically-verified sub-bound — see §7 H2)]. Under the more conservative window quoted by Lagarias (1.16), n ≤ T₀²/(4 log²T₀), the same chain gives N₁* = 2.726×10²¹ (§6).

2. The chain

λ_n = S_∞(n) − S_f(n) + 1 (Bombieri–Lagarias 1999, Thm 2) (2.1) ⟹ λ_n ≥ S_∞^lower(n) − B(n) + 1 =: margin(n)

with S_∞^lower the explicit archimedean lower bound (§3) and B(n) the explicit finite-part upper bound (§4). Positivity for n ≥ N₀ follows from margin > 0 (§5); n < N₀ by direct computation (§5 table).

3. Archimedean part: explicit S_∞ lower bound [PROVED, elementary]

Lagarias (4.11): S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j with a₁ = (log 4π + γ)/2, a_j = (1−2^{−j})ζ(j) = Σ_{m odd ≥ 1} m^{−j} (j ≥ 2). The double sum converges absolutely for j ≥ 2 (terms ~ C(n,2)/m²), so

S_∞(n) = (1−a₁)n − 1 + Σ_{m odd ≥ 3} h⁺(m), h⁺(m) := (1−1/m)ⁿ − 1 + n/m ≥ max(0, n/m − 1) (Bernoulli)

(dropping (1−1/m)ⁿ ≥ 0 for m ≤ n; h⁺ ≥ 0 for m > n). With K = ⌊(n−1)/2⌋ and Σ_{k=1}^K 1/(2k+1) = H_{2K+1} − ½H_K − 1, using the standard explicit harmonic bounds log M + γ + 1/(2M) − 1/(12M²) ≤ H_M ≤ log M + γ + 1/(2M):

Σ h⁺ ≥ n[½ log n + (log 2 + γ)/2 − 1 − 2/n] − n/2 (n ≥ 4)

Assembly (the γ and log 2 pieces combine to exactly C₁ − γ/2, C₁ = (γ−1−log 2π)/2 = −1.13033…):

S_∞(n) ≥ ½ n log n + (C₁ − γ/2) n − 4 for n ≥ 20 (3.1)

with C₁ − γ/2 = −1.41894…. E-023 V1: validated against E-021's EXACT S_∞ (dps-3300, itself validated 4.8e-25 vs E-015) for all 20 ≤ n ≤ 5000; min slack 9.52 at n = 20, growing ~ 0.29n (the truncation loss, since the true O(1) constant is c₀ = −1/4, E-021 V3). The bound is weak by (γ/2)n but that loss is irrelevant to N₀ (see §5).

4. Finite part: explicit |S_f| upper bound

Contour (variant B of Lagarias Thm 6.1's proof, D-036): rectangle σ₀ = −5/2, σ₁ = 2√n, Im = ±T, T ∈ [√n, √n+1] chosen zero-avoiding (pigeonhole: ≤ C₀(√n+1) zeros in the interval ⟹ gap center with d_min ≥ 1/(3C₀), D-036 §2). Integrand k_n(w−1)(−ζ′/ζ(w)), k_n(s) = (1+1/s)ⁿ − 1. Identity:

S_f(n) = Σ_{|γ|≤T}′ [1 − (ρ/(ρ−1))ⁿ]·(−1) + (1/2πi)(I_I+I_II+I_III+I_IV) + triv(−2)

Constants (all explicit): Trudgian 2014 Thm 1: N(T) = F(T) + S(T), F(T) = (T/2π)log(T/2πe) + 7/8, |S(T)| ≤ 0.137 log T + 0.443 log log T + 1.588 (T ≥ e) [PROVED lit]; C₀(t) := F(t+1)−F(t) + S_bnd(t+1) + S_bnd(t) (zeros in unit interval). R-bound (Lemma 6.1 for ζ, D-036 §1): for −5/2 ≤ σ ≤ 4, |t| ≥ 10, |R(w)| := |ζ′/ζ(w) − Σ_{|γ−t|<1} 1/(w−ρ)| ≤ A log(|t|+2) + B₀ with TRACED A = 2.0, B₀ = 2.0 (see §7 H2); E-021 measured A = 0.9, B₀ = 1.0 suffice (15 points, max |R| = 4.75).

Pieces (T = √n + 1 used for the bounds):

**B(n) := 2N(T) + 4T[(2/3)C₀(T) + A log(T+2) + B₀] + 40M₀

     + 2(e⁴+1)[7H(T) + 3.3] + I_I + 1**,  T = √n + 1     (4.1)

Leading behavior: B(n) ≈ 2.54√n log n + O(√n) + O(log²n) with the O(log²n) horizontals term dominant up to n ~ 10⁵ (2(e⁴+1)·21C₀² ≈ 1170 C₀²).

5. Margin, N₀, and the finite verification table

margin(n) = ½n log n + (C₁−γ/2)n − 4 − B(n) + 1.

Convexity. For n ≥ 20 every component of B(n) is concave in n (√n log n, √n·log, log²n, log n pieces: second derivatives < 0; the I_I term is < 10⁻³⁰ with |I_I″| comparably tiny), while (S_∞^lower)″ = 1/(2n) > 0. Hence margin is convex for n ≥ 20; with margin(N₀) > 0 and margin′(N₀) > 0, margin(n) > 0 for ALL n ≥ N₀. E-023 V2: convexity confirmed on a 4000-point log grid to N₁, contiguity on step-1 grid to 4×10⁵. (D-054 F4: the "every component concave" sentence is not a proof — products like 4T·f(T) need case analysis; grid-verified here, symbolic proof = task 4.5b.)

E-023 results (first-estimate constants A = 2.0, B₀ = 2.0):

E-028 results (2026-08-19, FULLY TRACED constants A = 10.5, B₀ = 48 from D-056 — supersede the 2.0/2.0 numbers above; honest C₀ incl. the log log term, D-036 §0 erratum):

Finite verification (n < N₀): | range | source | tag | |-------|--------|-----| | 1 ≤ n ≤ 3000 | E-011/E-015 (arithmetic side, dps 1450, cross-validated vs E-008 zero side and E-021 V1 4.8e-25); E-023 V3 reconfirmed | [NUMERICAL-VALIDATED] (ledger #3) | | 3000 < n ≤ 5×10⁵ | Misguich–Voros (Voros 1703.02844 reports λ_n > 0 computed to n = 5·10⁵; also Keiper to 7000, Maślanka to 3300) | [NUMERICAL literature] | | N₀ = 8×10⁴ ≤ n ≤ N₁ | margin bound, this file + E-028 (traced) | analytic |

Overlap: N₀ = 8×10⁴ < 5×10⁵ — contiguous coverage with 6.25× margin.

6. The bridge condition and N₁

The only use of RH: zeros with |γ| ≤ T = √n+1 must be exactly on the line (for |(ρ/(ρ−1))ⁿ| = 1). With RH verified to T₀ this requires √n + 1 ≤ T₀, i.e.

N₁ = (T₀ − 1)², T₀ = 3×10¹² (Platt–Trudgian 2021, arXiv:2004.09765) ⟹ N₁ = 8 999 999 999 994 000 000 000 001 ≈ 9.0×10²⁴.

The contour tail bounds (I_I…I_IV, R-bound, zero-avoidance) are UNCONDITIONAL (Trudgian + partial fractions + elementary kernel bounds); the window zeros |γ| ∈ (√n, T] contribute ≤ 2 each unconditionally (|(ρ−1)/ρ|²ⁿ ≤ (1+1/n)ⁿ ≤ e for |γ| ≥ √n, any β ∈ [0,1] — Lagarias's own bound after (6.7)).

Lagarias's printed bridge (1.16) states the weaker window n ≤ T²/(4 log²T). Our n ≤ (T−1)² follows his proof line by line (the 4 log²T slack is not in the argument; it appears only in his summary statement). Fallback if a reviewer insists on (1.16) as printed: N₁* = T₀²/(4 log²T₀) = 2.726×10²¹ — the theorem is robust either way.

7. Adversarial review (input inventory)

# Input Status
P1 λ_n = S_∞ − S_f + 1 (BL Thm 2) [PROVED] literature
P2 Trudgian N(T), S(T) bounds [PROVED] literature
P3 σ₂ = Σ|ρ|⁻² = 0.046191…, B = −0.0230955… exact, machine-verified (E-011/E-016c)
P4 kernel bounds (e⁴+1, ≤2, e^{√n/2}+1), stepping (6.12), trivial residue ≤ 1 elementary, re-derived D-036
P5 S_∞ lower bound (3.1) [PROVED] elementary (§3), E-023 V1 vs exact values
P6 convexity/contiguity of margin PROVED (D-057, 2026-08-19, task 4.5b): chain-rule reduction φ(T(n))″ = ψφ/(4n) + 11-block table with elementary sign arguments + I_I direct bound; majorant chain Ĉ₀ ≥ C₀ with margiñ(8×10⁴) = 16 020 > 0, margiñ′(8×10⁴) = 3.7 > 0. E-029 ALL CHECKS PASS (sympy table match, ψᵢ < 0 on [T₀, 3.1×10¹²], convex grid, majorant sanity)
H1 Platt–Trudgian RH to T₀ = 3×10¹² computational fact (interval arithmetic), accepted
H2 R-bound PROVED (D-056, 2026-08-19, task 4.5a): reference-point rewrite — |R(s)| ≤ 10.5 log(|t|+2) + 48 for σ ∈ [−5/2, 3], |t| ≥ 10, every piece traced with the honest C₀ (incl. log log term; Z₂ certified ≤ 0.5700; digamma remainder |r(w)| ≤ 1.2/|w|² proved via Binet split at t ~ |V|/2 + correct majorant recurrence estimate). E-028 V-R: holds at all 15 sample points with 26× slack. Supersedes the broken D-036 §1 / D-039 (D-054 errata F1–F3). With traced constants: N₀ = 75 451, adopted N₀ := 80 000 (E-028), overlap vs MV 6.25×, margin(N₁) = 2.458×10²⁶.
H3 M₀ ≤ 1.3352 on the short piece grid + sampled-Lipschitz ×2 (E-023 S1); upgrade: acb box cover. Insensitive: 40 M₀ = 53.4 enters B(n) as an additive constant.
H4 Misguich–Voros λ_n > 0 to 5×10⁵ [NUMERICAL] literature; overlapped 6.25× by N₀
H5 exact T₀: "3×10¹²" per Platt–Trudgian title/abstract; if the exact certified height is marginally different, N₁ changes by < 1 % confirm at write-up

Sanity gates. The argument uses only ζ-specific inputs (Trudgian bounds, Platt–Trudgian height) and does not claim anything for Davenport–Heilbronn/Epstein analogues — no gate violation. The theorem does NOT claim λ_n > 0 beyond N₁ (that would be RH, Voros — D-032 §2). No contradiction with the |S_f| ≤ 13.52 measurement (n ≤ 5000): the bound B(n) is worst-case and ~170× loose there (D-036 §6) — slack is expected, not a bug.

8. What this is and is not