Recursion invariant
= Recursion invariant
A relationship between a recursive procedure's arguments, accumulated state and original input that holds at every reachable <recursive call>. For accumulator-based <exponentiation by squaring>, $acc\,base^{remaining}=x^n$ is a <recursion invariant> under exact arithmetic. The base case converts it into the desired result, while the recursive step and a decreasing argument justify preservation and termination.