Dependencies: R-001, D-032, D-033, D-036, D-037, E-021, E-023, E-023b, Trudgian 2014, Platt-Trudgian 2021, Lagarias math/0404394, Bombieri-Lagarias 1999, Johansson 2015

R-004 — Explicit finite-height Li theorem: λ_n > 0 for all n ≤ (T₀−1)² = 8.999…×10²⁴

Date: 2026-08-19 | Session: 008 | Track: C (task 3.8) Tag: [PROVED-CONDITIONAL(computational RH-to-height-T₀; computational finite verification)] — R-bound FULLY TRACED 2026-08-19 (D-056, task 4.5a: reference-point method, A = 10.5, B₀ = 48 with the honest C₀ incl. log log term; digamma remainder 1.2/|w|² proved; E-028 verified, 26× slack); N₀ = 80 000 (1.25× overlap with Johansson's 10⁵ table). M₀ = 1.3352 interval-rigorous (E-023b acb box cover, session 043 — supersedes "grid-verified, E-023 S1"). Margin convexity: PROVED (D-057, task 4.5b; E-029 ALL CHECKS PASS). History: tag downgraded then restored same day (D-054 erratum: broken D-039/D-036-§1 proofs; repairs D-056–D-059). Lean closure (2026-08-26, session 041, tier ii′ COMPLETE): the analytic chain is now FULLY MACHINE-PROVED — LiSideBounds.sfBoundProp (the contour bound |S_f(n)| ≤ Bn FAlt n on [10⁵, N₁]) and LiClosed.lambda_pos_finite_height_closed (λ_n > 0 for all 1 ≤ n ≤ N₁) in Lean 4, from exactly SEVEN declared hypotheses: RHUpTo (Platt–Trudgian), LiVerifiedUpTo(10⁵) (finite Li verification: E-011/E-015 to 3000 + Johansson 2015 § 4.2, rigorous interval-arithmetic ordinary-λ_n table to 10⁵), ZeroCountProp/ZeroCountProp2/ ZeroCountGlobalProp (Trudgian N(T)/S(T) forms), NoLowZeros (Platt-class zero-location), MZeroProp (M₀ interval certificate). Axiom audit on the full chain: [propext, Classical.choice, Quot.sound] only, 0 sorryAx. The B(n) account was corrected in four places during the closure (F-A/F-B/F-D/F-E — see the D-037 erratum block and Paper A §3 Step-2 footnote); the theorem statement is unchanged. Certificate correction (2026-08-26, session 042, user review): the finite-verification citation Misguich–Voros (Voros 2020, Exp. Math. 29(4)) was found to carry a DEFORMED sequence Λ_n (Misguich, private communication), not the ordinary λ_n — it has been replaced by Johansson 2015 § 4.2 (rigorous, published, ordinary Keiper–Li coefficients to n = 10⁵, all positive) and the Lean perimeter LiVerifiedUpTo reduced from (5·10⁵) to (10⁵) to match the checkable evidence (commit 79c96f2; the assembly's hfinite branch uses exactly n < 10⁵, so nothing else changes). Alignment pass (2026-08-29, vs the frozen Paper A): margin base value corrected to the final certified ≥ 4 001 (item 5 below); overlap margin corrected 6.25× → 1.25× (Adversarial review); novelty claim hedged with the Oesterlé precursor (Statement); M₀ status updated (above); paper pointer moved draft.tex → paperA.tex (Paper section). The theorem statement and tag are untouched.

Statement

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

λ_n > 0 for every 1 ≤ n ≤ N₁ := (T₀−1)² = 8 999 999 999 994 000 000 000 001 ≈ 9.0×10²⁴.

