pub fn verify_lia(goal: &Syn) -> boolExpand description
try_lia goal reduces to DLiaSolve goal, verified from a certificate this module both
produced and then checked without reference to how it was produced.
COMPLETENESS, stated so the one-sided contract can be audited: a verified certificate means
the negated system is genuinely infeasible over ℚ, and Fourier–Motzkin is complete for
exactly that, so the first kernel succeeds wherever this returns true. The converse is not
claimed — a false is Unchecked, never a disagreement.