Number Theory

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $6101$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 6101,\ \textstyle\sum s = n.$$

This is the campaign template with the value $6101$ filled in. The source proves the stronger statement that every odd $n \ge 12\,203$ is a sum of exactly $6101$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the first moment:

1. Whole-triangle count. Counting all pairs with $p + q \le x$ gives $\sum_{s \le x} r(s) \ge 2(x-2000)^2/(9(\log x)^2)$ for $x \ge 2000$.
2. Weighting. Weighting $r(s)$ by $(\log s)^2/s$ cancels the varying factor in the sieve bound $r(s) \le 9\,C(s)\,s/(\log s)^2$, giving a weighted first moment of at least $\tfrac{44}{100}x$.
3. Second moment of $C$. With $\sum_{s \le x,\, 2\mid s} C(s)^2 \le \tfrac{21}{2}x$, Cauchy–Schwarz yields $\sigma(A) \ge 1/2200$ for $A = B + B$, $B = \{(p-3)/2\}$.
4. Schnirelmann's inequality with $m = 1525$ (the least $m$ with $(1 - 1/2200)^m < 1/2$) gives $K = 4m + 1 = 6101$.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$.
3. Moment bounds for the singular-series factor $C(s)$.
4. Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$.

Formalization scope

The Lean statement is the campaign template verbatim with $6101$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $6101$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $97\,041$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 97\,041,\ \textstyle\sum s = n.$$

This is the campaign template with the value $97\,041$ filled in. The source proves the stronger statement that every odd $n \ge 194\,083$ is a sum of exactly $97\,041$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It is the argument behind the $100\,001$ entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give $\sigma(A) \ge 1/35\,000$ for $A = B + B$, $B = \{(p-3)/2 : p \text{ odd prime}\}$. The only change is to take the smallest admissible $m$ in Schnirelmann's inequality: $(1 - 1/35\,000)^{m} < 1/2$ first holds at $m = 24\,260$ (rather than the rounded $25\,000$), so $2mA = \mathbb{Z}_{\ge 0}$ and $K = 4m + 1 = 97\,041$.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$.
3. Moment bounds for the singular-series factor $C(s)$.
4. Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$.

Formalization scope

The Lean statement is the campaign template verbatim with $97\,041$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $97\,041$; not peer reviewed.

Motivation

Goldbach's problem asks whether every integer greater than $1$ can be written as a sum of a small number of primes. The first unconditional result of this kind was obtained by Schnirelmann around 1930: there is an absolute constant $k$ such that every integer $n > 1$ is a sum of at most $k$ primes. His argument is elementary. It uses an upper-bound sieve and Chebyshev-type prime estimates, together with a notion of additive density, and it does not need the prime number theorem or complex analysis.

The constant has since been reduced by much deeper methods. A short timeline for odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes, with an ineffective threshold in the original argument.
• Ramaré (1995): every even integer is a sum of at most six primes, which gives at most seven primes for every odd $n > 1$. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): every odd $n > 1$ is a sum of at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes (the ternary Goldbach conjecture). (arXiv:1312.7748)

This mission targets a much weaker constant than any of these, $k = 100\,001$. It does so because the constant comes from Schnirelmann's elementary method with every estimate made explicit, and that proof is short enough to be a realistic target for a complete formalization.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset $s$ of natural numbers such that every element of $s$ is prime, the elements of $s$ sum to $n$, and $s$ has at most $k$ elements counted with multiplicity. Repetitions are allowed and order is irrelevant.

The number $1$ is not a sum of primes, so the question concerns odd $n \ge 3$. Even numbers are excluded from the campaign statement.

The Schnirelmann density of a set $A \subseteq \mathbb{Z}_{\ge 0}$ is

$$\sigma(A) = \inf_{N \ge 1} \frac{|A \cap \{1, \dots, N\}|}{N}.$$

This notion is the additive tool behind the elementary approach. Mathlib provides it as schnirelmannDensity.

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 100\,001,\ \textstyle\sum s = n.$$

This is the campaign template of Odd numbers as sums of primes with the value $100\,001$ filled in. A stronger explicit form in the source is that every odd $n \ge 200\,003$ is a sum of exactly $100\,001$ primes; the at-most form for all odd $n > 1$ follows from it immediately.

