Skip to content

Commit 31b7b1e

Browse files
committed
docs(science): add mathematical basis and clarify numerical guarantees
- define the binary64, factorization, determinant-filter, exact-arithmetic, tolerance, and error contracts - align README, API documentation, examples, and LDLT diagnostics with guarantees over stored values - audit academic references and extend Criterion coverage for determinant error-bound paths Closes #159 Closes #164
1 parent b1e431a commit 31b7b1e

23 files changed

Lines changed: 670 additions & 194 deletions

CONTRIBUTING.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,7 @@ Use the existing canonical documents instead of duplicating their guidance:
6969
|-------|---------------------|
7070
| Agent rules and repository invariants | [`AGENTS.md`](AGENTS.md) |
7171
| User-facing API, examples, and project scope | [`README.md`](README.md) |
72+
| Mathematical basis and numerical validity | [`docs/mathematical_basis.md`](docs/mathematical_basis.md) |
7273
| Package metadata, features, and dependencies | [`Cargo.toml`](Cargo.toml) |
7374
| Commands and validation workflow | [`justfile`](justfile), `just --list` |
7475
| Python support tooling | [`scripts/README.md`](scripts/README.md) |

README.md

Lines changed: 94 additions & 59 deletions
Large diffs are not rendered by default.

REFERENCES.md

Lines changed: 49 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Tagged releases are archived on Zenodo under the all-versions concept DOI
1515
- CodeRabbit AI, Inc. "CodeRabbit." <https://coderabbit.ai/>.
1616
- KiloCode. "KiloCode AI Engineering Assistant." <https://kilocode.ai/>.
1717
- OpenAI. "ChatGPT." <https://openai.com/chatgpt>.
18+
- OpenAI. "Codex." <https://openai.com/codex/>.
1819
- Warp Dev, Inc. "WARP." <https://www.warp.dev/>.
1920

2021
All AI-generated output was reviewed and/or edited by the maintainer.
@@ -62,50 +63,62 @@ matrix and RHS. After back-substitution, multiplying by the exact power-of-two s
6263

6364
Both the determinant and solve paths convert their finite-by-construction entries via
6465
`decompose_proven_finite_f64`, which extracts the IEEE 754 binary64 sign, unbiased exponent,
65-
and significand [9] and strips trailing zeros from the significand so `|x| = m · 2^e` with
66-
`m` odd. The integer matrix is then assembled by shifting each mantissa left by
66+
and significand [9]. For nonzero `x`, it strips trailing zeros from the
67+
significand so `|x| = m · 2^e` with `m` odd; signed zeros use a separate zero
68+
component. The integer matrix is then assembled by shifting each mantissa left by
6769
`exp − e_min`, giving a GCD-free exact-integer starting point. Solves and D ≥ 5 determinants
6870
then apply Bareiss elimination; D ≤ 4 determinants use direct expansions. The test-only
6971
fallible wrapper `decompose_f64` verifies rejection of non-finite raw scalars, while the
7072
test-only `f64_to_big_rational` helper packages the same decomposition into a single
71-
`BigRational`. See Goldberg [10] for background on IEEE 754 representation and exact rational
72-
reconstruction.
73+
`BigRational`. See Goldberg [10] for background on floating-point representation and
74+
conversion.
7375

74-
### LDL^T factorization (symmetric SPD/PSD)
76+
### LDLᵀ factorization (exactly symmetric positive-definite inputs)
7577

76-
The LDL^T (often abbreviated "LDLT") implementation in `la-stack` is intended for symmetric positive
77-
definite (SPD) and positive semi-definite (PSD) matrices (e.g. Gram matrices), and does not perform
78-
pivoting.
78+
The no-pivot LDLT implementation targets `A = L D Lᵀ` for exactly symmetric
79+
positive-definite inputs [4-5, 11-12]. Successful construction requires every
80+
computed diagonal pivot to be positive and greater than the caller's tolerance.
81+
Computed zero and tolerance-small positive pivots are therefore part of the
82+
typed diagnostic domain, not returned in a usable factorization. Because the
83+
pivots are computed in binary64, a successful factorization is not an exact
84+
certificate that the represented matrix is positive definite.
7985

