Finite Bartels–Stewart statuses and successful-pivot uniqueness

The default sign program is a fixed finite expression tree or its finite encoded-integer recipe. A bounded custom interpreter takes at most its per-call instruction budget, while every arbitrary-terminating program ends by its input contract; invalid/undecided outcomes propagate as failure. The two delegated Schur calls terminate by [F3], and failed calls return immediately. Exact matrix-entry/pattern certificate tests are finite.

There are finitely many block pairs and finitely many terms in each substitution sum. Each local determinant, separation-bound expression and adjugate formula is a finite expression on a matrix of dimension at most four. A rejected test returns its declared failure. Otherwise $\det M_{ij}\mathrm{\ne }0$, so [F2] gives a unique exact local solution. Thus the whole traversal and final finite transforms terminate.

On success consider a homogeneous transformed equation $TY+YS=0$. In the algorithm's traversal order, its first block satisfies $M_{ij}\mathrm{vec}{Y}_{ij}=0$, hence $Y_{ij}=0$ by step 2.1. Inductively, all earlier blocks entering the current right-hand side are zero, so its unique invertible pivot again forces $Y_{ij}=0$. Every block therefore vanishes. Exact unitary Schur factors are invertible, so the original homogeneous operator $AX+XB$ also has zero kernel.

By [F4] the successful output is a solution. If two solutions existed, their difference would be in the homogeneous kernel, which is zero by step 3.1. Thus the output is unique without needing to assume a spectral premise not established by the caller. The positive threshold test may reject an invertible small pivot, so no converse failure conclusion is made.