Finite Francis procedure terminates with explicit statuses and verifies its Schur pattern on success

Initialization uses at most $\max (n-2,0)$ reflector stages. Each active reflector formation and both specified applications have finite loops over matrix rows and columns. A main invalid/range/formation failure returns at once. Hence initialization ends with its stored factors or an explicit status.

Every sweep has a finite active partition and a dimension-bounded bulge chase per block. Deflation tests, shift-table lookups and exact pattern checks are finite; each supplied sign or outward-bound call terminates by the input contract. A missing shift, unavailable type sign or failed invariant/range test gives the declared main failure. There are at most $N$ sweeps, including the initial target test when $N=0$. Bookkeeping makes finitely many calls per stage and sets its own flag inconclusive on unavailable data. Thus all main and bookkeeping paths terminate.

After initialization's full pattern check, every position below the first subdiagonal is zero; for $n\le 2$ there is no such position. A block chase on $[a,b]$ changes matrix entries only in rows or columns of that interval: every left update and target overwrite has a row in it, and every right update has a column in it. Its complementary below-subdiagonal entries therefore stay unchanged and zero. The explicit row ranges in [F1] test every remaining below-subdiagonal position, without repetition and in row-major order. An accepted block check thus establishes the entire global Hessenberg pattern again; a rejected check detects exactly a nonzero entry that a full row-major pattern check would first detect at the same block boundary. Deflation writes are on the first subdiagonal, so preserve this invariant. Induction over all processed blocks and scans proves that the final target check starts from a globally verified Hessenberg matrix.

The only Schur-computed branch checks the entire target pattern and all required exact discriminant signs, which is exactly [F3]. Every exact factor appended is unitary by [F2]; the adjoint of a finite product reverses the factors and cancels them pairwise, so the recorded product remains unitary. No exact original-matrix factorization is inferred from a rounded update or a residual diagnostic. The flag branch is the actual availability test in [F1], not a new backward-error proof.