proof(numbers): approxGroup witness for float/complex + Rational/Symbolic value-model design (gap-005)#57
Merged
Conversation
…esign 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
hyperpolymath
marked this pull request as ready for review
June 21, 2026 23:18
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Advances value-level number-system semantics (
gap-005) for the four carrier-distinct systems — 2 witnessed now, 2 designed + tracked (see #58).Float & Complex — approxGroup witness (Rust)
Both are
f64-based, soaddis non-associative (approxGroup → Neutral, never the exactabelianGroup → Safetier).number.rsmod approx_group_witness(4 tests):(0.1 + 0.2) + 0.3 ≠ 0.1 + (0.2 + 0.3)viaValue::add, forValue::FloatandValue::ComplexThis is not 0-axiom Lean-provable: Lean's
Floatis an opaque@[extern]primitive, andnative_decidewould inject theLean.ofReduceBoolaxiom (forbidden here). The differential witness against native f64 is the faithful check.Rational & Symbolic — designed (Lean)
Both admit real 0-axiom Lean value models (rational = exact abelian group; symbolic = associative / non-commutative / non-group). Designed pick-up-ready in the new
docs/proofs/number-system-value-models.adoc; tracked in #58.Verification
cargo test -p jtv-coregreen (4 new tests);cargo fmt --check+clippyclean. Lean suite unchanged (no.leanedits).Docs
New
docs/proofs/number-system-value-models.adoc(status table + f64-wall rationale + Rational/Symbolic designs);PROOF-CAPABILITY-MATRIXscope section links it;gap-005updated inSTATE.a2ml.CI note
The two red checks (Hypatia + governance Workflow Staleness) are not caused by this change — both trace to the stale
hyperpolymath/standardsreusable pins (see #56); they fail onmaintoo. Lean/test/Check are all green.🤖 Generated with Claude Code