Module certified 

Certified dot products and affine differences.

Vector::dot_with_errbound() evaluates the same left-to-right FMA tree as Vector::dot() and returns its estimate together with a certified absolute roundoff bound. Vector::dot_difference_with_errbound() directly evaluates

Σᵢ axis[i] × (left[i] - right[i])

as two FMAs per coordinate. It does not first round left - right into a new Vector, so the certificate covers the intended expression over the original stored binary64 coordinates.

The opaque ScalarWithErrorBound exposes the estimate, absolute error bound, and finite outward-rounded lower and upper bounds. Those endpoints support positive, negative, and caller-selected threshold proofs:

A certified dot-product sign

use la_stack::prelude::*;

let axis = Vector::<5>::try_new([2.0, -1.0, 3.0, 1.0, -2.0])?;
let point = Vector::<5>::try_new([4.0, 1.0, 2.0, 3.0, 1.0])?;
let positive = axis.dot_with_errbound(&point)?.and_then(|value| {
    if value.lower_bound() > 0.0 {
        Some(true)
    } else if value.upper_bound() <= 0.0 {
        Some(false)
    } else {
        None // An enclosure overlapping zero is inconclusive.
    }
});
assert_eq!(positive, Some(true));

An affine threshold test

use la_stack::prelude::*;

fn is_separated<const D: usize>(
    axis: &Vector<D>,
    left: &Vector<D>,
    right: &Vector<D>,
    threshold: f64,
) -> Result<Option<bool>, LaError> {
    let Some(value) = axis.dot_difference_with_errbound(left, right)? else {
        return Ok(None);
    };
    if value.lower_bound() > threshold {
        Ok(Some(true))
    } else if value.upper_bound() <= threshold {
        Ok(Some(false))
    } else {
        Ok(None)
    }
}

let axis = Vector::<2>::try_new([2.0, -1.0])?;
let left = Vector::<2>::try_new([4.0, 1.0])?;
let right = Vector::<2>::try_new([1.0, 3.0])?;
assert_eq!(is_separated(&axis, &left, &right, 1.0)?, Some(true));

An interval that overlaps the threshold is inconclusive, not equal. Likewise, Ok(None) means gradual underflow or proof-only range exhaustion prevented a certificate. A filtered-exact caller should rebuild the same dot or affine expression in BigRational (available through the exact feature) or another exact backend. A LaError::NonFinite instead reports that the specified FMA estimate itself overflowed. These certified bounds describe roundoff in a fixed arithmetic tree; they are distinct from user-selected numerical tolerances.