= Binary-addition carry invariant
{title2=$V(x_{\rm suffix})+V(y_{\rm suffix})=V(result_{\rm 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)\bmod2$ 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.
Back to article page
