# Elementary proof of bounds on factor polynomials

The question Getting a bound on the coefficients of the factor polynomial got very nice answers on Gelfond's theorem. But for work on proof theory of arithmetic I want a proof in arithmetic. The published proofs use Mahler measure defined in complex analysis. Are there published proofs of Gelfond's theorem in arithmetic in the first place. I should say, proofs published in English or some Western European language. I cannot read Gelfond's paper in Russian.

In fact Mahler uses the sort of complex analysis which is probably conservative over Peano arithmetic along the lines of Takeuti's "A Conservative Extension of Peano Arithmetic." But I am not skilled at that yet. Can anyone here tell me if that will work for Mahler measure? or won't? Or point me to a better source?

Emil Jeřábek asks reasonably if I need Gelfond's theorem. In fact I do need something close to it. I want polynomial factorization over algebraic number fields. This is probably best approached in terms of two-variable integer polynomials where the first variable is really to be taken modulo an irreducible polynomial over $\mathbb{Z}$. This would be a pretty special case of Gelfond's theorem, but not obviously reducible to one-variable polynomials over $\mathbb{Z}$.

To be clear I am asking to know a proof, so I can check if it works in EFA. The project is to establish that EFA suffices for the classical Galois theory of number fields inclduing the Artin-Schreier theorem -- which is not obvious, since results in Reverse Math show even PRA does not suffice for the more general theory of algebraic extensions of $\mathbb{Q}$.

-
Why do you spell it as Gelfand rather than Gelfond? At least according to wikipedia, the name of Alexander Gelfond is spelt with an o, and Israel Gelfand with an a; not only in English, but also in Russian. –  Lucia Jan 17 at 16:50
Because Joe Silverman does in his answer to the cited question, and elsewhere. Both spellings exist on line. –  Colin McLarty Jan 17 at 16:54
Do you really need Gelfond’s theorem? Pietro Majer gave a completely elementary answer that will formalize in PA (or a much weaker theory, for that matter) with no difficulty. –  Emil Jeřábek Jan 17 at 17:17
Dear colleagues! Israil GelfAnd and Alexandr GelfOnd are two different people (as you can easily check with Mathscinet). The theorem in question is due to Alexandr Gelfond. Each of them has only one correct spelling. –  Alexandre Eremenko Jan 17 at 19:18
@ColinMcLarty I have a great talent for misspelling names (and other words, but spell-check helps with those), so even I wouldn't cite myself as a source for the correct spelling of someone's name. :) –  Joe Silverman Jan 18 at 3:24

The Henselian strategy of Zassenhaus uses $p$-adic bounds rather than the integer exponential bounds of Gelfond's theorem. Weinberger and Rothschild develop this approach over algebraic number fields, by an algorithm explicit enough to be its own proof, in Factoring Polynomials Over Algebraic Number Fields,'' ACM Transactions on Mathematical Software,1976, 335--50.