Excluding the Bounded Negative Part

Introduction

Sylvester’s sequence $2,3,7,43,1807,\ldots$ is generated by $a_{n}=a_{n-1}^{2}-a_{n-1}+1$ and has reciprocal sum $1$ ; the recurrence is exactly the statement that the tail beyond $a_{n-1}$ equals $1/(a_{n-1}-1)$ . Erdős Problem #243 asserts that this is the only way a sequence of that growth can have a rational reciprocal sum:

See [3] and [4]. Bloom’s current catalogue record reproduces the displayed problem and labels it open, while explicitly warning that the status is the website owner’s present assessment and may not reflect all relevant literature . We therefore use the catalogue for numbering and current reported status only; the original publications carry the mathematical claims. Below we index the same recurrence as $a_{n+1}=a_n^{2}-a_n+1$ , which is the shift the formal sources use; the two forms are the same statement. Write $\operatorname{syl}(a)=a^{2}-a+1$ , the .

Relation to prior work.

Two published results reach the original problem under analytic hypotheses that are not assumed below. Their hypotheses are conditions on the sequence $(a_n)$ itself. Duverney’s is not comparable with the state-level hypotheses used here; the Erdős–Straus one, read through the dictionary of the next paragraph, is implied by nonnegativity of $E$ , the hypothesis of Theorem , so that criterion already covers the descent proved below (see [6]). Erdős and Straus proved that if $\lim a_n/a_{n-1}^{2}=1$ , the reciprocal sum is rational, and $a_n$ does not satisfy the recurrence, then $\limsup_{n\to\infty}\ \frac{[a_1,\ldots,a_n]}{a_{n+1}} \left(\frac{a_{n+1}^{2}}{a_{n+2}}-1\right)>0,$ where $[a_1,\ldots,a_n]$ is the least common multiple [1]. This is the indexing in the original theorem. Erdős’s 1988 survey, followed by the current catalogue summary, instead prints $a_n^2/a_{n+1}-1$ in the second factor while retaining the same prefix-LCM quotient; that displayed summary is off by one and is not followed here [7]. Koizumi records the convenient sufficient rate $a_n^2/a_{n+1}=1+o(1/n)$ under which the Erdős–Straus criterion settles the problem . Duverney proved a conditional signed form of the problem itself: if $\sum_{n\ge0}\left|a_{n+1}/a_n^{2}-1\right|$ converges, then the reciprocal sum, even with numerators in $\{-1,1\}$ , is rational if and only if the corresponding signed recurrence holds for all large $n$ . The all-positive specialisation is the form relevant here. Neither result is formalised here, and the results below do not recover either of them.

Koizumi’s work on doubly exponential sequences [6] bears directly on the state system used below, and supplies the coordinates in which several of the statements of this note are most naturally read. For a rational $r=p/q$ with pseudo-greedy expansion $(a_n)$ , remainders $(x_n)$ and gap sequence $\varepsilon_n=x_n^{-1}+1-a_n$ , his Lemma 15 [6] produces integers $c_n>0$ , $d_n$ and $e_n$ with $x_n=c_n/d_n$ and $\varepsilon_n=e_n/c_n$ , satisfying $a_n=\frac{d_n-e_n}{c_n}+1,\qquad c_{n+1}=c_n-e_n,\qquad d_{n+1}=a_nd_n ,$ and the proof of that lemma also gives $c_{n+1}=a_nc_n-d_n$ . Under the dictionary $(C_n,D_n,E_n)=(c_n,d_n,e_n)$ these are exactly the objects of Section : the first relation is the centring map $\operatorname{ctr}$ rewritten as $e_n=d_n-(a_n-1)c_n$ , the second is Proposition , the third is the denominator update, and the fourth is the tail update. The lower-case $e_n$ of Section is $-E_n$ , so it is the negative of Koizumi’s $e_n$ at an index where the centred state is negative. His Theorem 16 shows that his Conjecture 6 — that for a positive rational $r$ whose gap sequence satisfies $\varepsilon_n\to0$ one has $\varepsilon_n=0$ for all large $n$ — is equivalent to an affirmative answer to the question of Erdős and Graham recorded as his Question 5, which is Problem above. Two of the implications proved below have prior art in these canonical coordinates: his Lemma 13, that $\varepsilon_n=0$ forces $\varepsilon_{n+1}=0$ , is the absorption of Theorem , and his Proposition 19(2), that $\varepsilon_n\ge0$ for all large $n$ forces $\varepsilon_n=0$ for all large $n$ , is the descent of Theorem . These appear in canonical coordinates in [6]; no question of priority or independence is adjudicated here.

The growth hypothesis in Problem is calibrated by two facts about Sylvester’s sequence. It satisfies $a_n\approx c_0^{2^{n}}$ with $c_0=1.2640847\ldots$ , and shifting it further produces sequences with $a_n\approx C^{2^{n}}$ for arbitrarily large $C$ whose reciprocals still sum to a rational number [5]. The classical sufficient condition for irrationality, $\lim_n a_n^{1/2^{n}}=\infty$ , is therefore sharp. Kovač and Tao identify that condition as folklore [5]; they attribute the sharpness observation to Erdős (1975). A sequence with $a_n/a_{n-1}^{2}\to1$ has $a_n^{1/2^{n}}$ convergent, so that criterion says nothing about the sequences of Problem , and rationality is genuinely possible there. Sylvester’s sequence is A000058 in the OEIS and its shifts A129871. For the recent literature on irrationality of Ahmes series we refer to Kovač and Tao [5], who resolve several problems of Erdős and Graham drawn from the same two sources cited above, and whose introduction gives a sample of the intermediate work, including Sándor (1984) and Badea (1987). They do not treat Problem #243; the rigidity conclusion asked for there is not among their results.

