math.NT — Number Theory

Products of $p$-adic logarithms of algebraic numbers that are not linear forms in logarithms, and a machine-checked $p$-adic linear-subgroup theorem

Contributed by Shawn Krisman

Let $p$ be a prime, $\mathbb{C}_p$ the completion of an algebraic closure of $\mathbb{Q}_p$, $\overline{\mathbb{Q}}$ the algebraic numbers in $\mathbb{C}_p$, $L$ the $\mathbb{Q}$-vector space of $p$-adic logarithms of algebraic numbers, and $\mathcal{L}=\overline{\mathbb{Q}}+\overline{\mathbb{Q}}L$ the space of $p$-adic linear forms in logarithms of algebraic numbers with algebraic coefficients. We prove, in Lean 4 with Mathlib and from the three standard axioms only, that $\log_p 2\cdot\log_p(3+\sqrt2)\notin\mathcal{L}$ for every prime $p\equiv\pm3 \pmod 8$, together with a family of similar statements for real quadratic fields, and the general principle behind them: if $\sigma$ is a continuous automorphism of $\mathbb{C}_p$ fixing a nonzero $t\in L$ and moving $u\in L$ to a conjugate $\sigma u\neq\pm u$ of finite orbit, then $tu\notin\mathcal{L}$. This is G. Diaz's use of complex conjugation with an element of $\mathrm{Gal}(\overline{\mathbb{Q}}_p/\mathbb{Q}_p)$ in its place; the complex analogue $\log 2\cdot\log(3+\sqrt2)\notin\mathcal{L}$ is open. The deep input is Roy's form of Waldschmidt's linear-subgroup theorem for $\mathbb{G}_a^{d_0}\times\mathbb{G}_m^{d_1}$ over $\mathbb{C}_p$, with a derivative subspace, which we also prove in Lean, from Philippon's multiplicity estimate; the strong six exponentials theorem and the inhomogeneous Baker--Brumer theorem in two logarithms over $\mathbb{C}_p$ follow. The $p$-adic linear-subgroup theorem has been used since Laurent and Roy, but we were unable to locate a proof written for $\mathbb{C}_p$ of the version with derivatives. The Lean development is the proof of record; the paper explains the statements, the route, and how to check the certificate. The code is available at https://github.com/telaviv/p-adic-log-products.