Yup, modulo one nit, but let me expand a bit on this answer.

Suppose the statement C doesn't contain K at all (or else it contains K in a way that provably doesn't matter).

Then C is a theorem of PA (and we're assuming that PA is sound).

Nit: C ranges over all statements; for example, it is an axiom of PPT.2 that "if K>0, and PPT.2 proves '0=1', then 0=1", even though 0=1 is not a theorem of PA. However, unless my proof is borked, it should be the case that if C doesn't contain K, then (PPT.2 proves C) iff (PA proves C), and also (PPT.2 proves C) iff (PPT.2 proves "PPT.2 proves 'C'"). Therefore, in a sense you can't apply the axiom involving C unless C is provable in PA, which is what I think you had in mind.

Then PPT.2 contains the axiom "If K>0, and C is provable in PPT.2, then C". For all n>0, if we replace K by n, we get the axioms of BAD, which is inconsistent.

PPT.2 != BAD, so you don't have exactly the same axioms as BAD.

One possible point of confusion here is that it might seem as if replacing K by 15 would yield the proof system

NOTGOOD := PA + for every statement C, "If 15>0, and 'C' is provable in NOTGOOD, then C,"

because it may seem as if replacing every occurrence of K in the formula "PPT.2 proves 'C'" should yield the statement "NOTGOOD proves 'C'".

But this is not true: the formula "PPT.2 proves 'C'" contains no occurrence of K, not even if C contains K. This is because the formula doesn't literally contain C, it contains the unary representation of the Gödel number of C, and similarly, the predicate "PPT.2 proves ..." only talks about Gödel numbers, not about K.