v0.15.3 — von Mangoldt Λ + prime side; the Bombieri–Lagarias n=1 decomposition

von Mangoldt Λ, the explicit-formula prime side, and the Bombieri–Lagarias n = 1 decomposition

Pure Lean 4 (no Mathlib), choice-free ({propext, Quot.sound} only), no sorry/native_decide. 1215/1215 proof-layer theorems audited; the proof layer is warning-free. The crux stays none; RH is OPEN.

Added — the von Mangoldt function Λ (F1Square/Analysis/Mangoldt.lean)

• vonMangoldt n = log p when n = pᵏ is a prime power, else 0 — built with no primality predicate beyond the smallest factor spf n (least d ≥ 2 dividing n) and a prime-power test (strip spf to 1). Computable, so the defining values hold by reduction: Λ(1) = 0, Λ(2) = Λ(4) = Λ(8) = log 2, Λ(3) = Λ(9) = log 3, Λ(6) = 0; and Λ ≥ 0 everywhere (vonMangoldt_nonneg).
• spf is proved to be the least PRIME factor — spf_dvd (divides n), spf_two_le (≥ 2), spf_prime (only 1/itself divide it), via the fuel-sufficient search spec spfFrom_spec. So Λ is genuinely the von Mangoldt function, not a table matching at sampled points: vonMangoldt_prime gives Λ(p) = log p for every prime p.

Added — the explicit-formula prime side

• primeSide h N = Σ_{n=2}^N Λ(n)·h(log n) — the prime side Σ_p Σ_k log p · h(k·log p) reindexed through k·log p = log(pᵏ) = log n. A finite sum, hence a genuine constructive real with no convergence hypothesis; primeSide_stable proves it is constant past the support cutoff, so a compactly supported h gives a single well-defined real.

Added — the Bombieri–Lagarias decomposition of λ₁ (F1Square/Analysis/LiOne.lean)

• Rlambda1_decomposition : λ₁ ≈ λ₁^{arith} + λ₁^{∞} — the two-place split of the explicit formula:
  • Rlambda1_arith = γ — the finite/arithmetic place S_f(1) = −η₀ (the regularized von Mangoldt / prime-power contribution).
  • Rlambda1_arch = 1 − γ/2 − ½·log(4π) — the archimedean Gamma-factor place S_∞(1) (incl. the trivial-pole "1").
  • proved by reducing both λ₁ = ½·(2 + γ − log 4π) and arith + arch to the canonical form (1 + γ/2) − ½·log(4π) via the pointwise Rhalf distribution (Rhalf_Radd, Rhalf_Rneg, Rhalf_two) and γ − γ/2 ≈ γ/2 (Rhalf_double).
• Li.LiDecomposition is now realized non-trivially — li_decomposition_realized: a proven instance whose n = 1 slice is the genuine arithmetic/archimedean split, promoting the interface from the trivial inhabitant λ = λ + 0 (Li.liDecomposition_genuine).

Honest scope

Deriving the value S_f(1) = γ from the prime sum needs ζ'/ζ and its analytic continuation (v0.16.0+), so the Bombieri–Lagarias value is stated faithfully and not identified with the built primeSide — nothing is fabricated. None of this bears on positivity: liPositivityHolds = none (RH open) is untouched. Critical strip, zeros, and the genuine λₙ for n ≥ 2 remain deferred.

See CHANGELOG.md and ROADMAP.md. Next (v0.16.0, stage B): Γ via Spouge, the Euler–Maclaurin critical-strip ζ, and higher Stieltjes γₙ → λₙ values for n ≥ 2.