Module linalg 

Exact linear algebra over ℚ — the certified core of the LOGOS numerical stack.

Floating-point LAPACK runs a solve; this proves one. Every entry is an exact BigInt-backed Rational, so A·x = b is decided as an EXACT identity — the residual is identically zero, not “close enough” — and det A ≠ 0 certifies nonsingularity outright. These are the primitives the proof engine reasons about, and they are FAIL-CLOSED in the same discipline as the mod-p / SoS routes: the certificate (residual_zero) is an independent re-multiplication, never trust in the solver. An ill-conditioned system (e.g. a Hilbert matrix) that floating point cannot solve to zero residual is solved here EXACTLY, and the exactness is a checkable fact.

Structs

Certified

A solve carrying its own certificate: the exact solution plus independently re-checked flags that A·x = b holds exactly and det A ≠ 0. This is what “prove, not just run” means for a solve.

Lu

An exact LU factorization P·A = L·U: perm is the row permutation (P), l is unit lower-triangular, u is upper-triangular. None iff singular.

Functions

certify_solve

Solve and certify in one call. None iff singular.

det

Exact determinant via forward elimination (product of pivots × permutation sign).

identity

The exact n×n identity matrix.

inverse

Exact matrix inverse via Gauss–Jordan on [A | I]. None iff singular.

is_inverse

Is A·B == I exactly? (independent re-check behind a certified inverse)

lu

Exact LU with partial (nonzero) pivoting. Every multiplier is an exact rational.

lu_is_exact

Certify a factorization: is P·A == L·U exactly? (P·A is A with its rows permuted by perm.)

matmul

Exact matrix product A·B.

matvec

A·x over the rationals, computed exactly.

rank

Exact rank (works for rectangular matrices) via row reduction — the number of nonzero pivots.

residual_is_zero

Is A·x == b exactly, component by component? The independent re-check behind a certified solve.

solve

Solve A·x = b exactly by Gauss–Jordan elimination with nonzero pivoting (n×n). Returns None iff A is singular. All arithmetic is exact — the answer 1/3 stays 1/3.

transpose

Exact transpose.