Number Theory

Motivation

A standard way to prove that a real number $\alpha$ is irrational is to produce integer linear forms $b+a\alpha$ that are nonzero but arbitrarily small: if $\alpha=p/q$ were rational, then $bq+ap$ would be a nonzero integer of absolute value below $1$ once the form is smaller than $1/q$. This is the shape of every hypergeometric construction of linear forms in odd zeta values — Rivoal's proof that infinitely many $\zeta(2n+1)$ are irrational and Zudilin's proof that at least one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational both produce such forms and read off irrationality (of at least one member of a finite set) from a determinant condition.

The same reduction is useful in the other direction: it isolates exactly what a construction has to supply — small forms — from the arithmetic that consumes them. This mission formalizes that abstract layer: the criteria that turn small integer forms into irrationality, together with the positivity and quadrature lemmas used to certify that a form is nonzero.

The material is distilled from a research note on $\zeta(9)$ (Xu, 2026). That note does not prove the irrationality of $\zeta(9)$, and nothing in this mission depends on whether it can be: every statement below is a statement about real numbers, integer linear forms, real polynomials, and finite sums, with $\zeta(9)$ and every other specific constant removed.

Setting

All objects live over $\mathbb{R}$.

• An integer linear form in $x$ is a number $b+a\,x$ with $a,b\in\mathbb{Z}$; the pair $(b,a)$ is its coefficient vector. Two forms are independent when their coefficient vectors have nonzero cross determinant, $b_1a_2\neq b_2a_1$.
• Irrational x is Mathlib's predicate: $x\notin\mathbb{Q}$ as a real number.
• The moment-matching hypothesis for a linear functional $L$ on real polynomials, a five-point node vector $y$ and a weight vector $w$, is $L(X^m)=\sum_{j}w_j\,y_j^{\,m}$ for every $m\le 4$. A functional satisfying it is exact on a polynomial $p$ when $L\,p=\sum_j w_j\,p(y_j)$.
• A positive weight vector has $w_j>0$ for all $j$; a node vector is injective when $y$ is injective on Fin 5.
• Polynomial.taylor u₀ p is the Taylor expansion of $p$ about $u_0$; its coefficients are nonnegative when $($taylor u₀ p$).\mathrm{coeff}\ i\ge 0$ for every $i$.
• Matrix.mulVec M v is the usual matrix–vector product over Fin 5; $\sum'$ denotes tsum over a Summable family.

Formalization targets

Goal — the one-form criterion

$$ \bigl(\forall \varepsilon>0,\ \exists, b,a\in\mathbb{Z}:\ b+ax\neq 0\ \wedge\ |b+ax|<\varepsilon\bigr)\ \Longrightarrow\ \text{$x$ irrational.}

The goal is the weakest non-vacuous statement in the family: it assumes one form at a time and no rate. ### Stronger — the two-form criterion

\bigl(\forall \varepsilon>0,\ \exists, b_1a_1b_2a_2\in\mathbb{Z}:\ b_1a_2\neq b_2a_1\ \wedge\ |b_1+a_1x|<\varepsilon\ \wedge\ |b_2+a_2x|<\varepsilon\bigr)\ \Longrightarrow\ \text{$x$ irrational.} $$

Supporting targets

1. Moment-matching quadrature — matching the five moments $m\le 4$ implies exactness on every polynomial of degree at most $4$.
2. Weighted average is interior — with positive weights summing to $1$, a non-constant five-tuple has its weighted average strictly between its minimum and maximum.
3. Mediant is interior — the ratio $\sum w_ia_i\,/\,\sum w_ib_i$ with $w,b>0$ lies strictly between the extreme values of $a_j/b_j$.
4. Positive matrices — an entrywise positive $5\times5$ matrix sends every nonzero nonnegative vector to a strictly positive vector.
5. Taylor-sign kernel sum — nonnegative Taylor coefficients at a lower bound of a sequence, positive summable weights, and one positive sample force a strictly positive weighted sum.
6. Five-sample nonvanishing — under moment matching with positive weights and injective nodes, a nonzero polynomial of degree $\le 4$ whose five sampled values share a sign has $L\,p\neq 0$.

Targets 1–6 correspond to the mission's milestones; the goal and the two-form criterion close the mission.

Significance

The results. The two criteria are the exact statements that a linear-form construction has to feed, and they are what turns "small forms exist" into irrationality without any analytic input. The supporting lemmas are the standard certificates used to show a form is nonzero — which is the other half of the argument, and the half that finite checks can actually settle.

Formalizing them. All eight statements are elementary and already have informal proofs; each also has a locally compiled Lean proof (lake env lean, exit 0, no sorry) against Lean 4.33.1 and Mathlib revision 0df444a3, held by the mission captain and published in the companion repository. What this mission adds is platform verification plus reusable infrastructure: the moment-matching quadrature lemma, the weighted-average and mediant inequalities, and the positivity lemmas are stated in a form that transfers to any setting where five-point data is certified by moments. Alternative proofs, generalizations to $n$-point quadrature, and sharper variants are welcome contributions.

Difficulty

The integrality step, not the estimate. In the one-form criterion the obvious move — take $\varepsilon=1/|q|$ — leaves the real inequality $|b+ax|<1/|q|$, which says nothing until the form is rewritten as $(bq+ap)/q$ with $bq+ap\in\mathbb{Z}$; only then does $|\,\cdot\,|<1$ force vanishing and contradict nonzeroness. Writing that rewrite in Lean means carrying the cast from $\mathbb{Z}$ through field_simp and back through exact_mod_cast, which is where naive attempts break.

