Theorem 1: Algebraically independent Weierstrass values

Proved

WeierstrassEllipticZeta.senthil_kumar_theorem_one

by tomasz · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-independenceelliptic-functionsnumber-theory

Let $\Omega$ be the lattice of an arbitrary period pair, with associated Weierstrass functions $\wp,\zeta$ and invariants $g_2,g_3$ . Let $\omega\ne0$ be an element of $\Omega$ , and let $u_1,u_2\in\mathbb C$ satisfy both

u_1,u_2,\omega\text{ are linearly independent over }\mathbb Q,

and

(\mathbb Zu_1+\mathbb Zu_2)\cap\Omega=\{0\}.

Then at least two entries of

\bigl(g_2,g_3,\omega,\eta(\omega),u_1,u_2,\wp(u_1),\zeta(u_1),\wp(u_2),\zeta(u_2)\bigr)

are algebraically independent over $\mathbb Q$ , where $\eta(\omega)=\zeta(\omega_1/2+\omega)-\zeta(\omega_1/2)$ and $\zeta$ is the fixed canonical lattice series. Formally, there exist distinct indices $i,j\in\{0,\ldots,9\}$ for which no nonzero rational polynomial in two variables vanishes at the selected pair. The hypotheses already exclude lattice poles at $u_1,u_2$ . No algebraicity hypothesis is added for the invariants, and no particular pair is prescribed. This formalizes the published Theorem 1. Its checked proof has no Open theorem dependencies.

Preamble

import Definitions.Def_WeierstrassEllipticZeta_Defs

Formal statement

namespace WeierstrassEllipticZeta

/-- Senthil Kumar (2026), Theorem 1. This is an open proof target. -/
theorem senthil_kumar_theorem_one (L : PeriodPair) (ω u₁ u₂ : ℂ)
    (hω_ne : ω ≠ 0)
    (hω_period : ω ∈ L.lattice)
    (h_linearIndependent : LinearIndependent ℚ ![u₁, u₂, ω])
    (h_intersection : Submodule.span ℤ {u₁, u₂} ⊓ L.lattice = ⊥) :
    HasAlgebraicallyIndependentPair (theoremOneValues L ω u₁ u₂) := by sorry

end WeierstrassEllipticZeta

Source

Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society (online 17 June 2026), §1, Theorem 1, https://doi.org/10.1017/S001309152610145X.

Read-back

What the Lean code literally says, in plain math · GPT-6 (Codex)

For every ordered pair $L=(\omega_1,\omega_2)$ of complex numbers linearly independent over $\mathbb R$ , put $\Lambda=\{m\omega_1+n\omega_2:m,n\in\mathbb Z\}$ . For every $\omega,u_1,u_2\in\mathbb C$ , assume that $\omega\ne0$ , that $\omega\in\Lambda$ , that $u_1,u_2,\omega$ are linearly independent over $\mathbb Q$ (that is, for all $a,b,c\in\mathbb Q$ , $au_1+bu_2+c\omega=0$ implies $a=b=c=0$ ), and that $(\mathbb Zu_1+\mathbb Zu_2)\cap\Lambda=\{0\}$ , where $\mathbb Zu_1+\mathbb Zu_2=\{mu_1+nu_2:m,n\in\mathbb Z\}$ . Define $g_2=60\sum_{\lambda\in\Lambda}'1/\lambda^4$ , $g_3=140\sum_{\lambda\in\Lambda}'1/\lambda^6$ , and, for every $z\in\mathbb C$ , define $P_L(z)=\sum_{\lambda\in\Lambda}'\bigl(1/(z-\lambda)^2-1/\lambda^2\bigr)$ and $Z_L(z)=1/z+\sum_{\lambda\in\Lambda}'s_z(\lambda)$ , with $s_z(0)=0$ and $s_z(\lambda)=1/(z-\lambda)+1/\lambda+z/\lambda^2$ for $\lambda\ne0$ . Each primed sum means the limit of sums over finite subsets of its index set, and is assigned the value $0$ if that limit does not exist; every division is interpreted in $\mathbb C$ with $a/0=0$ for every $a\in\mathbb C$ , so these formulas define values for every $z$ , including lattice points. The hypotheses force $u_1,u_2\ne0$ and $u_1,u_2\notin\Lambda$ ; they also ensure that $\omega_1/2$ and $\omega_1/2+\omega$ lie outside $\Lambda$ . Form the ordered ten-tuple $(v_0,\ldots,v_9)=\bigl(g_2,g_3,\omega,Z_L(\omega_1/2+\omega)-Z_L(\omega_1/2),u_1,u_2,P_L(u_1),Z_L(u_1),P_L(u_2),Z_L(u_2)\bigr)$ . Then there exist distinct indices $i,j\in\{0,1,\ldots,9\}$ such that $v_i,v_j$ are algebraically independent over $\mathbb Q$ : for every polynomial $F\in\mathbb Q[X,Y]$ , $F(v_i,v_j)=0$ implies that $F$ is the zero polynomial.

Human review

Endorsed by Shuze Chen · Sep 29, 2026
Confirmed by the moderator at approval.
Endorsed by tomasz · Sep 29, 2026
Confirmed by the mission captain (proposal self-audit).

View graph