docs: add runnable examples and link interval proofs

README.md

@@ -238,9 +238,11 @@ for the full contracts.
 
 ¹ Requires `features = ["exact"]`.
 
-For tested usage examples, see [exact dot products and column selection][guide-exact-reductions],
-[interval division and solution enclosures][guide-intervals], and the runnable
-[polynomial determinant example][example-polynomial].
+For tested usage, see the guides to [exact dot products and column selection][guide-exact-reductions]
+and [interval division and solution enclosures][guide-intervals]. Runnable workflows cover
+[column selection][example-column-basis], [interval solves][example-interval-solve],
+[exact rational solves and objectives][example-rational-input], and
+[polynomial determinants][example-polynomial].
 
 [api-reference]: https://docs.rs/la-stack/latest/la_stack/
 [api-guide]: https://docs.rs/la-stack/latest/la_stack/guide/index.html
@@ -457,22 +459,26 @@ for current release planning.
 
 The `examples/` directory contains small, runnable programs:
 
+- **[`column_basis`][example-column-basis]** — select columns of a rectangular matrix and handle partial numerical rank
 - **[`const_det_4x4`][example-const-det]** — compile-time 4×4 determinant via `det_direct()`
 - **[`det_5x5`][example-det]** — determinant of a 5×5 matrix via LU
 - **[`exact_det_3x3`][example-exact-det]** — exact determinant value of a near-singular 3×3 matrix (requires `exact` feature)
 - **[`exact_sign_3x3`][example-exact-sign]** — exact determinant sign of a near-singular 3×3 matrix (requires `exact` feature)
 - **[`exact_solve_3x3`][example-exact-solve]** — exact solve of a near-singular 3×3 system vs f64 LU (requires `exact` feature)
+- **[`interval_solve`][example-interval-solve]** — divide by a zero-free interval, enclose all admitted solutions, and identify when fallback is required
 - **[`ldlt_solve_3x3`][example-ldlt-solve]** — solve a 3×3 symmetric positive definite system via LDLT
 - **[`polynomial_determinant`][example-polynomial]** — exact cancellation, leading coefficients, and explicit work limits (requires `exact` feature)
-- **[`rational_input_5x5`][example-rational-input]** — exact rational solve of a 5×5 system that becomes singular as f64 (requires `exact` feature)
+- **[`rational_input_5x5`][example-rational-input]** — exact solve and rational dot products for a system that becomes singular as f64 (requires `exact`)
 - **[`solve_5x5`][example-solve]** — solve a 5×5 system via LU with partial pivoting
 - **[`vector_angles`][example-vector-angles]** — unsigned angles for fixed vectors and borrowed slices, including extreme magnitudes and subnormal separations
 
+[example-column-basis]: https://github.com/acgetchell/la-stack/blob/main/examples/column_basis.rs
 [example-const-det]: https://github.com/acgetchell/la-stack/blob/main/examples/const_det_4x4.rs
 [example-det]: https://github.com/acgetchell/la-stack/blob/main/examples/det_5x5.rs
 [example-exact-det]: https://github.com/acgetchell/la-stack/blob/main/examples/exact_det_3x3.rs
 [example-exact-sign]: https://github.com/acgetchell/la-stack/blob/main/examples/exact_sign_3x3.rs
 [example-exact-solve]: https://github.com/acgetchell/la-stack/blob/main/examples/exact_solve_3x3.rs
+[example-interval-solve]: https://github.com/acgetchell/la-stack/blob/main/examples/interval_solve.rs
 [example-ldlt-solve]: https://github.com/acgetchell/la-stack/blob/main/examples/ldlt_solve_3x3.rs
 [example-polynomial]: https://github.com/acgetchell/la-stack/blob/main/examples/polynomial_determinant.rs
 [example-rational-input]: https://github.com/acgetchell/la-stack/blob/main/examples/rational_input_5x5.rs
