Expand description
Outward-rounded interval expressions and determinant signs.
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.