Uniform bound |logμ(x)|≤ c (-logμ(p)) for algebraic x

Let $K$ be a field of characteristic zero, let $x \in K$ be nonzero and algebraic over $\mathbb{Q}$ (in the sense that $x$ is a root of a nonzero polynomial with rational coefficients, under the canonical map $\mathbb{Q} \to K$), and let $p$ be a prime natural number. The assertion is the existence of a real constant $c \ge 0$, depending only on $x$ and $p$, with the following uniformity property: for every real-valued absolute value $\mu$ on $K$ which is non-archimedean, i.e. satisfies $\mu(a+b) \le \max(\mu(a),\mu(b))$ for all $a,b \in K$, and which satisfies $\mu(p) < 1$ for the image of $p$ in $K$, one has

Note that $\mu(p) < 1$ together with $\mu(p) > 0$ makes the right-hand side a nonnegative multiple of $c$, so the inequality bounds $\log\mu(x)$ above and below simultaneously; the point is that $c$ is independent of $\mu$, so in particular the bound is invariant under replacing $\mu$ by a power $\mu^t$.

This is the elementary valuation-theoretic statement that a fixed nonzero algebraic number has logarithmic size $O(-\log\mu(p))$ uniformly over all non-archimedean absolute values lying over $p$; no classification of absolute values is involved. It is used in the analysis of absolute values of values of modular functions on $X_0(N)$, for instance in ModularCurve.JZero.exists_abv_evalAt_eq_abv_evalAt_of_le_prox, ModularCurve.JZero.exists_chart_of_isPivot and ModularCurve.JZero.exists_one_le_abv_evalAt_of_le_prox, where constants attached to fixed algebraic data must be expressed homogeneously in $-\log\mu(p)$.