They applied Lob's theorem correctly. "X is a theorem of PA" and "X is provable in PA" mean the same thing, and both are represented by ◻X. The antecedent of "if it's a theorem of PA that it's provable in PA that FB cooperates with me, then cooperate" would be represented as ◻(◻(FB(FB) = C)), but this never appears either in the code or in the antecedent for Lob's theorem. "FB(FB) = C" on its own, without the box, would mean it is true that fairbot cooperates with itself, not that PA can prove that fairbot cooperates with itself.