v0.3.0 — ℤ ring normalizer + constructive ℝ

v0.3.0 — the analysis substrate, brick two: a ℤ ring normalizer + constructive ℝ

This release builds the next piece of the analysis substrate the UOR way (canonical forms +
soundness, pure Lean 4, no Mathlib, no sorry) and lifts the standing no-ring ceiling. RH remains
open; the substrate makes the analytic half statable and checkable, never proven.

Added (+29 axiom-clean theorems)

• A reflective commutative-ring normalizer over ℤ (F1Square/Analysis/RingNF.lean). Polynomial
  expressions get a canonical form — a sorted, merged (monomial, coefficient) list, their
  content-address. One soundness theorem (norm_sound) + the decision lemma (nf_eq) turn equal
  canonical forms into genuine ℤ identities for all integers: (a+b)², (a+b)(a−b),
  (a+b+c)², freely-commuted distributivity — proved by decide on the finite normal form.
  Soundness is built from the core ℤ ring lemmas, never assumed. Large-scale computational reflection
  (à la Coq/Mathlib ring), implemented from scratch.
• General ℚ field laws (F1Square/Analysis/Rat.lean). The v0.2.0 ℚ brick verified its laws only
  on numerals; the normalizer makes them hold for all rationals — add_comm, mul_comm,
  add_assoc, mul_assoc, mul_add, mul_one, add_zero, add_neg.
• Constructive ℝ as Bishop regular sequences (F1Square/Analysis/Real.lean):
  |xₘ − xₙ| ≤ 1/(m+1) + 1/(n+1), the modulus baked into the index (no choice). The Real type, the
  regularity/positivity predicates, the canonical embedding ℚ ↪ ℝ (proved regular and
  value-respecting), and the Bishop equality setoid (Req_refl, Req_symm).

Honesty

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

Scope / next

ℝ field arithmetic (+, ·), ≈-transitivity (a limiting argument), and completeness are the
v0.4.0 continuation, followed by ℂ + transcendentals. Literature note: the Feb-2026
Connes–Consani Jacobian of Spec ℤ̄ (arXiv:2602.15941) is Arakelov–Picard — it does not
construct the square or prove Hodge positivity; RH is open as of mid-2026.