Conservative variant (using Lagarias's printed bridge window (1.16) instead of the traced proof): N₁* = T₀²/(4 log²T₀) = 2.726×10²¹.

We have found no previous assembled EXPLICIT finite-height Li bound: the chain "RH to height T₀ + fully traced constants ⟹ λ_n > 0 to n ~ T₀²" existed only with untraced O-constants (Lagarias math/0404394 Thm 1.1/(1.16)). Statement-level precursor: Oesterlé 2000 (unpublished, prop. 2 — RH-to-T₀ ⟹ λ_n ≥ 0 for n ≤ T₀², cited in Voros 2020); published weaker window: Lagarias 2007. By Voros's sharpening, no statement of the form "λ_n > 0 ∀n ≥ N₀" is possible short of RH — this finite-height theorem is the maximal content of the Li route (D-032/D-033).

Proof / Derivation

Full assembly: D-037 (derivation), support computation E-023 (ALL CHECKS PASS). Skeleton:

λ_n = S_∞(n) − S_f(n) + 1 (Bombieri–Lagarias Thm 2).
Archimedean: S_∞(n) ≥ ½n log n + (C₁−γ/2)n − 4 for n ≥ 20, C₁ = (γ−1−log 2π)/2 — elementary from Lagarias (4.11) via finite differences + explicit harmonic bounds; validated against E-021's exact S_∞ to n = 5000 (E-023 V1, min slack 9.52).
Finite: |S_f(n)| ≤ B(n) (D-037 (4.1)) — Lagarias Thm 6.1 contour with all constants traced (Trudgian N(T)/S(T); kernel e⁴+1; R-bound A = 10.5, B₀ = 48 traced (D-056, reference-point method) / 0.9, 1.0 measured; short-segment max M₀ = 1.3352 closing the D-036 |t|<10 gap).
Bridge (CORRECTED ii′-6, F-A): RH to height √n+1 ⟹ each zero contributes ≤ 2 ⟹ |λ_n(T)| ≤ 4F(T) (both signs of γ; F the global Trudgian majorant); holds for n ≤ (T₀−1)².
margin(n) := S_∞^lower − B + 1 is convex for n ≥ 20 (PROVED D-057; E-029), margin(8×10⁴) ≥ 4 001 > 0 (Lean-certified base point) with positive derivative ⟹ margin(n) > 0 for all n ∈ [8×10⁴, N₁] (margin(N₁) = 2.458×10²⁶). [Margin trail: 16 020 (E-028, pre-correction) → 15 764 → ≥ 8 001 certified (session 012) → ≥ 4 001 certified (ii′-6-a2, the honest B(n) after F-A/F-B/F-E).]
Finite verification (CORRECTED session 042): n ≤ 3000 (E-011/E-015, cross-validated, ledger #3) ∪ n ≤ 10⁵ (Johansson 2015 § 4.2, rigorous interval-arithmetic ordinary-λ_n table, all positive) — covers N₀ = 8×10⁴ by a factor 1.25 and meets the n = 10⁵ split exactly. [Supersedes: "n ≤ 5×10⁵ (Misguich–Voros)" — that source verifies a deformed sequence, not the ordinary λ_n.]

Dependencies

R-001 (finite verification), D-032/D-033 (design + wall), D-036 (contour constants), D-037 (assembly), E-021 (exact S_∞/measured constants), E-023 (assembly numerics), E-023b (M₀ interval certificate), Trudgian 2014 [PROVED lit], Platt–Trudgian 2021 [computational], Lagarias math/0404394, Bombieri–Lagarias 1999, Johansson 2015 (Numer. Algor. 69:253–270, § 4.2) [finite verification].

Adversarial review

D-037 §7: full input inventory P1–P6 (proved/elementary) vs H1–H5 (computational/heuristic). Update (session 009 repairs): H2 (digamma sub-bound) is now PROVED (D-056: |r| ≤ 1.2/|w|², Binet split + max-modulus majorant). Update (session 043): H3 (M₀ = 1.3352) is now interval-rigorous (E-023b, acb box cover) — NO grid-verified constant links remain. The theorem's sensitivity to M₀ is negligible — it enters a sub-dominant additive constant; even 5× worse moves N₀ by ~15 %, irrelevant against the 1.25× overlap margin (Johansson 10⁵ vs N₀ = 8×10⁴). Sanity gates: no claim beyond N₁ (Voros wall respected); no D-H/Epstein analogue claimed. Honest scope: this is NOT progress on "λ_n > 0 ∀ large n" (⟺ RH).

Paper section