proof(numbers): approxGroup witness for float/complex + value-model design sketch (gap-005)

Advances value-level number-system semantics for the four carrier-distinct
systems: 2 witnessed now, 2 designed + tracked.

- Float & Complex are f64-based, so their `add` is non-associative
  (approxGroup → Neutral, never the exact abelianGroup → Safe tier). Witnessed
  in Rust (number.rs `mod approx_group_witness`, 4 tests): non-associativity via
  `Value::add`, commutativity holds. This is NOT 0-axiom Lean-provable — Lean's
  `Float` is opaque `@[extern]`, and `native_decide` would inject the
  `Lean.ofReduceBool` axiom (forbidden) — so the differential witness against
  native f64 is the faithful check.

- Rational (exact abelian group) and Symbolic (associative, non-commutative,
  non-group) admit real 0-axiom Lean value models — designed in the new
  docs/proofs/number-system-value-models.adoc (pick-up-ready; tracking issue).

Docs: PROOF-CAPABILITY-MATRIX scope-of-model section links the sketch; gap-005
updated in STATE.a2ml. cargo test/fmt/clippy green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -50,7 +50,7 @@ issues = [
   { id = "gap-002", description = "typing_coercion in JtvTypes.lean weaker than docstring — proves existence not coercion to target type", severity = "low", status = "known", follow-up = "ADR needed" },
   { id = "gap-003", description = "Coprocessor implementation gated on PataCL Phase 1", severity = "medium", status = "external-dependency" },
   { id = "gap-004", description = "Reversibility round-trip not guaranteed end-to-end at integration level", severity = "medium", status = "known" },
-  { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo). PARTIAL 2026-06-21: type_preservation lifted past τ=int to the whole integer-represented family {int,hex,binary} (these share the Int carrier; generalised via JtvType.isIntRepr; type_preservation_int recovers τ=int; #print axioms ⇒ no axioms). Remaining open half: value-level semantics for the carrier-DISTINCT systems float/rational/complex/symbolic", severity = "medium", status = "known", follow-up = "value-level semantics for float/rational/complex/symbolic (need their own value carriers; int/hex/binary done 2026-06-21)" },
+  { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo). PARTIAL 2026-06-21: type_preservation lifted past τ=int to the whole integer-represented family {int,hex,binary} (these share the Int carrier; generalised via JtvType.isIntRepr; type_preservation_int recovers τ=int; #print axioms ⇒ no axioms). PARTIAL 2026-06-21b: float+complex are f64-based → approxGroup non-associativity WITNESSED in Rust (number.rs mod approx_group_witness) — NOT 0-axiom Lean-provable (opaque @[extern] Float; native_decide would add Lean.ofReduceBool). rational (exact abelian group) + symbolic (assoc/non-comm/non-group) Lean value models DESIGNED in docs/proofs/number-system-value-models.adoc (tracking issue filed). Remaining: land the two designed Lean models", severity = "medium", status = "known", follow-up = "land rational + symbolic 0-axiom Lean value models (designed in docs/proofs/number-system-value-models.adoc); float/complex are honestly Rust-witnessed (f64 opaque in Lean)" },
   { id = "gap-006", description = "RESOLVED 2026-06-15: license decision = MPL-2.0 (code) + CC-BY-SA-4.0 (docs), full per-file. 75 doc headers -> CC-BY-SA-4.0; code stragglers (3 PMPL-1.0 workflows, MPL-2.0-or-later, PLMP/GPL typos, and a deliberate MIT-OR-GPL-3.0-or-later-OR-Palimpsest tri-license on formatter/repl/rsr_check) -> MPL-2.0; PALIMPSEST.adoc (both copies) retired; LICENSING.md rewritten; PMPL badges replaced. Follow-ups: populate LICENSES/ with canonical MPL-2.0 + CC-BY-SA-4.0 texts; add SPDX headers to ~49 header-less docs.", severity = "low", status = "resolved", follow-up = "LICENSES/ texts + header-less docs" }
 ]
 
@@ -93,7 +93,8 @@ sessions = [
   { date = "2026-06-18", subject = "@epi(...) epistemic-grade surface (ADR-0009 D2) — mirror of the @echo surface. @epi(Opaque|Partial|Transparent) annotation on functions: grammar.pest epi_marker; parser.rs marker loop also consumes epi_marker → FunctionDecl.epi_annotation (order-independent with @pure/@echo). Epistemic enum moved epistemic.rs→ast.rs (gains Serialize) with `pub use crate::ast::Epistemic` re-export, same cycle-break as Echo. typechecker.rs check_echo_annotations renamed check_effect_annotations: now checks BOTH axes (inferred.echo ⊑ @echo, inferred.epi ⊑ @epi) against resolved_effects (FunctionEffect carries .echo + .epi). pretty.rs + formatter.rs emit @epi after @echo. 5 new tests (parser @epi + echo&epi-together, typechecker epi accept/reject, round-trip); 138 lib tests, fmt/clippy green. Completes the ADR-0009 D1+D2 function-DECLARATION effect surface. REMAINING on this axis: carry the (echo,epi) row in TypeAnnotation::Function (function-VALUED params) — has a function-type grade-syntax + variance design choice to settle." },
   { date = "2026-06-18", subject = "Function-TYPE grade carrying (ADR-0009 D1/D3) — completes the ADR-0009 effect surface. A function type Fn(...) -> T may now carry the (echo,epi) row with PREFIX markers (user choice): @echo(Neutral) @epi(Partial) Fn(Int) -> Int. ast.rs: new EffectGrade { echo: Option<Echo>, epi: Option<Epistemic> } (Default); TypeAnnotation::Function gains a trailing EffectGrade; typechecker Type::Function likewise. grammar.pest function_type now (echo_marker|epi_marker)* ~ 'Fn' ...; parser splits the leading markers from the param/return type_annotations. annotation_to_type carries the grade into Type::Function; Display + pretty.rs + formatter.rs emit the prefix markers (round-trip). coercible_to gains a function-type case: COVARIANT in the grade (grade_leq — a function that loses/reveals LESS is usable where MORE is allowed; None target = unconstrained; None source can't satisfy a Some ceiling; params/return invariant for now). 4 tests (parse graded + ungraded; round-trip; covariance accept/reject/unconstrained); 142 lib tests, fmt/clippy green. HONEST SCOPE: representational/forward-infrastructure — JtV has no first-class function VALUES (no lambdas/indirect calls) yet, so the value-against-type coercion is correct but LATENT until function values land. ADR-0009 D1+D2+D3 declaration+type effect surface now COMPLETE." },
   { date = "2026-06-21", subject = "type_preservation lifted past τ=int to the integer-represented family {int,hex,binary} (gap-005 partial). LOCAL LEAN TOOLCHAIN UNBLOCKED: elan 4.2.2 was present but had no toolchain, and `release.lean-lang.org` is off the egress allowlist (its 'Host not in allowlist' page is the stray 'H' that broke elan's release-metadata parse). Bypassed by fetching the v4.12.0 linux tarball straight from GitHub releases (github.com + the asset host ARE allowlisted) and unpacking it into ~/.elan/toolchains/leanprover--lean4---v4.12.0 — elan then recognises the pinned toolchain; full `lake build` exit 0 (suite is mathlib-free, zero packages, no network). PROOF (JtvTypes.lean SECTION 6): inductive TypedValue gains hex + binary constructors (all three number systems share the Int runtime carrier — hex/binary ARE int-represented); new predicate JtvType.isIntRepr {int,hex,binary}↦True else False; type_preservation generalised from `τ=int → …` to `(hτ : τ.isIntRepr) → TypedValue (evalDataExpr e σ) τ`, proved `cases τ <;> first | exact TypedValue.{int,hex,binary} | simp only [JtvType.isIntRepr] at hτ`; type_preservation_int corollary recovers the original τ=int statement (via subst + trivial). `#print axioms` ⇒ BOTH new theorems depend on NO axioms. INVARIANTS held: full lake build exit 0; 0 sorry/admit/axiom (word-boundary grep); 0 True-typed theorems. DOCS synced: PROOF-CAPABILITY-MATRIX (scope-of-model rewrite + new key-theorems row + 'checked 2026-06-04; re-verified 2026-06-21' note), ADR-0007 consequence #1, ADR-0010 §gap-005 + §Open. float/rational/complex/symbolic REMAIN stated-unproven (distinct carriers, each needs its own value model). NOTE for next session: the local toolchain at ~/.elan is ephemeral (container reclaimed on inactivity) — re-run the GitHub-releases bypass to restore `lake build`; CI (proof-regression.yml) is the durable verifier." },
-  { date = "2026-06-21", subject = "interpreter_correctness (PROOF-2 / gap-001) rung — denotational correspondence harness. Ties the Lean denotational model evalDataExpr ↔ the Rust interpreter eval_data_expr over the integer fragment the model covers (lit|var|add|neg over σ:String→Int). crates/jtv-core/src/interpreter.rs gains `mod denotational_correspondence`: (1) `denot` re-encodes the four Lean rules in i128; (2) `interpreter_matches_denotational_model_on_int_fragment` EXHAUSTIVELY enumerates every height-≤2 integer-fragment expression (5 lits × 2 vars = 7 leaves → 4039 exprs) across 3 states ≈ 12k cases, asserting interpreter == denot on all; (3) `overflow_is_the_correspondence_boundary` pins that Value::Int is i64 with checked_add/checked_neg → ERRORS at the i64 edge, never wraps (so correspondence boundary is exactly i64 range, Lean ℤ being unbounded); (4) `shared_golden_corpus_matches_lean` mirrors 7 concrete (expr,σ,value) points that are ALSO pinned by `rfl` in JtvCore.lean (cross-side anchor; the 5 new Lean `example`s use State.empty[x↦v] updates, all close by rfl). HONEST BOUND: integer fragment only (strings/float/rational/complex/calls/lists/tuples out of model); within i64 range; exhaustive-up-to-depth, NOT a Lean-mechanised refinement of the Rust evaluator (the deeper PROOF-2 rung). VERIFIED locally: cargo test (145 lib incl. 3 new + full workspace green), cargo fmt --check + clippy -D warnings clean, full lake build exit 0, 0 sorry/admit/axiom, 0 True-typed theorems. DOCS: PROOF-CAPABILITY-MATRIX (interpreter_correctness row JtvCore+interpreter.rs/partial + new 'Interpreter ↔ denotational-model correspondence' section + outstanding-work bullet), gap-001 partial. NEXT on PROOF-2: mechanised refinement (model the Rust evaluator in Lean) and/or extend the harness past the integer fragment." }
+  { date = "2026-06-21", subject = "interpreter_correctness (PROOF-2 / gap-001) rung — denotational correspondence harness. Ties the Lean denotational model evalDataExpr ↔ the Rust interpreter eval_data_expr over the integer fragment the model covers (lit|var|add|neg over σ:String→Int). crates/jtv-core/src/interpreter.rs gains `mod denotational_correspondence`: (1) `denot` re-encodes the four Lean rules in i128; (2) `interpreter_matches_denotational_model_on_int_fragment` EXHAUSTIVELY enumerates every height-≤2 integer-fragment expression (5 lits × 2 vars = 7 leaves → 4039 exprs) across 3 states ≈ 12k cases, asserting interpreter == denot on all; (3) `overflow_is_the_correspondence_boundary` pins that Value::Int is i64 with checked_add/checked_neg → ERRORS at the i64 edge, never wraps (so correspondence boundary is exactly i64 range, Lean ℤ being unbounded); (4) `shared_golden_corpus_matches_lean` mirrors 7 concrete (expr,σ,value) points that are ALSO pinned by `rfl` in JtvCore.lean (cross-side anchor; the 5 new Lean `example`s use State.empty[x↦v] updates, all close by rfl). HONEST BOUND: integer fragment only (strings/float/rational/complex/calls/lists/tuples out of model); within i64 range; exhaustive-up-to-depth, NOT a Lean-mechanised refinement of the Rust evaluator (the deeper PROOF-2 rung). VERIFIED locally: cargo test (145 lib incl. 3 new + full workspace green), cargo fmt --check + clippy -D warnings clean, full lake build exit 0, 0 sorry/admit/axiom, 0 True-typed theorems. DOCS: PROOF-CAPABILITY-MATRIX (interpreter_correctness row JtvCore+interpreter.rs/partial + new 'Interpreter ↔ denotational-model correspondence' section + outstanding-work bullet), gap-001 partial. NEXT on PROOF-2: mechanised refinement (model the Rust evaluator in Lean) and/or extend the harness past the integer fragment." },
+  { date = "2026-06-21", subject = "Number-system value-model rung + session close-out triage. gap-005 advanced for 2 of the 4 carrier-distinct systems, the other 2 designed+issued: (a) FLOAT+COMPLEX approxGroup WITNESS landed (number.rs mod approx_group_witness, 4 tests): non-associativity of Value::Float / Value::Complex add via the public Value::add ((0.1+0.2)+0.3 ≠ 0.1+(0.2+0.3)), commutativity holds. Honest finding: f64 is opaque to Lean's kernel (@[extern] Float; native_decide=Lean.ofReduceBool axiom, forbidden) → these are Rust-witnessed not Lean-proved. (b) RATIONAL (exact abelian group: Q struct + cross-mult equiv + group laws up to equiv) and SYMBOLIC (string-concat: assoc + non-comm counterexample + non-group) Lean value models DESIGNED in new docs/proofs/number-system-value-models.adoc; tracking issue filed. cargo test/fmt/clippy green. Docs: PROOF-CAPABILITY-MATRIX scope-of-model section links the sketch; gap-005 updated. NOTE: parallel-subagent route was attempted but worktree isolation is unavailable in this env (agent cwd not a git repo) — did it directly instead. Close-out triage (branches/wiki/docs audit) recorded in session response." }
 ]
 
 [design-artefact-locations]

crates/jtv-core/src/number.rs

@@ -414,3 +414,63 @@ mod tests {
         assert_eq!(Value::Unit.reversal_echo(), Echo::Safe);
     }
 }
+
+// ===========================================================================
+// approxGroup witness (ADR-0010 / gap-005, value-level)
+//
+// Float and Complex are IEEE-754 f64-based (`Value::Float(f64)`,
+// `Value::Complex(Complex<f64>)`), so their `add` is NON-associative: they sit
+// at the `approxGroup -> Neutral` tier, never the exact `abelianGroup -> Safe`
+// tier (unlike Int/Hex/Binary/Rational). This is the value-level fact behind
+// `reversal_echo` returning `Neutral` for float.
+//
+// It is witnessed HERE (in Rust, against native f64) rather than in Lean
+// because Lean's `Float` is an opaque `@[extern]` primitive: f64 arithmetic
+// does not reduce in the kernel, and the only way to evaluate it
+// (`native_decide`) injects the `Lean.ofReduceBool` axiom, which the jtv_proofs
+// 0-axiom invariant forbids. So the faithful check is this differential
+// witness. (Rational and Symbolic, being exact, DO admit 0-axiom Lean value
+// models — see docs/proofs/number-system-value-models.adoc + the tracking
+// issue.)
+// ===========================================================================
+#[cfg(test)]
+mod approx_group_witness {
+    use super::*;
+
+    #[test]
+    fn float_add_is_non_associative() {
+        let (a, b, c) = (Value::Float(0.1), Value::Float(0.2), Value::Float(0.3));
+        let left = a.add(&b).unwrap().add(&c).unwrap(); // (0.1 + 0.2) + 0.3
+        let right = a.add(&b.add(&c).unwrap()).unwrap(); // 0.1 + (0.2 + 0.3)
+        assert_ne!(
+            left, right,
+            "float add must be non-associative (approxGroup, not an exact group)"
+        );
+    }
+
+    #[test]
+    fn float_add_is_commutative() {
+        let (a, b) = (Value::Float(0.1), Value::Float(0.2));
+        assert_eq!(a.add(&b).unwrap(), b.add(&a).unwrap());
+    }
+
+    #[test]
+    fn complex_add_inherits_f64_non_associativity() {
+        let a = Value::Complex(Complex64::new(0.1, 1.0));
+        let b = Value::Complex(Complex64::new(0.2, 1.0));
+        let c = Value::Complex(Complex64::new(0.3, 1.0));
+        let left = a.add(&b).unwrap().add(&c).unwrap();
+        let right = a.add(&b.add(&c).unwrap()).unwrap();
+        assert_ne!(
+            left, right,
+            "complex add is componentwise f64 -> non-associative (approxGroup)"
+        );
+    }
+
+    #[test]
+    fn complex_add_is_commutative() {
+        let a = Value::Complex(Complex64::new(0.1, 2.0));
+        let b = Value::Complex(Complex64::new(0.2, 3.0));
+        assert_eq!(a.add(&b).unwrap(), b.add(&a).unwrap());
+    }
+}

docs/proofs/number-system-value-models.adoc

@@ -0,0 +1,90 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Number-system value models (gap-005) — status + design sketch
+:toc:
+:revdate: 2026-06-21
+
+Value-level semantics for JtV's seven number systems. The Lean denotational
+model (`evalDataExpr`) is `Int`-only; this document tracks lifting *value-level*
+algebraic facts to the other systems, faithful to the Rust interpreter
+(`crates/jtv-core/src/number.rs`). It elaborates the `gap-005` row of
+`verification/PROOF-CAPABILITY-MATRIX.adoc` and realises ADR-0010's
+algebra → Echo-tier classification at the value level.
+
+== Status table (faithful to `number.rs`)
+
+[cols="1,2,2,2,1",options="header"]
+|===
+| System | Rust rep | `add` | Algebra | Value-level status
+
+| `int` / `hex` / `binary` | `i64` | `checked_add` | exact abelian group | *Verified* — share the `Int` carrier; `type_preservation` (`JtvTypes.lean`, 0 axioms)
+| `rational` | `Ratio<i64>` | exact fraction `+` | exact abelian group | *Designed* (Lean) — see §Rational
+| `symbolic` | `String` | `"{a} + {b}"` concat | associative, non-commutative, non-group | *Designed* (Lean) — see §Symbolic
+| `float` | `f64` | raw IEEE `+` | approxGroup (non-associative) | *Witnessed* (Rust) — see §Float/Complex
+| `complex` | `Complex<f64>` | componentwise `f64` | approxGroup (inherits f64) | *Witnessed* (Rust) — see §Float/Complex
+|===
+
+== Float / Complex — why a Rust witness, not a Lean proof
+
+`float` and `complex` are IEEE-754 `f64`-based, so their addition is
+*non-associative*: they are `approxGroup → Neutral` (ADR-0010), never the exact
+`abelianGroup → Safe` tier.
+
+This fact is *witnessed in Rust* (`number.rs`, `mod approx_group_witness`):
+`(0.1 + 0.2) + 0.3 ≠ 0.1 + (0.2 + 0.3)` through `Value::Float`/`Value::Complex`
++ `Value::add`, with commutativity shown to hold.
+
+It is **not** provable as a 0-axiom Lean theorem. Lean's `Float` is an opaque
+`@[extern]` primitive: f64 arithmetic does not reduce in the kernel
+(`decide`/`rfl` cannot evaluate `0.1 + 0.2`), and the only evaluator
+(`native_decide`) injects the `Lean.ofReduceBool` axiom — which the jtv_proofs
+0-axiom invariant forbids. So the differential witness against native f64 is the
+faithful check; a Lean "proof" here would be either vacuous or axiom-bearing.
+
+== Rational — Lean exact-group model (design sketch)
+
+Faithful to `Value::Rational(Ratio<i64>)` (exact, auto-reduced). Mathlib- and
+Batteries-free, so build from Lean-core `Int`:
+
+[source,lean]
+----
+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   -- cross-mult
+----
+
+Targets (0 axioms, no `sorry`/`native_decide`): `equiv` is a setoid
+(refl/symm/trans), `add` respects `equiv`, and the abelian-group laws *up to*
+`equiv` — `qadd_comm`, `qadd_assoc`, `qadd_zero`, `qadd_left_neg` — via core
+`Int` ring lemmas. Establishes `rational = exact abelian group → Safe`.
+
+Honest bound: i64 overflow not modelled (unbounded `Int`); worked up to
+cross-multiplication (no reduced-form normalisation). `equiv` transitivity is
+the fiddliest step (Int cancellation by nonzero denominators).
+
+== Symbolic — Lean free-algebra model (design sketch)
+
+Faithful to `Value::Symbolic(String)`: `add a b = a ++ " + " ++ b`,
+`neg s = "-(" ++ s ++ ")"`. Carrier `String` (or `List Char`).
+
+Targets (0 axioms): `sadd_assoc` (the `" + "` separator flattens — both sides
+are `a ++ " + " ++ b ++ " + " ++ c`, via append-associativity);
+`sadd_not_comm` (concrete counterexample `"a + b" ≠ "b + a"` by `decide`);
+a non-group witness (`sadd` strictly grows length → no inverse / no identity).
+Establishes `symbolic = associative, non-commutative, non-group → Breaking`
+— symbolic *retains* structure where int/rational collapse it.
+
+== The full ladder (where this sits)
+
+* *int/hex/binary* — done (`type_preservation`).
+* *float/complex* — approxGroup witnessed (this is the maximal honest 0-axiom
+  Lean statement; the real content lives in Rust).
+* *rational/symbolic* — Lean models designed above; tracked as an issue.
+* The deeper rung (separate): a *multi-sorted evaluator* `evalDataExpr` that
+  produces these carriers, so `type_preservation` extends to them directly.
+  That is a model refactor, not covered here.