Moment matching needs a degree bound, not interpolation. The quadrature lemma is not "five values determine a degree-$4$ polynomial": the hypothesis is about the functional $L$ on the five monomials, and the proof must expand an arbitrary $p$ in the monomial basis (as_sum_range_C_mul_X_pow' with natDegree < 5) and commute two finite sums.

Sign conditions are load-bearing. In target 6, the shared-sign hypothesis is what turns a vanishing weighted sum into vanishing samples; the root-counting step then needs injective nodes and positive weights. Dropping either silently makes the statement false, and both are easy to forget.

Formalization scope

Everything is over $\mathbb{R}$; no complex numbers appear. The quadrature statements are fixed at five nodes (Fin 5) and degree $\le 4$, as in the source note; the functional $L$ is a Polynomial ℝ →ₗ[ℝ] ℝ, not a measure. natDegree (not degree) is the degree notion. The infinite sum in target 5 is tsum with an explicit Summable hypothesis. Matrices are Matrix (Fin 5) (Fin 5) ℝ with mulVec; irrationality is Mathlib's Irrational.

Ruled out: a quadrature statement in which the weights are unconstrained by positivity but the conclusion is strengthened to a lower bound — target 1 assumes only moment matching, and any strengthening must add hypotheses rather than reinterpret the existing ones. A "criterion" whose hypothesis is vacuous for every real $x$ is likewise out of scope: both criteria are satisfiable hypotheses, not vacuous ones.

Infrastructure needed: the polynomial expansion and evaluation lemmas (as_sum_range, eval_eq_sum_range'), Finset sum rearrangement, Matrix.mulVec, Summable.tsum_lt_tsum_of_nonneg, and irrational_iff_ne_rational. The quadrature lemma, the mediant inequality, and the positivity lemmas are reusable beyond this mission.

Selected references

• Y. Xu, Research Notes on ζ(9): Constructions, Computations, and Open Problems, v0.1, Zenodo, 2026. https://doi.org/10.5281/zenodo.22951155
• W. Zudilin, Arithmetic of linear forms involving odd zeta values, J. Théor. Nombres Bordeaux 16:1 (2004), 251–291. https://arxiv.org/abs/math/0206176
• T. Rivoal, La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs, C. R. Acad. Sci. Paris Sér. I Math. 331 (2000), 267–270. https://arxiv.org/abs/math/0008051

Motivation

An integer winding label is discrete, but its exponential readout lies on a continuous circle. This mission makes that relationship exact. For a nonzero real algebraic angle $\alpha$, the map

$$n\longmapsto e^{i n\alpha}$$

is simultaneously a group character, a faithful encoding of $\mathbb Z$, and a countable dense orbit in the unit circle. Its complex values also form a linearly independent family over the algebraic complex numbers $\overline{\mathbb Q}$.

The result welds three previously completed interfaces. Circle covering theory produces canonical integer winding. Irrational-rotation theory classifies when an integer orbit is dense. Lindemann–Weierstrass gives the arithmetic rigidity that excludes resonance and algebraic linear relations. The point is not that topology alone proves transcendence, or that transcendence constructs winding: the theorem records the precise composition of the three layers.

The foundations are the completed private missions Winding Dynamics I, Lindemann–Weierstrass I, and Winding Arithmetic II. The transcendence layer is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.

Setting

Write $S^1\subset\mathbb C$ for the complex unit circle. For a real angle $\alpha$ and integer $n$, define

$$\operatorname{phase}_\alpha(n)=e^{i n\alpha}\in S^1.$$

This is an additive-to-multiplicative character: phase at $0$ is $1$, and phase at $m+n$ is the product of the phases at $m$ and $n$.

A based Circle loop $\gamma$ has a canonical integer $\operatorname{wind}(\gamma)$, obtained from the endpoint of its zero-based lift through the exponential cover. Its real phase readout is $\operatorname{phase}_\alpha(\operatorname{wind}(\gamma))$.

The orbit is dense when every nonempty open subset of $S^1$ contains some $\operatorname{phase}_\alpha(n)$. It is faithful when distinct integers have distinct phases. These properties are compatible: a countable subset may be dense without being all of the circle.

Formalization targets

Irrational rotation criterion

For every real $\alpha$,

$$\operatorname{DenseRange}(n\mapsto e^{i n\alpha}) \quad\Longleftrightarrow\quad \frac{\alpha}{2\pi}\notin\mathbb Q.$$

The proof identifies the phase orbit with integer multiples in $\mathbb R/(2\pi\mathbb Z)$ and transports Mathlib's irrational-rotation theorem through the standard homeomorphism with the complex unit circle.

Algebraic angles are nonresonant

If $\alpha\in\mathbb R$ is nonzero and algebraic over $\mathbb Q$, then $\alpha/(2\pi)$ is irrational. Otherwise $\pi$ would be algebraic, contradicting the proved transcendence of $\pi$. Consequently the real phase character has dense range.

Faithfulness and arithmetic rigidity

For the same nonzero algebraic $\alpha$, the character is injective and

$$\bigl(e^{i n\alpha}\bigr)_{n\in\mathbb Z}$$

is linearly independent over $\overline{\mathbb Q}$. The first conclusion says no two winding integers alias. The second says no nontrivial finite algebraic-coefficient linear relation exists among the phase values.

Actual Circle-loop consumer

For based Circle loops $\gamma$ and $\delta$,

$$e^{i\alpha\operatorname{wind}(\gamma)} =e^{i\alpha\operatorname{wind}(\delta)} \quad\Longleftrightarrow\quad \operatorname{wind}(\gamma)=\operatorname{wind}(\delta).$$

This consumes the canonical covering-space winding rather than an arbitrary externally supplied integer.

Resonance control

At the full-turn angle $\alpha=2\pi$, every integer phase is $1$, so the character is not injective. This negative control is outside the algebraic-angle regime because $\pi$ is transcendental. It records exactly why a nonresonance hypothesis is load-bearing.

Significance

The capstone exhibits one object with three complementary properties:

1. topological discreteness — values are indexed by integer winding;
2. dynamical density — the countable orbit visits every Circle neighborhood;
3. arithmetic rigidity — distinct values are faithful and linearly independent over $\overline{\mathbb Q}$.

This is a precise version of the intuitive claim that winding creates an integer coordinate whose phase representation explores a continuum. The continuum statement is density, not surjectivity: the image remains countable. The arithmetic statement is linear independence, not algebraic independence of the separate phase variables; the character law itself supplies multiplicative relations.

Together with Winding Arithmetic II, continuous homotopy preserves these readouts and a registered reset ledger factorizes their changes. This mission isolates the extra fact that the resulting character is both faithful and dense for every nonzero real algebraic angle.

Difficulty

No single layer implies the capstone by itself. The Circle exponential is periodic, so injectivity requires a genuine nonresonance argument. Density requires the exact normalization by $2\pi$ and transport through the AddCircle–Circle homeomorphism in both directions. Linear independence requires the completed Lindemann–Weierstrass theorem, not merely irrationality or transcendence of $\pi$.

The coercion bridge between the real Circle phase and the complex exponential character is also orientation-sensitive: the formal phase is exactly $\exp(i n\alpha)$. Reversing the sign would still define a dense faithful character, but it would not be the registered convention used by the prior winding arithmetic mission.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Circle density is stated only for real $\alpha$. The arithmetic conclusions require both IsAlgebraic ℚ α and $\alpha\ne0$.

The actual-loop theorem proves equality of phase values if and only if equality of canonical winding integers. It does not claim that the loops themselves are equal, and it does not add a new classification of homotopy classes. That classification remains the responsibility of the Circle covering-space layer.

The theorem proves a faithful representation of winding values, not the existence of winding in an arbitrary physical model. A Kuramoto, XY, or Lohe consumer must still provide a jointly continuous Circle field or a preserved non-simply-connected carrier and readout. No particle–wave or quantum-mechanical interpretation is asserted.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Lean mathematical library, Dense subgroups of the additive circle. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.html
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

Motivation

Winding number is a topological integer: continuous deformation preserves it, while crossing a branch cut or registering a reset can change it by an integer amount. Transcendence theory gives a different kind of rigidity. For a nonzero algebraic coupling $\alpha$, the phases $e^{i\alpha n}$ attached to distinct integers $n$ are linearly independent over the field $\overline{\mathbb Q}$ of algebraic complex numbers. This mission joins those statements at their exact formal interfaces.

The result is useful wherever a model first produces an integer winding label and then represents that label by a complex phase. Topology supplies the discrete coordinate, dynamics determines when it is conserved or reset, and Lindemann–Weierstrass supplies arithmetic distinguishability. None of those layers is asked to manufacture the others.

The foundation comes from three completed private missions: Winding Dynamics I: Homotopy Conservation and Reset Balance, Integer Winding Transcendence I: Exponential Phase Independence, and Lindemann–Weierstrass I: Exponential Independence. The transcendence proof is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.

Setting

Let $S^1$ be the complex unit circle. A based Circle loop is a continuous path in $S^1$ that starts and ends at $1$. Its canonical real lift through the exponential covering starts at $0$; the lift endpoint determines an integer $\operatorname{wind}(\gamma)$.

For $\beta\in\mathbb C$ and $n\in\mathbb Z$, define the integer exponential character

$$\chi_\beta(n)=\exp(n\beta).$$

The arithmetic consumer uses $\beta=i\alpha$, where $\alpha$ is nonzero and algebraic over $\mathbb Q$. Thus a loop $\gamma$ carries the phase $\chi_{i\alpha}(\operatorname{wind}(\gamma))$.

A closed Circle field is a jointly continuous map on the time/spatial square $I\times I$ whose two spatial endpoints agree at every time. Each spatial slice is normalized by its moving basepoint, producing a based loop. A carrier/readout segment generalizes this: an ambient trajectory remains in a registered carrier subspace and is observed through a continuous map from that carrier to $S^1$.

The discontinuous branch is represented separately by a finite reset ledger. It stores successive integer edge-turn cochains. Pairing those cochains with a certified closed edge cycle produces integer winding values and reset periods.

Formalization targets

Circle winding separates algebraic phases

For a family of loops $(\gamma_j)_{j\in J}$ with pairwise-distinct windings,

$$\left(e^{i\alpha\operatorname{wind}(\gamma_j)}\right)_{j\in J} \text{ is linearly independent over }\overline{\mathbb Q}.$$

Continuous evolution preserves the phase basis

If the initial windings of a family of closed Circle fields are distinct, then the initial phase family is linearly independent, every phase is unchanged between endpoint times, and the final phase family remains linearly independent. The same conclusion is exposed through the carrier/readout interface.

Reset balance becomes phase factorization

If a reset ledger has endpoint winding change $W_{\mathrm f}-W_{\mathrm i}$ and registered reset periods $\Delta W_j$, then

$$\chi_\beta(W_{\mathrm f}-W_{\mathrm i}) =\prod_j\chi_\beta(\Delta W_j).$$

This is the multiplicative image of the exact additive ledger balance.

The phase readout is faithful

For nonzero algebraic $\alpha$, the character $\chi_{i\alpha}$ is injective on $\mathbb Z$. Consequently, two actual Circle loops have equal algebraic phase readouts exactly when they have equal canonical winding. On the reset branch,

$$\prod_j\chi_{i\alpha}(\Delta W_j)=1 \quad\Longleftrightarrow\quad W_{\mathrm f}=W_{\mathrm i}.$$

Thus the multiplicative reset record detects zero net winding change without losing integer information.

Significance

The main theorem upgrades conservation of a single integer to conservation of an arithmetic basis. Distinct homotopy classes do not merely retain distinct integer labels: after the algebraic exponential readout, the corresponding phases admit no nontrivial finite linear relation with algebraic coefficients. This lets downstream consumers treat a family of winding sectors as a linearly independent family over $\overline{\mathbb Q}$.

The reset theorem provides the matching event law. Continuous evolution preserves the basis, whereas a registered reset multiplies phases according to the reset periods. The two branches share one character but retain different hypotheses, so a discontinuous ledger event is not misrepresented as a continuous homotopy.

The algebraic readout is also faithful: despite taking values on the complex exponential curve, it neither aliases two winding sectors nor hides a nonzero net reset behind total phase $1$ under the stated algebraic hypothesis.

This does not establish a particle–wave duality or a quantum-mechanical interpretation. It establishes a precise mathematical analogy: an integer topological label has a complex character representation whose distinct values enjoy a strong arithmetic independence theorem under an algebraic nonresonance condition.

Difficulty

The individual deductions are short only because three difficult interfaces have already been proved. Replacing an arbitrary integer map by actual Circle winding requires using the canonical covering lift rather than postulating labels. Preserving the phase basis requires transporting injectivity and linear independence through a jointly continuous moving-basepoint normalization. The reset branch requires respecting the sign convention and mapping a finite sum to a finite product, including the empty ledger.

Several tempting statements would be false. Duplicate winding labels cannot give a linearly independent family. The exponent $\alpha=0$ collapses every phase to $1$. Continuity of finitely many vertex phases does not by itself define a continuous spatial Circle field, and crossing the principal cut can change a discrete principal-turn winding. A global readout from a simply connected carrier such as all of $SU(2)$ cannot support nonzero loop winding without a separately registered non-simply-connected subcarrier or channel.

For a general complex coupling, exponential resonance can destroy injectivity. The nonzero algebraic hypothesis excludes that resonance here through the proved Lindemann--Weierstrass theorem; it is not merely a convenient side condition.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The Circle winding is the floor of the canonical zero-based lift endpoint divided by $2\pi$. Closed fields live on $I\times I$ and are normalized at spatial coordinate zero. The coupling $\alpha$ is an arbitrary complex algebraic number, not necessarily real, and must be nonzero.

The main carrier/readout theorem is conditional on an explicit continuous carrier-valued trajectory, closed spatial slices, and continuous Circle readout. It does not prove existence of a Kuramoto, XY, or Lohe solution, nor preservation of a particular carrier by such an ODE. Those are model-specific successors.

The reset factorization consumes the registered coherent ledger and certified closed cycle. It is an exact algebraic event law, not an energy estimate and not a claim that every physical trajectory realizes such a ledger. Its vertex and edge types retain the universe-zero scope of the existing reset interface.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

What this mission proves, and what it does not. The goal theorem is the explicit upper bound $F(N)<3\sqrt N+1$ of Erdős, Lev, Rauzy, Sándor and Sárközy (1999) — a published result, now formally verified here. Erdős problem #131 itself is NOT solved by this mission. Erdős asked for the order of growth of $F(N)$, which is known only to lie between $N^{1/5}$ and $N^{1/4+o(1)}$ and remains open. A goal theorem reading Proved therefore means the 1999 bound is formalized, nothing more.

Motivation

Call a finite set of positive integers non-dividing if no element of it divides the sum of any nonempty collection of the other elements. The condition is easy to state and immediately restrictive: taking the collection to be a single element already forbids $a \mid b$, so a non-dividing set is primitive, and taking larger collections forbids a great deal more. Paul Erdős asked, with Lev, Rauzy, Sándor and Sárközy, how large such a set can be inside $\{1,\ldots,N\}$. Writing $F(N)$ for that maximum, the question is to determine the order of growth of $F(N)$. It remains unanswered, and the gap between what is known from above and from below is a full factor of $N^{1/20}$.

The problem sits at the meeting point of divisibility and additive combinatorics. Its upper bounds come from the theory of non-averaging sets, since every non-dividing set is non-averaging; its lower bounds come from explicit constructions. The two sides have been improved independently for twenty-five years without meeting.

Setting

Work inside $\mathbb{N}$. For a finite $A \subseteq \mathbb{N}$ and $a \in A$, write $A \setminus \{a\}$ for $A$ with $a$ removed. Say that $A$ is non-dividing when

$$\forall a \in A,\ \forall S \subseteq A \setminus \{a\} \text{ with } S \neq \emptyset:\qquad a \nmid \sum_{x \in S} x .$$

Two conventions are forced. First, $S$ ranges over all nonempty subsets, singletons included, so primitivity is part of the property rather than an extra assumption. Second, $S$ must be nonempty: the empty sum is $0$ and every $a$ divides $0$, so admitting $S = \emptyset$ would leave no non-dividing sets at all.

Define the extremal function

$$F(N) \ =\ \max\{\,|A| \ :\ A \subseteq \{1,\ldots,N\},\ A \text{ non-dividing}\,\}.$$

A set is non-averaging if no element equals the average of some nonempty collection of the others. Every non-dividing set is non-averaging, which is the link through which the strongest upper bounds arrive.

Target

The goal is the explicit upper bound of Erdős, Lev, Rauzy, Sándor and Sárközy:

$$F(N) \ <\ 3N^{1/2} + 1 .$$

The question Erdős actually posed is stronger and remains open:

$$\textbf{Determine the order of growth of } F(N).$$

Significance

The bound above is the sharpest explicit constant in the literature, and it is the natural formalization target: it is a clean closed-form inequality valid for every $N$, with a self-contained combinatorial proof, and nothing about it is asymptotic.

Beyond it lies the open question. What is known:

• $F(N) > \exp\!\big((\sqrt{2/\log 2} + o(1))\sqrt{\log N}\big)$, due to Straus, which refuted Erdős's own initial guess that $F(N) < (\log N)^{O(1)}$.
• $F(N) \gg N^{1/5}$, from a construction Erdős credits to Csaba.
• $F(N) < 3N^{1/2} + 1$, the target above.
• $F(N) \le N^{1/4 + o(1)}$, from Pham and Zakharov's theorem on non-averaging sets. This settles Erdős's specific sub-question — whether $F(N) > N^{1/2 - o(1)}$ — in the negative.

So the truth lies between $N^{1/5}$ and $N^{1/4+o(1)}$, and which end is right is unknown.

Difficulty

The obvious argument gives almost nothing. Pigeonhole on partial sums shows $|A| \le \min A$: order the other elements arbitrarily, form the running sums, and if there are more of them than residues modulo $\min A$ then two agree, making a contiguous block sum divisible by $\min A$. That is genuinely all the elementary argument yields, and it is compatible with $|A|$ as large as $N$.

The difficulty is that the constraint is a statement about exponentially many subset sums, while the conclusion is about a single cardinality. Every strong bound known proceeds by discarding almost all of that information and keeping a structured fragment — contiguous blocks, or the averaging condition — and the loss at that step is exactly what separates $N^{1/5}$ from $N^{1/4}$. Improving either side appears to require using the divisibility conditions for several elements $a$ simultaneously, which no current argument does.

Formalization scope

Sets are Finset ℕ. The forbidden subsets are drawn from A.erase a, so the tested element never appears in the sum it is tested against, and they are quantified as members of (A.erase a).powerset rather than by the subset relation, which makes the property decidable — this is what allows an explicit finite witness to be checked by the kernel rather than asserted. $F(N)$ is a Finset.sup of cardinalities over the filtered powerset of Finset.Icc 1 N, so it is a total function with no junk-value caveats and lower bounds on it follow from exhibiting a single set.

The target inequality is stated over ℝ with Real.sqrt, matching the source's $3N^{1/2}+1$ rather than any integer rounding of it.

Timeline

• 1980s–1998. Erdős poses the problem repeatedly, initially conjecturing $F(N) < (\log N)^{O(1)}$.
• Straus. Disproves that guess, with $F(N) > \exp(c\sqrt{\log N})$.
• Csaba. A construction giving $F(N) \gg N^{1/5}$, credited by Erdős in 1997.
• 1999. Erdős, Lev, Rauzy, Sándor and Sárközy name the property non-dividing and prove $F(N) < 3N^{1/2} + 1$.
• 2024. Pham and Zakharov bound non-averaging sets, yielding $F(N) \le N^{1/4+o(1)}$ and answering Erdős's sub-question negatively.
• Open. The order of growth of $F(N)$, anywhere between $N^{1/5}$ and $N^{1/4+o(1)}$.

Selected references

• P. Erdős, V. Lev, G. Rauzy, C. Sándor, A. Sárközy, Greedy algorithm, arithmetic progressions, subset sums and divisibility, Discrete Mathematics 200 (1999), 119–135.
• H. T. Pham, D. Zakharov, Sharp bound for the Erdős–Straus non-averaging set problem, arXiv:2410.14624; Geom. Funct. Anal. (2025). Theorem 1: a non-averaging $A\subseteq[n]$ has $|A|\le n^{1/4+o(1)}$.
• R. K. Guy, Unsolved Problems in Number Theory, 3rd ed., Springer (2004), problem C16.
• Erdős problem #131, https://www.erdosproblems.com/131
• OEIS A068063, Maximum cardinality of a nondividing subset of $\{1,\ldots,n\}$.

Motivation

A set of integers is sum-free when no two of its members add up to a third. Schur's theorem (1916) says that for every $k$ there is a largest interval $[1,N]$ that can be split into $k$ sum-free classes, and the resulting Schur numbers $S(k)$ are notoriously hard to compute: $S(5) = 160$ was settled only in 2018, by a SAT computation with a machine-checked proof certificate.

Replacing "adds up to" by "adds up to, modulo $m$" gives a family that behaves very differently. Modular Schur numbers were introduced by Chappelon, Revuelta Marchena and Sanz Domínguez, who settled the moduli $m \in \{1,2,3\}$ and proved the universal bound $S_m(k,\ell) \le m-1$ (Electron. J. Combin. 20(2) (2013) #P61). D'orville, Sim, Wong and Ho then closed $m \in \{4,5,6,7\}$ by residue case analysis and posed the general modulus as an open problem (Integers 25 (2025) #A62, their Problem 1). Each additional modulus had cost a separate case analysis, and the case analysis grew with $m$.

The timeline matters for reading what follows. The 2013 paper supplies the universal cap. The 2025 paper supplies a singleton criterion (its Theorem 4) and a divisibility obstruction (its Corollary 3), and applies the latter only in the coprime case $\gcd(m,\ell-1)=1$ (its Corollary 5). What remained was to optimise that obstruction over every residue rather than only in the coprime case, which is what collapses the whole family to one formula.

Setting

Fix integers $m \ge 2$, $\ell \ge 2$ and $k \ge 1$. A set $S$ of integers is $\ell$-sum-free modulo $m$ when there are no $x_1, \dots, x_\ell \in S$ and $y \in S$, repetitions among the $x_i$ allowed, with

$$x_1 + \cdots + x_\ell \equiv y \pmod m .$$

The repetition clause is not a technicality: a single element can make its whole class unsafe. The modular Schur number $S_m(k,\ell)$ is the greatest $N \ge 0$ such that the interval $[1,N]$ can be partitioned into at most $k$ classes, each $\ell$-sum-free modulo $m$. A partition into such classes is called valid.

Two derived quantities carry the whole story. Write

$$d = \gcd(m, \ell - 1), \qquad n = \frac{m}{d} .$$

Then $dn = m$ exactly, and $d \mid (\ell - 1)$ by construction. All Lean statements in this mission use these same names.

Formalization targets

Goal: the closed form in the many-colours regime

$$S_m(k,\ell) = \frac{m}{\gcd(m,\ell-1)} - 1 = n - 1 \qquad \text{for all } m \ge 2,\ \ell \ge 2,\ k \ge n-1 .$$

Closed form here means something precise: the value is produced from $m$ and $\ell$ by one gcd, one division and one subtraction, with no search over colourings, no recursion, and no case split on $\ell \bmod m$. The statement fixes no constants and no modulus, so it is not invalidated by any later refinement of the threshold in $k$.

The single-colour value

$$S_m(1,\ell) = \min\!\left(\ell - 1, \left\lfloor \frac{m}{\ell} \right\rfloor\right) \qquad (2 \le \ell \le m),$$

together with the complementary regime $m < \ell$, where the value is $0$ if $\ell \equiv 1 \pmod m$ and $1$ otherwise. The two together give a value for every admissible pair $(m,\ell)$ at $k=1$, and the tree carries that combined formula at the residue level and at the integer level.

Significance

What the results give. One expression replaces an open-ended sequence of per-modulus case analyses. The moduli $m \in \{1,2,3\}$ of the 2013 paper and $m \in \{4,5,6,7\}$ of the 2025 paper are specialisations, and every remaining modulus is covered at once in the stated range of $k$.

The mechanism is a single self-defeating value. Take $\ell$ copies of $n$: they sum back to $n$ modulo $m$, so the lone class $\{n\}$ already breaks the rule, while every smaller value is safe. That one observation supplies a matching upper and lower bound.

• The upper bound is uniform in $k$. Adding colours never raises the value past $n-1$, which is what makes the formula stable.
• The lower bound costs $n-1$ colours, one per safe residue. Identifying the least sufficient number of colours is where the subject is still open.

Status of the tree, stated precisely. Everything listed under Formalization targets is both proved and machine-checked.

• 21 theorems and 3 definition bundles, each with a complete Lean proof verified by this platform.
• Axiom-clean: each closure is contained in {propext, Classical.choice, Quot.sound}.
• This mission therefore publishes a finished development rather than an open call on its stated goal.
• What is genuinely open is listed under Difficulty below, and is not part of the verified tree.

Relation to the accompanying paper. The paper states the single-colour value only under $2 \le \ell \le m$. Three results in the tree go beyond it: the complementary regime $m < \ell$, and the combined formula covering every $m \ge 2$ and $\ell \ge 2$, stated once at the residue level and again at the integer level. Two further results, the coset-cardinality bounds, are supporting work of the Lean development and are not numbered results of the paper. Each theorem's source field records which of these it is.

Difficulty

The threshold in $k$ is not $n-1$

The obvious attack on the general modulus is to guess that only singletons can be safe classes. The threshold in $k$ would then be exactly $n-1$, and the problem would close for all $k$ at once. That guess is false.

Take $m = 12$ and $\ell \equiv 11 \pmod{12}$, so $d = 2$ and $n = 6$. The two-element set $\{1,5\}$ is $\ell$-sum-free modulo $12$, and three colours then suffice where the singleton count would demand five.

So the least $k$ at which the closed form takes hold, written $k_0(m,\ell)$, is not $n-1$ in general. What is known about it:

• Prime moduli. $k_0(p,\ell) = p-1$ for every $\ell \ge p-1$ with $\ell \not\equiv 1 \pmod p$.
• Composite moduli. Bracketed above and below, but not determined.

A correction to the published prime-power formula

Theorem 8 of D'orville, Sim, Wong and Ho gives a three-branch formula at prime-power moduli. Its middle branch is false. The correction is stated here in full because it bears directly on the threshold.

• The counterexample. At $p = 2$, $i = 3$, $k = 3$ and $\ell = 8$ that branch gives $S_8(3,8) = 5$, while the correct value is $S_8(3,8) = 7$.
• Where the proof fails. In the supporting Lemma 2(2) of that paper. The pair $a = 2$, $b = 6$ satisfies every hypothesis of that lemma at $p = 2$, $i = 3$, $\ell = 8$, yet $\{2,6\}$ is $8$-sum-free modulo $8$.
• The replacement result.

$$S_{p^i}(k,\ell) = p^i - 1 \qquad \text{for } p \text{ prime},\ i \ge 1,\ \ell \ge 2,\ p \nmid (\ell - 1), \text{ and every } k \ge i(p-1) .$$

It is proved from a valuation-layer colouring that consumes $i(p-1)$ classes, together with the universal cap. The hypothesis $p \nmid (\ell-1)$ forces $d = 1$ and $n = p^i$, so the replacement reaches the goal theorem's value at $k \ge i(p-1)$ in place of $k \ge p^i - 1$, and it contradicts the printed middle branch for infinitely many triples $(p, i, \ell)$.

Status of that correction, stated precisely.

• It is a prose proof in a draft note, listed under Selected references below and readable in full there.
• It is not formalized, and it is not part of this mission's verified tree.
• Nothing in the verified tree depends on it.
• It is recorded here because a reader who compares this mission against the 2025 paper will otherwise meet the contradiction with no explanation. Formalizing it is the subject of a separate mission.

The intermediate regime

For $1 < k < n-1$ the classes must be simultaneously large and $\ell$-sum-free, and no formula is known. The value is empirically eventually periodic in $\ell \bmod m$ for fixed $k$, verified through $m \le 13$.

None of these open directions is weakened by the goal theorem, which deliberately assumes enough colours to avoid the question.

Formalization scope

Two levels of statement

Two levels appear in the tree, and the distinction between them is the first thing to fix.

• At the integer level the objects are the integers $1, \dots, N$ themselves.
• At the residue level they are their classes modulo $m$, which in Lean is the type ZMod m: Mathlib's type of residues modulo $m$, a commutative ring with exactly $m$ elements for $m \ge 1$, carrying the reduction map from $\mathbb{Z}$ and the arithmetic that map preserves.

Working in ZMod m turns "adds up to, modulo $m$" into a plain equation instead of a divisibility side condition, and it makes every colour class a subset of a finite type.

Conventions

The development works residue-by-residue in ZMod m and commits to the following conventions, all of which are silent in the prose and load-bearing in Lean.

• $\ell$-tuples are functions Fin ℓ → ZMod m valued in the class. This builds in "repetitions allowed" rather than leaving it to a side condition.
• Classes are Finsets, so finiteness is structural.
• A valid partition is a structure with four fields: covering, pairwise disjointness, containment in the target set, and $\ell$-sum-freeness of each class.
• Empty classes are permitted. This is what makes "at most $k$" and "exactly $k$" interchangeable once any colouring exists.

The two numbers, and the cap in their definition

Both a residue-level and an integer-level number are defined, and a reduction theorem proves them equal for every $m \ge 2$. Bounds are proved on the residue side and quoted on the integer side.

Both are defined with Nat.findGreatest against the bound $m-1$. That cap is neither an approximation nor a trivialising choice: a separate theorem shows any $N$ admitting a valid partition satisfies $N \le S_m(k,\ell)$ with no hypothesis on $N$, because $N \ge m$ admits no valid partition at all. A reader checking for a vacuous formalization should also note that the goal is an equality, not a bound, so it cannot be satisfied by weakening a hypothesis.

Reusable beyond this mission

• the residue-reduction bridge;
• the singleton criterion;
• the two coset-cardinality bounds, which are pure counting statements about subsets of a cyclic group whose differences lie in a proper subgroup.

Contributions welcome on the open directions named under Difficulty, in particular any lowering of the threshold in $k$ toward $k_0$, and a closed form for $k_0$ at composite moduli.

Selected references

• J. Chappelon, M. P. Revuelta Marchena, M. I. Sanz Domínguez, Modular Schur numbers, Electron. J. Combin. 20(2) (2013) #P61. https://doi.org/10.37236/2374 (also arXiv:1306.5635)
• J. D'orville, K. A. Sim, K. B. Wong, C. K. Ho, Modular generalizations of Schur numbers, Integers 25 (2025) #A62. https://math.colgate.edu/~integers/z62/z62.pdf
• M. J. H. Heule, Schur number five, AAAI 2018. arXiv:1711.08076
• A. McKenna, A correction to a prime-power formula for modular Schur numbers, 2026. Draft note, not submitted for publication. Released in the repository below on 2026-09-20: PDF · Markdown source
• A. McKenna, Prime-power structure of the stable regime for modular Schur numbers, 2026. Lean development and paper: https://github.com/mysticflounder/modular-schur

Motivation

The exponential function turns addition into multiplication. When its inputs are algebraic numbers, that elementary identity meets a rigid arithmetic boundary: distinct algebraic exponents cannot produce an algebraic linear relation among their exponentials. This principle is the Lindemann–Weierstrass theorem, one of the central results of transcendence theory. Its familiar consequences include the transcendence of Euler's number $e$ and of $\pi$, and therefore the impossibility of squaring the circle with straightedge and compass.

The historical line runs from Hermite's 1873 proof that $e$ is transcendental, through Lindemann's 1882 proof that $\pi$ is transcendental, to Weierstrass's general formulation in 1885. Modern algebraic presentations organize the theorem around conjugates, Galois symmetry, algebraic integers, and an auxiliary-polynomial estimate. The Lean development formalized here follows Yuyang Zhao's mathlib contribution PR #28013, whose mathematical reference is Jacobson's Basic Algebra I, §4.12, Theorem 4.22.

Setting

A complex number is algebraic if it is a root of a nonzero polynomial with rational, equivalently integer, coefficients. A complex number is transcendental if it is not algebraic. Write $\overline{\mathbb Q}\subset\mathbb C$ for the field of algebraic complex numbers and $\exp(z)=e^z$ for the complex exponential.

For a family $(u_i)_{i\in I}$ in $\overline{\mathbb Q}$, injectivity means that distinct indices carry distinct exponents. A family $(x_i)$ is linearly independent over $\overline{\mathbb Q}$ when every finite relation $\sum_i a_i x_i=0$ with algebraic coefficients has all $a_i=0$. It is algebraically independent over $\overline{\mathbb Q}$ when no nonzero multivariate polynomial with algebraic coefficients vanishes on the family.

The strongest target uses natural-number linear independence of $(u_i)$: distinct finitely supported tuples of natural coefficients give distinct sums $\sum_i n_i u_i$. This is exactly the condition needed to distinguish the exponent attached to every monomial.

Formalization targets

Exponential linear independence

For every injective algebraic family $(u_i)$,

$$\{e^{u_i}:i\in I\}\text{ is linearly independent over }\overline{\mathbb Q}.$$

This includes the finite Lindemann–Weierstrass relation as its load-bearing finite core.

Hermite–Lindemann and classical constants

For every nonzero algebraic $a\in\mathbb C$,

$$e^a\text{ is transcendental}.$$

The same development records the transcendence of $e$, the transcendence of $\pi$, and the transcendence of every nonzero principal logarithm of an algebraic complex number.

Integer winding consumer

Let $\alpha\ne0$ be algebraic and let $w:I\to\mathbb Z$ be injective. The proved Hermite–Lindemann theorem discharges the formerly conditional winding interface and gives

$$\bigl(e^{i\alpha w(j)}\bigr)_{j\in I}\text{ linearly independent over }\overline{\mathbb Q}.$$

The integer labels are inputs to this arithmetic theorem. A separate topological or dynamical development is responsible for producing them as winding numbers.

Algebraic independence capstone

If $(u_i)$ is a natural-number-linearly-independent family in $\overline{\mathbb Q}$, then

$$\{e^{u_i}:i\in I\}\text{ is algebraically independent over }\overline{\mathbb Q}.$$

This is the mission's capstone because it turns the linear theorem into a reusable multivariate interface: polynomial monomials become exponentials of distinct natural combinations.

Significance

The theorem separates two kinds of structure that otherwise coexist in the exponential map. The character law $e^{x+y}=e^xe^y$ supplies exact multiplicative relations, but the theorem rules out unintended linear relations over algebraic coefficients. For integer winding consumers, one algebraic nonzero generator $a$ produces the two-sided phase family $(e^{na})_{n\in\mathbb Z}$; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over $\overline{\mathbb Q}$. Winding supplies the discrete labels, while transcendence supplies arithmetic distinguishability.

The formalization contributes more than the named corollaries. It exposes a finite exponential-relation theorem, the algebraic orbit-sum reduction used by it, and general infinite-family interfaces. These components can be reused in later work on exponential polynomials, logarithms of algebraic numbers, and arithmetic representations of topological charges.

This mission formalizes a known theorem; it is not presented as an open mathematical problem. The private theorem graph is already machine-checked against Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The mission records that proof as an independently inspectable dependency graph before any later upstream integration.

Difficulty

The analytic approximation alone is insufficient. It produces a small complex error, but smallness does not imply vanishing, and taking a field norm does not repair the gap because the other embeddings have no corresponding analytic bound. Likewise, a field automorphism of $\overline{\mathbb Q}$ cannot be moved through the complex exponential as an algebraic operation.

The formal statement therefore requires both an analytic and an arithmetic layer. The arithmetic layer must replace a hypothetical algebraic relation by a Galois-stable relation with integer data and a genuinely nonzero integer contribution. The analytic layer must then make the absolute value of that integer strictly less than one. Managing conjugacy classes, root multisets, denominator clearing, finite supports, and the asymptotic prime choice in one kernel-checked chain is the central formalization difficulty.

Formalization scope

The development is pinned to Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Algebraic complex numbers are represented by integralClosure ℚ ℂ; transcendence corollaries are stated with Transcendental ℤ, which is equivalent to the usual absence of a nonzero integer polynomial relation. The finite theorem uses Fintype; the general linear and algebraic independence theorems permit arbitrary universe-zero index types and reduce relations to finite support internally.

The auxiliary algebraic theorem is stated over an arbitrary algebraically closed field over $\mathbb Q$ and a multiplicative character on its additive group. The analytic consumer specializes this character to the complex exponential. Two small support modules provide quotient lifting for finitely supported functions and evaluation identities for symmetric multivariate polynomials.

The condition $a\ne0$ in Hermite–Lindemann is load-bearing: $e^0=1$ is algebraic. Injectivity of the exponent family is load-bearing for linear independence: duplicate exponents duplicate vectors. The capstone's natural-number linear independence is not algebraic independence of the exponents and must not be silently strengthened or weakened.

The source is an attributed, compatibility-preserving port of the May 2026 Lean 4.30 snapshot of mathlib PR #28013. Platform packaging uses the conservative ASCII rename linearIndependent_exp_finite for the upstream private helper and phi for one Greek binder. The elaborated theorem types were compared against the upstream source; these are naming changes only.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Mathlib contributors, AnalyticalPart: the analytic estimate for Lindemann–Weierstrass. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.html

Motivation

Integer winding is one of the simplest ways that continuous geometry produces discrete arithmetic. A loop in the circle has an integer winding number, while the complex exponential turns an additive parameter into a multiplicative phase. This mission asks what arithmetic information survives when those two constructions are combined. Its answer is a conditional but exact bridge: once Hermite--Lindemann supplies one transcendental phase, distinct integer winding labels produce a linearly independent family over the algebraic numbers.

The transcendence input is classical. Lindemann proved in 1882 that the exponential of a nonzero algebraic number is transcendental, and Weierstrass subsequently established the broader theorem now called Lindemann--Weierstrass. A modern statement appears as Theorem 1.1 of Javier Fresán's notes on the Hermite--Lindemann--Weierstrass theorem: exponentials of rationally linearly independent algebraic numbers are algebraically independent. The present mission deliberately does not formalize that analytic theorem. It isolates and formalizes the algebraic consumer that becomes available immediately after its one-variable consequence is supplied.

Setting

Let $K\subseteq E$ be a field extension and let $z\in E$. For every integer $n$, the Laurent power $z^n$ is defined when $z\ne0$. An element $z$ is transcendental over $K$ when no nonzero polynomial with coefficients in $K$ vanishes at $z$. The first target proves that transcendence rules out every finite $K$-linear relation among the two-sided family

$$\{z^n:n\in\mathbb Z\}.$$

For a complex parameter $\beta$, define the integer exponential character

$$\chi_\beta(n)=\exp(n\beta),\qquad n\in\mathbb Z.$$

It satisfies $\chi_\beta(n)=\exp(\beta)^n$ and the character law $\chi_\beta(m+n)=\chi_\beta(m)\chi_\beta(n)$. The mission registers the Hermite--Lindemann assertion as an explicit proposition: for every nonzero complex number $\beta$ algebraic over $\mathbb Q$, $\exp(\beta)$ is transcendental over $\mathbb Q$.

Write $\overline{\mathbb Q}$ for the subfield of complex numbers algebraic over $\mathbb Q$. If $\alpha\ne0$ is algebraic, then $i\alpha$ is nonzero and algebraic. Hermite--Lindemann therefore makes $z=\exp(i\alpha)$ transcendental, first over $\mathbb Q$ and then over $\overline{\mathbb Q}$. Integer phases are exactly the Laurent powers $z^n$.

Formalization targets

Laurent-power independence

For every field extension $E/K$ and every $z\in E$ transcendental over $K$,

$$\bigl(z^n\bigr)_{n\in\mathbb Z} \quad\text{is linearly independent over }K.$$

Integer exponential character

For every $\beta\in\mathbb C$ and $m,n\in\mathbb Z$,

$$\chi_\beta(n)=\exp(\beta)^n, \qquad \chi_\beta(m+n)=\chi_\beta(m)\chi_\beta(n), \qquad \chi_\beta(0)=1.$$

Conditional all-integer phase independence

Assuming Hermite--Lindemann, if $\alpha\in\mathbb C$ is nonzero and algebraic over $\mathbb Q$, then

$$\bigl(\exp(i\alpha n)\bigr)_{n\in\mathbb Z} \quad\text{is linearly independent over }\overline{\mathbb Q}.$$

Winding-labelled capstone

For any injective integer label $w:I\to\mathbb Z$ under the same hypotheses,

$$\bigl(\exp(i\alpha w(j))\bigr)_{j\in I} \quad\text{is linearly independent over }\overline{\mathbb Q}.$$

The label $w$ may be supplied downstream by a winding-number construction, a self-linking number, or another independently proved integer invariant. This packet consumes the integer; it does not manufacture winding from continuous data.

Significance

The result separates topology from arithmetic cleanly. A geometric or dynamical development is responsible for producing an integer label and proving when labels are distinct. The present mission then turns that discrete distinction into a strong arithmetic conclusion about the corresponding complex phases. Because the Laurent-power theorem is stated over an arbitrary field extension, it is reusable outside circle topology and transcendence theory.

The formalization also records the exact limits of the conclusion. The phase with label zero is $1$ and is not individually transcendental. Repeated winding labels force repeated vectors and therefore destroy linear independence. At zero coupling every phase collapses to $1$. Finally, the character law supplies multiplicative relations, so the indexed phases are not being claimed algebraically independent as separate variables. The theorem is linear independence over $\overline{\mathbb Q}$, not algebraic independence of an unconstrained family.

Difficulty

The main algebraic difficulty is the presence of negative exponents. Ordinary polynomial evaluation detects finite relations among nonnegative powers, but an integer-indexed relation is a Laurent polynomial. The formal statement must ensure that evaluation of Laurent polynomials at a nonzero transcendental element is injective. It must also transport transcendence from $\mathbb Q$ to the algebraic closure embedded in $\mathbb C$ without replacing the registered field by an informal copy.

The transcendence theorem itself is a much larger analytic and algebraic-number-theoretic development. Treating it as an explicit hypothesis is therefore load-bearing: no unproved axiom or hidden instance may assert Hermite--Lindemann. Full Lindemann--Weierstrass is stronger than needed for this one-parameter family, since all exponents are integer multiples of a single algebraic generator.

Formalization scope

The mission targets Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f with Lean 4.30. Laurent polynomials are Mathlib's finitely supported integer-indexed monoid algebra. The algebraic numbers are represented by algebraicClosure ℚ ℂ, the subtype of complex numbers algebraic over the rationals. Linear independence is the ordinary Mathlib module-theoretic predicate.

The reusable core proves Laurent-power independence for arbitrary fields and arbitrary field extensions. The complex consumer uses Mathlib's complex exponential, the algebraicity of $i$, and the algebraic-closure transcendence transfer. The mission includes explicit degenerate controls for zero coupling and duplicate labels. It does not prove Hermite--Lindemann, Lindemann--Weierstrass, transcendence of $\pi$, a topological winding theorem, or algebraic independence of the phase family.

Selected references

• Javier Fresán, Gevrey Arithmetic and E-functions, Chapter 1, Theorem 1.1 (Hermite--Lindemann--Weierstrass), 2023. https://javier.fresan.perso.math.cnrs.fr/gevrey.pdf
• Encyclopedia of Mathematics, Lindemann theorem. https://encyclopediaofmath.org/wiki/Lindemann_theorem
• Mathlib, Mathlib.Algebra.Polynomial.Laurent, Laurent-polynomial definitions and evaluation. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Laurent.html

Motivation

The fundamental lemma is a family of identities between orbital integrals on a reductive group and stable orbital integrals on a smaller group attached to it, its endoscopic group. Langlands isolated these identities in the 1970s as the last missing ingredient in the comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987; Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form implies the group form. The Lie algebra statement was proved in equal characteristic by Bao Chau Ngo in Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), by a global geometric argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to mixed characteristic. The identity is the engine behind the stabilization of the trace formula and behind the computation of the cohomology of Shimura varieties.

Both sides of the identity carry a normalizing factor built from the discriminant, and the exact power of $q$ relating the two normalizations is fixed by a purely root-theoretic computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this mission. It is self-contained, it uses no geometry, and it is the first piece of the paper that can be stated in Lean today.

Setting

Let $G$ be a split reductive group over a field with maximal torus $T$, character lattice $X^*(T)$, cocharacter lattice $X_*(T)$, root system $\Phi \subset X^*(T)$ and Weyl group $W$. Write $\mathfrak{t}$ for the Cartan subalgebra, so that each root $\alpha$ has a differential $d\alpha$, a linear form on $\mathfrak{t}$. Ngô's discriminant is the product

$$D_G \;=\; \prod_{\alpha \in \Phi} d\alpha ,$$

a $W$-invariant polynomial function on $\mathfrak{t}$ and hence a function on the space $\mathfrak{c} = \mathfrak{t} /\!/ W$ of characteristic polynomials.

An endoscopic datum is an element $\kappa$ of the dual torus $\hat{T} = \operatorname{Hom}(X_*(T), \mathbb{G}_m)$. The endoscopic group $H$ attached to it is the group whose root system is

$$\Phi_H \;=\; \{\alpha \in \Phi \;:\; \kappa(\alpha^\vee) = 1\} ,$$

with Weyl group $W_H \subset W$ and its own discriminant $D_H = \prod_{\alpha \in \Phi_H} d\alpha$. Choose a subset $\Lambda \subset \Phi - \Phi_H$ containing exactly one root out of each pair $\{\alpha, -\alpha\}$ of opposite roots outside $\Phi_H$, and set

$$R^G_H \;=\; \prod_{\alpha \in \Lambda} d\alpha .$$

Finally let $F$ be a non-archimedean local field with valuation $v$ and residue cardinality $q$, and recall Ngô's normalizing factors $\Delta_G(a) = q^{-v(D_G(a))/2}$ and $\Delta_H(a_H) = q^{-v(D_H(a_H))/2}$.

Formalization targets

Goal (1.11.3): the transfer factor identity

$$v\bigl(D_G(a)\bigr) \;=\; v\bigl(D_H(a_H)\bigr) \;+\; 2\, v\bigl(R^G_H(a_H)\bigr)$$

for a point $a_H$ of the endoscopic Cartan with image $a$. Equivalently $\Delta_H(a_H)\Delta_G(a)^{-1} = q^{\,r}$ with $r = v(R^G_H(a_H))$: this is exactly what lets one pass between the two forms of the fundamental lemma, $O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = q^{\,r} SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$ and $\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = \Delta_H(a_H) SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$.

Milestones

The identity above is the image under $v$ of the divisor identity $\nu^* D_G = D_H + 2 R^G_H$ of 1.10.3, which in turn rests on the fact that $R^G_H$ — which depends on a choice of $\Lambda$ — is nevertheless $W_H$-invariant, and on the fact that $\Phi_H$ really is a root subsystem. The milestone list follows that order.

Significance

Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity $\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}, dt) = \Delta_H(a_H) SO_{a_H}(\mathbf{1}_{\mathfrak{h}}, dt)$ for corresponding regular semisimple stable classes, under the hypothesis that twice the Coxeter number of $G$ is smaller than the residue characteristic. Nothing in that statement can be written in Lean today: reductive group schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals and affine Springer fibers are all absent from Mathlib. What can be written, faithfully and without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that is what this mission asks for. It is a genuine prerequisite: the two displayed forms of Theorem 1 differ precisely by the identity above.

