Skip to main content

Module intervals

Module intervals 

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