Summary
Add a small fixed-dimension, outward-rounded interval matrix surface with a
division-free determinant-sign query that returns positive, negative, zero, or
inconclusive evidence without pretending an inconclusive interval is an exact
result.
This is not a request for a generic alternate scalar family or a broad interval
arithmetic package. It is a proof-bearing f64 boundary for the small,
robustness-sensitive reductions already central to la-stack's computational
geometry use case.
Downstream motivation: delaunay
Delaunay currently owns a private F64Interval plus subset-DP determinant
evaluator for the relative-coordinate lifted in-sphere matrix. The entries are
derived by subtraction and squaring, so Matrix::det_direct_with_errbound()
cannot certify the exact-real expression after those operations have already
been rounded to single f64 entries.
This is reusable bounded floating-point mathematics, not Delaunay topology or
predicate classification. Delaunay should continue to assemble its geometric
expressions and interpret signs as Orientation/InSphere; la-stack should
own the outward rounding and small determinant proof. Certified dot-product and
linear-form bounds are deliberately tracked separately so the two APIs can be
implemented and audited independently.
This proposal does not replace exact fallbacks. It centralizes a sound fast
filter and returns inconclusive at the boundary.
Requested contract
The exact API can vary, but it should provide proof-bearing equivalents of:
- construct a point interval for a finite
f64;
- enclose an exact-real subtraction of two finite
f64 values;
- outward-rounded addition, multiplication, negation, and square;
- inspect lower and upper bounds without allowing callers to create inverted or
non-finite intervals;
- compute the sign of a small square interval-matrix determinant using a
division-free algorithm through at least dimension 7;
- distinguish
Positive, Negative, Zero, and Inconclusive rather than
coercing overlap with zero into equality;
- surface range failure explicitly so callers can proceed to exact arithmetic.
The core types should remain fixed-size and stack-backed. A dedicated
Interval/IntervalMatrix<D> or narrowly named bounded-result types are both
acceptable; making Matrix<D> generic over arbitrary scalars is not required.
Numerical requirements
- Every successful interval must contain the exact-real result of the stated
operation on its binary64 inputs.
- Underflow, overflow, subnormal values, cancellation, and signed zero need
explicit documented behavior.
- The determinant algorithm must avoid unsound interval division around a zero-
containing pivot; a Leibniz/subset-DP expansion or another justified
division-free method is appropriate for these small dimensions.
- Inconclusive evidence must be cheap to detect and must never be published as
an exact sign.
Acceptance criteria
- Property tests compare interval containment and sign decisions with an
independent BigRational oracle through the supported dimensions.
- Adversarial tests cover cancellation, exact zero, subnormal products,
overflow, wide intervals, row swaps, and singular matrices.
- Benchmarks cover conclusive and inconclusive determinant workloads
representative of downstream geometric filters.
- Documentation keeps the bounded
f64 surface distinct from the exact
feature and explains the expected filtered-exact composition.
Downstream cleanup enabled
After release, Delaunay can remove its local F64Interval and interval
determinant DP while retaining geometric matrix assembly, exact rational
fallback, and semantic predicate enums.
Summary
Add a small fixed-dimension, outward-rounded interval matrix surface with a
division-free determinant-sign query that returns positive, negative, zero, or
inconclusive evidence without pretending an inconclusive interval is an exact
result.
This is not a request for a generic alternate scalar family or a broad interval
arithmetic package. It is a proof-bearing
f64boundary for the small,robustness-sensitive reductions already central to
la-stack's computationalgeometry use case.
Downstream motivation:
delaunayDelaunay currently owns a private
F64Intervalplus subset-DP determinantevaluator for the relative-coordinate lifted in-sphere matrix. The entries are
derived by subtraction and squaring, so
Matrix::det_direct_with_errbound()cannot certify the exact-real expression after those operations have already
been rounded to single
f64entries.This is reusable bounded floating-point mathematics, not Delaunay topology or
predicate classification. Delaunay should continue to assemble its geometric
expressions and interpret signs as
Orientation/InSphere;la-stackshouldown the outward rounding and small determinant proof. Certified dot-product and
linear-form bounds are deliberately tracked separately so the two APIs can be
implemented and audited independently.
This proposal does not replace exact fallbacks. It centralizes a sound fast
filter and returns inconclusive at the boundary.
Requested contract
The exact API can vary, but it should provide proof-bearing equivalents of:
f64;f64values;non-finite intervals;
division-free algorithm through at least dimension 7;
Positive,Negative,Zero, andInconclusiverather thancoercing overlap with zero into equality;
The core types should remain fixed-size and stack-backed. A dedicated
Interval/IntervalMatrix<D>or narrowly named bounded-result types are bothacceptable; making
Matrix<D>generic over arbitrary scalars is not required.Numerical requirements
operation on its binary64 inputs.
explicit documented behavior.
containing pivot; a Leibniz/subset-DP expansion or another justified
division-free method is appropriate for these small dimensions.
an exact sign.
Acceptance criteria
independent
BigRationaloracle through the supported dimensions.overflow, wide intervals, row swaps, and singular matrices.
representative of downstream geometric filters.
f64surface distinct from theexactfeature and explains the expected filtered-exact composition.
Downstream cleanup enabled
After release, Delaunay can remove its local
F64Intervaland intervaldeterminant DP while retaining geometric matrix assembly, exact rational
fallback, and semantic predicate enums.