Skip to main content

Module intervals

Module intervals 

Source
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.