Verification theorems for models of optimal consumption and investment with retirement and constrained borrowing

Proving verification theorems can be tricky for models with both optimal stopping and state constraints. We pose and solve two alternative models of optimal consumption and investment with an optimal retirement date (optimal stopping) and various wealth constraints (state constraints). The solutions are parametric in closed form up to at most a constant. We prove the verification theorem for the main case with a nonnegative wealth constraint by combining the dynamic programming and Slater condition approaches. One unique feature of the proof is the application of the comparison principle to the differential equation solved by the proposed value function. In addition, we also obtain analytical comparative statics.