v0.9.0 — the general exponential exp(q) on [0,1]

v0.9.0 — the general exponential exp(q) on the rational interval [0,1] (+ peer-review hardening)

Continues the transcendentals arc opened by e = exp(1) (v0.8.0).

Added — F1Square/Analysis/ExpGen.lean

• exp(q) = Σ qⁱ/i! for rational q ∈ [0,1] as a constructive real (Rexp), with a rigorous
  rational error bound. The only genuinely new input is termwise domination: for q ∈ [0,1] every
  power qⁱ ≤ 1 (qpow_le_one), so each term qⁱ/i! ≤ 1/i! (expTerm_le) and the exp(q)
  partial-sum gaps are dominated termwise by those of e (expdiff_dom). Hence the same tail bound
  S_q(b) − S_q(a) ≤ 2/(a+1)! (expdiff_bound) and the same reindex prove regularity — no new tail
  analysis. Rational powers qpow built from scratch (core has no q^i).
• Correctness anchors: Rexp_zero (exp 0 ≈ 1), Rexp_one_pos (exp 1 > 0), and
  Rexp_one_eq_e (exp 1 ≈ e — the construction specializes to v0.8.0's Euler number, a regression
  anchor). New reusable ℚ infrastructure: Qeq_trans, Qadd_congr.

Hardened — peer-review readiness

• Self-enforcing audit coverage: honesty_audit.sh now checks that every non-private proof-layer
  theorem/lemma (248) is #print axioms-audited and fails CI otherwise; closed the prior ~30-declaration
  gap so the "every theorem is checked" invariant can no longer drift.
• Honest prose pass: T1 scoped to point-set level (surface unbuilt); §2.3 leads with the vacuity
  of the shift-length positivity (it equals RH); §9.1 labelled as re-verification on genuine product
  surfaces C × C (not the unbuilt 𝕊); char-1 status distinguishes kernel-checked from
  numerically-checked results; stale v0.0.1 instructions updated.

Pure Lean 4, no Mathlib, no sorry; axiom-clean and choice-free; CI machine-verified green (coverage 248/248).

RH remains open (June 2026); no 𝔽₁-square construction exists — Connes–Consani arXiv:2602.15941
is a Jacobian/adele-class-space construction, not the square nor an intrinsic intersection theory. The
crux stays none.

🤖 Generated with Claude Code