v0.5.0 — ℝ multiplication, ≈ an equivalence, ℂ = ℝ×ℝ

v0.5.0 — ℝ's equality is an equivalence, ℝ multiplication, ℂ = ℝ×ℝ

This release completes the constructive field arithmetic over the Bishop reals and makes Bishop
equality a genuine equivalence relation — all pure Lean 4 core, no Mathlib, no sorry, every
theorem axiom-clean. RH remains open; the substrate makes the analytic half statable and
checkable, never proven.

Added

• ≈ is now a full equivalence (QOrder.lean, Real.lean). Transitivity Req_trans is the
  genuine limiting argument: for each n, the gap |xₙ − zₙ| is bounded — for every auxiliary
  index m — by 2/(n+1) + 6/(m+1) (four triangle steps through xₘ, yₘ, zₘ), and the
  Archimedean lemma Qarch (if p ≤ q + 6/(m+1) for all m then p ≤ q) kills the tail.
• ℝ multiplication Rmul (Real.lean). Reindex both factors at r(n) = 2K(n+1) − 1, where
  K = max(K_x, K_y) bounds both sequences via the canonical bound |xₙ| ≤ |x₀| + 2 (canon_bound);
  regularity is proved because each factor is ≤ K and the 2K reindexing cancels it exactly
  (2K·(1/(2K(m+1)) + 1/(2K(n+1))) = 1/(m+1)+1/(n+1), discharged by ring_uor). Commutative
  (Rmul_comm). Supporting ℚ multiplication-order library in QOrder.lean (Qabs_mul,
  Qmul_le_mul, the product-difference triangle Qabs_mul_diff).
• Operation-congruence over ≈: Rneg_congr, Radd_congr, Rsub_congr (the operations are
  well-defined on the Bishop setoid).
• ℂ = ℝ×ℝ (Complex.lean) with componentwise Bishop equality (an equivalence) and all four
  operations — Cadd, Cneg, Cmul ((ac−bd, ad+bc)), 0, 1, i, and ℝ ↪ ℂ — the additive-group
  laws and commutative multiplication Cmul_comm (up to ≈).

Honesty

The mechanized gate (scripts/honesty_audit.sh) is green: every proof-layer theorem is axiom-clean
(#print axioms ⊆ {propext, Classical.choice, Quot.sound}). The crux (Hodge index on 𝕊 = RH) stays
none because it is open, never because it is forbidden.

Next (v0.6.0)

The remaining ℂ ring laws — associativity and distributivity — need Rmul-congruence and
Rmul-associativity (a reindex-reconciliation theorem, harder than the additive congruences); then
completeness (every regular sequence of reals converges) and the transcendentals.