2 added 27 characters in body

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. Some programs can indeed have a non termination non-termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof”proof applicable to all programs. The reason is that such a notion is (provably) provably nonexistent (formally, the set of non-halting programs is not recursively enumerable).

1

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. Some programs can indeed have a non termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof”. The reason is that such a notion is (provably) nonexistent (formally, the set of non-halting programs is not recursively enumerable).