v0.15.1 — exp∘log = id (the ζ-convergence gate)

The ζ-convergence gate exp∘log = id, via genuine power-series composition

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

Added

• exp(2·artanh τ) = (1+τ)/(1−τ) at the real level — Rexp_two_artanh_ofQ. The roadmap's research-grade base identity, built from scratch as a power-series composition (the elementary squeeze 1 + log x ≤ exp(log x) ≤ 1/(1−log x) never pins equality). Core: the composition corner bound exp_corner_le, the formal-ODE identity formal_exp_geom, the rational identity exp_artanh_rat_cleared, lifted to ℝ by the diagonal reconciliation Rexp_two_artanh_via.
• exp(log n) = n for the literal Rlog term — Rexp_log_nat_Rlog : RexpReal (Rlog (ofQ n) …) ≈ n, where Rlog (ofQ n) is the actual constructive logarithm 2·artanh((n−1)/(n+1)). The base construction is radius-general (the convergence radius enters only through the depth reindex, abstracted by Rexp_two_artanh_via), so it applies at Rlog's own radius ρ_M directly and Rlog (ofQ n) = TwoArtanhConst (tmap n) ρ_M by rfl. No τ²≤½ smallness needed.

Why it matters

Closes the discovered dependency of stage A: Σ n^{-s} converges because |n^{-s}| = n^{-Re s}, i.e. exp(log n) = n. The honesty gate is met (axiom-clean), so the ζ-complex tail (v0.15.2) need not ship its convergence as an interface.

See CHANGELOG.md and ROADMAP.md. Next (v0.15.2): real exponents nᶜ and Czeta for Re s > 1.