The mission also produces reusable infrastructure — the discriminant of a root system, the notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an element of the dual torus — none of which currently exists in Mathlib, and all of which any future formalization of endoscopy will need.

Difficulty

Only one of the four milestones is a routine manipulation. Splitting $\Phi - \Phi_H$ into pairs $\{\alpha,-\alpha\}$ and collecting squares is bookkeeping; that $D_G$ is $W$-invariant is immediate because $W$ permutes $\Phi$. The content is in Lemma 1.10.2: $\Lambda$ is not stable under $W_H$, so $w \in W_H$ carries $\prod_{\alpha\in\Lambda} d\alpha$ to $(-1)^{m(w)} \prod_{\alpha\in\Lambda} d\alpha$, where $m(w)$ counts the roots of $\Lambda$ sent into $-\Lambda$; the claim is that $m(w)$ is always even. The naive attempt — check it on the generating reflections of $W_H$ — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside $\Phi_H$. Ngô's argument identifies the sign with $(-1)^{\ell_G(w)} (-1)^{\ell_H(w)}$, the ratio of the sign characters of $W$ and $W_H$, and observes that both compute the determinant of $w$ acting on the same reflection representation.

Formalization scope

Root systems are modelled with Mathlib's RootPairing ι R M N: the module $M$ plays the role of $X^*(T)$, the module $N$ the role of $X_*(T)$ and of the Cartan on which the differentials $d\alpha$ are evaluated, and $P.root' i$ is the linear form $d\alpha$. The endoscopic subsystem is cut out by an element $\kappa$ of the dual torus, taken as a group homomorphism from the cocharacter lattice to an arbitrary commutative group, and is expressed over $\mathbb{Z}$ coefficients as in the definition of a root datum. Products over $\Phi$ and $\Phi_H$ are finite products over a Fintype index, and a choice $\Lambda$ is a Finset satisfying an exclusive-or condition, which automatically rules out the degenerate case $\alpha = -\alpha$.

