Note that in both this and the other model of Agent Simulates Predictor, the agent’s formal system does not know that the predictor’s formal system is consistent. One could argue that in this case it’s right to two-box. However, it’s still worrisome that the agent’s formal system proves $A()=1 \to U()= $0$ and does not prove $A()=1 \to U()= $1000000$, rather than proving both counterfactuals (spuriously) or neither.
Note that in both this and the other model of Agent Simulates Predictor, the agent’s formal system does not know that the predictor’s formal system is consistent. One could argue that in this case it’s right to two-box. However, it’s still worrisome that the agent’s formal system proves $A()=1 \to U()= $0$ and does not prove $A()=1 \to U()= $1000000$, rather than proving both counterfactuals (spuriously) or neither.