Significance

The result itself. The bound $100\,001$ is far from the best known constants; five (Tao) and three (Helfgott) are both known on paper. Its value is that it rests on an elementary argument with every constant written out. There is no "sufficiently large" threshold and no appeal to the prime number theorem, zero-density estimates, or large-scale computation.

Formalizing it. No finite bound in this problem has a machine-checked proof on this platform yet. A proof of this goal would be the campaign's first proved value. The components are reusable beyond this mission:

1. Explicit Chebyshev-type bounds for $\pi(y)$.
2. An explicit Selberg upper-bound sieve for the number of representations of an even number as a sum of two odd primes.
3. An averaged bound for the associated singular-series factor.
4. Schnirelmann's density inequality $\sigma(D + E) \ge \sigma(D) + \sigma(E) - \sigma(D)\sigma(E)$.

Difficulty

The only substantial step is an upper bound for

$$r(s) = \#\{(p, q) : p, q \text{ odd primes},\ p + q = s\}$$

that is sharp up to a constant factor, namely of order $s/(\log s)^2$ times an arithmetic factor depending on the prime divisors of $s$, with an explicit constant. The trivial bound $r(s) \le \pi(s)$ is weaker by a factor of $\log s$. That loss makes the density of sums of two primes appear to be zero, so the additive argument cannot start. Everything after the sieve bound is short and explicit.

Formalization scope

The Lean statement is the campaign template verbatim with $100\,001$ in place of the value. It uses Multiset ℕ, Nat.Prime, and Odd n ∧ 1 < n. The statement is fixed by the campaign, and it has no vacuous hypotheses: every odd $n > 1$ is covered.

Mathlib already contains schnirelmannDensity and the fact that $\sigma(A) + \sigma(B) \ge 1$ with $0 \in A \cap B$ implies $A + B = \mathbb{N}$. It also contains the Λ² setup of the Selberg sieve (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial-coefficient bounds. Missing, and welcome as contributions:

1. The explicit sieve bound for $r(s)$.
2. The mean-square bound for the arithmetic factor.
3. Schnirelmann's inequality for $\sigma(D + E)$.
4. The explicit lower bound for $\pi(y)$ in the form needed here.

Selected references

• P. Pollack, Not Always Buried Deep: A Second Course in Elementary Number Theory, AMS, 2009. Chapter 6, §6, "An application to the Goldbach problem", pp. 196–201. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa Cl. Sci. (4) 22 (1995), 645–706. http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), 997–1038. https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• An explicit elementary constant for sums of primes, unpublished note, September 2026, Theorem 1. Source of the constant $100\,001$ (with $c_1 = 1/9$, $c_2 = 860$, $x_0 = e^{2000}$, $\sigma(A) \ge 1/35\,000$, $m = 25\,000$).

Motivation

The representation function $r_{2}(n)=\#\{(a,b)\in\mathbb Z^{2}:a^{2}+b^{2}=n\}$ is one of the oldest objects in number theory. Fermat characterised the integers with $r_{2}(n)>0$ — those in which every prime congruent to $3$ modulo $4$ occurs to an even power — and Euler's proof supplied the closed form $r_{2}(n)=4\,(d_{1}(n)-d_{3}(n))$, where $d_{j}(n)$ counts divisors congruent to $j$ modulo $4$ (sum of two squares theorem).

That description counts representations but does not relate them to one another. The integers carrying several essentially different representations,

$$50=1^{2}+7^{2}=5^{2}+5^{2},\qquad 65=1^{2}+8^{2}=4^{2}+7^{2},$$

are exactly the integers that produce quadruples $(a,b,c,d)$ with

$$a^{2}+b^{2}=c^{2}+d^{2}$$

whose two sides are not identified by swapping the two entries or changing their signs. Three reasons make this relation worth a formal development rather than a passing remark.

• Energy counts. Counting solutions of the equation inside a box is the additive energy of the set of sums of two squares, the quantity controlling mean-square errors for $r_{2}$; it is a genuinely different problem from determining $r_{2}(n)$ for a single $n$, and every estimate for it starts from a description of the solution set.
• Composition of representations. The Brahmagupta–Fibonacci identity

