\documentclass[11pt]{amsart} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amssymb} \usepackage{amsthm} \usepackage{booktabs} \usepackage{array} \usepackage{xcolor} \usepackage{fancyvrb} \usepackage{url} \usepackage{hyperref} % --------------------------------------------------------------------------- % Theorem environments % --------------------------------------------------------------------------- \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \numberwithin{equation}{section} \setlength{\emergencystretch}{2em} % --------------------------------------------------------------------------- % Macros % --------------------------------------------------------------------------- \newcommand{\NN}{\mathbb{N}} \newcommand{\ZZ}{\mathbb{Z}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\CC}{\mathbb{C}} \newcommand{\Cp}{\mathbb{C}_p} \newcommand{\Qp}{\mathbb{Q}_p} \newcommand{\Qbar}{\overline{\mathbb{Q}}} \newcommand{\Qpbar}{\overline{\mathbb{Q}}_p} \newcommand{\cL}{\mathcal{L}} \newcommand{\cU}{\mathcal{U}} \newcommand{\Ga}{\mathbb{G}_{\mathrm{a}}} \newcommand{\Gm}{\mathbb{G}_{\mathrm{m}}} \newcommand{\Gal}{\operatorname{Gal}} \newcommand{\logp}{\log_p} \newcommand{\house}[1]{\overline{\lvert #1\rvert}} \DeclareUrlCommand\lean{\urlstyle{tt}} \newcommand{\leans}[1]{\texttt{\detokenize{#1}}} % --------------------------------------------------------------------------- % Lean code blocks: fancyvrb, with the Unicode used in them mapped for pdflatex % --------------------------------------------------------------------------- \fvset{frame=single,fontsize=\footnotesize,xleftmargin=1em,framesep=2mm} \DeclareUnicodeCharacter{2102}{\ensuremath{\mathbb{C}}} \DeclareUnicodeCharacter{211A}{\ensuremath{\mathbb{Q}}} \DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}} \DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}} \DeclareUnicodeCharacter{2113}{\ensuremath{\ell}} \DeclareUnicodeCharacter{03B2}{\ensuremath{\beta}} \DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}} \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} \DeclareUnicodeCharacter{2192}{\ensuremath{\to}} \DeclareUnicodeCharacter{2208}{\ensuremath{\in}} \DeclareUnicodeCharacter{2209}{\ensuremath{\notin}} \DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}} \DeclareUnicodeCharacter{2228}{\ensuremath{\vee}} \DeclareUnicodeCharacter{2211}{\ensuremath{\sum}} \DeclareUnicodeCharacter{2260}{\ensuremath{\neq}} \DeclareUnicodeCharacter{2264}{\ensuremath{\le}} \DeclareUnicodeCharacter{2293}{\ensuremath{\sqcap}} \DeclareUnicodeCharacter{21A5}{\ensuremath{\uparrow}} \DeclareUnicodeCharacter{22A4}{\ensuremath{\top}} \DeclareUnicodeCharacter{2016}{\ensuremath{\|}} \DeclareUnicodeCharacter{2097}{\ensuremath{{}_{\ell}}} \DeclareUnicodeCharacter{207B}{\ensuremath{{}^{-}}} \DeclareUnicodeCharacter{00B9}{\ensuremath{{}^{1}}} \DeclareUnicodeCharacter{221A}{\ensuremath{\surd}} \DeclareUnicodeCharacter{2223}{\ensuremath{\mid}} \begin{document} \title[Products of $p$-adic logarithms and a $p$-adic linear-subgroup theorem]{Products of $p$-adic logarithms of algebraic numbers that are not linear forms in logarithms, and a machine-checked $p$-adic linear-subgroup theorem} \author{Shawn Krisman} \subjclass[2020]{Primary 11J81; Secondary 11J86, 11J61, 68V20} \keywords{$p$-adic transcendence, linear forms in logarithms, strong six exponentials theorem, linear-subgroup theorem, interpolation determinants, formal verification, Lean} \date{\today} \begin{abstract} Let $p$ be a prime, $\Cp$ the completion of an algebraic closure of $\Qp$, $\Qbar$ the algebraic numbers in $\Cp$, $L$ the $\QQ$-vector space of $p$-adic logarithms of algebraic numbers, and $\cL=\Qbar+\Qbar 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 $\logp 2\cdot\logp(3+\sqrt2)\notin\cL$ 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 $\Cp$ 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\cL$. This is G.~Diaz's use of complex conjugation with an element of $\Gal(\Qpbar/\Qp)$ in its place; the complex analogue $\log2\cdot\log(3+\sqrt2)\notin\cL$ is open. The deep input is Roy's form of Waldschmidt's linear-subgroup theorem for $\Ga^{d_0}\times\Gm^{d_1}$ over $\Cp$, 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 $\Cp$ follow. The $p$-adic linear-subgroup theorem has been used since Laurent and Roy, but we were unable to locate a proof written for $\Cp$ 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 \url{https://github.com/telaviv/p-adic-log-products}. \end{abstract} \maketitle % =========================================================================== \section{Main theorems}\label{sec:main} % =========================================================================== Fix a prime $p$. Let $\Cp$ be the completion of an algebraic closure of $\Qp$, with the absolute value $|\cdot|$ normalized by $|p|=p^{-1}$; it is complete and algebraically closed \cite[Ch.~3]{Robert2000}. Let $\Qbar\subset\Cp$ be the set of elements algebraic over $\QQ$; it is an algebraic closure of $\QQ$. Let \[ \cU=\{x\in\Cp : |x-1|<1\},\qquad \log x=\sum_{n\ge1}\frac{(-1)^{n+1}}{n}(x-1)^n\quad(x\in\cU), \] and, following Roy \cite[p.~24]{Roy1992}, \[ L=\text{the $\QQ$-span of }\log(\Qbar\cap\cU),\qquad \cL=\Qbar+\Qbar\cdot L\subset\Cp . \] Every $\alpha\in\Qbar^\times$ has a power $\alpha^N$ with $\alpha^Np^{-m}\in\cU$ for some $m\in\ZZ$, and $\logp\alpha:=N^{-1}\log(\alpha^Np^{-m})$ is the Iwasawa logarithm ($\logp p=0$); so $L=\logp(\Qbar^\times)$, and $\cL$ is the set of numbers $\beta_0+\sum_i\beta_i\logp\alpha_i$ with $\beta_i\in\Qbar$ and $\alpha_i\in\Qbar^\times$: the $p$-adic linear forms in logarithms of algebraic numbers with algebraic coefficients, with a constant term. The formalization is public at \begin{center} \url{https://github.com/telaviv/p-adic-log-products}, \end{center} at the revision pinned in Section~\ref{sec:verify}. Its endpoints are the following five statements. For each we give the name of the Lean declaration; Section~\ref{sec:defs} reproduces the Lean definitions of $\cU$, $\log$, $\Qbar$, $L$, $\cL$ and of the numbers involved, which is what a reader has to check to trust the certificate. \begin{theorem}[\lean{LogIrr.e2_unconditional}, \lean{LogIrr.e2'_unconditional}]\label{thm:e2} Let $p$ be a prime with $p\equiv3$ or $5\pmod 8$, and let $\sqrt2$ be either square root of $2$ in $\Cp$ (it lies in $\Qpbar\setminus\Qp$). Then \[ \logp2\cdot\logp(3+\sqrt2)\notin\cL \qquad\text{and}\qquad \logp2\cdot\logp(3-\sqrt2)\notin\cL . \] \end{theorem} Theorem~\ref{thm:e2} is an instance of a uniform statement for real quadratic fields. For an integer $d$ write $x=a'+b'\sqrt d$ for elements of $\ZZ[\sqrt d]$, $\bar x=a'-b'\sqrt d$ and $N(x)=x\bar x$. \begin{theorem}[\lean{LogIrr.Quad.main_unconditional}] \label{thm:quad} Let $d>0$ be an integer that is not a square modulo $p$, let $a\in\ZZ$ with $p\nmid a$ and $|a|\ge2$, and let $x=a'+b'\sqrt d\in\ZZ[\sqrt d]$ with $a',b'>0$, $p\nmid N(x)$ and $|N(x)|\ge2$. Then $\logp a\cdot\logp x\notin\cL$, and likewise $\logp a\cdot\logp\bar x\notin\cL$ (\lean{Quad.main'_unconditional}). \end{theorem} The instances in the repository (\lean{LogIrr/Inst/}) are: $d=2$, $x=3+\sqrt2$, $p\equiv\pm3\pmod8$, any such $a$ (\lean{e2a_unconditional}; with $a=2$ this is Theorem~\ref{thm:e2}); $d=3$, $x=4+\sqrt3$, $p\equiv\pm5\pmod{12}$, $p\neq13$ (\lean{e4_unconditional}); $d=5$, $x=4+\sqrt5$, $p\equiv\pm2\pmod5$, $p\neq2,11$ (\lean{e5_unconditional}). The congruence conditions say that $d$ is a quadratic non-residue modulo $p$, and the excluded primes divide $N(x)$. Both theorems come from one principle. Call $\sigma$ a \emph{continuous automorphism} of $\Cp$ if it is an isometric ring automorphism (every element of $\Gal(\Qpbar/\Qp)$ extends uniquely to one, Section~\ref{sec:galois}). \begin{theorem}[\lean{LogIrr.thm51_pm_unconditional}, \lean{thm51_unconditional}]\label{thm:general} Let $\sigma$ be a continuous automorphism of $\Cp$, let $t\in L$ be nonzero with $\sigma t=t$, and let $u\in L$ be nonzero with $\sigma^n u=u$ for some $n\ge1$ and $\sigma u\neq\pm u$. Then $tu\notin\cL$. More generally the conclusion holds if $\sigma t\in\Qbar+\Qbar t$, $t\neq0$, and $u,\sigma u$ are linearly independent over $\QQ$. \end{theorem} This is \cite[Cor.~2(2)]{Diaz2007} with $\sigma$ in place of complex conjugation. Over $\CC$ the only continuous automorphisms are the identity and conjugation, both of which fix $\log2$ and $\log(3+\sqrt2)$, and $\log2\cdot\log(3+\sqrt2)\notin\cL$ is open \cite{Diaz2007,Waldschmidt2005b,Waldschmidt2023}. Over $\Cp$ the group $\Gal(\Qpbar/\Qp)$ acts continuously, which is the whole point. The input to Theorem~\ref{thm:general} is Roy's form of Waldschmidt's linear-subgroup theorem for $\Ga^{d_0}\times\Gm^{d_1}$ \cite[Theorem~1]{Roy1992}, \cite[Theorem~4.1]{Waldschmidt1988}, over $\Cp$. For $d_0,d_1\ge0$ put $E=\Cp^{d_0}\times\Cp^{d_1}$. A $\Cp$-subspace of $E$ is \emph{rational over $\Qbar$} if it is spanned by vectors with coordinates in $\Qbar$. \begin{theorem}[\lean{LogIrr.Padic.waldschmidtTheorem1_p}]\label{thm:waldschmidt} Let $Y\subset\Qbar^{d_0}\times L^{d_1}$ be a finite-dimensional $\QQ$-subspace of $E$, let $W\subset E$ be a $\Cp$-subspace rational over $\Qbar$, and let $V\subset E$ be a $\Cp$-subspace containing $Y$ and $W$. If $V\neq E$, there are $d_0',d_1'\ge0$ and a surjective $\Cp$-linear map $s\colon E\to E'=\Cp^{d_0'}\times\Cp^{d_1'}$ with $s(\Qbar^{d_0}\times0)\subset\Qbar^{d_0'}\times0$ and $s(0\times\QQ^{d_1})\subset0\times\QQ^{d_1'}$, such that $W'=s(W)\neq E'$ and, with $Y'=s(Y)$, \[ \frac{d_1'+\dim_{\QQ}Y'}{d_0'+d_1'-\dim_{\Cp}W'} \;\le\; \frac{d_1}{d_0+d_1-\dim_{\Cp}V}. \] \end{theorem} This is Roy's Theorem~1 verbatim for $K=\Cp$. Roy states it for $K=\CC$ and $K=\Cp$ at once, with a period lattice $\Omega=0\times\omega\QQ^{d_1}$ where $\omega=2\pi i$ over $\CC$ and $\omega=0$ over $\Cp$ \cite[p.~24]{Roy1992}; the terms $\dim_{\QQ}(Y\cap\Omega)$ of his inequality vanish $p$-adically, and the Lean statement keeps them literally with $\Omega=0$ (Section~\ref{sec:defs}). Roy's reduction from Theorem~\ref{thm:waldschmidt} to his Corollary~2 is field-independent and is also formalized, so we get the two consequences that Theorem~\ref{thm:general} actually uses. \begin{corollary}[strong six exponentials over $\Cp$; \lean{LogIrr.royCor2}]\label{cor:six} If $x_1,x_2\in\Cp$ are linearly independent over $\Qbar$ and $y_1,y_2,y_3\in\Cp$ are linearly independent over $\Qbar$, then $x_iy_j\notin\cL$ for some $i,j$. Equivalently \cite[Cor.~2]{Roy1992}: a $2\times3$ matrix with entries in $\cL$ whose rows and whose columns are $\Qbar$-linearly independent has rank $2$. \end{corollary} \begin{corollary}[Baker--Brumer over $\Cp$, $n\le2$; \lean{LogIrr.bakerBrumer}] \label{cor:baker} A nonzero element of $L$ is transcendental. If $\ell_1,\ell_2\in L$ are linearly independent over $\QQ$, then $1,\ell_1,\ell_2$ are linearly independent over $\Qbar$. \end{corollary} \subsection*{What is new} The mathematics of Theorems~\ref{thm:e2}--\ref{thm:general} is a transposition of Diaz's complex-conjugation argument \cite{Diaz2004,Diaz2007}, and Theorem~\ref{thm:waldschmidt} is a statement Roy made in 1992 and attributed to Waldschmidt. The claims of novelty are therefore modest and all of the form ``we could not find this in print'' (the search is recorded in Section~\ref{sec:related}): \begin{enumerate} \item no statement of the form ``a product of two $p$-adic logarithms of algebraic numbers lies outside $\cL$'' was found in the literature; Momot \cite[\S1.3]{Momot2010} explicitly leaves the ultrametric analogue of Diaz's results to a further paper; \item no proof written for $\Cp$ of the \emph{mixed} linear-subgroup theorem (a $\Ga$ factor, derivatives along a subspace $W\neq0$, a general $V$) was found; the published $p$-adic results are the Schneider case without derivatives \cite{Waldschmidt1981,Dasgupta2023} and the analytic subgroup theorem \cite{Matev2010,FuchsPham2015a,FuchsPham2015b}; \item we are not aware of an earlier machine-checked proof of any six-exponentials-type theorem, of a linear-subgroup theorem with derivatives, or of any $p$-adic transcendence theorem. \end{enumerate} The proof of record for everything in this paper is the Lean library \lean{LogIrr} \cite{PadicLogProducts}, which depends only on Lean's three standard axioms and contains no \lean{sorry}. The prose proofs were written first and the Lean files follow them; where they differ, the Lean files are authoritative. % =========================================================================== \section{The statements in Lean}\label{sec:defs} % =========================================================================== Mathlib provides $\Cp$ as \leans{PadicComplex p}, written $\CC$\texttt{\_[p]}, with its norm, completeness and algebraic closedness, and the generic exponential \lean{NormedSpace.exp}; it has no $p$-adic logarithm, which the library defines. We reproduce the definitions on which the meaning of the theorems depends (\lean{LogIrr/LogDisc.lean}, \lean{Lp.lean}, \lean{Arith.lean}). Throughout, \lean{p} is a natural number with a \leans{Fact p.Prime} instance. \begin{Verbatim} def U : Set ℂ_[p] := {x | ‖x - 1‖ < 1} noncomputable def logTerm (x : ℂ_[p]) (n : ℕ) : ℂ_[p] := ((-1 : ℂ_[p]) ^ n / ((n : ℂ_[p]) + 1)) * (x - 1) ^ (n + 1) noncomputable def logU (x : ℂ_[p]) : ℂ_[p] := ∑' n, logTerm p x n abbrev Qb : IntermediateField ℚ ℂ_[p] := algebraicClosure ℚ ℂ_[p] noncomputable def L : Submodule ℚ ℂ_[p] := Submodule.span ℚ (logU p '' {x | x ∈ Qb p ∧ x ∈ U p}) noncomputable def Lt : Submodule (Qb p) ℂ_[p] := Submodule.span (Qb p) (insert (1 : ℂ_[p]) (L p : Set ℂ_[p])) \end{Verbatim} So \leans{U p} is $\cU$, \leans{logU p} is the series $\log$ (with the junk value of a non-convergent \lean{tsum} off the disc, never used), \leans{Qb p} is $\Qbar$, \leans{L p} is Roy's $L$ and \leans{Lt p} is $\cL$. The numbers of Theorem~\ref{thm:e2} are defined with $N=p^2-1$ and a chosen square root \leans{s2 p} of $2$ in $\Qpbar\subset\Cp$: \begin{Verbatim} def N : ℕ := (p + 1) * (p - 1) def tE : ℂ_[p] := ((N p : ℂ_[p]))⁻¹ * logU p ((2 : ℂ_[p]) ^ N p) def uE : ℂ_[p] := ((N p : ℂ_[p]))⁻¹ * logU p ((3 + s2 p) ^ N p) def uE' : ℂ_[p] := ((N p : ℂ_[p]))⁻¹ * logU p ((3 - s2 p) ^ N p) theorem e2_unconditional (h8 : p % 8 = 3 ∨ p % 8 = 5) : tE p * uE p ∉ Lt p \end{Verbatim} (The actual definitions apply a ring homomorphism $\ZZ[\sqrt2]\to\Cp$ to $2$ and $3\pm\sqrt2$; the display is the unfolded form.) Since $2^N,(3\pm\sqrt2)^N\equiv1\pmod p$ for $p\equiv\pm3\pmod8$, these are $\logp2$, $\logp(3+\sqrt2)$, $\logp(3-\sqrt2)$ in the sense of Section~\ref{sec:main}; the identification with the Iwasawa logarithm is not needed inside the development, which works with Roy's $L$ directly. Theorem~\ref{thm:quad} is stated for \leans{Quad.tInt p R a}, which is $N^{-1}\log(a^N)$, and \leans{Quad.logN p R x}, which is $N^{-1}\log(x^N)$ with $x\in\ZZ[\sqrt d]$ mapped into $\Cp$ along a chosen root \lean{R} of $d$. Theorem~\ref{thm:waldschmidt} is stated for an arbitrary field $K$ of characteristic $0$ and an arbitrary $\QQ$-subspace \lean{LK} playing the role of $L$ (\lean{LogIrr/Roy/Theorem1.lean}); with \leans{E K d0 d1} the product $(\mathrm{Fin}\,d_0\to K)\times(\mathrm{Fin}\,d_1\to K)$, \lean{AlgVec} and \lean{RatVec} the predicates ``all coordinates algebraic'' and ``all coordinates rational'', \leans{RationalOverQbar W} the predicate ``$W$ is the $K$-span of its algebraic points'', and \leans{Omega K d0 d1} the zero submodule: \begin{Verbatim}[fontsize=\scriptsize] def WaldschmidtTheorem1 (LK : Submodule ℚ K) : Prop := ∀ (d0 d1 : ℕ) (Y : Submodule ℚ (E K d0 d1)) (W V : Submodule K (E K d0 d1)), FiniteDimensional ℚ Y → (∀ p ∈ Y, AlgVec p.1 ∧ ∀ j, p.2 j ∈ LK) → RationalOverQbar W → (∀ p ∈ Y, p ∈ V) → W ≤ V → V ≠ ⊤ → ∃ (d0' d1' : ℕ) (s : E K d0 d1 →ₗ[K] E K d0' d1'), Function.Surjective s ∧ (∀ u : Fin d0 → K, AlgVec u → ∃ u', AlgVec u' ∧ s (u, 0) = (u', 0)) ∧ (∀ v : Fin d1 → K, RatVec v → ∃ v', RatVec v' ∧ s (0, v) = (0, v')) ∧ W.map s ≠ ⊤ ∧ ((d1' : ℚ) - finrank ℚ ↥(Y.map (s.restrictScalars ℚ) ⊓ Omega K d0' d1') + finrank ℚ ↥(Y.map (s.restrictScalars ℚ))) / ((d0' + d1' : ℚ) - finrank K ↥(W.map s)) ≤ ((d1 : ℚ) - finrank ℚ ↥(Y ⊓ Omega K d0 d1)) / ((d0 + d1 : ℚ) - finrank K ↥V) theorem waldschmidtTheorem1_p : WaldschmidtTheorem1 ℂ_[p] (L p) \end{Verbatim} Corollary~\ref{cor:six} is \leans{RoyCor2 p}, the product form of Roy's Corollary~2 with ``$\Qbar$-linearly independent'' expressed as: no nontrivial relation with algebraic coefficients; Corollary~\ref{cor:baker} is \leans{BakerBrumer p}, the conjunction of the two statements as written (\lean{LogIrr/Lp.lean}). Theorem~\ref{thm:general} is stated for \leans{ContAut p}, the structure of ring automorphisms of $\Cp$ that are isometries (\lean{LogIrr/Galois.lean}). % =========================================================================== \section{Mathematical route}\label{sec:route} % =========================================================================== \subsection{The logarithm and the Galois action}\label{sec:galois} On $\cU$ the series $\log$ converges and is a homomorphism $(\cU,\cdot)\to(\Cp,+)$ (\lean{LogIrr.logHom}; proved by a binomial double series, without formal power series). Its kernel consists of $p$-power roots of unity (\lean{logKer}). On the disc $D=\{|x-1|<\rho_p\}$, $\rho_p=p^{-1/(p-1)}$, one has $\exp\circ\log=\mathrm{id}$, and $\log\circ\exp=\mathrm{id}$ on $\{|y|<\rho_p\}$ (\lean{exp_logU}, \lean{logU_exp}). The last two are proved without composing power series: the defect $g(v)=\exp(\log v)/v$ satisfies $|g(v)-1|\le|v-1|^2/\rho_p$ by quadratic bounds on both series and is a homomorphism on $D$, while $|w^{p^k}-1|=|w-1|\,p^{-k}$ exactly on $D$; applying the bound to $v^{p^k}$ gives $|g(v)-1|\le|v-1|^2p^{-k}/\rho_p$ for every $k$, so $g(v)=1$. Every $\sigma\in\Gal(\Qpbar/\Qp)$ is an isometry, by the uniqueness of the extended absolute value, and extends uniquely to a continuous ring automorphism of $\Cp$ fixing $\Qp$. Any continuous ring homomorphism commutes with the series $\log$ on $\cU$, and an isometric automorphism preserves $\Qbar$, $\cU$, $L$ and $\cL$ (\lean{LogIrr/Galois.lean}, \lean{Galois2.lean}). There is no branch issue: $\logp$ is single-valued, so $\sigma(\logp\alpha)=\logp(\sigma\alpha)$ is an identity, not a congruence modulo $2\pi i\ZZ$. \subsection{The conjugation argument}\label{sec:conj} \begin{proposition}[\lean{LogIrr.thmA}]\label{prop:A} Let $\sigma$ be a continuous automorphism of $\Cp$, $t\in\cL\setminus\Qbar$ and $u\in\cL$. Suppose $\sigma t\in\Qbar+\Qbar t$ and that $1,u,\sigma u$ are linearly independent over $\Qbar$. Then $tu\notin\cL$. \end{proposition} \begin{proof} Write $\sigma t=a+bt$ with $a,b\in\Qbar$; then $b\neq0$, since $t\notin\Qbar$ and $\sigma$ preserves $\Qbar$. Suppose $v=tu\in\cL$. Then $\sigma v=a\,\sigma u+bt\,\sigma u$, so $t\,\sigma u=b^{-1}(\sigma v-a\,\sigma u)\in\cL$, because $\sigma(\cL)=\cL$. The matrix \[ \begin{pmatrix}1&u&\sigma u\\ t&tu&t\,\sigma u\end{pmatrix} \] has entries in $\cL$, rank $\le1$, rows that are $\Qbar$-independent (as $t\notin\Qbar$) and columns that are $\Qbar$-independent (by hypothesis). Corollary~\ref{cor:six} says its rank is $2$. \end{proof} Theorem~\ref{thm:general} follows from Proposition~\ref{prop:A} and Corollary~\ref{cor:baker}: a nonzero $t\in L$ is transcendental, and if $u,\sigma u\in L$ are $\QQ$-independent then $1,u,\sigma u$ are $\Qbar$-independent. For the first form of Theorem~\ref{thm:general}, if $\sigma u=ru$ with $r\in\QQ$ then $\sigma^nu=r^nu$, so $r^n=1$ and $r=\pm1$ (\lean{linearIndependent_pair_of_orbit}). \subsection{The quadratic instances}\label{sec:instances} Let $d>0$ be a non-residue modulo $p$. Then $d$ is not a square in $\Qp$, $X^2-d$ is irreducible over $\Qp$, and some $\sigma\in\Gal(\Qpbar/\Qp)$ swaps the two roots $\pm\sqrt d$; it fixes $\Qp$, hence $t=\logp a$ for $a\in\ZZ$, and sends $\logp x$ to $\logp\bar x$ for $x\in\ZZ[\sqrt d]$ (\lean{LogIrr/Quad.lean}). For $N=p^2-1$ the Frobenius congruence $x^p\equiv\bar x\pmod p$ in $\ZZ[\sqrt d]$ (Euler's criterion for the non-residue $d$) gives $x^N\equiv1\pmod p$ whenever $p\nmid N(x)$, so $\logp x=N^{-1}\log(x^N)$ is defined by the series and lies in $L$. That $t\neq0$ follows from the kernel description: $a^{NM}=1$ is impossible for $|a|\ge2$. The one arithmetic input of Theorem~\ref{thm:quad} is that $\logp x$ and $\logp\bar x$ are $\QQ$-linearly independent when $a',b'>0$, $p\nmid N(x)$ and $|N(x)|\ge2$ (\lean{Quad.linearIndependent_pair}). A relation gives $(x^b\bar x^c)^M=1$ in $\Cp$ for integers $b,c$ not both zero and some $M\ge1$; applying $\sigma$ and multiplying, $N(x)^{(b+c)M}=1$ in $\QQ$, so $c=-b$; then $x^{bM}=\bar x^{bM}$ in $\ZZ[\sqrt d]$, which is impossible for $b\neq0$ because the $\sqrt d$-coordinate of $x^k$ is positive for all $k\ge1$. For Theorem~\ref{thm:e2} the original development (\lean{LogIrr/Indep.lean}) argues instead with the $2$-adic and $7$-adic valuations of a relation $2^{aM}(3+\sqrt2)^{bM}(3-\sqrt2)^{cM}=1$ in $\ZZ[\sqrt2]$, which is a Euclidean domain in which $\sqrt2$, $3\pm\sqrt2$ are non-associate primes; the repository keeps both proofs, and \lean{Inst/Sqrt2.lean} re-derives Theorem~\ref{thm:e2} from Theorem~\ref{thm:quad}. Why these numbers: the hypotheses of Theorem~\ref{thm:general} need a logarithm whose $\Qbar$-line is $\sigma$-stable and a logarithm whose line is moved to an independent one. A rational $a$ gives $t\in\Qp$, fixed by all of $\Gal(\Qpbar/\Qp)$. Units such as $1+\sqrt2$ fail, since $\sigma\varepsilon=-\varepsilon^{-1}$ keeps the line stable; so do $\logp2\cdot\logp3$ and all squares $(\logp\alpha)^2$, whose lines are stable. The congruence $p\equiv\pm3\pmod 8$ is exactly the condition $\sqrt2\notin\Qp$. \subsection{From Theorem~\ref{thm:waldschmidt} to the corollaries}\label{sec:roy} Roy's derivation of his Corollary~2 from Theorem~1 \cite[\S\S1--4]{Roy1992} is linear algebra over $K$, $\Qbar$ and $\QQ$ together with the combinatorics of his admissible categories; the only field-dependent datum is $\omega$. The formalization of that derivation over $\CC$ \cite{StrongSixLean} was ported to a field $K$ of characteristic $0$ and a $\QQ$-subspace \lean{LK} by a script (replacing $\CC$ by $K$, the logarithms by \lean{LK}, and $\Omega$ by $0$) with a few hand patches; with $\Omega=0$ every occurrence of the period terms collapses, which is Roy's remark on p.~24. The result (\lean{LogIrr/Roy/}, about $2{,}700$ lines) is \begin{Verbatim} theorem strongSix_of_theorem1 : WaldschmidtTheorem1 K LK → StrongSixExponentials K LK \end{Verbatim} Corollary~\ref{cor:baker} is derived from Theorem~\ref{thm:waldschmidt} directly (\lean{LogIrr/Roy/Baker.lean}), along the lines of \cite[Cor.~3.3]{Waldschmidt1988} to which Roy points in his Remark~(iii), p.~37: transcendence of a nonzero $\ell\in L$ from the Gel'fond data $\Ga\times\Gm$, $Y=\QQ(1,\ell)$, $W=V=K(1,\ell)$, where Roy's inequality forces $s$ to kill $Y$; the homogeneous relation $\ell_2=\beta_1\ell_1$ from Schneider data $\Ga\times\Gm$, $W=0$; and the inhomogeneous relation $\ell_2=\beta_0+\beta_1\ell_1$ from $\Ga^2\times\Gm$, $V=\{w=\beta_0z_0+\ell_1z_1\}$, $W=K\cdot((1,0),\beta_0)$, with a case analysis on the two blocks of $s$. Only two logarithms are needed for Theorem~\ref{thm:general}. The homogeneous statement for all $n$ is Brumer's $p$-adic theorem \cite{Brumer1967}; we did not formalize it. \subsection{Theorem~\ref{thm:waldschmidt}: what changes over $\Cp$}\label{sec:thm1} The proof over $\CC$ \cite{StrongSixLean} is a transcendence proof by Laurent's interpolation determinants \cite{Laurent1994}. Given $(Y,W,V)$ and parameters $(S,T,D_0,D_1)$ one forms the matrix of the derivatives $D_{w_1}\cdots D_{w_t}X^\lambda Y^\mu$ along a basis of the algebraic points of $W$, evaluated at the grid points $\exp_G(\sum s_i\eta_i)$, $\eta_i$ a $\QQ$-basis of $Y$. Either the columns are dependent, and Philippon's multiplicity estimate \cite{Philippon1986} produces an obstruction subgroup $H=h_0\times T_U$ whose cokernel is the map $s$; or a maximal minor $\Delta\neq0$ is bounded above analytically and below by Liouville's inequality, and the bounds contradict each other for large parameters. The $p$-adic proof keeps this architecture and the same parameters, and changes four things. \emph{The multiplicity estimate} needs nothing: \lean{StrongSix.M2.multEst_of_isAlgClosed} of \cite{StrongSixLean} is Philippon's theorem with derivatives on $\Ga^{d_0}\times\Gm^{d_1}$ over every algebraically closed field of characteristic $0$ (following Roy's affine treatment in \cite[Ch.~5, 8]{DALAG}), and $\Qbar\subset\Cp$ is algebraically closed. \emph{The field-generic half} of the proof (the reduction to the case $1\le\dim V$, $d_0\le\dim V$; multilinearity of words of derivations; the interpolation matrix and the dichotomy; the exponent bookkeeping; the obstruction subgroup, the map $s$ and $\dim s(W)$; the count of inequivalent grid points; the number field containing the data and the denominators and houses of the entries) was checked over $\CC$ by the Lean kernel and re-checked over a field $\mathbb K$ after a mechanical port (\lean{LogIrr/Thm1/}, about $1{,}700$ lines). Three hand patches: Roy's preliminary quotient by $K\cdot(Y\cap\Omega)$ is vacuous since $\Omega=0$; the point data no longer carry $\exp$; and the step ``equivalent grid points satisfy $s(\gamma-\gamma')\in\Omega'$'', which over $\CC$ uses $\ker\exp=2\pi i\ZZ$, takes the multiplicative relation as a hypothesis, discharged $p$-adically by the injectivity of $\exp$ on its disc. \emph{The $p$-adic half} (\lean{LogIrr/Padic/}, \lean{LogIrr/PadicCore/}) replaces the archimedean ingredients: \begin{enumerate} \item \emph{The exponential and the small basis.} $\exp$ converges only on $|z|<\rho_p$. Every $\ell\in L$ satisfies $N\ell=\log y$ with $y\in\Qbar$ arbitrarily close to $1$: clear the denominators of a representation $\ell=\sum q_k\log x_k$ (induction over the span), then take a $p$-power, using $|x^{p^r}-1|\le|x-1|\max(|x-1|^{p-1},p^{-1})^r$. Hence a $\QQ$-basis $\eta_1,\dots,\eta_\ell$ of $Y$ can be rescaled by one integer $N$, which changes neither $Y$ nor $\dim_{\QQ}Y$, so that all second coordinates lie in the disc of $\exp$ and $\exp\eta_{i,2j}$ is algebraic, and all first coordinates are as small as required. Then $\exp$ is additive on the grid, the grid points are algebraic, and the injectivity of $\exp$ on its disc gives the multiplicative relation above. This is the rescaling $x''=p^ax'$ of \cite[\S\S4--5]{Waldschmidt1981}. \item \emph{The entries.} The entry $(D_{w_1}\cdots D_{w_t}X^\lambda Y^\mu)(g_\gamma)$ at $g_\gamma=(\gamma_0,\exp\gamma_1)$ is the sum of its Taylor coefficients along $z\mapsto z\gamma$, computed algebraically as $c_k=(1/k!)(D_\gamma^kP)(e)$; the factor $1/k!$ is absorbed by the radius, and the Gauss norm of $D_{w_1}\cdots D_{w_t}X^\lambda Y^\mu$ is at most $A^{t}$ when the coordinates of the $w_i$ have norm $\le A$, since the integers produced by differentiation cost nothing $p$-adically. No analytic function of several variables is needed. \item \emph{The Schwarz lemma.} The maximum modulus principle on $|z|=2$ is replaced by the ultrametric multilinear expansion of the determinant with tails: the determinant of the Taylor-coefficient rows vanishes to order $\ge K=M(N-M^n)-\sum t_\nu$, a purely combinatorial count shared with the complex proof, and $|\Delta|\le A^{NT_J}p^{-K}$. This is the principle of \cite[Lemme~3.4.p]{Waldschmidt1981} and \cite[\S5]{Dasgupta2023}; there is no $N!$ and no maximum over a circle. \item \emph{Liouville at the $p$-adic place.} For a nonzero algebraic integer $\beta$ of a number field $F$ of degree $k$ and an embedding $\varphi\colon F\to\Cp$, $1\le|\varphi\beta|\cdot\house{\beta}^{\,k}$, where $\house{\beta}$ is the house: the norm $N_{F/\QQ}(\beta)$ is the product of the $k$ embeddings $F\to\Cp$, which exist because $\Cp$ is algebraically closed, each factor is integral and so has $|\cdot|\le1$, and $N_{F/\QQ}(\beta)$ is a nonzero integer bounded by $\house\beta^{\,k}$ at the complex places. The exponent is $k$ rather than $k-1$ as over $\CC$, which only changes constants. \end{enumerate} The assembly is the complex one with the radius $r_0=1/p$, the two new bounds, and the logarithmic inequality $(M/2-T_J)\log p\le T_J\log A+k\log N+k\log E+k\log H$ in place of its complex counterpart; the final growth comparison is reused verbatim. The $p$-adic analytic side is smaller than the complex one: no $N!$, no exponential of the size of the grid, no Siegel lemma, no auxiliary function on a polydisc. \emph{Comparison with the published $p$-adic results.} Waldschmidt \cite{Waldschmidt1981} proves, for any complete non-archimedean field of characteristic $0$ and residue characteristic $p$, the splitting theorem (Th\'eor\`eme~1.1.p) and the rank bound (Th\'eor\`eme~2.1.p) by Schneider's method, with a $p$-adic Siegel lemma, the ultrametric interpolation lemma and Masser's zero estimate without multiplicities; there is no derivative, no $\Ga$ factor and no subspace $W$. Theorem~\ref{thm:waldschmidt} adds the $\Ga^{d_0}$ factor (algebraic constants in the entries), derivatives along a $\Qbar$-rational $W\neq0$, the general $V$ and the cokernel $s$, and uses interpolation determinants instead of Siegel's lemma. Th\'eor\`eme~2.1.p is the case $d_0=0$, $W=0$, through Roy's \S4. The analytic subgroup theorem of \cite{FuchsPham2015b} is the Gel'fond case $W=V$ with one point. Dasgupta \cite[\S5]{Dasgupta2023} proves the $p$-adic Waldschmidt--Masser theorem (entries in $L$, no constants, no derivatives). Laurent's paper \cite{Laurent1989}, which Roy says uses the $p$-adic theorem, was not accessible to us. % =========================================================================== \section{Related work}\label{sec:related} % =========================================================================== \emph{The $p$-adic linear-subgroup theorem.} Serre proved the $p$-adic six exponentials theorem \cite{Serre1967} and Brumer the $p$-adic Baker theorem \cite{Brumer1967}. Waldschmidt's \cite{Waldschmidt1981} has a second part, ``le cas $p$-adique'', proving the several-variable generalization of the six exponentials theorem and the bound $r_p\ge r/2$ for the $p$-adic rank of units; the Budapest and Grenoble talks \cite{Waldschmidt1984} present the same result. The mixed statement with a derivative subspace is Theorem~4.1 of \cite{Waldschmidt1988}, stated and proved over $\CC$. Roy \cite{Roy1992} states it for $K=\CC$ or $\Cp$ with $\omega=0$, builds his rank theory on it for both fields, and applies it $p$-adically in his \S6; see also \cite{Roy1993}. Later $p$-adic uses cite Roy: \cite{Jaulent2002}, \cite[\S3]{CalegariMazur2009}, \cite[Thm~1.8]{BetinaDimitrov2021}, \cite[Thm~2.2.1]{Maksoud2023}. Waldschmidt's survey \cite[\S\S5--6]{Waldschmidt2023} says that for the strong six exponentials theorem ``as always, the situation is the same in the $p$-adic case''. On the Gel'fond side, the $p$-adic analytic subgroup theorem is due to Matev \cite{Matev2010} and Fuchs--Pham \cite{FuchsPham2015a,FuchsPham2015b}; Dasgupta \cite{Dasgupta2023} and Dasgupta--Kakde \cite{DasguptaKakde2026} treat the archimedean and $p$-adic structural rank conjectures. We found no proof written for $\Cp$ of the mixed statement. The statement should be regarded as folklore since Roy, and our claim is only that we could not locate a written proof. \emph{Products of logarithms and conjugation.} Diaz \cite{Diaz2004} used complex conjugation with the six exponentials theorem to show, for instance, that $\log a\cdot\log(2+i)\notin\cL$ for real $\log a$, and in \cite{Diaz2007} derived from Roy's theorem partial cases of the strong four exponentials conjecture, including the ``one of two implies both'' upgrade that Theorem~\ref{thm:general} transposes. Waldschmidt's surveys \cite{Waldschmidt2005a,Waldschmidt2005b} collect these results; none has $p$-adic content. Momot \cite{Momot2010} generalizes Diaz by Weil restriction to real subfields and leaves the ultrametric analogue to a further paper. Betina--Dimitrov \cite{BetinaDimitrov2021} and Maksoud \cite{Maksoud2023} use the strong six exponentials theorem over $\Qpbar$ for ``one of two'' non-vanishing statements and leave ``both'' to the strong four exponentials conjecture; the quantities there are $2\times2$ minors, not products. \emph{Formalizations.} Machine-checked transcendence results before this work: $e$ and $\pi$ in several provers, Lindemann--Weierstrass \cite{Bernard2017,Eberl2021}, Liouville numbers (Mathlib), Gelfond--Schneider in Lean \cite{KaratarakisWiedijk2026}, and the author's strong six exponentials theorem over $\CC$ with Waldschmidt's theorem and Philippon's multiplicity estimate \cite{StrongSixLean}, on which the present library is built. The library \cite{DiazModulus} (unrefereed; its README reports standard axioms) claims the classical six exponentials theorem, qualitative Baker's theorem and Gelfond--Schneider over $\CC$, and carries Roy's strong six exponentials theorem as a hypothesis; its README mentions a branch, not inspected by us, for Brumer's $p$-adic theorem. Mathlib has $\Cp$ and the generic exponential but no $p$-adic logarithm and no radius bound for $\exp$ over $\Cp$; these were built here. The novelty claims of Section~\ref{sec:main} rest on web, arXiv and zbMATH searches recorded with the paper; MathSciNet was not available to us. % =========================================================================== \section{AI-assisted formalization}\label{sec:workflow} % =========================================================================== The prose proofs, the Lean code and the text of this paper were produced by AI models (Claude, Anthropic) working in Claude Code under the direction of the author, in the following order. A note was written stating Theorem~\ref{thm:e2} and proving it modulo two inputs labelled as taken from the literature, Corollaries~\ref{cor:six} and~\ref{cor:baker} over $\Cp$, and checking line by line that Roy's reduction is field-independent. A second note classified every lemma of the complex Lean proof of Waldschmidt's theorem as field-independent or archimedean and supplied the four $p$-adic replacements of Section~\ref{sec:thm1}. The Lean files were then written against these notes: first Theorem~\ref{thm:e2} with Corollaries~\ref{cor:six} and~\ref{cor:baker} as explicit hypotheses, then the two corollaries from Theorem~\ref{thm:waldschmidt} as a hypothesis, then Theorem~\ref{thm:waldschmidt} itself, so that each implication was checked before the next input was attempted. The complex formalization was reused by mechanical renaming where it was field-generic and reproved where it was not. The whole development took two days. An independent AI session, separate from the ones that wrote the proofs, audited the definitions of Section~\ref{sec:defs} against Roy's paper and wrote the trust document in the repository; another ran the literature search of Section~\ref{sec:related}. Apart from the check by the Lean kernel, all verification so far has been carried out by AI systems. No human expert has yet reviewed the Lean definitions against the literature or read the proofs; we would be grateful for corrections. The author is responsible for the intended statements and for the claims made here. % =========================================================================== \section{Formal artifact and verification}\label{sec:verify} % =========================================================================== The formalization uses Lean~4 \cite{Lean4} and Mathlib \cite{Mathlib}. \begin{center}\small \begin{tabular}{@{}ll@{}} \toprule Repository & \url{https://github.com/telaviv/p-adic-log-products} \\ Commit & \lean{9e4570067a2140f7193e3befee3bf0f1335419d8} \\ Lean & \lean{leanprover/lean4:v4.35.0} \\ Mathlib & \lean{v4.35.0} \\ Mathlib commit & \lean{56a005855ea17e0b0958f73ec801ae140b0a1679} \\ Dependency & \url{https://github.com/telaviv/strong-six-exponentials} \\ Dependency commit & \lean{1625bdf3c0a7d9222bacd876d738d7540109bea6} \\ \bottomrule \end{tabular} \end{center} The toolchain and package revisions are pinned in \lean{lean-toolchain} and \lean{lake-manifest.json}. The library \lean{LogIrr} has 50 files and about $10{,}400$ lines; from the dependency it imports only field-generic modules (the multiplicity estimate, the invariant derivations, heights and houses, Liouville's inequality), none of which mentions $\CC$. \begin{center} \begin{tabular}{@{}lrp{0.55\textwidth}@{}} \toprule Directory & Lines & Content \\ \midrule \lean{LogIrr/} (top level) & 3{,}022 & the logarithm on $\cU$, $\exp\circ\log$, the Galois action, the arithmetic of $3\pm\sqrt2$, Proposition~\ref{prop:A}, Theorems~\ref{thm:e2}, \ref{thm:quad}, \ref{thm:general} \\ \lean{LogIrr/Roy/} & 3{,}376 & Theorem~\ref{thm:waldschmidt} $\Rightarrow$ Corollaries~\ref{cor:six}, \ref{cor:baker}, over any field of characteristic $0$ \\ \lean{LogIrr/Thm1/} & 1{,}680 & the field-generic half of the proof of Theorem~\ref{thm:waldschmidt} \\ \lean{LogIrr/Padic/} & 982 & the $p$-adic half and the assembly \\ \lean{LogIrr/PadicCore/} & 942 & the $p$-adic exponential and the ultrametric determinant bound \\ \lean{LogIrr/Inst/} & 270 & the instances of Theorem~\ref{thm:quad} \\ \bottomrule \end{tabular} \end{center} To build the library at the pinned revision: \begin{Verbatim} git clone https://github.com/telaviv/p-adic-log-products cd p-adic-log-products git checkout 9e4570067a2140f7193e3befee3bf0f1335419d8 lake exe cache get lake build \end{Verbatim} The build compiles the dependency's multiplicity estimate and takes about fifteen minutes on a desktop once Mathlib is cached. To inspect the endpoints and their axiom closures, run \texttt{lake env lean Axioms.lean}; the file contains, among queries for the intermediate results, \begin{Verbatim} #print axioms LogIrr.e2_unconditional #print axioms LogIrr.Quad.main_unconditional #print axioms LogIrr.thm51_pm_unconditional #print axioms LogIrr.Padic.waldschmidtTheorem1_p #print axioms LogIrr.royCor2 #print axioms LogIrr.bakerBrumer \end{Verbatim} Every one of the 44 queries yields \texttt{[propext, Classical.choice, Quot.sound]}; the output is recorded in the repository's \lean{TRUST.md}. The source contains no \lean{sorry}, no \lean{axiom} declaration and no \lean{native_decide}. These checks concern the named declarations and their dependencies; the mathematical meaning of the results also depends on the definitions reproduced in Section~\ref{sec:defs}, and \lean{TRUST.md} compares each of them with its source. % =========================================================================== \section{Open questions}\label{sec:open} % =========================================================================== \begin{enumerate} \item A proof written for $\Cp$ of the mixed Theorem~\ref{thm:waldschmidt} in the literature, perhaps in \cite{Laurent1989}, would make Section~\ref{sec:thm1} a confirmation rather than a first proof. \item The complex analogue of Theorem~\ref{thm:e2}, and the strong four exponentials conjecture over $\Cp$: the method says nothing about $\logp2\cdot\logp3$ or about $(\logp\alpha)^2$, whose $\Qbar$-lines are stable under $\Gal(\Qpbar/\Qp)$. \item A ``swap'' version of Theorem~\ref{thm:general}, with $\sigma t\in\Qbar+\Qbar u$ and $1,t,\sigma u$ independent, gives instances in cyclic cubic fields such as $\logp\theta\cdot\logp\tau\theta$ for $\theta=2\cos(2\pi/7)$; it has no complex counterpart, since it needs a Galois element of order $3$ acting continuously. It is proved in the project notes but not formalized. \item Brumer's theorem for all $n$, and the ``one of two'' statements of \cite{BetinaDimitrov2021,Maksoud2023} that the local Galois action upgrades to ``both''. \end{enumerate} % =========================================================================== \section*{Acknowledgements} % =========================================================================== We thank Michel Waldschmidt for making his papers and \cite{DALAG} freely available. \bibliographystyle{amsplain} \bibliography{references} \end{document}