v0.8.0 — the first transcendental: Euler's number e

The first transcendental — Euler's number e = Σ 1/i! as a constructive real, via the exponential series with a rigorous rational error bound. Pure Lean 4, no Mathlib, no sorry, axiom-clean (choice-free).

Standing on v0.7.0 completeness (a convergent series is a regular sequence of its partial sums), and since the partial sums are rational, the reindexed partial-sum sequence is directly a regular sequence of rationals — a Real.

• fct — factorial from scratch (Lean core has no Nat.factorial), with fct_pos, self_le_fct, and the step 2·(k+1)! ≤ (k+2)!.
• eSum — the partial sums S(N) = Σ_{i=0}^N 1/i!.
• ediff_bound — the rigorous error bound S(b) − S(a) ≤ 2/(a+1)! for a ≤ b. The crux is a telescoping observation: U(n) := S(n) + 2/(n+1)! is decreasing (because 2/(n+2)! ≤ 1/(n+1)!, i.e. 2 ≤ n+2), so S(b) ≤ U(b) ≤ U(a) = S(a) + 2/(a+1)!. A fully rational, explicitly computable tail bound that inducts in one line — cleaner than the usual geometric-ratio argument.
• eSeq_regular — the reindex n ↦ S(n+1) makes 2/(n+2)! ≤ 1/(n+1), so the partial sums are regular and e is a genuine constructive real.
• e_pos — e is positive (its index-0 approximant is 2).

Honesty. CI machine-verified green (the "Mechanized-honesty audit" step is success for the release commit): no sorry, no native_decide, no stray axioms — and no Classical.choice (the construction is choice-free). The crux (Hodge index on 𝕊 = RH) stays none.

Status (fresh mid-2026 synthesis). RH remains open; there is still no accepted 𝔽₁-scheme theory realizing Spec ℤ ×_𝔽₁ Spec ℤ with an intrinsic intersection theory (the Feb-2026 Connes–Consani On the Jacobian of Spec ℤ̄ is an Arakelov–Picard reinterpretation, not the square). The transcendentals make more of the analytic half statable and checkable, never proven — proving λₙ ≥ 0 ∀n is RH.

Next (v0.9.0+ transcendentals arc). The general exp(q) on [0,1] (the e-bound dominates each term since |q^i/i!| ≤ 1/i!), cos/sin via alternating series (error ≤ first omitted term), and log.