I think to be rigorous you need to consider proof lengths explicitly (like cousin_it did with his proofs).

This is clearly not what orthonormal meant, but I think if you interpret the "provable in PA+i" function as a call to a halting oracle, all the parts that raise questions about proof lengths just go through. (I also had the impression that each step in the post should break down to a formal proof whose length is O(l), where l is the length of the expression specifying how many proofs are searched; if so, everything should work out for a large enough proof limit. I think this was orthonormal's intent. However, I haven't checked this in detail.)

Can you explain how PA+3 can prove that PA through PA+2 won't have found proofs of contrary conclusions?

Let me try something, without a high degree of confidence--

The following reasoning is in PA+3, using the halting oracle interpretation so that I do not need to worry about proof lengths. We assume that 'M(FB)=C' is provable in PA+3 and that FB(M) != C, and try to derive a contradiction.

It follows directly that FB(M)=D; given our assumption, this means that PA+2 proves 'M(FB)=D'. Since we're in PA+3, it follows that M(FB)=D. But we also know that if 'FB(M)=C' is provable in PA+3, then M(FB)=C (as stated in the proof of Lemma 8, right before the contentious argument). Thus, if M(FB)=D, then PA+3 does not prove 'FB(M)=C'. This means that PA+3 is consistent. But we also know (given our assumptions) that PA+3 proves both 'M(FB)=C' and 'M(FB)=D' (the latter because PA+3 proves everything that PA+2 proves); contradiction.