(There was a LaTeX error in my comment, which made it totally illegible. But I think you managed to resolve my confusion anyway).
I see! It’s not provable that Provable(A=10⇒U=10) implies A=10. It seems like it should be provable, but the obvious argument relies on the assumption that, if *A=10⇒U=0 is provable, then it’s not also provable that A=10⇒U=10 - in other words, that the proof system is consistent! Which may be true, but is not provable.
The asymmetry between 5 and 10 is that, to choose 5, we only need a proof that 5 is optimal, but to choose 10, we need to not find a proof that 5 is optimal. Which seems easier than finding a proof that 10 is optimal, but is not provably easier.
(There was a LaTeX error in my comment, which made it totally illegible. But I think you managed to resolve my confusion anyway).
I see! It’s not provable that Provable(A=10⇒U=10) implies A=10. It seems like it should be provable, but the obvious argument relies on the assumption that, if *A=10⇒U=0 is provable, then it’s not also provable that A=10⇒U=10 - in other words, that the proof system is consistent! Which may be true, but is not provable.
The asymmetry between 5 and 10 is that, to choose 5, we only need a proof that 5 is optimal, but to choose 10, we need to not find a proof that 5 is optimal. Which seems easier than finding a proof that 10 is optimal, but is not provably easier.