v0.7.0 — Cauchy completeness of ℝ

ℝ is now Cauchy complete — every regular sequence of reals converges. Pure Lean 4, no Mathlib, no sorry, axiom-clean, and choice-free.

With ℝ a commutative ring up to ≈ (v0.6.0), this brick proves the constructive analogue of "ℝ is complete" — the foundation the transcendentals will stand on (a power series is exactly a regular sequence of its partial sums).

• RReg — a regular sequence of reals: X j and X k agree within 1/(j+1)+1/(k+1) as reals (with the canonical index modulus 2/(n+1)).
• Rlim — Bishop's diagonal limit n ↦ (X(4n+3))_{4n+3}. The 4n+3 reindex reads each real far enough out that the diagonal is itself a regular sequence of rationals (RlimSeq_regular), so Rlim X is a genuine constructive real.
• Rlim_tendsTo — convergence with an explicit rate: X k → Rlim X within 1/(k+1).
• RTendsTo_unique — limits are unique up to ≈ (via the generalized Archimedean lemma + the linear-bound criterion).

Choice-free. Because the regular-sequence data carries its own modulus, the diagonal construction needs no countable choice — the #print axioms audit shows only propext, Quot.sound, never Classical.choice. (For modulus-free Cauchy reals, completeness is independent of constructive ZF; carrying the modulus is what avoids that.)

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

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 substrate makes the analytic half statable and checkable, never proven — proving λₙ ≥ 0 ∀n is RH.

Next (v0.8.0). The transcendentals — exp/log/cos via convergent series with rigorous rational error bounds, standing directly on this completeness.