The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an identity of divisors, so the unit $(-1)^{|\Lambda|}$ is carried explicitly rather than discarded. Lemma 1.10.2 is stated over $\mathbb{Q}$ for an honest root system, since the sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive valuation with values in $\mathbb{Z} \cup \{\infty\}$, which is what makes the two sides comparable when a discriminant vanishes.

There is no trivializing formalization here: the hypotheses of every item are satisfiable — any root system with any closed subsystem and any choice of $\Lambda$ gives an instance — so none of the statements is vacuous, and none of them is an identity between two occurrences of the same expression.

Contributions of the surrounding theory are welcome: a positive system compatible with a subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor (the remaining half of Lemme 1.10.1) are all natural next steps.

Selected references

• Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169. https://doi.org/10.1007/s10240-010-0026-7
• R. Langlands, D. Shelstad, On the definition of transfer factors, Math. Ann. 278 (1987), 219-271. https://doi.org/10.1007/BF01458070
• J.-L. Waldspurger, Endoscopie et changement de caracteristique, J. Inst. Math. Jussieu 5 (2006), 423-525. https://doi.org/10.1017/S1474748006000041
• R. Kottwitz, Transfer factors for Lie algebras, Represent. Theory 3 (1999), 127-138. https://doi.org/10.1090/S1088-4165-99-00077-6
• T. Hales, A statement of the fundamental lemma, in Harmonic Analysis, the Trace Formula, and Shimura Varieties, Clay Math. Proc. 4 (2005), 643-658. https://arxiv.org/abs/math/0312227

