Binary-addition carry invariant ($V(x_{\mathrm{suffix}})+V(y_{\mathrm{suffix}})=V(resul{t}_{\mathrm{suffix}})+carry{2}^k$)

After adding $k$ least-significant binary digits, the numerical sum of the two processed input suffixes equals the written $k$ result digits plus $carry{2}^k$, with $carry\in \{0,1\}$. Initially both suffixes are empty. For the next column, write $(x_k+y_k+carry)\mathrm{mod}2$ and pass $\lfloor (x_k+y_k+carry)/2\rfloor$ to the next column. Multiplying these column quantities by $2^k$ preserves the equation. After all columns, the remaining carry supplies the extra leading digit, proving correctness without converting either full input to a machine integer.