Struct SystemCert 

pub struct SystemCert {
    pub x: Vec<Rational>,
    pub solve_proofs: Vec<Term>,
    pub det: Rational,
    pub nonsingular_proof: Term,
}

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.

Fields

x: Vec<Rational>

solve_proofs: Vec<Term>

det: Rational

nonsingular_proof: Term