v0.12.0 — ℝ as a constructive field with powers, and exp on ℝ

ℝ becomes a constructive field with powers, and exp is defined on all of ℝ — pure Lean 4 (no Mathlib), no sorry, axiom-clean (⊆ {propext, Classical.choice, Quot.sound}); coverage 341/341 enforced.

Field / powers

• Pow.lean — real powers Rpow (iterated Rmul), Rpow_one, Rpow_congr.
• Inv.lean — the reciprocal 1/x of a positive real via positivity-as-data (witness k with x_k > 1/(k+1); floor by L = δ/2, reindex R n = 4δ.den²(n+1)+2δ.den, full Bishop regularity), plus rational Qinv and division Rdiv.

exp on ℝ (ExpReal.lean)

The everywhere-defined real exponential as the diagonal of rational partial sums exp(x)_j = S_{R j}(x_{R j}). The diagonal sequence of rationals is itself Bishop-regular (|exp(x)_j − exp(x)_k| ≤ 1/(j+1)+1/(k+1)), so it is a constructive real directly — no completeness/Rlim needed. Three axiom-clean rational bounds on expSum make it rigorous:

• truncation expSum_trunc_bound — |S_q(b) − S_q(a)| ≤ 2Mᵃ⁺¹/(a+1)! (dominating M-series + telescoping tail + termwise domination);
• Lipschitz expSum_Lip_le + LipS_le_U — |S_q(N) − S_{q'}(N)| ≤ C·|q−q'|, C uniform in N;
• factorial growth fct_ge_geom + trunc_reindex — the factorial outpaces Mⁱ past 2M, converting the tail to a 1/(j+1) reindex.

Honesty

The crux stays none on both faces (Hodge index = geometric; λₙ > 0 ∀n = analytic) — RH remains open (June 2026); no 𝔽₁-square construction exists. Next: v0.13.0 cos/sin + log (prerequisites all in place).

🤖 Generated with Claude Code