OK, so just spelling out the argument for my own amusement:

The agent can prove the implications "agent() == 1 implies world() == 1000000" and "agent() == 2 implies world() == 1000", both of which are true.

Let x and y in {1, 2} be such that agent() == x and agent() != y.

Let Ux be the greatest value of U for which the agent proves "agent() == x implies world() == U". Let Uy be the greatest value of U for which the agent proves "agent() == y implies world() == U".

Then Ux is greater than or equal to Uy.

If the agent's formalised reasoning is consistent then since agent() == x is true, Ux must be the only U such that "agent() == x implies world() == U" is provable.

Now, if there is more than one U such that "agent() == y implies world() == U" is provable then "agent() == y implies contradiction" is provable, and hence so is "agent() == y implies world() == U" for some value of U larger than Ux. Hence Uy would be larger than Ux, which is impossible.

Therefore, the implications "agent() == 1 implies world() == 1000000" and "agent() == 2 implies world() == 1000" are the only ones provable.

Therefore, agent() == 1.