Arithmetic relations among elliptic-function values

Formalization status, 29 September 2026: the main theorem and all nine linked milestones are Proved, with zero Open leaves. The selected proof uses the now-Proved Philippon Theorem 2.1 and the completed Weierstrass application bridges. The linked statements retain their explicit formalization conventions and intermediate variants.

Algebraic independence measures whether several complex numbers satisfy a polynomial relation with rational coefficients. For two numbers, independence means that no nonzero polynomial in two variables vanishes at that pair. This is stronger than asking that each number separately be transcendental: two transcendental numbers can still satisfy a polynomial relation with each other. The distinction matters when describing the arithmetic information carried jointly by periods, lattice invariants, and values of analytic functions.

The completed target is Theorem 1 of Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions (2026). It concerns ten numbers attached to a complex lattice and two evaluation points. The conclusion selects an algebraically independent pair from those ten entries; it does not specify that the pair must consist of two particular function values. The mathematical result is published, and this mission now supplies its checked Lean proof. A source comparison on 29 September 2026 checked the main theorem’s hypotheses, ten values, full-period quasi-period normalization and pair-independence conclusion. The main statement needs no correction.

A lattice and its canonical functions

Take complex numbers $\omega_1,\omega_2$ that are linearly independent over the real numbers. Their integer linear combinations form the period lattice

$$\Omega=\mathbb Z\omega_1+\mathbb Z\omega_2.$$

The formal representation is Mathlib's PeriodPair. Its lattice determines the Weierstrass elliptic function $\wp$ and invariants $g_2,g_3$, using Mathlib's existing definitions. Thus the lattice, function, and invariants are linked by their construction; they are not unrelated parameters.

The Weierstrass zeta function is fixed by the lattice series

$$\zeta_\Omega(z)=\frac1z+\sum_{\lambda\in\Omega\setminus\{0\}} \left(\frac1{z-\lambda}+\frac1\lambda+\frac{z}{\lambda^2}\right).$$

This is the normalization in DLMF equation 23.2.5. For a lattice element $\omega$, its quasi-period is represented by

$$\eta_\Omega(\omega)=\zeta_\Omega(\omega_1/2+\omega)-\zeta_\Omega(\omega_1/2).$$

Both arguments lie outside the lattice. Relating this fixed increment to the increment at an arbitrary regular point is part of the established analytic infrastructure. The normalization concerns the full period $\omega$; references using half-periods require the corresponding factors of two, as in DLMF equation 23.2.11.

Formalization targets

Theorem 1: an algebraically independent pair

Let $\omega\ne0$ belong to $\Omega$. Suppose $u_1,u_2,\omega$ are linearly independent over $\mathbb Q$ and

$$(\mathbb Z u_1+\mathbb Z u_2)\cap\Omega=\{0\}.$$

Define the indexed tuple

$$V=(g_2,g_3,\omega,\eta_\Omega(\omega),u_1,u_2, \wp(u_1),\zeta_\Omega(u_1),\wp(u_2),\zeta_\Omega(u_2)).$$

The proved conclusion is

$$\exists i,j\in\{0,\ldots,9\},\quad i\ne j\quad\text{and}\quad (V_i,V_j)\text{ is algebraically independent over }\mathbb Q.$$

These are the hypotheses and conclusion of the paper's Theorem 1. No algebraicity assumption is imposed on $g_2$ or $g_3$, and the conclusion does not assert independence of all ten entries.

Equations (5) and (6): supporting addition identities

The initial supporting targets are the two identities used in §4 of the paper. For $z,v,z+v\notin\Omega$, write $\Delta=\wp(v)-\wp(z)$. They assert

$$2\Delta\zeta_\Omega(z+v) =2(\zeta_\Omega(z)+\zeta_\Omega(v))\Delta+\wp'(v)-\wp'(z),$$

and

$$4\Delta^2\wp(z+v) =-4(\wp(z)+\wp(v))\Delta^2+(\wp'(v)-\wp'(z))^2.$$

The statements preserve the paper's multiplied-out forms. They do not require $\Delta\ne0$. These targets supply reusable identities; proving them alone does not establish the arithmetic conclusion of Theorem 1.

Nine completed milestones

