That is so cool. Exceptional work, friend.
That makes this thread a bit more interesting now.
https://stackoverflow.com/questions/60479571/is-there-a-bug-...
Thank you! Indeed it's the infamous Step D3. In my opinion, with the new changes and the new Theorem B, this step will feel more natural, because it's essentially extending the 2/1 division into a 3/2 division.
Wow I had forgotten that I had answered that question on StackOverflow!
So at the time my conclusion had been that there was no mistake (interpreting the "repeat" as a loop), but it's arguable… maybe if the person who posted the question had asked Knuth instead, he'd have had a reward check?