feat: Add certified dot-product and linear-form bounds

[acgetchell]

Summary

Add certified absolute error bounds for fixed-vector dot products and affine
linear forms, so callers can prove a sign or inequality in the fast f64 path
and explicitly fall back when the bound is inconclusive.

This issue is deliberately separate from both Euclidean norm calculation and
interval-matrix determinant signs. It owns one linear reduction contract and
can be implemented, benchmarked, and audited independently.

Downstream motivation: delaunay

Delaunay's Level 4 simplex-intersection fast path currently hand-codes a
conservative lower bound for axis . (left - right). It tracks product
overflow and underflow, a deterministic FMA accumulation, the magnitude sum,
and a gamma-style roundoff coefficient before accepting a separating-axis
certificate.

That is reusable fixed-vector numerical linear algebra. Delaunay should retain
the geometric meaning of the axis and the threshold comparison, while
la-stack owns the rounded reduction and its proof.

Requested contract

The API should expose a proof-bearing result rather than a caller-computed
tolerance. One possible shape is:

pub struct ScalarWithErrorBound {
    // private fields
}

impl ScalarWithErrorBound {
    pub const fn estimate(self) -> f64;
    pub const fn absolute_error_bound(self) -> f64;
    pub const fn lower_bound(self) -> f64;
    pub const fn upper_bound(self) -> f64;
}

impl<const D: usize> Vector<D> {
    pub fn dot_with_errbound(
        &self,
        other: &Self,
    ) -> Result<Option<ScalarWithErrorBound>, LaError>;
}

An additional dot_difference_with_errbound(axis, left, right) or general
small affine-linear-form API is desirable if it can compute the intended
arithmetic tree directly, without first rounding left - right into a new
Vector. The exact names can vary.

The operation should:

• bind the estimate and its matching absolute error bound in one result;
• document the exact arithmetic tree and deterministic accumulation order;
• return Ok(None) when gradual underflow or another range condition prevents
  the proof while the finite inputs remain valid;
• return a typed LaError for non-finite computed results;
• let callers prove positive, negative, or threshold-separated results without
  treating an inconclusive bound as equality;
• remain allocation-free and available without the exact feature.

Acceptance criteria

• Property tests compare the bounded interval with an independent exact
  BigRational dot/linear-form oracle through dimensions used downstream.
• Tests cover cancellation, exact zero, signed zero, subnormal products,
  overflow, mixed magnitudes, and both conclusive and inconclusive bounds.
• The affine difference form is verified against the exact expression
  sum_i axis_i * (left_i - right_i), not merely against already-rounded
  coordinate differences.
• Focused benchmarks cover well-separated hot cases and inconclusive boundary
  cases, and compare with the current plain Vector::dot where meaningful.
• Documentation explains filtered-exact composition and distinguishes a
  certified roundoff bound from a user-selected numerical tolerance.

Downstream cleanup enabled

After release, Delaunay can remove
certified_dot_difference_lower_bound and product_underflowed from its exact
simplex-intersection implementation, while retaining the geometric separating-
axis decision and exact fallback.