v0.16.0 — critical-strip ζ, the archimedean Γ′/Γ place, and Pos λ₂

Stage B — the heavy analytic mechanization. Pure Lean 4, no Mathlib, choice-free (#print axioms = {propext, Quot.sound}); all 1597 non-private proof-layer theorems audited; build green and the mechanized-honesty gate passes. RH stays OPEN — the crux liPositivityHolds/hodgeIndexHolds remain none.

(B) ζ(s) on the critical strip 0 < Re s < 1

Built the integration-free way, via the Dirichlet eta η(s) = Σ (−1)^{n−1} n⁻ˢ, which converges by bounded variation across the whole strip the raw ζ series cannot reach.

• Ceta / CetaW — η(s) on Re s > 0 as a genuine constructive ℂ (the Bishop limit of the reindexed paired partial sums; CetaW is concretely instantiable, with CetaW = η tied to the genuine partial sums czEtaSum and shown witness-independent).
• CzetaStrip / CzetaStripW — ζ(s) = η(s) / (1 − 2^{1−s}), with the non-vanishing etaDenom_Pos_normSq (|1 − 2^{1−s}|² ≥ (2^{1−σ}−1)² > 0), the functional relation (1 − 2^{1−s})·ζ ≈ η, and uniqueness (etaDenom_cancel). The parts are ExactBoundedReal. Non-vacuity is witnessed on the critical line (s = ½).

(A) The Gamma function via Spouge — the archimedean Γ′/Γ place

• RrpowPos — the real power x^y = exp(y·log x) (so √(2π) = exp(½·log 2π); no sqrt primitive, no complex Clog), with the strongest positivity API (Pos_RrpowPos_of_base_ge_one).
• Digamma — the archimedean place ψ = Γ′/Γ as the exact constructive real −γ + Σ[1/(n+1) − 1/(n+z)] (and ψ(1) = −γ).
• SpougeGamma — Spouge's Γ-approximant, built only from exp/log/reciprocal of positive reals (error bound cited, not formalized).

(C) Pos λ₂

Rlambda2_pos — the second Li/Keiper coefficient is positive (λ₂ ≈ 0.0043 > 0), the higher-Stieltjes-γₙ → λₙ capstone; evidence for Li's criterion at n = 2, not the crux.

Honest scope (unchanged)

λₙ > 0 ∀ n (= RH), the off-critical-line zeros, and analyticity remain out of scope. RH stays open. See CHANGELOG.md and docs/v0160_peer_review.md.