I did overlook the definition of H. Apologies.

The point is that the behavior of H is paradoxical. We can prove that it can't return true or false without contradiction. But if that's provable, that also creates a contradiction, since H can prove it to.

More precisely, H will encounter a proof that the question is undecidable. It then runs into the following two if statements:

if check_if_proof_proves_x_halts(proof, x, i)

if check_if_proof_proves_x_doesnt_halt(proof, x, i)

Both return "false", so H moves into the next iteration of the while loop. H will generate undecidability proofs, but as implemented it will merely discard them and continue searching. Since such proofs do not cause H to halt, and since there are no proofs that the program halts or does not, then H will run forever.