Finite QR basis recomputation has sound residual and stored-data audit statuses

If $m=0$, the empty basis is nonsingular on the zero space. For $m\ge 1$, an exact inverse witness $G$ gives $C^{-1}=G$. Otherwise let $E=I-HC$ with $\mathrm{\parallel }E{\mathrm{\parallel }}_{\mathrm{\infty }}\le q<1$. The row-sum norm inequality gives $(1-q)\mathrm{\parallel }v{\mathrm{\parallel }}_{\mathrm{\infty }}\le \mathrm{\parallel }HCv{\mathrm{\parallel }}_{\mathrm{\infty }}$ for every $v$, so both $HC$ and $C$ have trivial kernel and, being square, are nonsingular. If $M\ge \mathrm{\parallel }H{\mathrm{\parallel }}_{\mathrm{\infty }}\mathrm{/}(1-q)$ is supplied, applying this inequality to $v=(HC{)}^{-1}w$ gives $\mathrm{\parallel }(HC{)}^{-1}w{\mathrm{\parallel }}_{\mathrm{\infty }}\le \mathrm{\parallel }w{\mathrm{\parallel }}_{\mathrm{\infty }}\mathrm{/}(1-q)$, and $C^{-1}=(HC{)}^{-1}H$ yields $\mathrm{\parallel }{C}^{-1}{\mathrm{\parallel }}_{\mathrm{\infty }}\le M$. The same argument applies to each separately checked $D=C$ or $C^{\mathsf{T}}$ witness in interval mode.

If $m=0$, the empty solve residuals are zero and only the finite audit and budget branches remain. If $m\ge 1$, step 1.1 makes each square $D$ nonsingular and hence full column rank. Apply [F2] under [A1]; since the exact representative is square, $\widehat{Q}{\widehat{Q}}^{\mathsf{T}}=I$. Multiplication of its triangular equation therefore gives $(D+{\mathrm{\Delta }}_D)\widehat{z}=r+\delta r$, where ${\mathrm{\Delta }}_D={\mathrm{\Delta }}_Q+\widehat{Q}{\mathrm{\Delta }}_R$. No nonsingularity of $\widehat{R}+{\mathrm{\Delta }}_R$ or exact orthogonality of a rounded dense output is used.

Orthogonality and [F2] imply $\mathrm{\parallel }\widehat{R}{\mathrm{\parallel }}_F=\mathrm{\parallel }D+{\mathrm{\Delta }}_Q{\mathrm{\parallel }}_F\le (1+\beta )\mathrm{\parallel }D{\mathrm{\parallel }}_F$. Hence $\mathrm{\parallel }{\mathrm{\Delta }}_D{\mathrm{\parallel }}_F\le [\beta +{\gamma }_{m+3}(1+\beta )]\mathrm{\parallel }D{\mathrm{\parallel }}_F={\beta }_D\mathrm{\parallel }D{\mathrm{\parallel }}_F$. Rearranging step 2.1 yields $\mathrm{\parallel }D\widehat{z}-r{\mathrm{\parallel }}_2\le \mathrm{\parallel }\delta r{\mathrm{\parallel }}_2+\mathrm{\parallel }{\mathrm{\Delta }}_D{\mathrm{\parallel }}_F\mathrm{\parallel }\widehat{z}{\mathrm{\parallel }}_2\le \beta \mathrm{\parallel }r{\mathrm{\parallel }}_2+{\beta }_D\mathrm{\parallel }D{\mathrm{\parallel }}_F\mathrm{\parallel }\widehat{z}{\mathrm{\parallel }}_2$.

The triangle inequality and [F3] give the independent upper bound $\mathrm{\parallel }D\widehat{z}-r{\mathrm{\parallel }}_2\le \mathrm{\parallel }\widehat{w}{\mathrm{\parallel }}_2+W$. Both quantities in the reported minimum are upper bounds, so their minimum is an upper bound. Applying this to each current primal, transpose-multiplier and direction solve proves all residual conclusions. The same conclusion holds when the algorithm uses rational or other certified upper bounds, since both evaluated candidates remain upper bounds. Finally $D(\widehat{z}-z_{\ast })=D\widehat{z}-r$, so the defining induced-norm inequality gives $\mathrm{\parallel }\widehat{z}-z_{\ast }{\mathrm{\parallel }}_2\le \mathrm{\parallel }{D}^{-1}{\mathrm{\parallel }}_2\mathrm{\parallel }D\widehat{z}-r{\mathrm{\parallel }}_2\le \mathrm{\parallel }{D}^{-1}{\mathrm{\parallel }}_2\eta$. This is conditional on the actual inverse norm, not an assertion that the procedure computes it. For interval mode, [F1] forms each coordinate interval with radius $M_D\eta$; step 1.1 gives $\mathrm{\parallel }{D}^{-1}{\mathrm{\parallel }}_{\mathrm{\infty }}\le M_D$, while step 3.1's residual bound and $\mathrm{\parallel }z{\mathrm{\parallel }}_{\mathrm{\infty }}\le \mathrm{\parallel }z{\mathrm{\parallel }}_2$ imply $\mathrm{\parallel }\widehat{z}-D^{-1}r{\mathrm{\parallel }}_{\mathrm{\infty }}\le M_D\eta$. Thus the intervals contain the exact solution.

The interval addition and subtraction endpoints bound the corresponding sums and differences; the four endpoint products bound every product, and reciprocal endpoints bound reciprocals on either interval that avoids zero. Induction therefore encloses every exact reduced cost and ratio evaluated by [F1]. Any endpoint comparison that admits a sign or order is true of the enclosed exact value; any unresolved comparison either is checked by an exact inverse witness or returns inconclusive. Hence every admitted exact-witness or interval record satisfies the corresponding primal or dual pivot rule. If position $i$ is replaced by column $j$, then $C^{-1}{A}_{B^{\mathrm{\prime }}}$ is the identity with column $i$ replaced by $d=C^{-1}{a}_j$, so $\det (A_{B^{\mathrm{\prime }}})=\det (C)d_i\mathrm{\ne }0$ by the checked pivot sign. The replacement basis is nonsingular.

By [F1], the completed audit uses the actual stored candidate vectors and original stored LP data. Apply [F4] to obtain the displayed identity, norm bound and exactly conditional optimality statement. Since [F1] labels no other branch verified-optimal and rejects unestablished transitions, no small residual, unresolved sign/ratio comparison or numerical failure is converted into a pivot, optimality or infeasibility certificate.

Each canonical factorization, vector application, substitution and residual loop has finite dimensions; each elementary call either completes or returns its first failure by [F1]. Verifying a transition record uses only finitely many exact rational matrix products or certified interval operations over the finite basis and column sets; unresolved comparisons return inconclusive. The dyadic audit uses finitely many exact integer/rational operations. Before each attempt the counter increases, and [F1] allows at most $K$ attempts and no unbounded internal transition search. Every admitted basis replacement discards old factors before computing new certificates. Consequently the procedure terminates with only the stated current-basis outputs or failure/inconclusive status, proving the remaining claims.