80-
For background on the SPD/PSD setting, see [4-5]. For pivoted variants used for symmetric *indefinite*
81-
matrices, see [6].
86+
For pivoted variants used for symmetric *indefinite* matrices, see [6, 11-12].
8287

8388
### LU decomposition (Gaussian elimination with partial pivoting)
8489

85-
The LU implementation in `la-stack` follows the standard Gaussian elimination / LU factorization
86-
approach with partial pivoting for numerical stability.
90+
The LU implementation targets `P A = L U` and uses partial pivoting: each step
91+
selects the remaining entry of largest magnitude in the active column. Partial
92+
pivoting is a practical stability strategy, not an unconditional accuracy
93+
guarantee; worst-case growth and average-case behavior are distinct concerns.
8794

88-
See references [1-3] below.
95+
See [1-3, 11-12] for stability analysis, finite-precision behavior, and standard
96+
algorithmic background.
8997

9098
## References
9199

92100
1. Trefethen, Lloyd N., and Robert S. Schreiber. "Average-case stability of Gaussian elimination."
93101
*SIAM Journal on Matrix Analysis and Applications* 11.3 (1990): 335–360.
102+
[DOI](https://doi.org/10.1137/0611023) ·
94103
[PDF](https://people.maths.ox.ac.uk/trefethen/publication/PDF/1990_44.pdf)
95104
2. Businger, P. A. "Monitoring the Numerical Stability of Gaussian Elimination."
96-
*Numerische Mathematik* 16 (1970/71): 360–361.
97-
[Full text](https://eudml.org/doc/132040)
105+
*Numerische Mathematik* 16.4 (1971): 360–361.
106+
[DOI](https://doi.org/10.1007/BF02165006) · [Full text](https://eudml.org/doc/132040)
98107
3. Huang, Han, and K. Tikhomirov. "Average-case analysis of the Gaussian elimination with partial pivoting."
99108
*Probability Theory and Related Fields* 189 (2024): 501–567.
100-
[Open-access PDF](https://link.springer.com/article/10.1007/s00440-024-01276-2) (also: [arXiv:2206.01726](https://arxiv.org/abs/2206.01726))
101-
4. Cholesky, Andre-Louis. "On the numerical solution of systems of linear equations"
102-
(manuscript dated 2 Dec 1910; published 2005).
103-
Scan + English analysis: [BibNum](https://www.bibnum.education.fr/mathematiques/algebre/sur-la-resolution-numerique-des-systemes-d-equations-lineaires)
104-
5. Brezinski, Claude. "La methode de Cholesky." (2005).
105-
[PDF](https://eudml.org/doc/252115)
106-
6. Bunch, J. R., L. Kaufman, and B. N. Parlett. "Decomposition of a Symmetric Matrix."
107-
*Numerische Mathematik* 27 (1976/1977): 95–110.
108-
[Full text](https://eudml.org/doc/132435)
109+
[DOI](https://doi.org/10.1007/s00440-024-01276-2) ·
110+
[Open-access article](https://link.springer.com/article/10.1007/s00440-024-01276-2) ·
111+
[arXiv:2206.01726](https://arxiv.org/abs/2206.01726)
112+
4. Cholesky, André-Louis. "Sur la résolution numérique des systèmes d'équations linéaires."
113+
*Bulletin de la Sabix* 39 (2005): 81–95. Manuscript dated 2 December 1910.
114+
[DOI](https://doi.org/10.4000/sabix.529)
115+
5. Brezinski, Claude. "La méthode de Cholesky."
116+
*Revue d'histoire des mathématiques* 11.2 (2005): 205–238.
117+
[DOI](https://doi.org/10.24033/rhm.30) ·
118+
[Full text](https://www.numdam.org/articles/10.24033/rhm.30/)
119+
6. Bunch, James R., Linda Kaufman, and Beresford N. Parlett. "Decomposition of a Symmetric Matrix."
120+
*Numerische Mathematik* 27 (1976): 95–109.
121+
[DOI](https://doi.org/10.1007/BF01399088) · [Full text](https://eudml.org/doc/132435)
109122
7. Bareiss, Erwin H. "Sylvester's Identity and Multistep Integer-Preserving Gaussian
110123
Elimination." *Mathematics of Computation* 22.103 (1968): 565–578.
111124
[DOI](https://doi.org/10.1090/S0025-5718-1968-0226829-0) ·
@@ -123,6 +136,15 @@ See references [1-3] below.
123136
10. Goldberg, David. "What Every Computer Scientist Should Know About Floating-Point
124137
Arithmetic." *ACM Computing Surveys* 23.1 (1991): 5–48.
125138
[DOI](https://doi.org/10.1145/103162.103163) ·
126-
[PDF](https://www.validlab.com/goldberg/paper.pdf)
127-
Comprehensive survey of IEEE 754 representation, rounding, and exact rational
128-
reconstruction of floating-point values.
139+
[Authorized HTML reprint](https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html)
140+
Comprehensive survey of floating-point representation, rounding, and conversion.
141+
11. Higham, Nicholas J. *Accuracy and Stability of Numerical Algorithms*. 2nd ed.
142+
Society for Industrial and Applied Mathematics, 2002.
143+
[DOI](https://doi.org/10.1137/1.9780898718027)
144+
12. Golub, Gene H., and Charles F. Van Loan. *Matrix Computations*. 4th ed.
145+
Johns Hopkins University Press, 2013.
146+
[DOI](https://doi.org/10.56021/9781421407944) ·
147+
[Publisher record](https://www.press.jhu.edu/books/title/10678/matrix-computations)
148+
13. Kalibera, Tomas, and Richard Jones. "Rigorous Benchmarking in Reasonable Time."
149+
*Proceedings of the 2013 International Symposium on Memory Management* (ISMM '13),
150+
2013: 63–74. [DOI](https://doi.org/10.1145/2464157.2464160)

benches/common/exact.rs

Lines changed: 24 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -493,9 +493,9 @@ fn assert_approximate_determinant(actual: f64, exact: &BigRational, operation: &
493493
/// Validate the floating-point determinant operations used by Criterion.
494494
///
495495
/// This runs during setup, outside timed closures. The deterministic `det` and
496-
/// `det_direct` results are compared with the independent Leibniz oracle; on
497-
/// current revisions the combined direct result is additionally checked
498-
/// against its certified absolute bound.
496+
/// `det_direct` results are compared with the independent Leibniz oracle, and
497+
/// `det_errbound` must certify the observed direct error. On current revisions,
498+
/// the paired result must also match the separate determinant and bound calls.
499499
///
500500
/// # Panics
501501
///
@@ -513,11 +513,24 @@ pub fn validate_f64_determinant_benchmarks<const D: usize>(input: &ValidatedExac
513513
.matrix()
514514
.det_direct()
515515
.or_abort("direct f64 determinant oracle check");
516+
let standalone_bound = input
517+
.matrix()
518+
.det_errbound()
519+
.or_abort("standalone determinant error-bound oracle check");
516520
if D <= 4 {
517521
let Some(direct) = direct else {
518522
panic!("det_direct must support benchmark dimension {D}");
519523
};
524+
let Some(standalone_bound) = standalone_bound else {
525+
panic!("det_errbound must support benchmark dimension {D}");
526+
};
520527
assert_approximate_determinant(direct, &exact, "direct f64 determinant");
528+
let observed_error = (rational_from_f64(direct) - &exact).abs();
529+
let certified_bound = rational_from_f64(standalone_bound);
530+
assert!(
531+
observed_error <= certified_bound,
532+
"direct determinant error {observed_error} exceeds standalone certified bound {certified_bound}",
533+
);
521534

522535
#[cfg(not(la_stack_v0_4_3_api))]
523536
{
@@ -529,19 +542,21 @@ pub fn validate_f64_determinant_benchmarks<const D: usize>(input: &ValidatedExac
529542
panic!("the baseline fixture must have a certified D={D} determinant bound");
530543
};
531544
assert_eq!(estimate.determinant().to_bits(), direct.to_bits());
545+
assert_eq!(
546+
estimate.absolute_error_bound().to_bits(),
547+
standalone_bound.to_bits(),
548+
);
532549
assert!(
533550
estimate.determinant().abs() > estimate.absolute_error_bound(),
534551
"the headline D={D} det_sign_exact benchmark must exercise the fast filter",
535552
);
536-
let observed_error = (rational_from_f64(direct) - &exact).abs();
537-
let certified_bound = rational_from_f64(estimate.absolute_error_bound());
538-
assert!(
539-
observed_error <= certified_bound,
540-
"direct determinant error {observed_error} exceeds certified bound {certified_bound}",
541-
);
542553
}
543554
} else {
544555
assert!(direct.is_none(), "det_direct unexpectedly supports D={D}");
556+
assert!(
557+
standalone_bound.is_none(),
558+
"det_errbound unexpectedly supports D={D}",
559+
);
545560

546561
#[cfg(not(la_stack_v0_4_3_api))]
547562
assert!(

benches/exact.rs

Lines changed: 52 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@
88
//! 1. **General-case benches** (`exact_d{2..5}`) — a single
99
//! well-conditioned diagonally-dominant matrix per dimension. These
1010
//! measure typical-case performance and track regressions against a
11-
//! reproducible input.
11+
//! reproducible input. D=2..=4 also include the direct determinant and
12+
//! certified error-bound f64 baselines.
1213
//! 2. **Adversarial / extreme-input benches** — matrices chosen to
1314
//! stress specific corners of the exact-arithmetic pipeline:
1415
//! near-singularity (forces the exact integer fallback), large f64 entries
@@ -200,9 +201,57 @@ fn bench_det_direct<const D: usize>(
200201
});
201202
}
202203

203-
macro_rules! register_det_direct_benchmark {
204+
/// Add the standalone certified determinant-bound baseline.
205+
fn bench_det_errbound<const D: usize>(
206+
group: &mut BenchmarkGroup<'_, WallTime>,
207+
input: &ValidatedExactInput<D>,
208+
) {
209+
let bound = input
210+
.matrix()
211+
.det_errbound()
212+
.or_abort("determinant error-bound setup")
213+
.or_abort("determinant error-bound setup");
214+
black_box(bound);
215+
group.bench_function("det_errbound", |bencher| {
216+
bencher.iter(|| {
217+
let bound = black_box(input.matrix())
218+
.det_errbound()
219+
.or_abort("f64 determinant error bound")
220+
.or_abort("f64 determinant error bound");
221+
black_box(bound);
222+
});
223+
});
224+
}
225+
226+
/// Add the paired direct-determinant and certified-bound baseline.
227+
#[cfg(not(la_stack_v0_4_3_api))]
228+
fn bench_det_direct_with_errbound<const D: usize>(
229+
group: &mut BenchmarkGroup<'_, WallTime>,
230+
input: &ValidatedExactInput<D>,
231+
) {
232+
let estimate = input
233+
.matrix()
234+
.det_direct_with_errbound()
235+
.or_abort("paired determinant-bound setup")
236+
.or_abort("paired determinant-bound setup");
237+
black_box((estimate.determinant(), estimate.absolute_error_bound()));
238+
group.bench_function("det_direct_with_errbound", |bencher| {
239+
bencher.iter(|| {
240+
let estimate = black_box(input.matrix())
241+
.det_direct_with_errbound()
242+
.or_abort("paired f64 determinant and error bound")
243+
.or_abort("paired f64 determinant and error bound");
244+
black_box((estimate.determinant(), estimate.absolute_error_bound()));
245+
});
246+
});
247+
}
248+
249+
macro_rules! register_det_filter_benchmarks {
204250
($group:expr, $input:expr, supported) => {{
205251
bench_det_direct(&mut $group, &$input);
252+
#[cfg(not(la_stack_v0_4_3_api))]
253+
bench_det_direct_with_errbound(&mut $group, &$input);
254+
bench_det_errbound(&mut $group, &$input);
206255
}};
207256
($group:expr, $matrix:expr, unsupported) => {};
208257
}
@@ -227,7 +276,7 @@ macro_rules! gen_exact_benches_for_dim {
227276
});
228277
});
229278

230-
register_det_direct_benchmark!(group, input, $direct);
279+
register_det_filter_benchmarks!(group, input, $direct);
231280

232281
for &operation in GENERAL_OPERATIONS {
233282
bench_exact_operation(&mut group, operation, &input);

benches/vs_linalg.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@
66
//! fixed dimensions.
77
//!
88
//! Notes:
9-
//! - Determinant is benchmarked via LU on all sides (nalgebra uses closed-forms for 1×1/2×2/3×3).
9+
//! - Determinant groups distinguish factorization-inclusive LU, `Matrix::det`,
10+
//! precomputed LU determinant queries, and precomputed LDLT/Cholesky queries.
1011
//! - Matrix infinity norm is the maximum absolute row sum on all sides.
1112
1213
use std::hint::black_box;

docs/BENCHMARKING.md

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,9 @@ factorization in the dependency version used here.
5656
**`exact`** (`benches/exact.rs`) measures exact-arithmetic methods
5757
(`det_exact`, `solve_exact`, `det_sign_exact`, strict `*_result` conversions,
5858
and lossy `*_rounded_f64` conversions) alongside the f64 `det` baseline across
59-
D=2-5 and `det_direct` across its supported D=2-4 range. Use this suite to
60-
understand exact-arithmetic cost and track optimization progress.
59+
D=2-5. Its supported D=2-4 range also includes `det_direct`, the paired
60+
`det_direct_with_errbound`, and the bound-only `det_errbound`. Use this suite
61+
to understand exact-arithmetic cost and track optimization progress.
6162

6263
## Common Workflows
6364

@@ -91,6 +92,11 @@ at warning for both revisions because the current manifest's lint policy may
9192
reject historical source that predates a lint, even though that source remains
9293
valid benchmark input.
9394

95+
The paired `det_direct_with_errbound` API postdates v0.4.3, so its D=2-4
96+
baseline rows remain explicitly unavailable in that comparison. The older
97+
bound-only `det_errbound` API is source-compatible and remains a required
98+
shared-harness baseline.
99+
94100
The v0.4.3 LU/LDLT balanced-range determinant paths return an incorrect zero,
95101
so their two D=8 stress rows are deliberately not timed as baselines. Reports
96102
leave those baselines explicitly unavailable rather than presenting invalid
@@ -179,7 +185,7 @@ coverage or provenance aborts publication. Use `--allow-partial` only for
179185
exploratory CSV/SVG output; it cannot update README and its sidecar explicitly
180186
marks measurement provenance unavailable.
181187

182-
See `scripts/criterion_dim_plot.py --help` for plotting options.
188+
See `uv run --locked criterion-dim-plot --help` for plotting options.
183189

184190
### Create The Release Performance Report
185191

@@ -247,6 +253,9 @@ The README table uses `median.point_estimate` in nanoseconds. Lower is better,
247253
but point-estimate ratios alone are descriptive and do not establish a
248254
statistically supported performance difference. Preserve Criterion confidence
249255
intervals or repeat controlled runs when making a stronger claim.
256+
For experimental-design background on controlled repetitions and uncertainty,
257+
see [REFERENCES.md](../REFERENCES.md) \[13\]; these workflows do not claim to
258+
implement every recommendation in that study.
250259

251260
All three crates receive equivalent deterministic inputs for a given dimension:
252261

@@ -341,7 +350,8 @@ Before timing begins, every fixed, adversarial, and corpus input is consumed int
341350
a private-field `ValidatedExactInput` after checks by an independent exact
342351
oracle. Timed and registration helpers accept only that proof-bearing wrapper. A
343352
factorial-time Leibniz determinant over exact rational reconstructions verifies
344-
determinant values and signs; exact residuals verify `A x = b`; and
353+
determinant values and signs, including each direct determinant's certified
354+
absolute bound; exact residuals verify `A x = b`; and
345355
strict/rounded binary64 results are checked for their exact bits, typed reason,
346356
and first failing component. These checks run outside timed Criterion closures.
347357
Any disagreement or unexpected error fails setup instead of becoming an

0 commit comments

Comments
 (0)