Published 2026-09-14
- Maintainers
- Viktor Mikhalkin
- License
- Apache-2.0
Problem
A real linear equality system (Ax=b) need not be consistent, full rank, or uniquely solvable. A numerical solver can nevertheless return a plausible vector without making clear which exact solution class the data support. This project treats status classification as part of the result and declines to force a binary conclusion near a rank transition.
Scope
The implementation targets dense real systems. It reports UNIQUE, INFINITE, INCONSISTENT, UNDECIDABLE, or FAIL; the last two distinguish numerical uncertainty from resource failure. Sparse solvers and portable performance guarantees are outside the current scope.
Architecture
The solver state is an affine bundle consisting of accepted normal directions and their right-hand-side functional. For each incoming equality, the unexplained normal component determines whether the bundle grows, while the compatibility residual distinguishes a redundant row from a contradiction.
A fast router performs the numerical classification. A separate strict checker works from the source data and independently verifies typed proof objects for nearby exact systems in the unique, non-unique consistent, and inconsistent classes. The checker, rather than the router, owns the reported perturbation radii.
Current result
Release v0.4.4 provides the C11 implementation, public C API, regression and property-based test batteries, manuscript source, reproducible numerical experiments, and immutable result records. The release source is preserved by Zenodo under DOI 10.5281/zenodo.22753773.
A preprint has been submitted to HAL and is awaiting moderation. No public HAL publication is claimed here until that process is complete.
Verification
The build gates directed rounding and checks that loading the fast router does not alter the floating-point mode used by the strict certificate kernels. CI exercises GCC and Clang builds, portable/native classification agreement, sanitizer configurations, BLAS variants, regression suites, and two property batteries. The retained manuscript values are checked against an immutable benchmark package.
Reproducibility
The canonical path uses a C11 compiler, OpenMP, Python, SciPy, and the exact public release:
git clone https://github.com/metronforge/affine-bundle-solver.git
cd affine-bundle-solver
git checkout v0.4.4
pip install -r requirements.txt
ARCH_FLAGS='' ./build.sh
python3 tests/check_paper_claims.py
python3 tests/check_paper_claims.py --audit-performance-artifacts . \
--require-publication-ready
The repository README documents the full regression and property-test commands, build outputs, and repository layout.
Limitations
The checker is a strict-C research prototype whose soundness contract depends on valid outward rounding. Property-based testing can expose broad classes of implementation defects but does not replace proof. Performance observations are limited to the recorded machine, software stack, inputs, and single-thread protocol; comparisons with DGELSY, DGESV, or LSMR do not imply equivalent internal work or universal speedups.