$$(p^{2}+q^{2})(r^{2}+s^{2})=(pr+qs)^{2}+(ps-qr)^{2}=(pr-qs)^{2}+(ps+qr)^{2}$$

takes two representations and produces a third. Known to Brahmagupta and stated by Fibonacci in Liber Quadratorum (1225), it is the multiplicativity of the norm in the Gaussian integers, and it is the engine behind every statement below.

• Geometry. Over a field, the locus $a^{2}+b^{2}=c^{2}+d^{2}$ in projective three-space is the split quadric, isomorphic to $\mathbb P^{1}\times\mathbb P^{1}$ under the Segre embedding; the four parameters introduced below are Segre coordinates in this sense. The arithmetic content of the equation is precisely the integrality that this geometry ignores.

The parametrisation targeted here is classical. Nothing in this mission claims new mathematics; the aim is a machine-checked development in which every hypothesis is explicit.

Setting

Fix integers. A solution is a quadruple $(a,b,c,d)\in\mathbb Z^{4}$ with $a^{2}+b^{2}=c^{2}+d^{2}$. It is trivial if the multisets $\{a^{2},b^{2}\}$ and $\{c^{2},d^{2}\}$ coincide, i.e. if $(c,d)$ equals $\pm(a,b)$ or $\pm(b,a)$; if entries are allowed to vanish, the least value carried by a non-trivial solution is $25=0^{2}+5^{2}=3^{2}+4^{2}$, and requiring all four entries to be positive raises that value to $50$. A solution is primitive when the four entries have greatest common divisor $1$, and positive when all four entries are positive and pairwise distinct — the case in which nothing about the relation is explained by signs, zeros or coincidences.

Two constructions produce solutions. The four-parameter family associates to integers $p,q,r,s$ the quadruple

$$a=pr+qs,\qquad b=ps-qr,\qquad c=pr-qs,\qquad d=ps+qr,$$

which solves the equation because both sides equal $(p^{2}+q^{2})(r^{2}+s^{2})$ by the identity above. Substituting particular parameters is unrevealing, so a genuine supply comes instead from the elementary one-parameter family

$$1^{2}+(n^{2}-n+1)^{2}=(2n-1)^{2}+(n^{2}-n-1)^{2},$$

whose four entries $1$, $n^{2}-n+1$, $2n-1$, $n^{2}-n-1$ are strictly increasing — hence positive and pairwise distinct — as soon as $n\ge 4$. The bound is sharp: at $n=3$ the two entries $2n-1$ and $n^{2}-n-1$ are equal.

In the reverse direction, rewrite the equation as $(a+c)(a-c)=(d+b)(d-b)$ and set

$$X=(a+c)/2,\quad Y=(a-c)/2,\qquad U=(b+d)/2,\quad V=(d-b)/2 .$$

The halves are integers exactly when $a$ and $c$ share a parity and so do $b$ and $d$, and in that case the equation becomes

$$XY=UV .$$

The development is organised in the namespace TwoSquares, with node names matching the roles above (four_param_identity, explicit_family_chain, sum_sq_eq_halves, four_factor_param, complete_parametrization).

Formalization targets

Goal — completeness of the four-parameter family

For all integers $a,b,c,d$ with $a^{2}+b^{2}=c^{2}+d^{2}$, there are integers $p,q,r,s$ with

$$a=pr+qs,\quad b=ps-qr,\quad c=pr-qs,\quad d=ps+qr,$$

possibly after interchanging $c$ and $d$. The goal asserts only the existence of integral parameters and the necessity of at most one swap; it does not assert uniqueness of $(p,q,r,s)$, which is false, and it says nothing about how many solutions lie in a given box.

The four-parameter identity

The identity itself, over an arbitrary commutative ring, together with the two forms of the Brahmagupta–Fibonacci identity that imply it — so that the reason it holds, rather than the expansion, is what is recorded.

An explicit infinite family

For every integer $n\ge 4$ the displayed family is a positive pairwise distinct solution; the parametrisation $n\mapsto(1,\,n^{2}-n+1,\,2n-1,\,n^{2}-n-1)$ is injective; the set of quadruples it produces is infinite; and no member is a nontrivial integer multiple of another, each member being primitive.

