Exact residual audit of finite-precision simplex candidates

Input a standard-form problem as in Revised simplex standard-form linear program, whose stored matrix, right-hand side, and cost entries are finite binary floating-point values, together with finite stored candidate vectors $\widehat{x}\in {\mathbb{R}}^n$ and $\widehat{y}\in {\mathbb{R}}^m$. A finite binary value is interpreted as its exact dyadic rational (an integer times an integer power of $2$). If a dimension is wrong or any value is NaN or infinite, return invalid-input. Otherwise use exact integer/rational arithmetic to compute $r_p=A\widehat{x}-b$, $r_d=c-A^{\mathsf{T}}\widehat{y}$, $g=c^{\mathsf{T}}\widehat{x}-b^{\mathsf{T}}\widehat{y}$, ${\rho }_p=\mathrm{\parallel }{r}_p{\mathrm{\parallel }}_{\mathrm{\infty }}$, and ${\rho }_d=\mathrm{\parallel }{r}_d{\mathrm{\parallel }}_{\mathrm{\infty }}$, where $\mathrm{\parallel }z{\mathrm{\parallel }}_{\mathrm{\infty }}={\max }_i\mathrm{\mid }{z}_i\mathrm{\mid }$ and the empty-vector value is zero. Return these exact values and $\mathrm{\mid }g\mathrm{\mid }$ as the exact primal-dual objective difference for the stored data. Return verified-optimal-for-stored-data exactly when $\widehat{x}\ge 0$, $r_p=0$, $r_d\ge 0$, and $g=0$. In every other finite-input case return candidate-only with the residuals and gap; a nonzero or small residual is never rounded to zero and does not certify infeasibility.

The exact arithmetic is a verification procedure for a candidate produced by a floating-point solver; it does not define a basis factorization or bound uncertainty in data before they were stored. If a statement about pre-rounded data is required, separate certified input intervals must be supplied and propagated. The procedure makes no operation-count or runtime claim.