Worked solution: Gelfond–Schneider transcendence proof via auxiliary functions (1934)

Jensen's formula states that for $f$ holomorphic on a disk of radius $r$ with zeros $a_1,\dots,a_n$ inside (and $f(0)\ne0$), $\log|f(0)|=-\sum_j\log(r/|a_j|)+\frac{1}{2\pi}\int_0^{2\pi}\log|f(re^{i\theta})|\,d\theta$; when $f$ vanishes to order $s$ at $0$ the formula generalizes to relate $\log|f^{(s)}(0)/s!|$ to the same quantities (Siu, 'Jensen's Formula'). Applied to $F(z)=\Phi(z)$, but restricted only to the $m$ points $z_1,\dots,z_m\ne z_0$ (each contributing a term $\log(r/|z_j|)$, using that $F$ has order $\ge L$ zeros there) gives an inequality, since these are not literally all the zeros of $\Phi$ in the disk (Siu, inequality labeled $(\ddagger)$).

Bounding the growth of $\Phi$ on the circle $|z|=r$: since $e^z$ and $e^{\beta z}$ have order $1$ (i.e. $|e^z|\le C_\epsilon e^{|z|^{1+\epsilon}}$), and $G$ has coefficients and degree of size $\lesssim L$, one gets $\log|\Phi(re^{i\theta})|\lesssim L+Jr^{1+\epsilon}$ (Siu, growth estimate via the Appendix's derivative bounds $\|D^\lambda(f^jg^k)\|\le(2J+L)^LC^{2J+L}$). Choosing $r=L^{1/2}$ balances the two terms and gives $\log|\Phi(re^{i\theta})|\lesssim L$.

Combining both sides of Jensen's formula (the left side contributing $\gtrsim mL\log r=\frac{m}{2}L\log L$ from the $m$ known zeros, the right side bounded by $[K:\mathbb{Q}]L\log L$ plus $O(L)$, since the 'size' of the algebraic number $\Phi^{(s)}(0)$ costs an extra factor of $[K:\mathbb{Q}]$ to account for its conjugates) yields the final analytic bound: $\log|\Phi^{(s)}(0)|\lesssim -c\,L\log L$ for an explicit constant $c>0$ depending on $[K:\mathbb{Q}]$ once $m$ is chosen large enough relative to $[K:\mathbb{Q}]$ (Siu, proof of Main Theorem, final comparison of growth orders).