A.L.E.T.H.E.A.N. — the engine behind this corpus

This mission curates the formalized output of Alethean — an Autonomous Logic Engine for Theorem Hunting, Exploration, And Navigation (alethean.org). Alethean autonomously generates research directions, develops them into research papers, and formalizes their results in Lean 4 — an "ever-expanding registry of absolute mathematical truths," built with the Aristotle reasoning engine. "The unconcealed truth between conjecture and proof."

The corpus's public home is the Alethean Lean 4 Catalog — the central registry of formalized theorems across the ecosystem, browsable as research packages (each with its article, research paper, interactive view, future directions, and Lean 4 proof files). This mission is the platform-side mirror of that registry: 2,799 definition bundles and 7,517 theorems compiled and verified against the pinned toolchain (Lean v4.30.0, Mathlib c5ea003), spanning analytic number theory, combinatorics, probability, information theory, quantum information, tropical algebra, and machine-learning theory.

What is being asked

The corpus arrives fully proved. The goal theorem is the corpus's universal error-detection bound for random checksums — the capstone of the Almost-Lossless compression thread (Compression Beyond the Pigeonhole Bound): appending an independent random checksum makes the probability of silent corruption at most $1/K$, uniformly over all source strings and all inner decoders. The milestones are capstone theorems from across the corpus: sphere-packing and VC-dimension bounds, second moments of central $L$-values, tropical Arrow-type impossibility, sums-of-three-cubes obstructions, and more.

