Function prove_solution 

pub fn prove_solution(
    ctx: &Context,
    a: &[Vec<Rational>],
    x: &[Rational],
    b: &[Rational],
) -> Option<Vec<Term>>

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.