It's just a way of breaking down the full proof into pieces.

Lemma 2.1 says 'if this assignment exists then X'

Then later in the proof you say 'here is such an assignment, so, applying lemma 2.1, therefore X'

You don't need to assume the existence of the assignment, you prove that if the assignment exists then something else follows, and then later if you can find that assignment then you get the result of lemma 2.1.

▲

Diogenesian 4 hours ago | parent [-]

I didn't see the next paragraph after the proof. This typography is hard to read on a phone. Wish HN would let me delete the comment.

	▲	Kotlopou 4 hours ago \| parent [-]
		Just dropping in to say it's nice to see somebody actually try to work through the proof, and it gives one confidence that the proof at least isn't complete nonsense (which is helpful given the few details provided about the process behind it). With the Erdős proof, OpenAI added perspectives from working mathematicians that gave some context -- hope something like that appears for this one eventually.