For solvers

Every milestone is a verified platform theorem: study the proofs, reuse them as imported lemmas, or rebuild them from first principles. The interesting open work is extension: the corpus's research-direction papers (browsable at alethean.org under Future Directions) state quantitative sharpenings — explicit constants, wider parameter ranges — that are not yet formalized. Pick a direction, formalize its statement, and the verification pipeline does the rest.

Provenance

• Source repository: github.com/raver1975/lean (commit 53c2925a02)
• Public registry: alethean.org
• Toolchain: Lean v4.30.0, Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f
• All uploaded items are tagged aether-catalog.

Motivation

Every introductory number theory course opens with the same fact: the integers factor into primes in exactly one way. Euclid's Elements (Book IX, Proposition 14) already proves a form of it for the case of two factorizations sharing no further structure, but the theorem is not stated in full generality — with existence and uniqueness as a single package — until Gauss's Disquisitiones Arithmeticae (1801, Art. 16). Every standard modern treatment restates it as the opening theorem of the subject: Hardy & Wright, An Introduction to the Theory of Numbers (Theorem 2), and Apostol, Introduction to Analytic Number Theory (1976, Theorems 1.9–1.10), both prove it in the first chapter, before anything else is developed. The reason is structural, not pedagogical convenience: gcd, lcm, multiplicative functions, the notion of "the" prime factorization of an integer, and the entire multiplicative structure of $\mathbb{Z}$ depend on it being true. Mathlib itself packages the general statement as UniqueFactorizationMonoid, of which $\mathbb{N}$ is one instance — this mission asks for the classical, elementary argument specific to $\mathbb{N}$, in the two-part shape every textbook gives it.

