v0.10.0 — λₙ/RH proof boundary; ζ and λₙ as exact-bounded objects

v0.10.0 — the λₙ / RH proof boundary, and ζ as an exact-bounded object

This release pins the analytic face of the RH crux and ships ζ as a genuine exact-bounded constructive real, before building the remaining transcendentals.

The proof boundary — F1Square/Li.lean

By Li's criterion (Li 1997), RH ⟺ λₙ > 0 ∀ n ≥ 1 (the non-strict ≥ 0 form is the general Bombieri–Lagarias 1999 multiset criterion). LiPositive/LiNonneg are genuine, satisfiable properties (template_liPositive); the crux LiCrux λ on the unconstructed genuine ζ-derived λ is OPEN (liPositivityHolds := none) — guarded by a detailed faithfulness caution (no ∃-witness, no manifestly-positive definition, no finite/truncated decide) and the finite-check guard liPositive_iff_all_upTo (LiPositive = ⋀ all finite truncations, so the numerical positivity of the first ~10⁵ λₙ is not a proof). The Bombieri–Lagarias decomposition and Weil explicit formula (Weil 1952 / Connes 1999) are honest interfaces; λₙ^arith and λₙ^∞ have opposite signs, so positivity is a cancellation — the open difficulty.

ζ and λₙ as exact-bounded objects

• F1Square/Analysis/ExactBounded.lean — ExactBoundedReal: a constructive real as a stream of certified rational enclosures of exact width 2/(n+1). λₙ is typed Nat → ExactBoundedReal.
• F1Square/Analysis/Zeta.lean — ζ(s) = Σ 1/iˢ for integer s ≥ 2 as a genuine exact-bounded real (npow from scratch), with the rigorous rational tail bound S(b) − S(a) ≤ 1/(a+1) via the telescoping decreasing U(N) := S(N) + 1/(N+1); the bound is already the Bishop modulus, so the partial sums are directly regular. zeta_pos: ζ(s) > 0.

Honest scope

ζ here is the convergent regime Re(s) > 1 — no zeros, not the critical strip. The analytic continuation and the genuine λₙ values (needing it and log) are deferred; only the exact-bounded type and the boundary are shipped — nothing fabricated. Both crux faces stay none (geometric hodgeIndexHolds, analytic liPositivityHolds).

Quality

Two adversarial peer reviews (faithfulness + Lean soundness) returned zero CRITICAL, zero MAJOR. The honesty gate is hardened to also fail on duplicate proof-layer theorem short-names (so leaf-name coverage matching can never mask an audit gap). Pure Lean 4, no Mathlib, no sorry; axiom-clean and choice-free; coverage 279/279; CI machine-verified green.

RH remains open (June 2026); no 𝔽₁-square construction exists — Connes–Consani arXiv:2602.15941 is a Jacobian/adele-class-space construction, not the square. The crux is never asserted.

🤖 Generated with Claude Code