Milestone	Linked result
Equation (5) — zeta addition identity	Proved
Equation (6) — elliptic addition identity	Proved
Lemma 6 — entire regularization and interpolation bounds	Proved
Lemma 8 — bounded auxiliary polynomial (formal-grid variant)	Proved
Appendix A.2 — Weierstrass model realization (application bridge)	Proved
Appendix A.2 / Lemma A.1 — subgroup degrees (application bridge)	Proved
Proposition A.1 — zero estimate on the mission’s rank-one grid	Proved
Lemma 9 — bounded-order nonvanishing on the enlarged grid	Proved
Lemma 10 — nonzero small arithmetic elements (linear-degree variant)	Proved

The grid and degree variants are described in the linked statements. The two application bridges identify the Weierstrass objects with the general group-theoretic objects used by Philippon’s theorem.

What the completed formalization establishes

The completed goal certifies that every period pair and every triple satisfying the stated hypotheses yields an independent pair in the precise ten-entry tuple. In particular, a proof must handle arbitrary complex lattice invariants and arbitrary admissible evaluation points. A result for a preferred lattice, algebraic arguments, or a predetermined choice of indices would leave the requested statement unresolved.

The definitions provide a reusable interface for elliptic zeta values: a canonical series, a fixed quasi-period convention, and an explicit finite-family independence predicate. The main theorem and all nine milestones have checked proofs; the theorem pages record their accepted submissions and dependencies.

Analytic identities and arithmetic independence

The central difficulty in the proof is passing from identities of analytic functions to exclusion of rational polynomial relations among selected complex values. Periodicity and the addition identities describe how values are related, but do not by themselves rule out algebraic dependence. Consequently, finishing the elementary function interface is only one part of the development.

The development also addresses a concrete analytic obligation in the chosen representation. An infinite-sum expression is a total Lean term even before summability is proved. Using it as the canonical analytic zeta function requires the appropriate convergence and differentiation results. The classical convergence statement is recorded in DLMF §23.2(ii); it is not introduced as an extra hypothesis of the main theorem.

Formalization scope and conventions

All custom declarations use the namespace WeierstrassEllipticZeta. The lattice intersection is an equality of $\mathbb Z$-submodules of $\mathbb C$. Rational linear independence and real linear independence have different roles: the first constrains the three inputs to the theorem, while the second is built into the period pair. Neither is replaced by numerical noncollinearity checks or approximate arithmetic.

The ten values form a Fin 10 family. The selected pair uses Mathlib's AlgebraicIndependent over $\mathbb Q$, so repeated numerical values cannot supply an independent pair merely by occupying different indices. The existing assumptions imply that both evaluation points are outside the lattice; no extra exclusion hypothesis is needed for the goal. Supporting addition identities state their pole exclusions explicitly because Lean's totalized division also assigns values at zero denominators.

The linked intermediate targets identify the variants sufficient for the completed main proof: Lemma 8 uses the stated formal-grid formulation; Proposition A.1 concerns the mission’s rank-one grid; and Lemma 10 uses linear coordinate-degree bounds rather than the source’s sharper O(N/log N) bounds. These distinctions are explicit in the milestone statements. They do not add assumptions to the main theorem. Further contributions can simplify the checked proofs, improve these intermediate bounds, or extend the general results beyond the existing mission target.

Extensions beyond the paper

Theorem 1 with only individual pole exclusions is an Open follow-up target. It retains the same nonzero period, rational linear independence, and ten-entry algebraic-independence conclusion, while replacing the lattice-intersection hypothesis with $u_1,u_2\notin\Omega$.

This extension is an additional deduction to formalize, not a numbered result of the paper, and no mathematical novelty is claimed. Its planned proof combines the completed Theorem 1 with a separate Chudnovsky period theorem and an arithmetic lemma recovering the quasi-period of an integer combination. These additional dependencies remain to be formalized. The mission's completed main goal and nine paper-related milestones continue to record the original scope.

Selected references

• Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society, published online 17 June 2026, pp. 1–33. DOI. Target: Theorem 1; supporting identities: §4, equations (5) and (6).
• NIST Digital Library of Mathematical Functions, Chapter 23, §23.2: Definitions and Periodic Properties, accessed 4 September 2026. Zeta normalization: equation 23.2.5; quasi-period convention: equation 23.2.11.
• Mathlib contributors, Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, pinned revision 0df444a360eaa60ab8c11dca51a86af692955474 (Lean 4.33.1).