The scaled real-column Householder procedure terminates with defined statuses

The zero test scans a finite column. If it succeeds, [F1] returns its initialized identity record, zero target and copied finite block without forming any squared-vector norm or quotient. Otherwise the scaling maximum, the two norm sums, coefficient formation, column dots and ordered update products each use finitely many indices. By [F2], each attempted arithmetic operation returns its next value or a first failure. The extra finite positivity and normality tests either return failure or allow the next finite stage. Thus formation and application terminate with a declared record.

A specified separate block has finitely many columns and rows. Its sequential dots, coefficient-vector products and ordered update products have finite bounds; [F2] again makes each attempt return or fail. Hence this additional application terminates, including zero columns of the separate block.

In a successful nonzero-column branch, the stored squared-norm sum is positive by [F1]. If the stored vector were zero, every square and every sum in that computation would be exact zero by [F2], contradicting that positive test. Therefore $v\mathrm{\ne }0$ and $d=v^{T}v>0$. For $K=v{v}^T\mathrm{/}d$, direct multiplication gives $K^T=K$, $K^2=K$ and $(I-2K{)}^T(I-2K)=I$. Its real entries give the same adjoint identity over $\mathbb{C}$. Together with steps 1.1–1.2 this proves every stated status and representative property.