v0.6.0 — ℝ and ℂ are commutative rings up to ≈

ℝ and ℂ are now commutative rings up to Bishop equality ≈ — pure Lean 4, no Mathlib, no sorry, axiom-clean (⊆ {propext, Classical.choice, Quot.sound}).

The reindex Rmul uses to keep products regular differs on ≈-equal inputs, so multiplication-congruence and associativity are not rfl. v0.6.0 resolves this with one reusable engine and lifts it to every ring law:

• Qarch_gen — generalized Archimedean lemma: p ≤ q + C/(m+1) for all m (any C) ⟹ p ≤ q.
• Req_of_lin_bound (the linear-bound criterion) — |xₙ − yₙ| ≤ C/(n+1) for all n ⟹ x ≈ y. Our packaging of the Bishop ε-shift transitivity argument into a single tool that turns every reindex-mismatch into a genuine ≈.
• Product-gap engine — Rmul_gap, Rgap_le, Rcross_le, canon_bound_mul.
• ℝ a commutative ring up to ≈ — Rmul_congr (multiplication well-defined on the setoid, deferred from v0.5.0), Rmul_assoc, Rmul_distrib, Rmul_one, Radd_assoc, plus negation/subtractive-distributivity helpers.
• ℂ a commutative ring up to ≈ — Cadd_assoc, Cmul_one, Cmul_distrib, Cmul_assoc (the bilinear (a+bi)(c+di) expansions reduce, via the ℝ ring laws, to pointwise additive re-associations). With v0.5.0's Cmul_comm, all commutative-ring axioms hold.

Honesty. CI green and machine-verified (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; no construction of the 𝔽₁-square / ℤ⊗_𝔹ℤ with intrinsic intersection theory exists (the Feb-2026 Connes–Consani On the Jacobian of Spec ℤ̄ is an Arakelov–Picard reinterpretation of the adele class space, not the square). The substrate makes the analytic half statable and checkable, never proven — proving λₙ ≥ 0 ∀n is RH.

Next (v0.7.0). Completeness (every regular sequence of reals converges) and the transcendentals (exp/log/cos via convergent series with rigorous error bounds).