Similarly, Benja's AI can think of itself as getting to choose whether to push the button without thereby thinking that it has the power to modify mathematical truth.

I think we're all on the same page about being able to choose some mathematical truths, actually. What FAWS and I think is that in the setup I described, the human/AI does not get to determine the digit of pi, because the computation of the digits of pi does not involve a computation of the human's choices in the thought experiment. [Unless of course by incredible mathematical coincidence, the calculation of digits of pi happens to be a universal computer, happens to simulate our universe, and by pure luck happens to depend on our choices just at the umpteenth digit. My math knowledge doesn't suffice to rule that possibility out, but it's not just astronomically but combinatorially unlikely, and not what any of us has in mind, I'm sure.]