@@ -482,12 +488,15 @@ The `examples/` directory contains small, runnable programs:
 ```bash
 just examples
 # or individually:
+cargo run --locked --example column_basis
 cargo run --example const_det_4x4
 cargo run --example det_5x5
 cargo run --features exact --example exact_det_3x3
 cargo run --features exact --example exact_sign_3x3
 cargo run --features exact --example exact_solve_3x3
+cargo run --locked --example interval_solve
 cargo run --example ldlt_solve_3x3
+cargo run --locked --features exact --example polynomial_determinant
 cargo run --features exact --example rational_input_5x5
 cargo run --example solve_5x5
 cargo run --locked --example vector_angles

docs/code_organization.md

@@ -116,10 +116,16 @@ The [Cargo manifest](../Cargo.toml) owns feature and dependency declarations.
 - `tooling/examples.toml` owns the Cargo example package, feature overrides and
   time budgets. The shared runner discovers every binary example from metadata;
   executable numerical assertions stay in `examples/`.
-- `examples/vector_angles.rs` demonstrates fixed-vector and borrowed-slice angles,
-  independent magnitude scaling, and subnormal separations.
+- `examples/column_basis.rs` demonstrates full and partial rectangular column
+  selections with explicit absolute tolerances and a rank check before extracting a minor.
+- `examples/interval_solve.rs` demonstrates zero-free division and reciprocals,
+  an analytical solution enclosure, and the two typed solve fallback cases.
 - `examples/polynomial_determinant.rs` demonstrates exact cancellation, borrowed
   leading coefficients and typed work-budget exhaustion.
+- `examples/rational_input_5x5.rs` demonstrates an exact rational solve and exact
+  objective evaluation with prepared vectors and checked borrowed slices.
+- `examples/vector_angles.rs` demonstrates fixed-vector and borrowed-slice angles,
+  independent magnitude scaling, and subnormal separations.
 
 Use [Testing guidance](dev/testing.md) for dimension coverage and test design,
 and [Documentation guidance](dev/docs.md) for executable-example ownership.

examples/column_basis.rs

@@ -0,0 +1,36 @@
+#![forbid(unsafe_code)]
+
+//! Select a provisional column basis from a rectangular matrix.
+//!
+//! See the [exact certification workflow](https://docs.rs/la-stack/latest/la_stack/guide/exact/index.html#exact-reductions-and-provisional-column-selection)
+//! for applications that need a proof about the selected minor.
+
+use std::array::from_fn;
+
+use la_stack::prelude::*;
+
+fn main() -> Result<(), LaError> {
+    // Column 0 is zero, column 2 is twice column 1, and column 3 adds a
+    // nonzero second coordinate. The expected basis uses columns 1 and 3.
+    let rows = [[0.0, 4.0, 8.0, 1.0], [0.0, 0.0, 0.0, 2.0]];
+    let basis = column_basis(&rows, Tolerance::try_new(1e-12)?)?;
+
+    // Check for full numerical row rank before extracting a square minor.
+    // Even at zero tolerance the rank is provisional because elimination rounds.
+    assert_eq!(basis.rank(), rows.len());
+    let columns = basis.columns();
+    assert_eq!(columns, &[1, 3]);
+    let minor = Matrix::<2>::try_from_rows(rows.map(|row| from_fn(|c| row[columns[c]])))?;
+    assert_eq!(minor.det()?.to_bits(), 8.0_f64.to_bits());
+    println!("Selected columns: {columns:?}");
+
+    // The absolute tolerance 2 rejects the second pivot (equal to 2).
+    // The partial selection describes this threshold's decision. The same
+    // input still has a nonzero 2×2 minor with determinant 8.
+    let partial = column_basis(&rows, Tolerance::try_new(2.0)?)?;
+    assert_eq!(partial.rank(), 1);
+    assert_eq!(partial.columns(), &[1]);
+    println!("Selected columns with tolerance 2: {:?}", partial.columns());
+
+    Ok(())
+}

examples/interval_solve.rs

@@ -0,0 +1,59 @@
+#![forbid(unsafe_code)]
+
+//! Divide by a zero-free interval and enclose the solutions of an interval system.
+
+use la_stack::prelude::*;
+
+fn main() -> Result<(), LaError> {
+    let divisor = Interval::try_new(2.0, 4.0)?;
+    assert_eq!(divisor.try_recip()?, Interval::try_new(0.25, 0.5)?);
+    let quotient = Interval::try_new(4.0, 8.0)?.try_div(&divisor)?;
+    assert_eq!(quotient, Interval::try_new(1.0, 4.0)?);
+
+    // For every a ∈ [2, 4] and b ∈ [6, 10], the equations a*x + y = b
+    // and 2*y = 4 have a unique solution with y = 2 and x = (b - 2)/a.
+    let two = Interval::point(2.0)?;
+    let matrix = IntervalMatrix::from_rows([[divisor, Interval::ONE], [Interval::ZERO, two]]);
+    let rhs = [Interval::try_new(6.0, 10.0)?, Interval::point(4.0)?];
+    let solution = matrix.solve(&rhs)?;
+    assert_eq!(solution, [Interval::try_new(1.0, 4.0)?, two]);
+    println!("Solution enclosure for every admitted system: {solution:?}");
+
+    // Direct division rejects a supplied divisor containing zero. A solve
+    // instead reports when elimination cannot certify a pivot.
+    let crosses_zero = Interval::try_new(-1.0, 1.0)?;
+    assert!(matches!(
+        Interval::ONE.try_div(&crosses_zero),
+        Err(LaError::IntervalZeroDivisor {
+            lower: -1.0,
+            upper: 1.0,
+            ..
+        })
+    ));
+
+    // The exact determinant is 3 × 2^-52. Rounding in elimination can still
+    // leave the final pivot enclosing zero.
+    let regular = IntervalMatrix::try_from_point_rows([[3.0, 3.0], [1.0, 1.0_f64.next_up()]])?;
+    match regular.solve(&[Interval::ONE; 2]) {
+        Err(LaError::IntervalSolveInconclusive { pivot_col, .. }) => {
+            assert_eq!(pivot_col, 1);
+            println!("Pivot {pivot_col} is inconclusive. Use a certified fallback.");
+        }
+        Err(error) => return Err(error),
+        Ok(bounds) => panic!("expected an inconclusive pivot, got {bounds:?}"),
+    }
+
+    // Here the unique real solution is 2 × f64::MAX, outside the finite
+    // endpoint range. A certified fallback needs a wider representation.
+    let small_pivot = IntervalMatrix::try_from_point_rows([[0.5]])?;
+    match small_pivot.solve(&[Interval::point(f64::MAX)?]) {
+        Err(LaError::IntervalRangeExhausted { operation, .. }) => {
+            assert_eq!(operation, ArithmeticOperation::IntervalSolve);
+            println!("Finite endpoint range exhausted. Use a certified fallback.");
+        }
+        Err(error) => return Err(error),
+        Ok(bounds) => panic!("expected finite endpoint range exhaustion, got {bounds:?}"),
+    }
+
+    Ok(())
+}

examples/rational_input_5x5.rs

@@ -1,6 +1,8 @@
 #![forbid(unsafe_code)]
 
-//! Solve a rational 5×5 system that becomes singular after conversion to binary64.
+//! Solve a rational 5×5 system and evaluate an exact linear objective.
+//!
+//! The reconstructed binary64 system is singular.
 
 use la_stack::prelude::*;
 
@@ -34,6 +36,32 @@ fn main() -> Result<(), LaError> {
     println!("exact determinant sign: {:?}", matrix.det_sign());
     println!("exact solution: {:?}", exact_solution.as_array());
 
+    let objective = RationalVector::try_new([
+        BigRational::new(1.into(), 3.into()),
+        BigRational::new(1.into(), 2.into()),
+        BigRational::from_integer(0.into()),
+        BigRational::from_integer(0.into()),
+        BigRational::new(1.into(), 4.into()),
+    ])?;
+    // For the known solution [1, -1, 2, 3, 4], the objective is 1/3 - 1/2 + 1.
+    let expected = BigRational::new(5.into(), 6.into());
+    let value = objective.dot(&exact_solution);
+    assert_eq!(value, expected);
+
+    // Borrowed slices support runtime lengths and check shape and denominators.
+    let weights = objective.as_array().as_slice();
+    let values = exact_solution.as_array().as_slice();
+    assert_eq!(rational_dot(weights, values)?, expected);
+    assert!(matches!(
+        rational_dot(weights, &values[..4]),
+        Err(LaError::DimensionMismatch {
+            left: 5,
+            right: 4,
+            ..
+        })
+    ));
+    println!("exact objective: {value}");
+
     let epsilon_f64 = epsilon.try_to_f64()?;
     assert_eq!((1.0 + epsilon_f64).to_bits(), 1.0_f64.to_bits());
     let f64_matrix = Matrix::<5>::try_from_rows([

pyproject.toml

@@ -185,7 +185,7 @@ exclude = [ "docs/archive/**", "docs/performance/**", "docs/performance-runs/**"
 path = "README.md"
 pattern = 'https://(?:github\.com/acgetchell/la-stack/(?:blob|raw|tree)/|raw\.githubusercontent\.com/acgetchell/la-stack/)(?P<value>main|v[0-9]+\.[0-9]+\.[0-9]+|[0-9a-f]{7,40})/[^\s)\]>"?]+'
 value = "main"
-count = 42
+count = 44
 exclude = '/docs/(?:assets/bench|performance-runs)/'
 
 [[tool.research-repo-tools.release.rules]]