gap-005: land Rational + Symbolic 0-axiom Lean value models

[hyperpolymath]

Goal

Land the two remaining 0-axiom Lean value models for gap-005 (value-level number-system semantics). Design is pick-up-ready in docs/proofs/number-system-value-models.adoc.

Context: int/hex/binary are done (type_preservation); float/complex are honestly Rust-witnessed as approxGroup (they're f64-based and opaque to Lean's kernel — a Lean proof would need the forbidden native_decide axiom). The two systems below are exact and so admit genuine 0-axiom Lean proofs.

1. JtvRational.lean — exact abelian group

Faithful to Value::Rational(Ratio<i64>). Mathlib/Batteries-free, so build from core Int:

structure Q where
  num : Int
  den : Int
  den_nz : den ≠ 0
def Q.add (a b : Q) : Q := ⟨a.num * b.den + b.num * a.den, a.den * b.den, …⟩
def Q.neg (a : Q) : Q := ⟨-a.num, a.den, a.den_nz⟩
def Q.zero : Q := ⟨0, 1, by decide⟩
def Q.equiv (a b : Q) : Prop := a.num * b.den = b.num * a.den

Targets: equiv is a setoid (refl/symm/trans — the fiddly one, Int cancellation by nonzero denominators); add respects equiv; abelian-group laws up to equiv (qadd_comm, qadd_assoc, qadd_zero, qadd_left_neg). → rational = exact abelian group → Safe.

2. JtvSymbolic.lean — free, non-group algebra

Faithful to Value::Symbolic(String): add a b = a ++ " + " ++ b, neg s = "-(" ++ s ++ ")". Carrier String/List Char.

Targets: sadd_assoc (the " + " separator flattens → append-associativity); sadd_not_comm (concrete "a + b" ≠ "b + a" by decide); a non-group witness (length strictly grows → no inverse/identity). → symbolic = associative, non-commutative, non-group → Breaking (retains structure).

Hard constraints (this repo's discipline)

• 0 axioms (#print axioms clean), no sorry/admit/axiom/native_decide, no True-typed theorems.
• Wire each new module into the lakefile + JtvAll + the matrix; pin in any smoke aggregator.
• Local Lean works via the GitHub-releases toolchain bypass (see STATE.a2ml 2026-06-21) — release.lean-lang.org is off the egress allowlist.

Out of scope here

The deeper rung — a multi-sorted evalDataExpr producing these carriers so type_preservation extends to them directly — is a separate model refactor.