The collection contains a mathematically equivalent unproved declaration, up to its zero-based indexing [8]. Its summand is $\mathbb{Q}$ -valued, so Lean’s Summable hypothesis asserts the existence of a sum in $\mathbb{Q}$ ; the finite indexing shift changes that sum only by a rational prefix. The declaration therefore does encode the rationality premise, but its proof is sorry. We use it as statement-level prior art, not as proof authority; the development below is independent of it. What is machine-checked below concerns the state system rather than the analytic problem: the exclusion of constant and periodic negative magnitudes, the bounded-rise barrier of Theorem , and the two conditional endpoints (Theorems and ), each stated with the exact hypotheses that separate it from Problem #243. No claim of priority is made for anything below.

The hypothesis is asymptotic and the conclusion is exact, so the argument must convert an analytic rate into an integer obstruction. The conversion used here is the classical one: clear denominators along the sequence, so that rationality makes a tail integral, and then centre that integer at the value it would take on Sylvester’s sequence. What remains is a single integer error $E$ , and the whole question is whether $E$ can avoid vanishing.

Statement	Status	Treatment here
Problem #243 as stated	Open	Not proved.
Defect identity	Proved here	Theorem , an identity in $\mathbb{Z}[a,a',D,C]$ .
Eventual vanishing forces the recurrence	Proved here	Theorem .
Zero is absorbing	Proved here	Theorem , under strict centring.
Nonnegative $E$	Proved here	Theorem , by descent.
Constantly negative $E$	Excluded here	Theorem , at any magnitude and scale.
Periodic negative magnitude	Excluded here	Theorem , in the regime $e_n<a_n$ and with positive drift $M>0$ .
Coprime-modulus barrier	Proved here	Theorem .
Bounded negative part	Excluded here; conditional	Theorem ; see its hypotheses.
Normalised vanishing alone	Gcd changes are sparse	Proposition ; arbitrarily late finite constant blocks, not eventual constancy.
Finite normalised negative mass	Excluded here; conditional	Theorem , Section ; normalised vanishing remains an input.
Factorial residue reduction	Proved here; superseded for its original purpose	Theorem , Appendix .
Normalised vanishing	Assumed here; supplied by prior art	Section ; derived in , see Section . The separate strict-centring hypothesis retained in the Lean-matching statement follows eventually by taking $K=1$ .
Unbounded, divergent-mass negative excursions	Necessary conditions proved here; orbit-level case open	Section : Proposition gives conditions any counterexample must satisfy, not a separate open problem; Problem is the surviving orbit-level obstruction.
Erdős–Straus criterion; Duverney	Proved elsewhere	Cited, not formalised; the Erdős–Straus hypothesis is implied by that of Theorem .
State system equals reciprocal tails	Not formalised	Section .

Taken together the exclusions constrain the shape of any counterexample. By Theorem a counterexample has $E_n\ne0$ for every large $n$ . By Theorem it cannot have $E$ eventually nonnegative. If its tail is all negative, Theorems and exclude, respectively, constant magnitude and periodic magnitude in the stated regime $e_n<a_n$ with positive drift; they are not a classification of a mixed-sign tail. Under normalised vanishing, Theorems and show that the negative part is neither bounded nor of finite normalised mass. What survives is stated in Section .

Structure

Section sets up the state system, and Section proves the defect identity, from which eventual vanishing of $E$ forces the Sylvester recurrence and a single vanishing error propagates. Section disposes of the case $E\ge0$ in three lines. The rest of the note is the case $E<0$ , in four widening steps: constant magnitude (Section ), periodic magnitude (Section ), bounded magnitude via a coprimality barrier (Sections and ), finite normalised negative mass (Section ), and what is left (Section ). These sections contain the new content; a reader who wants only the strongest statements should read Sections and , and then Section . Appendix is a guide to the formal sources, and Appendix records an exact residue reduction that an earlier finite search used. Linked phrases open the corresponding Lean declaration at the pinned source revision 64f33f3a134d.

Keywords. irrationality; Ahmes series; Sylvester’s sequence; unit fractions; Lean 4. MSC 2020. 11J72 (primary); 11B37, 11D68, 68V20 (secondary).

The centred integer state

The three maps defined next carry out the two steps announced at the end of Section . The first two clear denominators along the sequence, so that a rational reciprocal sum leaves a sequence of integers; the third subtracts from that integer the value it takes on Sylvester’s sequence, leaving one number whose vanishing is the whole question. All three are maps between integer tuples and carry no hypothesis of any kind.

For $a,D,C\in\mathbb{Z}$ define $\operatorname{den}(a,D)=aD, \quad \operatorname{tail}(a,D,C)=aC-D, \quad \operatorname{ctr}(a,D,C)=D-(a-1)C ,$ the , the , and the . Given a sequence $(a_n)$ of integers, whose terms we call the , we write $D_{n+1}=\operatorname{den}(a_n,D_n)$ for the , $C_{n+1}=\operatorname{tail}(a_n,D_n,C_n)$ for the , and $E_n=\operatorname{ctr}(a_n,D_n,C_n)$ for the , also called the . The word records what the third map does: it measures $D_n$ against $(a_n-1)C_n$ , and $D_n=(a_n-1)C_n$ holds at every index on Sylvester’s sequence (Example ), so $E$ is a deviation from that sequence rather than a size. At an index where $E_n<0$ we write $e_n=-E_n>0$ and call it the of the error there.

Proof. $C-\bigl(D-(a-1)C\bigr)=aC-D$ . ◻

Formalised as the . The state therefore moves by exactly the error at each step, which is what makes the sign of $E$ decisive: where $E$ is positive the state falls, where $E$ is negative it rises, and where $E$ vanishes it is stationary.

The intended reading, which is not formalised.

Let $T_n=\sum_{k\ge n}1/a_k$ and suppose $T_0\in\mathbb{Q}$ . Put $D_0$ equal to a common denominator and $D_n=D_0a_0\cdots a_{n-1}$ , and set $C_n=D_nT_n$ . Then $C_n\in\mathbb{Z}$ for every $n$ , and from $T_n=1/a_n+T_{n+1}$ one gets $C_{n+1}=a_nC_n-D_n$ , which is the tail update. On Sylvester’s sequence $T_n=1/(a_n-1)$ exactly, so $D_n=(a_n-1)C_n$ and $E_n=0$ : the centred state measures deviation from the Sylvester tail identity, and it vanishes identically on the Sylvester orbit.

None of this paragraph is formalised. The Lean module contains no series, no rationality hypothesis, and no growth hypothesis; it proves identities and implications about the integer system above, and about its natural-number realisation, for which the bridging identities are the , the , and the . A reader should treat the identification with reciprocal tails as motivation for the definitions and not as a checked step.

Formalised as the , the , and the . The system depends only on the ray through $(D,C)$ . This is used twice below: once to normalise the finite search of Appendix , and once, in Theorem , as the induction step that removes common scale.

The defect identity and its two consequences

Section connects the Sylvester recurrence to the error in one direction only: on Sylvester’s sequence the error vanishes. The converse is what the problem needs, and it comes from a single identity, which expresses the deviation of $a_{n+1}$ from the Sylvester successor, multiplied by the tail state $C_{n+1}$ , as a combination of the errors at $n$ and at $n+1$ , the first weighted by $a_n^{2}$ . Its two consequences are Theorem , in which an eventually vanishing error forces the recurrence provided the tail state is eventually nonzero, and Theorem , in which, under strict centring (the condition $|E_n|<C_n$ at every index), one vanishing error propagates to every later index.

Write $\operatorname{def}(a,a')=a'-\operatorname{syl}(a)$ for the deviation of the next term from the Sylvester successor, the .

Proof. A direct expansion: both sides equal $a'aC-a'D-a^{3}C+a^{2}D+a^{2}C-aD-aC+D$ . ◻

Formalised as the . It is a polynomial identity in four indeterminates, with no hypothesis of any kind, and it carries the whole argument twice over: once for rigidity, and once for absorption.

Proof. By Theorem the product $\operatorname{def}(a,a')\cdot\operatorname{tail}(a,D,C)$ is zero, and the second factor is nonzero by hypothesis. ◻

Formalised as the . The hypothesis $C_{n+1}\ne0$ is not removable: at $C_{n+1}=0$ the identity gives no information about $a'$ .

Formalised as the . The proof is routine: take the larger of the two thresholds and apply Theorem at each later index. Every later section is directed at the hypothesis of this theorem, that is, at forcing $E$ to vanish eventually.

The defect identity has a second consequence, which is what makes a single vanishing error worth having.

Proof. Putting $E_n=0$ in Theorem gives $\Delta_n C_{n+1}=-E_{n+1}$ , so $C_{n+1}$ divides $E_{n+1}$ . A multiple of $C_{n+1}$ of absolute value smaller than $C_{n+1}$ is zero, and $|E_{n+1}|<C_{n+1}$ by hypothesis. ◻

Formalised as the , with the companion : if zero is absorbing beyond some index and $E$ does not vanish eventually, then $E$ is nowhere zero beyond that index.

Absorption changes the shape of the problem. Without it, one would have to exclude an $E$ that dips to zero and recovers. With it, either $E$ hits zero once and is finished, or it is never zero at all. Sections and then restrict to the special all-negative case; this is not a without-loss reduction for a mixed-sign tail. The mixed-sign analysis in Sections and instead separates cofinally negative errors from an eventually positive tail.

Descent when the error is nonnegative

The hypothesis of the theorem below is the update law of Proposition read inside $\mathbb{N}$ : the error is nonnegative at every index, so the tail state never rises. This is the easy case, and it is settled in three lines.

Proof. A one-line descent. The relation forces $C_{n+1}\le C_n$ , so $C$ is a nonincreasing sequence of natural numbers and is eventually equal to its minimum; beyond that index $C_{n+1}=C_n$ , and the relation gives $E_n=0$ . ◻

Formalised as the , on the .

The hypothesis is exactly one-sidedness: $C$ and $E$ take values in $\mathbb{N}$ . If $E_n<0$ at infinitely many indices then $C$ rises there, nothing descends, and the argument is unavailable. That is the whole difficulty, and the rest of this note is directed at it.

Excluding a constant negative magnitude

Suppose the error is negative with a constant magnitude, $E_n=-m$ for a fixed $m>0$ and every $n$ . By Proposition the state then climbs by exactly $m$ each step, so $C_n=c+nm$ with $c=C_0$ , and the definition of the centred state becomes a $D_n+m=(a_n-1)\,(c+nm) . \tag{5.1}\label{eq:shape}$ Together with $D_{n+1}=a_nD_n$ this is a closed system in $(a,D)$ , and it has no solutions. The following instance shows how the failure happens; the theorem then shows that it cannot be avoided.

Proof when $c$ and $m$ are coprime. Assume first $\gcd(c,m)=1$ . Two facts about the multipliers do all the work, and the difficulty lies in the fact that they concern the same finite set of primes from opposite directions: the first makes every multiplier meet that set, the second lets each prime of the set meet at most one multiplier.

Suppose $\gcd(a_j,m)=1$ . Then $m$ is invertible modulo $a_j$ , so some $n$ has $c+nm\equiv0$ , that is $a_j\mid C_n$ ; and $a_j\mid D_n$ for every $n>j$ , since $D$ is multiplicative with $a_j$ among its factors. Choosing such an $n$ beyond $j$ and reading modulo $a_j$ gives $a_j\mid m$ , contradicting $\gcd(a_j,m)=1$ and $a_j\ge2$ .

Suppose $p\mid m$ and $p\mid a_j$ . For $n>j$ we have $p\mid D_n$ , so gives $(a_n-1)C_n\equiv0 \pmod p$ . Now $C_n=c+nm\equiv c$ , and $p\nmid c$ because $p\mid m$ and $\gcd(c,m)=1$ ; hence $p\mid a_n-1$ , so $p\nmid a_n$ . Thus $p$ cannot divide any later multiplier.

The two facts are incompatible. Each of the infinitely many multipliers needs a prime divisor of $m$ , and each prime divisor of $m$ serves at most one multiplier, while $m$ has only finitely many prime divisors. ◻

The case $\gcd(c,m)=1$ is the . The special case $m=c=1$ , worked through in Example , where $m$ has no prime divisors at all and the first fact is immediately contradictory, is recorded separately as the .

Removing the scale. For general $c$ , put $g=\gcd(c,m)$ . Equation shows $g\mid D_n$ for every $n$ , so dividing $D$ , $c$ and $m$ by $g$ leaves a system of the same shape with coprime data, which the previous case excludes. ◻

Formalised as the , and the eventual form, obtained by shifting the orbit to the first constant index, as the .

Theorem excludes a centred state that is eventually constant and negative, at every magnitude and every scale. It says nothing about a negative state whose magnitude changes, and the argument genuinely uses constancy: the finiteness of the set of prime divisors of $m$ is what the pigeonhole uses, and a varying magnitude presents a fresh set at each index.

Excluding a periodic negative magnitude

The next case allows the magnitude to vary, provided it repeats. Write $e_n=-E_n>0$ for the magnitude, as in Section , so that $C_{n+1}=C_n+e_n$ ; suppose $e$ has period $h$ , meaning $e_{n+h}=e_n$ for every $n$ , and that the state gains a fixed $M>0$ over one period, meaning $C_{n+h}=C_n+M$ for every $n$ .

At $h=1$ this says that the magnitude is constant and that $M$ is its value, which is the situation of Section ; Theorem already excludes it, and does so without the extra hypothesis $e_n<a_n$ imposed below. The new content is $h\ge2$ .

Section could run its pigeonhole on the prime divisors of the single number $m$ . Here the magnitude changes inside a period, and the number available to run it on is the drift $M$ . Three lemmas replace the two facts of Section . The first is that multipliers persist: every $a_j$ divides every strictly later denominator state, the . The second is a : a prime already dividing $D$ and also dividing the current multiplier is forced into the next tail state, the , and once present in both $D$ and $C$ it stays in every later $D$ , $C$ and magnitude, the . The third transports a lock backwards through the period: if a divisor of the drift $M$ occurs in two multipliers, it is a common divisor of $C_0$ and of every magnitude, the , using that both the period relation and the drift iterate over any number of periods, the and the .

Proof. Strong induction on the drift $M$ . The difficulty lies in the fact that a repeated prime divisor of $M$ need not contradict anything directly. It instead forces a common scale on the whole orbit, which can be divided out, and the induction runs on the drift that the division reduces.

Suppose first that no prime divisor of $M$ is a common divisor of $C_0$ and of every magnitude. Repeated-divisor transport then applies in the contrapositive: a prime divisor of $M$ occurring in two of the multipliers would be exactly such a common divisor, so each prime divisor of $M$ occurs in at most one multiplier. Against this, the argument of Section run phase by phase (along a fixed residue class modulo $h$ the magnitude is constant and $C$ advances by $M$ at each period, so the multipliers of that phase meet an arithmetic progression exactly as in Section ) makes every multiplier share a prime with $M$ . Since $M$ has only finitely many prime divisors and there are infinitely many multipliers, pigeonhole gives a contradiction.

Otherwise some prime $p$ divides $M$ , divides $C_0$ , and divides every magnitude. Then $p\mid C_n$ for every $n$ , since $C_{n+1}=C_n+e_n$ and both summands on the right are divisible by $p$ , and the shape equation $D_n+e_n=(a_n-1)C_n$ then gives $p\mid D_n$ for every $n$ . Divide $D$ , $C$ and $e$ by $p$ . The multipliers are untouched, so $a_n\ge2$ and $e_n<a_n$ persist and the magnitudes stay positive; the three recurrences are homogeneous in $(D,C,e)$ and so survive; the period is still $h$ ; and the drift becomes $M/p<M$ . The inductive hypothesis applies. ◻

The first of the two cases above is the , the induction is the , and the eventual form is the .

The bound $e_n<a_n$ is a genuine restriction and not a normalisation. It is the range in which a multiplier cannot divide its own phase magnitude, which is what the lock argument needs. It holds in the intended reading, where $e_n$ is a centred representative and $a_n$ grows quadratically, but it is assumed here and not derived. The drift hypothesis $M>0$ is also used: a periodic magnitude with zero drift would be identically zero, which is the case already settled by Section .

Bounded rise cannot remain coprime to fresh moduli

Periodicity is still a strong assumption. Removing it needs a different kind of obstruction, and the one used here is a counting argument about where an integer sequence with bounded upward steps must land.

Proof. Standard Chinese remaindering: solve $t\equiv-i \pmod{m_i}$ simultaneously, then add multiples of $\prod_i m_i$ to pass the bound. ◻

Formalised as the .

Proof. Take $B$ of the moduli, from indices beyond any chosen point, and use Lemma to find $t$ far out with the $i$ th of them dividing $t+i$ . The interval $[t,t+B)$ has length $B$ , and $u$ climbs by at most $B$ per step while tending to infinity, so some $u_s$ lands in it. Then $u_s=t+i$ for some $i<B$ , and the $i$ th modulus divides $u_s$ . Since that modulus is at least $2$ , this contradicts $\gcd(m_i,u_s)=1$ . ◻

Formalised as the . The key point is that the two hypotheses pull against each other exactly: divergence forces $u$ to travel arbitrarily far, and bounded rise forbids it from stepping over a window of width $B$ . Uniformity of the bound is what the proof uses, and it is the hypothesis that cannot be relaxed by this argument: a rise bounded only along a subsequence leaves the intervening steps free to jump the window. We have not looked for a sequence of unbounded rise remaining coprime to every fresh modulus. The statement is elementary and we are not aware of a prior published form of it, but we would not be surprised if one exists.

The moduli are indexed by the same set as the sequence, and the $i$ th of them is asked to divide no value $u_t$ with $t>i$ ; nothing at all is asked of it at or before its own index. That asymmetry is what makes the hypothesis available in the application below, where $m_i$ is the $i$ th multiplier and only the later numerators are known to be coprime to it.

The barrier applies to the problem because a exact tail already carries pairwise coprime moduli. Call $(u,v)$ a reduced exact tail with multipliers $a$ when $\gcd(u_n,v_n)=1$ , $u_{n+1}+v_n=a_nu_n,\qquad v_{n+1}=a_nv_n .$ Here $u$ is the numerator and $v$ the denominator: the two recurrences are those of Section , with $u$ in the role of the tail state $C$ and $v$ in that of the denominator state $D$ , and with coprimality imposed at every index.

These are the , the , and the . Feeding them to Theorem gives the form used later: there is no reduced exact tail whose numerator tends to infinity with a uniformly bounded upward increment, the , together with its eventual form, the .

An arbitrary orbit of Section need not be reduced, so one more step is needed before the barrier can be applied to it: the common factor must stop changing. We call a set of indices when it is infinite, and say that a property holds when the set of indices at which it holds is cofinal. The step below is the only one connecting the orbit of Section to the reduced tails of Proposition , and it is where the cofinal boundedness in the proof of Theorem is used.

Proof. The tail gcd $\gcd(C_n,D_n)$ divides its successor, the , so the tail gcds form a positive divisibility chain. At an index where the centred state is negative the tail gcd is exactly $\gcd(C_n,e_n)$ , the , and is therefore at most the magnitude there; so the chain is bounded along the cofinal set of negative indices. A positive divisibility chain whose values are bounded along a cofinal set is eventually constant, the . Hence cofinally bounded negative magnitudes make the tail gcd stabilise, the , and beyond that point dividing by the stable gcd leaves the numerator and denominator coprime, that is, a reduced exact tail. ◻

The stabilisation of the tail gcd is the checked statement cited at the end of the proof; the last clause, that the divided orbit is a reduced exact tail, is exposition and carries no separate label. The hypothesis is boundedness and not boundedness at every index. That is what the situation gives: the tail gcd is controlled only at the negative indices, and cofinally many of them is all the divisibility chain needs.

Normalised vanishing by itself gives a different, strictly weaker conclusion. For an exact natural orbit with $C_n>0$ , put $G_n=\gcd(C_n,D_n),\qquad \Gamma(N)=\#\{0\le j<N:G_j<G_{j+1}\}.$

The first assertion is the ; the second is the . The proof first converts normalised vanishing into subexponential growth of $C_n$ , then charges every strict divisibility increase of $G_n$ against a finite power-of-two budget. Sparse strict changes force long finite gaps between them.

The quantifiers matter. Proposition uses cofinally bounded negative magnitudes and yields eventual constancy. Proposition uses only normalised vanishing and yields arbitrarily late constant blocks of each prescribed finite length. It does not yield one infinite constant tail, and it does not exclude cofinally unbounded negative excursions.

Excluding a bounded negative part

Assembling the previous section gives Theorem , the endpoint of the barrier argument. Theorem in the next section is a second endpoint under a different finiteness hypothesis, and neither theorem contains the other. Theorem assumes no orbit structure, only the state recurrence with $C_n>0$ , so it is not a special case of Theorem ; conversely hypothesis (5) below does not imply finite , by which we mean convergence of $\sum_n(-E_n)_+/C_n$ , where $x_+=\max(x,0)$ , since a constant negative part $-b$ gives $C_n\sim bn$ and hence a divergent sum. The hypotheses of Theorem are listed in full, because two of them are analytic inputs that are assumed here rather than derived from the growth condition of Problem .

Informally, hypotheses (5) and (6) below pull against each other. By Proposition , hypothesis (5) caps the rise of the tail state at $B$ per step, while hypothesis (6), once the error is nowhere zero, forces the tail state to diverge. Proposition makes the orbit reduced, and Theorem then converts the tension into a contradiction: an integer sequence tending to infinity with upward steps of size at most $B$ cannot remain coprime to the pairwise coprime moduli a reduced tail carries. The complementary case, in which the error is eventually positive, is the descent of Theorem .

Proof. Suppose not. We first remove every late zero: by Theorem and its contrapositive form, $E$ is nowhere zero beyond the centring threshold. Two cases remain. If $E$ is negative cofinally, then (5) bounds those magnitudes, so Proposition makes the tail gcd stabilise and the orbit may be taken reduced past that point. Hypothesis (5) with Proposition gives $C_{n+1}\le C_n+B$ , a bounded rise; hypothesis (6) with $E$ nowhere zero gives $C_n\to\infty$ . A reduced exact tail with a divergent numerator and bounded rise is excluded by Theorem . It remains to treat the case that $E$ is eventually positive, and there the descent of Theorem applies and forces $E$ to vanish, contradicting nowhere-vanishing. ◻

Formalised as the , with the eventual form, in which the centring and the bound need only hold from some index, as the . The two auxiliary results it uses are the and the , the latter over the .

Proof. Theorem then Theorem . ◻

Hypotheses (1)–(3) are the state system, and (6) is the division-free form of $|E_n|/C_n\to0$ . Hypothesis (4) is logically redundant: hypothesis (6) with $K=1$ gives $|E_n|<C_n$ eventually. It is retained because the displayed statement tracks the linked Lean declaration; shifting to the resulting threshold gives the same conclusion without an independent centring input. The formal source does not derive normalised vanishing from $a_{n+1}/a_n^{2}\to1$ , so Theorem is, by itself, a conditional theorem about the state system. Combined with Koizumi’s bridge below, however, Corollary settles the bounded-negative canonical case of Problem . What is unconditional in this note is the all-negative constant and periodic exclusions, Theorems and , and the barrier itself, Theorem .

The conditionality can nevertheless be located precisely, because the missing inputs are supplied elsewhere. With the results of , Theorem becomes a conditional theorem about Problem itself rather than about the state system alone. Let $(a_n)$ satisfy the hypotheses of Problem . After deleting a finite prefix, Corollary 10 of [6] makes the sequence the pseudo-greedy expansion of its own reciprocal sum, and Lemma 15 there supplies the integers $c_n,d_n,e_n$ of Section . Hypothesis (1) then holds: $c_n$ is a positive integer by Lemma 15(1), and $a_n>1$ after a further finite shift, because summability of $\sum1/a_n$ forces $a_n\to\infty$ . Hypothesis (2) is the pair of recurrences $c_{n+1}=a_nc_n-d_n$ and $d_{n+1}=a_nd_n$ of Lemma 15(2), and hypothesis (3) is that lemma’s $a_n=(d_n-e_n)/c_n+1$ read as $e_n=d_n-(a_n-1)c_n$ , which is the map $\operatorname{ctr}$ . Hypothesis (4) holds at every index, not merely eventually, from the centring range $-c_n/2\le e_n<c_n/2$ of the same lemma. Hypothesis (6) is the vanishing of the gap sequence in Corollary 10, since $\varepsilon_n=e_n/c_n$ . The sole hypothesis not supplied is (5), the eventual bound on the negative part; nothing in [6] yields it and nothing here does either, so Problem #243 stays open.

Excluding finite normalised negative mass

Theorem uses a uniform bound on the negative part. A different finiteness hypothesis, on the total normalised negative mass, removes a further family of orbits, and the argument is multiplicative rather than arithmetic: it compares $C$ with a convergent product instead of with a system of congruences.

Proof. Put $\delta_n=(-E_n)_+/C_n$ . The update gives $C_{n+1}\le C_n(1+\delta_n)$ , so $C_N\le C_0\prod_{n<N}(1+\delta_n).$ The product is bounded because $\sum\delta_n$ converges. Choose an integer $M$ above that bound and apply normalised vanishing with $K=M$ . Then $M|E_n|<C_n<M$ for all sufficiently large $n$ , forcing the integer $E_n$ to be zero. The final recurrence is Theorem , whose hypothesis $C_{n+1}\ne0$ holds because $C_n>0$ throughout. ◻

The product argument is the ; its specialisation to negative mass is the , and the statement giving the recurrence directly is the . This is a checked implication about the state system, not a derivation of normalised vanishing from Problem #243. Normalised vanishing is still an input: it is what converts the bound on $C$ into a bound on $|E_n|$ , and nothing here derives it from the growth condition of Problem .

The transfer of the previous section applies here as well. On the canonical orbit of Corollary 10 of [6] the recurrence $C_{n+1}=C_n-E_n$ holds with $C_n>0$ by Lemma 15 [6], and normalised vanishing is the vanishing of the gap sequence, so Theorem is a conditional theorem about Problem whose sole remaining hypothesis is summability of $\sum_n(-E_n)_+/C_n$ . That hypothesis is not supplied there, and is the content of Problem below.

Complements and further questions

Problem #243 is open. The negative case has narrowed, and it is worth being precise about what is left.

Each exclusion holds only in its stated regime. Theorems and exclude the constant and the stated periodic magnitudes on an all-negative tail, and do not exclude those patterns merely along the negative indices of a mixed-sign tail; Theorems and exclude a bounded negative part and finite normalised negative mass under normalised vanishing. Together with absorption and descent they fix the profile of any counterexample.

Proof. Koizumi’s canonical-tail transfer gives strict centring and normalised vanishing after a finite shift; the strict-centring hypothesis of Theorem also follows from normalised vanishing with $K=1$ . Absorption then makes $E_n\ne0$ eventually, since eventual zero would give the Sylvester recurrence. Descent excludes an eventually nonnegative state. Theorem excludes a bounded negative part, and Theorem excludes finite normalised negative mass. These statements are unchanged by deleting a finite prefix. ◻

Put $\delta_n:=\frac{(-E_n)_+}{C_n}.$ Every argument in Sections – uses a finiteness hypothesis: a fixed set of prime divisors, a fixed period, or a fixed bound on the negative part. Theorem uses $\sum_n\delta_n<\infty$ . Proposition records that a counterexample has none of them; it is a frontier statement, not an additional problem equivalent to the original one. Stated at the level of state orbits, the surviving obstruction is the following.

Global height and old-factor overlap

The main arithmetic gap is global. Define the cumulative digit LCM and its overlap quotient by $L_0=D_0,\qquad L_{n+1}=\operatorname{lcm}(L_n,a_n),\qquad M_n=\frac{D_n}{L_n}.$ Since $D_n=D_0\prod_{j<n}a_j$ , the quotient is integral and $M_nL_n=D_n$ . It records the multiplicity lost when the full product scale is compressed to an LCM.

The two displayed formulations are equivalent up to changing the positive constant; the second is not a weaker target. A positive answer is not yet, by itself, a proof of Problem #243: the missing bridge is a comparison of $M_n$ with a subexponential state or exact cancellation-payment scale. No assertion such as $M_n\mid C_n$ or $M_n\le C_n$ is used here. Proving such a bridge together with Problem would collide with the subexponential tail-height budget forced by normalised vanishing.

There is also a more local-looking question whose content is nevertheless the entire prefix. Put $A_n=\prod_{j<n}a_j$ , so $D_n=D_0A_n$ . From $D_0A_n=(a_n-1)C_n+E_n$ one immediately obtains $\gcd(A_n,a_n-1)\mid E_n.$ The checked and normalised vanishing make $|E_n|$ subexponential in $n$ .

A positive answer contradicts the displayed divisibility and the subexponential error budget. Arbitrarily long locally admissible blocks do not answer this question: the gcd uses the complete prefix.

The direct analytic question

An affirmative answer closes Problem #243 by Theorem . Since $\delta_n\to0$ , convergence is equivalently expressible as boundedness of the partial products $\prod_{n<N}(1+\delta_n)$ ; that is an explanatory reformulation, not a second success criterion. A negative answer must be a sequence satisfying the full growth and rationality hypotheses, not merely a locally admissible state orbit.

A barrier extension

The displayed rate is a proposed threshold, not a proved sharp boundary. Either an extension of the CRT barrier or a counterexample with this rise rate would be informative independently of Problem #243.

Formalisation targets

Erdős–Straus.

Formalise Theorem 3 of [1], with its prefix-LCM quotient and correctly indexed growth factor, under the published analytic hypotheses.

Duverney.

Formalise Corollary 3.2 of [2], including its signed numerators and absolute convergence hypothesis, and then recover the all-positive specialisation used here. These are useful verification projects, but neither is an additional open mathematical problem.

Statements and declarations

Artefact and data availability.

The pinned formal-source revision contains the Lean sources, the fixed toolchain, and the library manifest used in the verification. This manuscript provides navigation rather than proof authority.

Declaration of generative AI use.

Every word of this manuscript was generated by agents based on large language models operating within Will Cook’s private research system for artificial intelligence. The formal proofs and repository software were likewise drafted and revised by the agents through that system under Cook’s direction. Cook set the objectives and acceptance criteria, selected and reviewed the public claims, and approved the published version. Cook assumes responsibility for the accuracy, interpretation, and presentation of the work. Generative systems are production tools, not authors, and supply no independent authority. Lean checks each proof term against the fixed library version, and the sources linked here contain no proof placeholders and no project-defined axioms; Lean does not authorise the exposition, the citation choices, or the interpretation, for which the author remains responsible.

Funding and competing interests.

This work received no external funding. The author declares no competing interests.

Acknowledgements.

The problem numbering and status follow the Erdős Problems catalogue maintained by Thomas Bloom [7].

Guide to the formal sources

Each linked phrase opens its Lean declaration at the pinned source revision 64f33f3a134d. The state system, the exclusions, the barrier, and the bounded-negative-part theorem are in ReciprocalTailRigidity.lean; the finite-negative-mass theorem is in SparseResetRecovery.lean; and the residue reduction of Appendix is in FiniteHorizonResidue.lean. Three distinctions are worth carrying into the source. The identification of any of these modules with reciprocal tails is the exposition of Section and is not a checked statement. The periodic exclusion assumes the regime $e_n<a_n$ . And the final Lean declaration lists strict centring and normalised vanishing as hypotheses; the former follows eventually from the latter with $K=1$ , while the formal source derives neither from the original analytic problem. For the external bridge supplying them, see Sections and .

A factorial residue reduction for forced orbits

In the case $m=c=1$ of Section , where the shape equation reads $D_n+1=(a_n-1)(n+1)$ , each multiplier is determined by its predecessor; we call such an orbit . At index $n$ the numerator of the next multiplier is $\operatorname{num}(n,a)=(n+1)a^{2}-(n+2)a+(n+3),$ the , and the divisor is $n+2$ . The orbit survives a step when that division is exact, giving a survival predicate, the . Example is the forced orbit from $a=3$ read this way: $\operatorname{num}(0,3)=6$ is divisible by $2$ and gives $a_1=3$ , while $\operatorname{num}(1,3)=13$ is not divisible by $3$ , so the orbit stops there. Deciding survival by iteration is expensive because the orbit grows doubly exponentially, and it is unnecessary: survival over a finite horizon depends on the initial value only through a factorial residue.

Proof. Let $M(0,i)=1$ and $M(h+1,i)=(i+2)M(h,i+1)$ , an ascending factorial with $M(h,0)=(h+1)!$ . The numerator is a polynomial with integer coefficients, so congruences transfer; reducing the modulus gives divisibility by $i+2$ for one exactly when for the other, and cancelling that common factor from both values and modulus leaves the inductive hypothesis at $M(h,i+1)$ . ◻

Formalised as the , over the , the , and the ; the modulus identifications are the and the .

At $h=1$ the modulus is $2!=2$ , and surviving one update means $2\mid a^{2}-2a+3$ , which holds exactly for odd $a$ : for instance $\operatorname{num}(0,3)=6$ but $\operatorname{num}(0,4)=11$ . So one step of survival is decided by the parity of $a$ alone, which is Theorem at its smallest nontrivial horizon.

The search this supported is superseded. Running it over initial states below $5000$ produced forced prefixes of length $17$ and no longer, which was evidence and not a proof; Theorem now excludes the constant-negative case outright, for every seed and at every scale. The reduction is retained because it is exact, and because the shrinking-modulus technique transfers to any forced orbit whose step is a polynomial division.

References

P. Erdős and E. G. Straus, , J. Indian Math. Soc. (N.S.) 27 (1964), 129–133. MR 175848.
D. Duverney, , J. Math. Sci. Univ. Tokyo 8 (2001), 275–316. MR 1837165.
P. Erdős and R. L. Graham, , Monogr. Enseign. Math. 28, Geneva, 1980, p. 64.
P. Erdős, , in A. Baker (ed.), , Cambridge UP, 1988, pp. 102–109, doi:10.1017/CBO9780511897184.009.
V. Kovač and T. Tao, , Acta Math. Hungar. 175 (2025), 572–608; preprint arXiv:2406.17593v4.
J. Koizumi, , Integers 26 (2026), Paper No. A28, 17 pp., doi:10.5281/zenodo.18714404; preprint arXiv:2504.05933v1.
T. F. Bloom, Erdős Problem #243, erdosproblems.com/243, accessed 28 July 2026 (page displays “last edited 21 January 2026”). The current record labels the problem open, cites [ErGr80, p. 64] and [Er88c, p. 105], and explicitly describes its status as the website owner’s present assessment rather than a literature-completeness guarantee.
The Formal Conjectures Authors, FormalConjectures.ErdosProblems.243, Lean source at commit f776d2f, 2025, accessed 28 July 2026. Its $\mathbb{Q}$ -valued Summable hypothesis encodes rationality, its indexing is zero-based, and its proof ends in sorry.