The finite budget RATTLE solver returns a status in finite work

If $h=0$, [F1] returns exact-identity immediately. For nonzero $h$, consider either chord call with budget $N$ and refresh period $1$. Its initial iterate lies in its open domain. At index $k$, its residual evaluation and norm comparison terminate by the admitted primitive contract. The tolerance and budget branches return the current valid iterate and its actual residual norm. If neither branch returns, then $k<N$; one terminating Jacobian evaluation and factorization attempt either return singular-jacobian with this same data or supply a retained factor. Its terminating exact solve produces the correction. The returning domain test either returns invalid-trial with the old valid iterate and evaluated residual or admits the new iterate and increments the index. Thus induction preserves domain membership and validity of all returned residual data.

Every continuing pass strictly increments $k$, and an entered pass $k=N$ returns before a factorization or correction. Consequently there are at most $N+1$ residual checks and at most $N$ correction attempts, Jacobian assemblies, factorization attempts, and retained-factor solves. Each pass consists of finitely many returning operations by step 1.1, so the call terminates, including when $N=0$. These are counts of loop operations, not a uniform bound on the internal cost of a supplied evaluation or backend.

Apply step 2.1 first with $N=N_q$. A non-root position status is returned immediately with its last valid multiplier and actual residual, without a momentum call. On position success the finite assignments in [F1] form the momentum residual. The all-$\lambda \in U_q$ admissibility condition ensures that even this approximate returned position multiplier supplies a $C^1$ momentum residual on the whole open $U_p$ with returning evaluations. Apply step 2.1 with $N=N_p$ to the second call. Any failure returns the last valid momentum multiplier and actual tangency residual together with the successful position-stage values. If it succeeds, the remaining assignments and output norms terminate and return the prescribed state, both multipliers, residual norms, and success status. There are at most two calls, at most $N_q+N_p+2$ loop residual checks, and at most $N_q+N_p$ correction/factorization/solve attempts in total. No branch or count asserts success for every finite budget, an exact zero from a positive tolerance, or a forward-error certificate.