v0.15.2 — ζ(s) = Σ n⁻ˢ for complex Re s > 1 (canonical, full-sequence convergence)

ζ(s) = Σ n⁻ˢ for complex s with Re s > 1, as a genuine constructive ℂ

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

Added — the Riemann zeta function for complex argument (F1Square/Analysis/ComplexZeta.lean)

• Czeta s — for any complex s with Re s ≥ 0 and a rational witness τ > 0 of Re s > 1 (τ ≤ (Re s − 1)·log 2, so the dyadic ratio 2^{1−Re s} < 1), ζ(s) = Σ_{n≥1} n⁻ˢ is a genuine constructive complex number — its real and imaginary parts are Bishop diagonal limits (Rlim) of the reindexed dyadic partial sums Σ_{n<2^{M(j)}} Re/Im(n⁻ˢ). This replaces the previous integer-only ζ (Σ 1/iˢ, s ≥ 2): convergence now holds across the full half-plane Re s > 1, with s genuinely complex.
• Convergence with a rate — Czeta_re/im_tendsTo: the partial sums converge to Re/Im ζ(s) with the canonical Bishop modulus 2/(k+1).

The dyadic-geometric convergence proof, from scratch

• exp injectivity → log-multiplicativity — RexpReal_inj, logN_mul, logN_pow_two (log(2ᵏ) = k·log 2), re-routing the artanh-addition boundary wall.
• dyadic block bound — czetaExp_block_geo: the [2ᵏ, 2ᵏ⁺¹) block modulus ≤ ofQ(rᵏ), r = 1/(1+τ) < 1.
• geometric tail — geoFrom_telescope, geoFrom_le (Σ rᵏ ≤ rʲ/(1−r)), czetaExp_tail.
• Bernoulli reindex — geom_reindex: the 1/(linear) decay qpow_geom_bound with quadratic index M(j) = (j+1)·r.den² collapses r^{M(j)}/(1−r) ≤ 1/(j+1).
• completeness bridge — seq_diff_le (real bound → same-index rational bound) and RReg_of_real_bound (pairwise real differences ≤ 1/(j+1)+1/(k+1) ⟹ a regular sequence of reals), feeding Bishop's Rlim.

Strengthened for peer review

• Non-vacuous — czeta_two_theta + a fully-closed ζ(2) = Σ 1/n² instance (the Re s > 1 hypothesis is satisfiable: τ = 1/2 ≤ log 2).
• Full-sequence convergence (not just the dyadic subsequence) — czetaRe/Im_cauchy_full: the whole partial-sum sequence is uniformly Cauchy (|S(N) − S(N')| ≤ 2/(j+1) for all N, N' ≥ 2^{M(j)}); czetaRe/Im_full_tendsTo (|S(N) − ζ(s)| ≤ 3/(k+1)). So Σ_{n=1}^N n⁻ˢ converges as a genuine series for every N.
• Canonical (witness-independent) — Czeta_re/im_canonical: any two witnesses τ₁, τ₂ give ≈-equal values (both are the limit of the same full sequence, via the real-level Archimedean Req_of_Rle_ofQ_all). So ζ(s) is a well-defined function of s alone on Re s > 1.

Honest scope

ζ ships in its convergent half-plane Re s > 1 (no zeros). The analytic continuation to the critical strip — where RH lives — is not built, and liPositivityHolds = none (RH open) is untouched.

See CHANGELOG.md and ROADMAP.md. Next (v0.15.3): von Mangoldt Λ and the n = 1 Bombieri–Lagarias decomposition.