In essence, it's just recursion that's only allowed when the recursive input is in some sense strictly "smaller" than its input and therefore necessarily termin

In essence, it's just recursion that's only allowed when the recursive input is in some sense strictly "smaller" than its input and therefore necessarily terminates if the input is of finite size and cannot drop below zero. However, it's not magic: it's not automatically trivial to generate such a proof of termination (I'd assume there exist definitely terminating programs for any given proof system that cannot be proven to terminate in that formalism), and it may be a moot point since a slow enough algorithm is for all intents and purposes non-terminating...