(Still trying to read, will comment as I go.)

if x proves "p is safe for K steps", then inst(n,x) is a PA(n+1) proof of "p is safe for n steps"

Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), 'x')->x; and then redefine PAK accordingly. (This seems possible, but it's definitely an extra step that for all I know could trip up somewhere, and ought to be stated explicitly.) If we don't take it, then inst(n, x) gives us something that seems like it ought to be provable by analogy, but isn't a direct translation, because the original PA(n) didn't contain a provability formula quantified over PA(.) into which we could plug K=n; and since I think we were proving things about inst later, that's not good.