Elementary proof of bounds on factor polynomials

Question

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}$.

Answer 1

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.

http://www.math.ucsd.edu/~lrothsch/Reprints/Factoring%20polynomials%201976.pdf

This solves the problem behind my question.

The original question sought an explicitly arithmetic proof of Gelfond's theorem, or an explicit metatheoretic proof that it must be so provable. Gelfond's theorem is probably provable in EFA and likely in some even weaker fragment which could be explored if we had a PA proof to begin with. Emil Jeřábek's suggestion using Gaussian rationals might work but it depends on approximating integer polynomials by ones with rational roots -- and the current state of the art on that seems to be the Henselian strategy rather than Gelfond's theorem.