v0.4.0 — from-scratch `ring` + ℚ ordered field + ℝ additive group

v0.4.0 — a from-scratch ring, ℚ as an ordered field, ℝ as an ordered additive group

This release completes the v0.3.0 ring normalizer into a real tactic and uses it to give the
constructive reals their arithmetic — all pure Lean 4 core, no Mathlib, no sorry. RH remains
open; the substrate makes the analytic half statable and checkable, never proven.

Added

• ring_uor — a from-scratch ring tactic (F1Square/Analysis/RingTac.lean). A genuine Lean
  tactic in core metaprogramming (Lean.Elab.Tactic — not Mathlib): it reifies an integer equality
  goal into the PExpr syntax, applies the v0.3.0 soundness lemma nf_eq, and discharges the
  residual norm lhs = norm rhs by decide. Reification is fuel-bounded (no partial def), and the
  tactic only builds an nf_eq proof term — so every goal it closes is as axiom-clean as nf_eq.
• ℚ as a verified ordered field (F1Square/Analysis/QOrder.lean): reflexivity/transitivity of ≤,
  Qeq → Qle, additive monotonicity, the absolute-value triangle inequality, |·| respecting
  value-equality, order transport along ≈, and the telescoping triangle |(a+b)−(c+d)| ≤ |a−c|+|b−d| — from the core ℤ order/natAbs lemmas plus ring_uor.
• ℝ as an ordered additive group (F1Square/Analysis/Real.lean): negation Rneg (an isometry)
  and the reindexed Bishop addition Radd ((x⊕y)ₙ = x₍₂ₙ₊₁₎+y₍₂ₙ₊₁₎), each with its
  regularity proof — the addition's bound is exactly the 2·1/(2k+2) = 1/(k+1) identity, discharged
  by ring_uor. The Real structure now carries den_pos.

Provenance note (purity)

ring is confirmed absent from Lean 4 core (it compiles with zero imports → "unknown tactic"),
which is why we built ring_uor. push_cast and omega, used for the cast/linear steps, are
core (they compile with zero imports, no Mathlib/Std) — same tier as decide/simp.

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.5.0)

ℝ multiplication, ≈-transitivity (an Archimedean argument), completeness, ℂ = ℝ×ℝ, and the
transcendentals (exp/log/cos via convergent series with rigorous error bounds).