Expand description
Outward-rounded interval expressions, determinant signs, and solutions.
Interval encloses expression construction that has not yet been reduced to a
single stored f64. Point intervals preserve finite binary64 values exactly;
try_from_subtraction, try_add, try_mul, negate, and try_square enclose
the corresponding exact-real operations. IntervalMatrix<D>::det_sign() then
uses a division-free subset expansion through D=7, returning positive,
negative, zero, or inconclusive evidence.
use la_stack::prelude::*;
fn main() -> Result<(), LaError> {
// Relative coordinates and the lifted norm retain their construction error.
let x = Interval::try_from_subtraction(0.1, 0.0)?;
let y = Interval::try_from_subtraction(0.1, 0.0)?;
let z = Interval::try_from_subtraction(0.1, 0.0)?;
let lifted = x
.try_square()?
.try_add(&y.try_square()?)?
.try_add(&z.try_square()?)?;
let matrix = IntervalMatrix::<4>::from_rows([
[Interval::ONE, Interval::ZERO, Interval::ZERO, Interval::ONE],
[Interval::ZERO, Interval::ONE, Interval::ZERO, Interval::ONE],
[Interval::ZERO, Interval::ZERO, Interval::ONE, Interval::ONE],
[x, y, z, lifted],
]);
assert_eq!(
matrix.det_sign()?,
IntervalDeterminantSign::Negative,
);
Ok(())
}Every successful interval keeps finite ordered endpoints. Subnormal bounds are
preserved, both signed zeros are treated as real zero and canonicalized to
+0.0, and underflowed nonzero products widen toward the least subnormal value.
If an exact result range cannot fit between finite binary64 endpoints, the
operation returns LaError::IntervalRangeExhausted with its interval operation
recorded in ArithmeticOperation.
Positive, Negative, and Zero are proofs. Inconclusive only means that
the determinant enclosure overlaps zero; it must not be converted to equality
or singularity. A filtered-exact caller should rebuild the same derived
expression with RationalMatrix and call det_sign() when the interval result
is inconclusive or reports range failure. Lifting a finished Matrix with
IntervalMatrix::from_matrix encloses its stored entries, but cannot recover
rounding that occurred while those entries were assembled.
Interval::try_recip and
Interval::try_div require a divisor excluding
zero. They return LaError::IntervalZeroDivisor otherwise. Direct division
can enclose tiny/tiny even when a reciprocal intermediate would overflow.
IntervalMatrix::solve takes a borrowed
[Interval; D] RHS. Every successful component encloses the corresponding
exact-real solution for every matrix and RHS admitted by the intervals;
success also certifies that every admitted matrix is nonsingular. The
Gaussian elimination uses outward arithmetic throughout, choosing each
pivot by its minimum distance from zero. Width and ill-conditioning can
make this test inconclusive even for invertible point matrices. All const
dimensions are supported with O(D²) stack storage; D=0 returns [].
use la_stack::prelude::*;
fn main() -> Result<(), LaError> {
let matrix = IntervalMatrix::try_from_point_rows([[3.0, 1.0], [1.0, 2.0]])?;
let rhs = [Interval::try_new(3.9, 4.1)?, Interval::point(3.0)?];
// A consumer may map these two failures to its exhaustive fallback.
let enclosure = match matrix.solve(&rhs) {
Ok(bounds) => Some(bounds),
Err(LaError::IntervalSolveInconclusive { .. }
| LaError::IntervalRangeExhausted { .. }) => None,
Err(error) => return Err(error),
};
assert!(enclosure.is_some_and(|bounds|
bounds[0].contains(1.0) && bounds[1].contains(1.0)));
Ok(())
}IntervalSolveInconclusive never proves singularity, including a final
pivot of [0, 0]. Finite-range exhaustion also leaves the solve uncertified.
Invalid raw endpoints are rejected by constructors. Geometry-specific
equation assembly, radius calculations, coordinate boxes, and broad-phase
fallback policy remain the consumer’s responsibility.