Finite matrix-function algorithms preserve primitive budgets and terminate with explicit statuses

Expand each candidate macro in [F1] into the actual [F2] scalar schedule. Induct over executed primitive requests: before a request the counter equals the number already executed. If the counter is $K_H$, no primitive is evaluated and the dispatcher returns exhaustion; otherwise it increments once and performs exactly the next prescribed rounded primitive. Thus it executes at most $K_H$ primitives and has the same intermediate values, branches and first arithmetic failure as the original schedule whenever the budget allows that prefix. Zero-column identity branches copy data and do not evaluate a zero-vector reflector denominator. Finite source index loops and finite exact control branches preclude a nonterminating primitive-free loop.

Each conversion, reflector, separate RHS application and triangular solve has finite dimensions. By step 1.1 their composition returns its defined result or a first budget/range/candidate failure in finite time. The completion mask is set only after each actual solution entry is computed; [F1] permits the exact row-major residual audit only after all $nr$ entries are set. That audit has $nr$ finite inner products and exact component tests, or the explicit finite-codebook adapter/failure, hence terminates. Neither partial values nor an unavailable representation are labeled a verified solution.

The Jordan routine checks finitely many exact identities and block entries and evaluates finitely many finite nilpotent sums using the supplied jets; missing data fail. Thus [F3] terminates. The Padé procedure forms finite polynomial matrices and calls the terminating solve of step 2.1 with $K_H$. Its complete-candidate gate excludes every partial or failure status from squaring. Each of its $s$ squares has finite scalar loops and a before-primitive squaring-budget check, proved bounded by the same counter argument as step 1.1. Exact defects, the finite series/tail expressions and the $s$ bound recurrences are finite; the finite cover validator in [F9] either succeeds or fails. Therefore every Padé path returns a declared status, and a failure/partial candidate cannot be interpreted as a conditional error-bound success.

Each polar/sign iteration makes one finite-budget denominator call and only continues on its complete verified solution; otherwise it returns the solve status and the last candidate. Its component update has finitely many operations and explicit range failures. At most $N$ such iterations occur by [F5], including no iteration at $N=0$, proving termination and the stated budget/status separation without asserting convergence of rounded iterates.

By [F6], each delegated Schur or Sylvester call terminates. A fixed Schur–Parlett partition has finitely many block pairs and Jordan calls, terminating by step 3.1 and [F6]. Each merge strictly lowers the initial block count, which is at most $n$, so at most $n-1$ restarts occur. Every other failure is returned. Thus [F7] terminates. The principal-function routine adds only finitely many exact branch/sign comparisons before that procedure, or an unavailable-comparison return, so [F8] also terminates. Its branch test supplies no claim beyond its original spectral/holomorphic-domain assumptions.

Steps 1.1–4.1 cover all seven procedures and their return branches. They bound only the explicitly counted rounded operations and finite loop counts; they neither bound the work of arbitrary-real exact arithmetic nor establish any separate analytic/error/iteration convergence premise. This is exactly the stated separation between termination, candidate generation and mathematical certificates.