Hexagon

math.NT — Number Theory

Four exponentials at CM and Beta periods

Contributed by Shawn Krisman

For every nonzero eigen-period $P$ of a CM abelian variety over $\overline{\mathbb{Q}}$ , we show that the four exponentials conjecture and its strong form hold at $t\in\overline{\mathbb{Q}}^\times P^{\pm1}$ and $t\in\overline{\mathbb{Q}}^\times(P/\pi)^{\pm1}$ ; these include Beta values such as $t=\Gamma(1/5)^2/\Gamma(2/5)$ . For an elliptic curve $E$ over $\overline{\mathbb{Q}}$ with complex multiplication, we also show that $e^{\pi^2}$ and $\wp_E(1/\pi)$ are not both algebraic. Further results concern two CM elliptic curves: for example, $\pi,\varpi,\Omega_\rho,\varpi\Omega_\rho$ are linearly independent over $\overline{\mathbb{Q}}$ , where $\varpi$ and $\Omega_\rho$ are periods of $y^2=4x^3-4x$ and $y^2=4x^3-4$ . These are explicit consequences of published theorems of Waldschmidt (1988) and Roy–Waldschmidt (1993), together with classical results of Baker, Schneider, Masser and Wüstholz; the contribution is the statements and the proofs written out at these periods. Cases at specific periods, such as that $2^{\varpi}$ and $3^{\varpi}$ are not both algebraic, are checked in Lean 4 and reported separately.

Primarily AI-generated textHuman understanding: no partsBeta valuesLeanalgebraic subgroup theoremcomplex multiplicationelliptic functionsformal verificationfour exponentials conjecturetranscendence

Nov 07, 202626 pages

PDF View work

hexagon:2611.00170v1

math.NT — Number Theory

A Lean formalization of Waldschmidt's subgroup theorem with period term for groups with elliptic factors

Contributed by Shawn Krisman

We formalize in Lean 4 with Mathlib Waldschmidt's algebraic subgroup theorem with period term (Theorem 4.1 of his 1988 Durham paper) for $G=\mathbb{G}_{\mathrm{a}}^{d_0}\times\mathbb{G}_{\mathrm{m}}^{d_1}\times E_1\times\dots\times E_m$ , with $E_j$ elliptic curves with algebraic invariants, under the additional hypothesis $2N\ge d_1+2d_0+\kappa$ . The proof uses only Lean's three standard axioms. Along the way we give what we believe are the first formal proofs of Schneider's theorems on elliptic functions and of the Schneider--Lang criterion, and the first Lean library for the Weierstrass $\sigma$ and $\zeta$ functions. Restricted forms of the theorem cover some vector extensions and the Jacobian of $y^5=x(1-x)$ . A companion certificate uses these to prove explicit cases of the four exponentials conjecture: for example, $2^{\varpi}$ and $3^{\varpi}$ are not both algebraic, where $\varpi$ is the real period of $y^2=4x^3-4x$ , and likewise $2^{B(1/5,1/5)}$ and $3^{B(1/5,1/5)}$ .

Primarily AI-generated textHuman understanding: no partsLeanSchneider's theoremSchneider-Lang criterionalgebraic subgroup theoremelliptic functionsformal verificationmultiplicity estimatestranscendence

Nov 07, 202630 pages

PDF View work

Matching works

Four exponentials at CM and Beta periods

A Lean formalization of Waldschmidt's subgroup theorem with period term for groups with elliptic factors

Advanced search

math.AC — Commutative Algebra
math.AG — Algebraic Geometry
math.AP — Analysis of PDEs
math.AT — Algebraic Topology
math.CA — Classical Analysis and ODEs
math.CO — Combinatorics
math.CT — Category Theory
math.CV — Complex Variables
math.DG — Differential Geometry
math.DS — Dynamical Systems
math.FA — Functional Analysis
math.GM — General Mathematics
math.GN — General Topology
math.GR — Group Theory
math.GT — Geometric Topology
math.HO — History and Overview
math.IT — Information Theory
math.KT — K-Theory and Homology
math.LO — Logic
math.MG — Metric Geometry
math.NA — Numerical Analysis
math.NT — Number Theory
math.OA — Operator Algebras
math.OC — Optimization and Control
math.PR — Probability
math.QA — Quantum Algebra
math.RA — Rings and Algebras
math.RT — Representation Theory
math.SG — Symplectic Geometry
math.SP — Spectral Theory
math.ST — Statistics Theory
cs.AI — Artificial Intelligence
cs.CC — Computational Complexity
cs.CG — Computational Geometry
cs.DM — Discrete Mathematics
cs.DS — Data Structures and Algorithms
cs.FL — Formal Languages and Automata Theory
cs.IT — Information Theory
cs.LO — Logic in Computer Science
cs.MS — Mathematical Software
cs.NA — Numerical Analysis
cs.SC — Symbolic Computation
math-ph — Mathematical Physics
quant-ph — Quantum Physics
stat.TH — Statistics Theory