For 0<=rho<1, every finite tail sum from K to K+M is <=rho^K/(1-rho), with denominator and rho=0 boundaries explicit.
Method: native-induction. Induction: M. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.