From the sum-of-squares equation to $XY=UV$

The equivalence of $a^{2}+b^{2}=c^{2}+d^{2}$ with $(a+c)(a-c)=(d+b)(d-b)$; the parity statement that matching entries share a parity after at most one swap; and the resulting existence of the half-sum variables satisfying $XY=UV$.

Parametrizing $XY=UV$

For all integers $X,Y,U,V$ with $XY=UV$ there are integers $p,q,r,s$ with $X=pr$, $Y=qs$, $U=ps$, $V=qr$ — the coordinate form of the statement that a rank-one $2\times2$ matrix factors through the integers.

Significance

The result. Taken together, the reverse chain converts the Diophantine equation $a^{2}+b^{2}=c^{2}+d^{2}$ into four free integer parameters, at the cost of one possible swap. In that form every question about the solution set becomes a question about four independent variables, which is what makes energy estimates, density statements and searches for primitive solutions tractable. The chain also isolates where integrality enters: over a field the parametrisation of $XY=UV$ is formal, so the content is carried entirely by the parity step and by divisibility over $\mathbb Z$.

Formalizing it. None of the mathematics is new, and that is the point: the value here is a development in which each link is a reusable statement with explicit hypotheses. Three conventions make the nodes reusable rather than bespoke. The algebraic identity is proved over a general commutative ring, not over $\mathbb Z$. The positivity and distinctness of a family are packaged as one strict chain rather than as a list of inequalities, since later arguments use the ordering, not merely the disequalities. The parity issue is isolated into a single node stating a disjunction, instead of being discharged by case splits buried inside a later proof. Conversely, the shape of the final theorem records honestly what is not claimed: parameters are not unique, and no normal form is asserted.

As difficulty, the early nodes have short proofs, while completeness requires the full chain and is the substantial part of the mission.

Difficulty

The obvious first idea is to use the Gaussian integers: $a+bi$ and $c+di$ have the same norm, so factor both and compare. It fails. Equal norm does not make two Gaussian integers associates or divisors of one another — $1+8i$ and $4+7i$ both have norm $65$ and are related by no divisibility — because uniqueness of factorisation regroups prime factors in ways that the norm alone cannot distinguish. The correct route recovers the four parameters from the product equation instead, and there the friction is entirely arithmetic:

Clearing halves. The substitution $X=(a+c)/2$ is not available for arbitrary solutions: $a^{2}+b^{2}=c^{2}+d^{2}$ forces only that the multiset of parities of $(a,b)$ matches that of $(c,d)$, so $(a,c)$ may have different parities and no integer $X$ may exist. The example $a=1,b=0,c=0,d=1$ shows this is not vacuous, and it is why the goal carries a swap.

Factoring $XY=UV$. Taking $p=\gcd(X,U)$ yields $X=pr$, $U=ps$ with $\gcd(r,s)=1$, and Euclid's lemma then forces $s\mid Y$ and $r\mid V$. The degenerate case $X=U=0$ — where the gcd vanishes and no cancellation is possible — must be handled separately, and because the variables range over $\mathbb Z$ rather than $\mathbb N$, every divisibility step must be tracked with signs. Working over a ring where division is available would delete both issues and with them the entire content of the statement.

Formalization scope

• All nodes are stated over $\mathbb Z$, except the Brahmagupta–Fibonacci identity and the four-parameter identity, which are proved over an arbitrary commutative ring. No node is stated over $\mathbb N$; transporting the prime-level statements is out of scope.
• Gaussian integers are deliberately unused. Mathlib carries them, but nothing here needs them, and a development depending on them would obscure the arithmetic that actually carries the proof.
• No quotient types, no permutation machinery: the possible swap of $c$ and $d$ is expressed as a disjunction, and the parity statement as a disjunction over Even.
• Trivializing formalizations are excluded. Over a field the parametrisation of $XY=UV$ holds trivially (take $p=X$, $r=1$, $s=U/X$), so the quarter-ring version carries no information; likewise, a completeness statement whose hypotheses already postulate the existence of the parameters would be vacuous. Both are explicitly not what is asked for.
• Expected to be reusable beyond this mission: the two forms of the Brahmagupta–Fibonacci identity; the strict-chain packaging of positivity and distinctness for a family given by polynomials; and the integer parametrisation of $XY=UV$, which is the Segre parametrization.
• Contributions are welcome for any node, and especially for the integer factoring lemma, for which several proofs are available. Explicitly out of scope: uniqueness or normal forms for $(p,q,r,s)$, counting asymptotics for solutions in a box, the Gaussian-integer reformulation, and all $\mathbb N$-level variants.

