Expand description
omega — linear INTEGER arithmetic, the discreteness-aware layer over the
rational Farkas core.
Rational Fourier-Motzkin (crate::linarith_solve) decides satisfiability
over ℚ; it is sound for ℤ but INCOMPLETE, because it cannot use the one fact
that distinguishes the integers: a strict a < b is a non-strict a+1 ≤ b,
since nothing lives strictly between consecutive integers. The classic
witness is x < y ∧ y < x+1 — rationally satisfiable (x=0, y=½), integer
UNSAT.
This module supplies exactly that missing step. It rewrites every strict
hypothesis a < b to a+1 ≤ b through the kernel axiom lt_succ_le (a
certified InferenceRule::LtSuccLe node), then hands the enlarged set of
≤-facts to the existing Farkas refutation ([crate::engine::cert_farkas]).
The result is one kernel-checked ⊥ derivation, so omega is exactly as
trusted as linarith — it just sees more contradictions.