Undecidability instance on a "find a proof/disproof" machine
So $f(M,I)$ is this machine that "takes our standard set of axioms (ZFC, let's say, or Peano arithmetic, or whatever) and first tries every one-page proof that machine M halts on input I"...

That's fine, but later on you say "The above constitutes a proof that $g(g)$ never terminates, and so the function $f(g,g)$ should find this proof."

That is not true, since you didn't write that proof as a formal proof in terms of "ZFC, let's say, or Peano arithmetic, or whatever", so there is no reason to expect $f(g,g)$ to find it.  You didn't even define $f(a,b)$ of $g(x)$ in terms that would translate into most such formal systems.

You assume that you would be able to specify a real formal system if you had to, with sufficient power to express $f$ and $g$ in concrete terms and prove what you say about them, but Godel's theorem says that's not necessarily so.

Furthermore, you say that $f$ and $g$ are real programs, but that is not true until this formal system is specified.  Because of this you have not proven what you set out to prove.  What you have proven is Godel's theorem -- any formal system that allows you to express your claim in terms of itself will either be inconsistent, or will not contain your proof.