Setting

A prime $p \in \mathbb{N}$ is a natural number $p \geq 2$ whose only divisors are $1$ and $p$ (Mathlib's Nat.Prime). A factorization of $n \in \mathbb{N}$ is represented here as a multiset $l$ of natural numbers — an unordered collection that tracks multiplicity but not order, so that two factorizations differing only by a reordering of their factors are already identified as the same multiset, with no separate permutation argument needed. Write $l.\mathrm{prod} = \prod_{p \in l} p$ for the product of the elements of $l$ with multiplicity, under the convention that the empty multiset has product $1$. The theorem concerns multisets all of whose elements are prime.

Formalization targets

Goal — unique factorization

$$\forall\, n \neq 0,\quad \exists!\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.$$

For every nonzero $n$ there is exactly one multiset of primes whose product is $n$. This is the capstone: existence and uniqueness combined into the single statement every textbook eventually asserts.

Milestone 1 — existence

$$\forall\, n \neq 0,\quad \exists\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.$$

Every nonzero natural number is a product of primes (Apostol, Theorem 1.9). This alone says nothing about how many such multisets there might be.

Milestone 2 — uniqueness

$$\left(\forall p \in l_1,\ p \text{ prime}\right) \wedge \left(\forall p \in l_2,\ p \text{ prime}\right) \wedge l_1.\mathrm{prod} = n = l_2.\mathrm{prod} \ \implies\ l_1 = l_2.$$

Any two multisets of primes with the same product are equal (Apostol, Theorem 1.10). Combined with Milestone 1, this gives the Goal.

Significance

The result itself. Unique factorization is what makes "the prime factorization of $n$" a well-defined object rather than a choice. Every downstream elementary and analytic number theory construction leans on it: $\gcd(a,b)$ and $\mathrm{lcm}(a,b)$ computed via shared prime exponents, multiplicative arithmetic functions ($\varphi$, $\sigma$, $\mu$) defined by their values on prime powers, the Euler product for $\zeta(s)$, and $p$-adic valuations. Without it, none of these constructions are canonical.

Formalizing it. The general statement is already machine-checked in Mathlib as an instance of UniqueFactorizationMonoid (and concretely realized for $\mathbb{N}$ via Nat.factors/Nat.factors_unique), so this is not open mathematics. What this mission asks for is the specific, elementary two-lemma argument — strong induction for existence, Euclid's lemma plus strong induction for uniqueness — spelled out for $\mathbb{N}$ with the Multiset representation used here, rather than a one-line appeal to the packaged Mathlib result. A solution that simply repackages Nat.factors_unique and its companions is a legitimate route (nothing here is designed to block it), but the more valuable contribution is the self-contained classical proof, since that is what a reader of Apostol or Hardy & Wright expects to see reconstructed.

Difficulty

For existence, ordinary induction on $n$ does not immediately work: if $n$ is composite, $n = ab$ with $1 < a, b < n$, and the inductive hypothesis is needed for both $a$ and $b$ at once, neither of which is simply $n - 1$. The fix is strong (well-founded) induction on $n$, splitting into the prime case (trivial single-element multiset) and the composite case (combine the two multisets for $a$ and $b$).

For uniqueness, the natural first attempt — "cancel a common prime factor from both sides and recurse" — silently assumes that the same prime appears in both multisets, which is exactly what needs to be proved. The step that actually does the work is Euclid's lemma: if a prime $p$ divides a product $l_2.\mathrm{prod}$, it divides one of the factors of $l_2$. This is not a restatement of primality (irreducibility, "no nontrivial divisors") but a genuinely separate fact about $\mathbb{N}$ that requires either Bézout's identity or a well-ordering argument to establish; conflating "prime" with "has this divisibility property" is the standard trap for a first attempt at this proof.

Formalization scope

The statement is specific to $\mathbb{N}$ (not $\mathbb{Z}$ or a general UniqueFactorizationMonoid), and factorizations are represented as Multiset ℕ rather than List ℕ up to permutation — this is a deliberate choice that folds "unique up to reordering" directly into multiset equality. The hypothesis is $n \neq 0$, not $n > 1$: the case $n = 1$ is included, and its unique witness is the empty multiset, since the empty product is $1$ and no nonempty multiset of primes (each $\geq 2$) can have product $1$. $n = 0$ is excluded because no multiset of natural numbers has product $0$ under this convention (every prime is $\geq 2$, and the empty product is $1$), so no factorization of $0$ exists to be unique.

No auxiliary platform Definitions are required — the statement is expressed entirely in terms of Nat.Prime and Multiset.prod from Mathlib. Reusable contributions welcome beyond the two milestones: an explicit construction of the canonical sorted List ℕ factorization (Nat.factors-style) connecting this multiset formulation to the more computational list representation, or a generalization of the uniqueness argument to an explicit statement and proof of Euclid's lemma as a standalone milestone.

Selected references

• C. F. Gauss, Disquisitiones Arithmeticae, 1801, Art. 16.
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Theorem 2.
• T. M. Apostol, Introduction to Analytic Number Theory, Springer, 1976, Theorems 1.9–1.10.
• The Mathlib Community, Mathlib4, Mathlib.RingTheory.UniqueFactorizationDomain, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.html

From individual representations to an arithmetic criterion

Writing a positive integer as a sum of two squares is an elementary question with a precise general answer. Some integers have such a representation and others do not; checking a few small inputs does not explain the distinction. A criterion expressed through prime factorization instead decides the question for every positive integer. This project follows Section 5.7 of William Stein's Elementary Number Theory: Primes, Congruences, and Secrets, including the section's supporting statements and one subsequent exercise. The selected material connects divisibility, coprimality, algebraic identities, and rational approximation within a single classical topic. The source is the author-hosted January 2017 text, using its numbering rather than the numbering of earlier drafts.

Integers, representations, and prime exponents

A two-square representation of an integer $n$ consists of integers $x,y$ satisfying $n=x^2+y^2$. Either coordinate may be zero or negative. A representation is primitive when the greatest common divisor of its coordinates is one; this restricts representations, not the definition of representability itself. For a positive integer $n$ and a prime $p$, the prime exponent $v_p(n)$ is the exponent of $p$ in the prime factorization of $n$. The congruence $p\equiv3\pmod4$ means that division of $p$ by four leaves remainder three.

The approximation statement uses a real number $t$, a positive integer $N$, and a reduced fraction $a/b$, where $a$ is an integer, $b$ is a positive integer, and their greatest common divisor is one. These conventions agree with Stein's section and its definition of primitive representations.

Formalization targets

The supporting targets retain their complete source statements. Lemma 5.7.4 concerns every positive integer $n$ with a prime divisor $p\equiv3\pmod4$:

$$\nexists x,y\in\mathbb Z:\quad n=x^2+y^2\quad\text{and}\quad\gcd(x,y)=1.$$

Equation (5.7.1) is the integer identity

$$(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2.$$

Lemma 5.7.5 states that, for every real $t$ and positive integer $N$, some reduced fraction satisfies

$$0<b\le N,\qquad |t-a/b|\le\frac{1}{b(N+1)}.$$

The capstone, Theorem 5.7.1, is the complete equivalence

$$n=x^2+y^2\text{ for some }x,y\in\mathbb Z \quad\Longleftrightarrow\quad \forall\text{ primes }p\mid n,\quad p\equiv3\pmod4\Longrightarrow v_p(n)\text{ is even},$$

for every positive integer $n$. Both implications are required. These four statements are located on printed pages 117–120 of the source PDF.

Exercise 5.11, on printed page 122, is an optional downstream target:

$$\forall n\in\mathbb Z,\ \exists k\in\{0,1,2,3\}:\quad \nexists x,y\in\mathbb Z,\ n+k=x^2+y^2.$$

It describes gaps among represented integers and is not a prerequisite milestone for the capstone.

What the criterion and its formalization provide

The criterion replaces a search for coordinates with a finite condition on the factorization of an input. It applies to composite integers as well as primes and distinguishes the exponent of a prime divisor from the mere presence of that divisor. The primitive obstruction also explains why a claim about coprime coordinates must not be confused with a claim that excludes all representations. The composition identity supplies an explicit statement of multiplicative closure, while the exercise gives a uniform restriction on consecutive runs. These are the consequences and accompanying results presented in Stein's treatment.

The mathematics is established, not an open research problem. Important formal ingredients already exist in Mathlib: the sum-of-two-squares development includes the arithmetic criterion and primitive obstruction, and the Diophantine approximation development supplies the bounded-denominator result. The work here is a source-aligned collection of exact theorem interfaces and independently checked proofs. Reusing those results does not claim a new proof of the classical mathematics or an exact transcription of Stein's argument.

Why the complete statement matters

A finite list of successful representations cannot establish an assertion about every positive integer. Similarly, a restriction on primitive representations is insufficient to settle general representability, because a nonprimitive pair is still a valid representation. The capstone must account for prime exponents and both directions of the equivalence simultaneously. The approximation result has its own coupled requirements: obtaining a small denominator without the stated error bound, or a good approximation with an uncontrolled denominator, does not meet the target. These distinctions are explicit in the source statements.

Formalization scope

The namespace is SteinENT. Inputs $n,p,N$ use natural numbers, with positivity hypotheses wherever the source uses positive integers. Coordinates and all subtraction in the composition identity use integers. Prime exponents use Nat.factorization; primitivity uses Int.gcd x y = 1. Approximation witnesses use Lean's rational type, whose canonical numerator and positive denominator already express a reduced fraction. The error inequality is an inequality of real numbers. The gap exercise allows every integer starting point, including negative ones.

No hypothesis assumes the desired representation or restricts the capstone to a bounded test range. There is no additional definition that hides a proof obligation, and no separate alias item for primitivity. Standard Mathlib arithmetic, rational approximation, and tactic libraries provide reusable infrastructure. Complete alternative proofs are welcome when they preserve these interfaces, including the explicit positive-input boundary and unrestricted integer coordinates.

Selected references

• William Stein, Elementary Number Theory: Primes, Congruences, and Secrets, Undergraduate Texts in Mathematics, Springer, 2008; author-hosted January 2017 version, Section 5.7 and Exercise 5.11. Author's book page.
• William Stein, author's source text at commit c4984c7ddb22258674816f8c000b0d8eb485d694, corresponding section and exercises.
• The Mathlib Community, Mathlib4 at commit 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, Lean 4 library, pinned formalization environment; number-theory modules linked above.

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).