Finite ADI shifts have well-defined solves and explicit statuses

In the pairing scan, each accepted real entry advances the index by one and each accepted nonreal pair advances it by two; an unpaired entry returns immediately. Thus the scan has at most $k$ checks, including the empty list. For a pair $(p,\bar{p})$ the second entry is consumed by the validation scan, not incorrectly tested for a third partner. The update loop still visits both indices.

Each valid update has $c_j=-2\mathrm{Re}{p}_j>0$. By [F2] its exact linear system has a unique solution. Other shift checks return their declared status. Each matrix operation and positive scalar square root is finite, and the update index increases until $k$ or an earlier return, so the procedure terminates.

Initialization has zero factor columns and $X_0=0$. Each successful update appends $r$ columns and sets $X_j=Z_j{Z}_j^{\ast }$ and $R_j$ by its explicit recurrence. Hence completion has at most $kr$ columns and exactly the recorded output relations, also for $k=0$. No contraction or limiting shift property was used.