Module linalg_certify 

Kernel-certified linear algebra: turn an exact solve into a KERNEL-CHECKED PROOF TERM.

crate::linalg solves A·x = b exactly over ℚ and re-checks the residual. This module goes one level deeper: it emits, for each row, an honest kernel proof term of type Eq Int lhsᵢ rhsᵢ, where the row identity Σⱼ Aᵢⱼ·xⱼ = bᵢ has been cleared of denominators to an INTEGER identity

bdᵢ · (Σⱼ Anᵢⱼ · Xnⱼ)  =  Da_i · Dx · bnᵢ

and proven by the ring-axiom oracle crate::arith::prove_int_eq, then RE-CHECKED by the kernel’s own infer_type. This is the same trust path the kernel’s Gödel/Chaitin theorems ride: the oracle is untrusted search, the kernel is the judge. A false identity is unprovable (the oracle returns None) and a forged proof fails the type-check — fail-closed. The current arith oracle is i64-wide, so systems whose cleared integers exceed i64 return None (an honest limit, not a wrong answer; a BigInt oracle would lift it).

Structs

SystemCert

The complete certificate that a linear system A·x = b has a UNIQUE exact solution: the exact x, a kernel proof of Aᵢ·x = bᵢ for every row, and a kernel proof that det A ≠ 0 (so the solution is unique, not merely one of many). Every term is re-checked by the kernel. This is the full “prove, not just run” object for a linear system. None iff singular or past the i64 width.

Functions

certify_system

Solve and produce the complete unique-solution certificate.

prove_dot

Prove the dot-product identity Σₖ psₖ·qsₖ = r as ONE kernel-checked term (type Eq Int lhs rhs). Clears denominators to rd·Σₖ (Pnₖ·Qnₖ) = Dp·Dq·rn — structure preserved — proves it with the untrusted oracle, then RE-CHECKS with the kernel. None if false or past i64. This one identity underlies every certificate below: a solve is a row·x = b, a factorization entry is Lrow·Ucol = (PA)ᵢⱼ, an inverse entry is Arow·(A⁻¹col) = Iᵢⱼ.

prove_inverse

Invert A and PROVE it in the kernel: every entry of A·A⁻¹ = I is a dot-product proof Aᵢ·(A⁻¹)ⱼ = Iᵢⱼ (the off-diagonal = 0 identities are proven too). None iff singular / past i64.

prove_lu

Factor A and PROVE the factorization in the kernel: every entry of P·A = L·U is a dot-product proof Lᵢ·Uⱼ = (PA)ᵢⱼ. Returns the exact factorization and an n×n grid of kernel-checked terms.

prove_nonzero

Prove r ≠ 0 in the kernel by EXHIBITING its inverse: a kernel-checked proof of r·(1/r) = 1. A value with a multiplicative inverse is nonzero, so this certifies nonsingularity when applied to a determinant. None iff r == 0 — correctly unprovable, since 0 has no inverse.

prove_solution

Prove A·x = b for a GIVEN candidate x, one kernel-checked proof term per row (each is the row dot-product identity Aᵢ·x = bᵢ). None if any row is false (fail-closed) or past i64.

prove_solve

Solve A·x = b exactly and hand back the exact x together with a kernel-checked proof that it solves the system (one proof term per row). None iff singular or beyond the i64 oracle width.

ring_context

A kernel context of its own carrying the ring/field/order axioms the oracle proves against: a copy-on-write clone of the standard library’s one registration.