v0.14.0 — the first Li coefficient λ₁ as a positivity-certified constructive real (Pos λ₁; crux none, RH open)
v0.14.0 — Pos λ₁: the first Li/Keiper coefficient is positive, from first principles
Built in pure Lean 4 (Lean core + UOR-Foundation, no Mathlib, no sorry/native_decide, choice-free). This release builds the analytic constants of the Li/Keiper bridge and certifies that the first Li coefficient is positive.
Bright line (unchanged): λ₁ > 0 is the n = 1 slice of Li's criterion, realized as evidence — not the crux. It does not assert λₙ > 0 ∀ n (which is RH). liPositivityHolds = none, hodgeIndexHolds = none; RH stays open. The manifest binds this honestly: Pos Rlambda1 ∧ liPositivityHolds = none.
π as a constructive real (Pi.lean)
Rpi via Machin's π = 16·arctan(1/5) − 4·arctan(1/239) as one Bishop-regular diagonal. Lower bracket Rpi_lower (π ≥ 6/5) gives Pos Rpi; the tight Rpi_seq_ub_tight (π ≤ 3.142) comes from a one-sided alternating-arctan truncation (arctanSum_deep_le/arctanSum_deep_ge) at the tightest radius ρ = t.
log 2, log π, log 4π (GammaAccel.lean)
Clean 2·artanh((x−1)/(x+1)) logs Rlog2c, Rlogπc, with kernel-certified upper bounds Rlog2c_le (log 2 ≤ 0.6931) and Rlogπc_le (log π ≤ 1.1453). The varying π-argument is dominated by the constant 15/29 = tmap(22/7) (artSum_base_mono, since π ≤ 22/7), then truncated with an explicit geometric tail (artSum_le_value).
Euler–Mascheroni γ, convergence-accelerated (GammaAccel.lean)
Rgamma_h = the harmonic-telescoped γ = Σ(1/i − 2·artanh(1/(2i+1))), with the kernel-certified lower bracket Rgamma_h_lower (γ ≥ 0.54). This route is feasible where the alternating-ζ-series γ is not — that series carries the running lcm denominator (already ~7000 digits at depth 2), putting a positivity certificate out of computational reach.
Pos λ₁ (LambdaOne.lean)
Rlambda1 = ½·(2 + γ − log 4π) (Bombieri–Lagarias), with Rlambda1_pos : Pos Rlambda1 — λ₁ ≈ 0.0231 > 0. Proven through 2λ₁ = 2 + γ − log 4π (integer coefficients): 2λ₁ ≥ (2 + 0.54) − (2·0.6931 + 1.1453) = 0.0084 > 0. New ℝ-order bridges (Radd_le_add, Rneg_le, Rhalf/Rhalf_ge) carry the rational bounds through the ring operations.
Honesty gate
516/516 non-private proof-layer theorems #print axioms-audited; axiom-clean (choice-free {propext, Quot.sound}); CI green (build + mechanized-honesty audit).