Function prove_dot 

pub fn prove_dot(
    ctx: &Context,
    ps: &[Rational],
    qs: &[Rational],
    r: &Rational,
) -> Option<Term>

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ᵢⱼ.