Selected references

• Sum of two squares theorem — Fermat's characterisation and Euler's divisor formula for $r_{2}$.
• Brahmagupta–Fibonacci identity — the two-square composition identity, its history, and its interpretation through norms.
• Leonardo Pisano (Fibonacci), Liber Quadratorum, 1225. English translation: L. E. Sigler, The Book of Squares, Academic Press, 1987.
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008 — Chapter XX on representations by two squares.
• Segre embedding — the identification of the rank-one quadric in $\mathbb P^{3}$ with $\mathbb P^{1}\times\mathbb P^{1}$.

Motivation

For every integer base $b\ge2$, a finite-prime weighted summability witness on a positive-integer host $H$ makes the reciprocal Mersenne series irrational on every infinite subset of $H$. A base-two witness gives that conclusion at every integer base. This is the source paper's proved Theorem 1; Erdős's unrestricted question for every infinite support remains outside its conclusion.

Setting

For an integer $b\ge2$, write $X_A(b)=\sum_{a\in A}(b^a-1)^{-1}$. Given a finite nonempty set $P$ of primes, let $h_P(a)=\prod_{p\in P}p^{v_p(a)}$ be the $P$-part of $a$, and set

$$W_{b,P}(A)=\sum_{a\in A}\frac{h_P(a)}{a(b^{h_P(a)}-1)}.$$

All support elements are positive. The prime set specifies the weight, not which exponents may belong to the support; the weighted series must also converge.

Formalization targets

Theorem 1 has two clauses for an infinite positive-integer host $H$:

$$W_{b,P}(H)<\infty\quad\Longrightarrow\quad X_A(b)\notin\mathbb Q\qquad\text{for every infinite }A\subseteq H,$$ $$W_{2,P}(H)<\infty\quad\Longrightarrow\quad X_A(b)\notin\mathbb Q\qquad\text{for every infinite }A\subseteq H\text{ and every integer }b\ge2.$$

In each clause $P$ is finite and nonempty. In the second, one prime witness for $H$ is fixed before choosing $A$ and $b$. Taking $A=H$ recovers the two direct assertions. The public formal main item states both hereditary clauses and has an accepted proof in the pinned Lean 4.30 environment.

Significance

Since $h/(2^h-1)\le1$, this criterion includes reciprocal-summable supports. The paper also gives an explicit $A_\star$ with divergent reciprocal mass but finite weighted mass. The inherited conclusions let another formal result use one certified host for many infinite thinnings. The already proved Lean result makes the host criterion and its dependencies available for direct import; new applications can check the exact premise they need against the public statement.

Difficulty

Reciprocal summability cannot bound the tail for every weighted support. A faithful statement also has to preserve the different order of prime, subset and base quantifiers; dropping fixed-base inheritance changes Theorem 1.

Formalization scope

The formal support is a Set ℕ, and 0 ∉ H enforces positive exponents. FinitePrimeWeighted contains one finite nonempty set of primes and summability of its weighted terms. The public main item joins two accepted Lean results: the fixed-base hereditary theorem and the binary-host all-base theorem. These statements and their public definitions can be reused in the same pinned environment. The later no-cover host is a separate result; it is not a clause of Theorem 1 or the paper's $A_\star$ example. Will Cook is the named paper author; the paper discloses substantial AI-assisted research and drafting and does not claim independent human verification of every proof. Erdős’s earlier criterion and later platform contributions carry separate credit.

Selected references

• Will Cook, Weighted Support Criteria for Reciprocal Mersenne Subseries, Erdős Problem Note #257, 2026, Theorem 1.
• P. Erdős, On the irrationality of certain series, The Mathematics Student 36 (1968), 222–226 (issued 1969).

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