Capped RRQR interpolation returns a status and its direct certificate bounds the actual residual

In the rank test [F1], each of the $n$ columns scans at most $m$ rows. A nonzero pivot is the only divisor used in a row elimination, so every exact rational operation is defined and has finite integer numerators and denominators. Row swaps and subtracting a multiple of one row from another are invertible operations; they preserve all linear dependence relations among columns. At completion the echelon matrix has $r$ nonzero rows with distinct pivot columns, and all remaining rows vanish. Its pivot columns are independent by triangular back-substitution, and its image is contained in the $r$-dimensional space of vectors supported on the nonzero rows. Its rank is therefore exactly $r$, which equals the original rank. The same finite argument applies to the represented selected-block singularity test. Thus no rounded pivot threshold or undecidable limiting test is involved in either finite-precision rank decision. In exact mode the same rank-preserving operations and finite pivot scans apply over the exact input field, using the assumed exact arithmetic and comparisons.

Each QR initialization or refactorization has finitely many pivot scans and at most $mn$ local updates by [F1]. Their scalar operations terminate individually in the specified model. A zero target is skipped, and division is performed only after its denominator check. An inadmissible rounded operation exits with range-failure; a singular selected block exits with singular-selected-block. Otherwise triangular solves and inverse-row calculations use finitely many nonzero diagonal divisions, and finitely many norms and comparisons produce a score-test pass. In exact arithmetic the corresponding finite QR eliminations, norms, and comparisons are defined by the exact model; the same singular-block branch prevents an undefined solve.

Starting with zero swaps, every score-test pass either returns success, returns another nonsuccess status, or finds a violation. At a violation the procedure returns when the count is already $S$; otherwise it increments the count and repeats. Hence there are at most $S$ swaps and $S+1$ score-test passes. Each has finite work by step 2.1. The rank-deficient and $k=0$ QR branches return earlier. The optional QR certificate check uses only its fixed finite budget, so failure to certify cannot cause another unbounded loop or change a core status. The ordered exit branches assign exactly one core status.

The ID endpoint branches [F2] return after constructing finite empty or identity matrices. Every interior call terminates by step 3.1. Nonsuccess is propagated with both certificate statuses not applicable. On success the permutation determines distinct valid selected indices, and insertion and permutation of finitely many entries constructs $T$ in finite work. Every finite candidate entry is rational in the represented mode. Thus all entries of $D$, all squared moduli and their finite sum and maximum are exactly computable rationals, regardless of their magnitude; the symbolic square root $\sqrt{r^2}$ requires no rounded conversion. Identity and rational inequality checks terminate, assigning either certified or uncertified; endpoint certificate statuses are not required. This proves termination and well-definedness of all outputs and statuses.

On an ID-certified branch the explicit checks [F2] give $T(:,J)=I_k$ and $c^2\le f^2$. Since $f\ge 1$ and all moduli are nonnegative, $\mathrm{\mid }{T}_{ab}{\mathrm{\mid }}^2\le c^2\le f^2$ gives $\mathrm{\mid }{T}_{ab}\mathrm{\mid }\le f$. For every unit vector $x\in {\mathbb{F}}^n$, apply [F3] to each row of $D$ to obtain $\mathrm{\mid }(Dx{)}_a{\mathrm{\mid }}^2\le {\sum }_b\mathrm{\mid }{D}_{ab}{\mathrm{\mid }}^2$. Summing over rows gives $\mathrm{\parallel }Dx{\mathrm{\parallel }}_2^2\le {\sum }_{a,b}\mathrm{\mid }{D}_{ab}{\mathrm{\mid }}^2=r^2$. Taking the supremum over unit $x$ proves $\mathrm{\parallel }D{\mathrm{\parallel }}_2\le \sqrt{r^2}$ for the actual reconstruction residual. This uses only the direct exact data and no RRQR score certificate, as claimed.