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, 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.
New to topics? Read the docs here!