Erdős problem #243

Reciprocal-tail rigidity near the Sylvester recurrence

Under a rapid-growth hypothesis on an integer sequence, does rationality of its reciprocal sum force the sequence to satisfy the Sylvester recurrence eventually?

Open Problem on GitHub

Read the short paper PDFOpen the PDF, 21 pages Map of results

The problem

The question

Take a strictly increasing sequence of positive integers $a_{1}, a_{2}, \dots$ with $a_{n + 1} / a_{n}^{2} \to 1$ : each term is approximately the square of its predecessor, in relative error. If the reciprocal sum is rational, must $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ hold for every sufficiently large $n$ ? Finitely many early exceptions are allowed.

An example

The rule says “square, subtract the original term, add 1”. Starting at 2 gives $2, 3, 7, 43, 1807, \dots$ . Its reciprocal partial sums are $1 / 2, 5 / 6, 41 / 42, \dots$ . The shortfalls from 1 are $1 / 2, 1 / 6, 1 / 42, \dots$ . The shortfall after $1 / a_{n}$ is $1 / (a_{n + 1} - 1)$ . These shortfalls tend to zero, so the infinite sum equals 1. The sequence also satisfies the required approximate squaring.

Let $1 \leq a_{1} < a_{2} < \dots$ be a sequence of integers such that $lim_{n \to \infty} \frac{a_{n}}{a_{n - 1}^{2}} = 1$ and $\sum \frac{1}{a_{n}} \in Q$ . Then, for all sufficiently large $n \geq 1$ , $a_{n} = a_{n - 1}^{2} - a_{n - 1} + 1$ .

Erdős problem #243, as erdosproblems.com/243 states it

The setup in detail

The limit concerns a quotient, not an absolute difference. For instance, the exact squares $2, 4, 16, 256, \dots$ have $a_{n + 1} / a_{n}^{2} = 1$ at every index, but do not obey the proposed rule. The rationality assumption is therefore essential to the question. The growth condition ensures convergence: eventually $a_{n + 1} \geq a_{n}^{2} / 2 \geq 2 a_{n}$ , so the reciprocals are bounded by a convergent geometric series.

Equivalently, the conjecture says that any such sequence violating the recurrence infinitely often has an irrational reciprocal sum. No general proof or counterexample is known. The cubic-rate theorem in the result panel treats a specified subclass, rather than proving this equivalence's conclusion for all sequences.

The example in detail

The recurrence gives $a_{n + 1} - 1 = a_{n} (a_{n} - 1)$ , and therefore

\frac{1}{a_{n} - 1} - \frac{1}{a_{n}} = \frac{1}{a_{n} (a_{n} - 1)} = \frac{1}{a_{n + 1} - 1} .

For example, $1 / 6 - 1 / 7 = 1 / 42$ and $1 / 42 - 1 / 43 = 1 / 1806$ . Repeated subtraction leaves a shortfall $1 / (a_{n + 1} - 1)$ , which tends to zero. More generally, whenever the rule holds from index $N$ onwards,

\sum_{n \geq N} 1 / a_{n} = 1 / (a_{N} - 1) .

The finite prefix is rational too, so every eventual Sylvester sequence has rational reciprocal sum. The name Sylvester refers to this recurrence.

The rule has the required asymptotic growth because

a_{n + 1} / a_{n}^{2} = 1 - 1 / a_{n} + 1 / a_{n}^{2} ⟶ 1.

For the illustrated sequence, the products of earlier terms are $1, 2, 6, 42, 1806, \dots$ , while the tails are $1, 1 / 2, 1 / 6, 1 / 42, 1 / 1806, \dots$ . Their products are all 1. Within each bar the hatched portion is the product times the current reciprocal, and the red portion is the product times all later reciprocals. The arrows multiply the red portion by the current term, incorporating that term into the product for the next row.

The crux

Each bar is the remaining reciprocal sum, multiplied by the product of earlier terms. The first three bars have lengths $1 \times 1 = 1, 2 \times (1 / 2) = 1, 6 \times (1 / 6) = 1$ . Blue hatching marks the scaled current reciprocal; red is the scaled sum of later reciprocals. Multiplying that red piece by the current term produces the next unit bar. The general question asks whether a rational sum forces these scaled tails to stay constant from some index onwards. Our result excludes rationality at a more restrictive growth rate; the general question remains open.

Assume the total is $p / q$ with positive integers $p, q$ . Write the remaining sum and its clearing denominator as

x_{n} = \sum_{k \geq n} 1 / a_{k}, D_{n} = q \prod_{j < n} a_{j}, C_{n} = D_{n} x_{n} .

The empty product at $n = 1$ is 1. Subtracting the finite prefix from $p / q$ shows that $C_{n}$ is a positive integer: $D_{n}$ is divisible by every denominator in that prefix. Removing the current reciprocal gives the exact updates

C_{n + 1} = a_{n} C_{n} - D_{n}, D_{n + 1} = a_{n} D_{n} .

These are Koizumi's integer tail coordinates. Their change is

C_{n + 1} - C_{n} = D_{n} ((a_{n} - 1) x_{n} - 1) .

Thus $C_{n}$ is unchanged precisely when the tail is $1 / (a_{n} - 1)$ . If $C_{n} = C_{n + 1} = C_{n + 2} = C$ , the first update gives $D_{n} = (a_{n} - 1) C$ ; applying it once more gives $a_{n + 1} - 1 = a_{n} (a_{n} - 1)$ . Eventual constancy is therefore equivalent to the eventual recurrence in the question.

Exact squaring shows how these coordinates can prove irrationality. For $2, 4, 16, 256, \dots$ , each tail satisfies

x_{n} = 1 / a_{n} + 1 / a_{n}^{2} + 1 / a_{n}^{4} + \dots < 1 / a_{n} + 1 / a_{n}^{2} + 1 / a_{n}^{3} + \dots = 1 / (a_{n} - 1) .

If the sum were rational, its positive integer $C_{n}$ would strictly decrease at every step, which is impossible.

The short paper proves the eventual rule when upward steps of these integers are bounded by a fixed constant. It also proves irrationality under the separate condition

a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3}) .

Here the error after subtracting $1 + 3 / n$ , multiplied by $n^{3}$ , must tend to zero. This forces eventual cubic tail numerators; the result diagram shows the final contradiction. A possible counterexample to the full problem must evade both conclusions. Its tail numerators would have unbounded upward steps, with a divergent sum of their relative increases.

Our theorem concerns strictly increasing positive integers with $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ , where the error after subtracting $1 + 3 / n$ , multiplied by $n^{3}$ , tends to zero. Example: start at 8 and round $n a_{n}^{2} / (n + 3)$ up, giving 8, 16, 103, 5305, … . Suppose the reciprocal sum were $p / q$ . The arrows remove successive reciprocals from that sum. The tail after the first $n - 1$ terms has denominator $D_{n} = q a_{1} \dots a_{n - 1}$ and integer numerator $C_{n}$ . Removing $1 / a$ sends $C / D$ to $(a C - D) / (a D)$ . The rate forces the numerators to be cubic: their fourth differences are integers tending to zero, hence eventually zero. The triangle illustrates differences by repeatedly subtracting adjacent entries. A further argument leaves just two possible numerator polynomials, $2 n (n + 1) (n + 2) \pm 1$ , after common factors are removed. Taking remainders on division by 7 gives the four-term blocks 1, 6, 0, 2 and 4, 5, 0, 1. The coefficient reduction is proved in the paper, not by these sample values. Now all calculations use remainders modulo 7: zero means divisible by 7. The ringed $d$ is the denominator just before that zero. The two adjacent updates force $d^{2} = 2$ : their neighbouring numerators give $- 6 \times 2 \equiv - 5 \times 1 \equiv 2 (\mod 7)$ . The lower diagram squares every possible remainder. The outputs are 0, 1, 4, 2, 2, 4, 1. Only 3 and 4 square to 2, so $d$ must be one of these. The preceding update also requires $d + 2$ to be a square. But $3 + 2 = 5$ and $4 + 2 = 6$ , neither in the square table. Both possible polynomials are impossible. Thus the specified rate forces an irrational sum. The full approximate-squaring question remains open.

The hypothesis is $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ : after subtracting $1 + 3 / n$ , the error times $n^{3}$ must tend to zero. This is much stronger than the original limit $a_{n + 1} / a_{n}^{2} \to 1$ . The example starts at $a_{1} = 8$ and uses $a_{n + 1} = ⌈ n a_{n}^{2} / (n + 3) ⌉$ . Its rounding error gives $0 \leq 1 + 3 / n - a_{n}^{2} / a_{n + 1} < 16 / a_{n}^{2} = o (n^{- 3})$ , which verifies the infinite hypothesis; the four sample terms do not.

If the sum were $p / q$ , write its tail as $C_{n} / D_{n}$ , with $D_{n} = q a_{1} \dots a_{n - 1}$ . Subtracting the finite prefix makes $C_{n}$ a positive integer. Removing a reciprocal uses the identity $C / D - 1 / a = (a C - D) / (a D)$ , so $C_{n + 1} = a_{n} C_{n} - D_{n}$ and $D_{n + 1} = a_{n} D_{n}$ . The growth rate gives $C_{n} = A n (n + 1) (n + 2) + o (n)$ . Controlling the first difference of the error then makes the integer fourth differences tend to zero. They eventually vanish, giving $C_{n} = A n (n + 1) (n + 2) + B$ (short paper §3.1).

The common divisor of numerator and denominator eventually stabilizes. Dividing it out preserves the updates and leaves $u_{n} = (m / 6) n (n + 1) (n + 2) + c$ , where $m$ is a positive integer and $c = \pm 1$ . A zero numerator modulo a prime forces the negative product of its neighbours to be a square modulo that prime. Applying this at all roots of the cubic, Chebotarev’s theorem and trace identities in a cubic number field force $m = 12$ (§§3.2–3.4). This substantial reduction is outside the diagram; its output is the pair of polynomials in stage 3.

For the final calculation (§3.5), write either block as $(A, L, 0, R)$ , with denominator residues $d_{0}, d, w$ under its first three entries. Every equality here is modulo 7. The update out of zero gives $w = - R$ ; into zero, with multiplier $b$ , it gives $d = b L$ and $w = b d$ . Hence $d^{2} = L w = - L R = 2$ . The first update gives $d_{0}^{2} + L d_{0} = A d$ . Completing the square yields $d + 2 = (d_{0} + 3)^{2}$ for the first block and $d + 2 = 2 (d_{0} - 1)^{2}$ for the second. Since $2 \equiv 3^{2} (\mod 7)$ , both require a square. The square table rules this out for $d = 3, 4$ . This excludes rationality under the stated rate, while Erdős–Graham’s unrestricted question remains open.

Results and open questions

#243. Under the exact cubic rate $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ , every strictly increasing positive integer sequence has an irrational reciprocal sum. Lean checks the zero-indexed theorem through a square-specialisation argument using Mathlib’s Dedekind-zeta simple pole; the short paper transfers it to one-based indexing by an ordinary finite-prefix argument. Its printed proof uses classical Chebotarev instead. This rate does not cover the unrestricted Sylvester-tail question.

More generally, the nonintegral regular-rate theorem checks irrationality when $λ > 1$ is nonintegral and $a_{n}^{2} / a_{n + 1} = 1 + λ / n + o (n^{-} λ)$ . Its Lean statement derives convergence for a positive, strictly increasing sequence indexed from zero. The long paper gives the ordinary finite-prefix transfer to one-based indexing. The integer-extraction lemma rules out nonintegral coefficients; the separate cubic argument rules out coefficient three. No rational examples are asserted for the remaining integer coefficients.

The rounded sequence $a_{1} = 8$ , $a_{n + 1} = ⌈ n a_{n}^{2} / (n + 3) ⌉$ has precisely this rate and product-ratio increments of order $n^{2}$ . Thus the separate bounded-increment recurrence criterion below gives no conclusion for it, while the cubic-rate theorem proves its reciprocal sum irrational. Duverney’s Corollary 3.2 supplies an earlier signed recurrence criterion under its printed one-sided growth-defect condition. In the all-positive, absolutely summable specialisation, the product-ratio increments tend to zero. For the rounded example, $a_{n + 1} / a_{n}^{2} - 1 \sim - 3 / n$ , so its signed defect series diverges and that absolutely summable specialisation does not apply. The exact $o (n^{- 3})$ remainder matters to the polynomial-exclusion proof. These comparisons locate the contribution without deciding its novelty or priority; the short paper’s argument and example give the proof and source locators.

The short paper also proves an ordinary original-sequence corollary. Let $a_{1} < a_{2} < \dots$ be positive integers, $a_{n + 1} / a_{n}^{2} \to 1$ , $\sum 1 / a_{n}$ rational, and $P_{n} = \prod_{j < n} a_{j}$ . If $lim sup (P_{n} / a_{n}) (a_{n}^{2} / a_{n + 1} - 1) < + \infty$ , then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ eventually. The needed limsup bound, or the paper’s alternative weighted record budget, is not proved for the unrestricted problem. Take a positive denominator $q$ of the full reciprocal sum and clear the nth tail by qP_n. The resulting integer error is minus $q$ times the scaled defect, up to a term tending to zero.

This cancellation turns the upper bound in the original sequence into the lower bound on the integer error used below. The proof passes through a signed bounded-negative theorem. Lean checks that theorem and the canonical tail transfer described below. Let a,C,D : ℕ → ℕ and E : ℕ → ℤ. Assume $a (n) > 1$ , $C (n) > 0$ , the exact recurrences $C (n + 1) + D (n) = a (n) C (n)$ and $D (n + 1) = a (n) D (n)$ , and that $E (n)$ is the exact centered state with $| E (n) | < C (n)$ . If one constant $B$ satisfies $E (n) \geq - B$ for every $n$ , and for every $K$ one eventually has $K | E (n) | < C (n)$ , then $E (n) = 0$ eventually (boundedNegativePart_eventually_zero).

The checked centered-zero theorem then gives the Sylvester recurrence once the exact product-cleared orbit has an eventually nonzero next-tail state. Lean carries that chain to the original denominators in boundedNegativePart_sylvesterNext_eventually, and checks the LCM-weighted bounded-defect corollary from the rational reciprocal sum in original_coordinate_lcm_bounded_defect (ErdosProblems/Erdos243/PaperCompleteR7/LcmDefect.lean:49); the paper derives the displayed $P_{n}$ form from that corollary by $A_{n} | P_{n}$ . For the state-system endpoint, no uniform lower bound on the centered error is proved.

Unbounded negative excursions and the full Erdős endpoint remain open. The signed recovery develops Koizumi’s canonical-tail framework under an additional bounded-negative premise. Read the short paper, long record, or selected formal checks.

The long record also proves an exact maximal-gap theorem for a separate static sieve. Let $m_{0} < m_{1} < \dots$ be pairwise coprime integers at least $2$ , with $ℓ (m_{j}) = j + O (1)$ for $ℓ (x) = \log_{2} \log_{2} max (4, x)$ . If $σ = \prod_{j} (1 - 1 / m_{j}) > 0$ and $u_{n}$ lists the positive integers divisible by none of the $m_{j}$ , then $lim sup (u_{n + 1} - u_{n}) / ℓ (u_{n}) = 1 / σ$ . Lean checks the general theorem maximal_gap_limsup_eq_inv_sigma with the convergence to $σ$ stated explicitly. The paper’s finite-product calculation gives $σ = 1 / 2$ and thus coefficient $2$ for the Fermat moduli $m_{j} = 2^{2^{j}} + 1$ . This concerns avoidance of whole moduli, not coprimality to composite moduli or construction of a reciprocal-tail orbit; the unrestricted #243 question remains open.

Read the public result guide

Short paper, 21 pages

Reciprocal Sums and the Sylvester Recurrence

PDFOpen the PDF, 21 pages Open as its own page Current source

In this paper

Introduction

The Sylvester recurrence $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ gives a rational reciprocal sum by telescoping:

\frac{1}{a_{n} - 1} = \frac{1}{a_{n}} + \frac{1}{a_{n + 1} - 1} .

For an increasing sequence of positive integers that eventually satisfies this recurrence, the tail sum at every sufficiently large index is $1 / (a_{n} - 1)$ . Erdős and Graham asked whether every rational reciprocal sum with $a_{n + 1} \sim a_{n}^{2}$ arises in this way.

Problem 1.1 (Erdős Problem 243). Let $1 \leq a_{1} < a_{2} < \dots$ be a sequence of integers with

lim_{n \to \infty} \frac{a_{n}}{a_{n - 1}^{2}} = 1 and \sum \frac{1}{a_{n}} \in Q .

Then $a_{n} = a_{n - 1}^{2} - a_{n - 1} + 1$ for all sufficiently large $n$ .

Erdős and Graham [5] asked this question; see also Erdős [6] and Bloom’s catalogue [11]. We prove the following irrationality result for a restricted class of sequences with $a_{n + 1} \sim a_{n}^{2}$ .

Theorem 1.2 (cubic-rate irrationality). A strictly increasing sequence of positive integers with

a_{n}^{2} / a_{n + 1} = 1 + \frac{3}{n} + o (n^{- 3})

has irrational reciprocal sum.

The Sylvester recurrence gives $a_{n}^{2} / a_{n + 1} - 1 = O (1 / a_{n})$ , so the cubic-rate hypothesis excludes that behaviour. It imposes much more than the quadratic limit in Problem 1.1.

For example, set $a_{1} = 8$ and

a_{n + 1} = ⌈ \frac{n a_{n}^{2}}{n + 3} ⌉ .

This gives $8, 16, 103, 5305, \dots$ . From $a_{n + 1} \geq a_{n}^{2} / 4$ we obtain $a_{n} \geq 4 \cdot 2^{2^{n - 1}}$ by induction. The error introduced by the ceiling is less than one, and hence

0 \leq 1 + \frac{3}{n} - \frac{a_{n}^{2}}{a_{n + 1}} < \frac{16}{a_{n}^{2}} = o (n^{- 3}) .

The theorem applies to this explicitly defined sequence.

Koizumi’s product criterion [10] requires the increments of $P_{n} / a_{n}$ , where $P_{n} = \prod_{j < n} a_{j}$ , to have nonpositive upper limit. Corollary 4.9 below allows any finite upper limit. At the cubic rate, however, $P_{n} / a_{n}$ grows like $n^{3}$ and its increments like $n^{2}$ ; neither criterion applies. This comparison does not decide whether the LCM criteria apply: those also depend on repeated factors in $P_{n}$ .

Rationality supplies a positive integer tail numerator $C_{n}$ , but not a bounded one: here it grows cubically. We therefore apply integrality to its finite differences. The exact comparison sequence $F_{n} = n (n + 1) (n + 2)$ has $F_{n + 1} / F_{n} = 1 + 3 / n$ . The precision in the hypothesis forces $Δ^{4} C_{n} \to 0$ , hence eventual equality $C_{n} = A F_{n} + B$ . This extraction uses the numerator ratio and integrality, not the exact denominator recurrence.

The denominator recurrence now becomes decisive. It imposes a square condition at every root of a cubic modulo almost every prime. Chebotarev’s theorem turns these residue conditions into a square in a cubic number field, where traces restrict the numerator to two polynomials. A four-term calculation modulo seven excludes both. Section 3 follows these two stages: first extract the polynomial, then test whether it can satisfy the exact recurrence.

Sections 4 and 5 give bounded-increment and summability criteria. Section 6 clears tails by a least common multiple and uses congruences to control first crossings of new heights; its convergence hypothesis is not derived from the quadratic limit. The companion paper also treats nonintegral rates and proves a stronger cubic disagreement theorem. Its proof locations and the formal sources are listed in Appendix B.

Tail numerators

For the Sylvester sequence $2, 3, 7, 43, \dots$ , whose reciprocal sum is $1$ , the successive tails are $1, 1 / 2, 1 / 6, 1 / 42, \dots$ . Multiplication by the products $1, 2, 6, 42, \dots$ leaves the constant integer numerator $1$ . For any rational reciprocal sum, including a denominator of the whole sum in these products again gives integer numerators. We keep these fractions unreduced: the exact multiplicative denominator update will transfer the growth rate to the numerator.

Assume now that $a_{n}$ are strictly increasing positive integers, $a_{n + 1} / a_{n}^{2} \to 1$ , and $\sum_{n \geq 1} 1 / a_{n} = p / q$ with positive integers $p, q$ . All indices in this construction start at $1$ . Put

x_{n} = \sum_{k \geq n} \frac{1}{a_{k}}, P_{n} = \prod_{1 \leq j < n} a_{j}, D_{n} = q P_{n}, C_{n} = D_{n} x_{n} .

Here $P_{1} = 1$ , $D_{1} = q$ and $C_{1} = p$ . Since every $a_{k}$ with $k < n$ divides $P_{n}$ , subtracting the finite prefix from $p / q$ gives

C_{n} = p P_{n} - q \sum_{1 \leq k < n} \frac{P_{n}}{a_{k}} \in N_{> 0} .

Positivity comes from $C_{n} = D_{n} x_{n}$ . Removing $1 / a_{n}$ from the tail gives

\begin{matrix} (1) & C_{n + 1} = a_{n} C_{n} - D_{n}, D_{n + 1} = a_{n} D_{n} . \end{matrix}

Koizumi constructs these coordinates in Lemma 4 [10]. On a pseudo-greedy tail his $c_{n}, d_{n}, e_{n}$ correspond to $C_{n}, D_{n}, D_{n} - (a_{n} - 1) C_{n}$ . If the tail is restarted with its value in lowest terms, both coordinates are divided by the same fixed integer. Reducing at every step would instead introduce varying cancellation factors into the numerator ratio. We therefore extract the polynomial before dividing by the eventual fixed gcd in Section 3.2.

For large $n$ , $a_{n + 1} \geq a_{n}^{2} / 2 \geq 2 a_{n}$ . The terms after $1 / a_{n + 1}$ sum to at most $2 / a_{n + 2} \leq 4 / a_{n + 1}^{2}$ , so

\begin{matrix} (2) & x_{n} = \frac{1}{a_{n}} + \frac{1}{a_{n + 1}} + O (a_{n + 1}^{- 2}), \frac{C_{n + 1}}{C_{n}} = \frac{a_{n}^{2}}{a_{n + 1}} + O (1 / a_{n}) . \end{matrix}

For the second estimate, the first gives $a_{n} x_{n} = 1 + O (1 / a_{n})$ . Use this in

\frac{C_{n + 1}}{C_{n}} = \frac{a_{n}^{2}}{a_{n + 1}} \frac{a_{n + 1} x_{n + 1}}{a_{n} x_{n}} .

The last factor is $1 + O (1 / a_{n})$ , and $a_{n}^{2} / a_{n + 1} \to 1$ , giving the stated additive error. Quadratic growth makes $1 / a_{n} = o (n^{- k})$ for every fixed $k$ , so this error preserves the precision required in the cubic theorem. We keep the original index $n$ throughout that proof. Although an eventual recurrence survives removal of a finite prefix, the expression $1 + 3 / n + o (n^{- 3})$ changes its lower-order terms under an index shift.

Proof of cubic-rate irrationality

Suppose, towards a contradiction, that the reciprocal sum in Theorem 1.2 is rational. Construct $C_{n}, D_{n}$ as in Section 2. Equation (2) transfers the rate without changing its precision:

\begin{matrix} (3) & \frac{C_{n + 1}}{C_{n}} = 1 + \frac{3}{n} + o (n^{- 3}) . \end{matrix}

An eventual cubic polynomial

We use $F_{n} = n (n + 1) (n + 2)$ rather than $n^{3}$ : its successive ratio is exactly $1 + 3 / n$ , so dividing by it removes the model without introducing lower-order errors. Write (3) as $C_{n + 1} = (1 + 3 / n + ε_{n}) C_{n}$ , where $ε_{n} = o (n^{- 3})$ . Dividing out the exact model gives

z_{n} = \frac{C_{n}}{F_{n}}, \frac{z_{n + 1}}{z_{n}} = 1 + \frac{ε_{n}}{1 + 3 / n} .

The logarithmic increments are $o (n^{- 3})$ , so their absolute tails are $o (n^{- 2})$ . Hence $z_{n} \to A > 0$ with $z_{n} - A = o (n^{- 2})$ . Multiplying by $F_{n}$ gives

C_{n} = A F_{n} + δ_{n}, δ_{n} = o (n) .

An $o (n)$ error can still oscillate too much for finite differences. To control its first difference, subtract the numerator update for $C_{n}$ and the comparison update for $A F_{n}$ :

Δ δ_{n} = \frac{3}{n} δ_{n} + ε_{n} C_{n} = o (1), Δ h_{n} = h_{n + 1} - h_{n} .

Here $C_{n} = O (n^{3})$ makes the second term $o (1)$ . Three more differences still tend to zero and kill the cubic model:

Δ^{4} C_{n} = Δ^{3} (Δ δ_{n}) ⟶ 0.

Integrality turns this limit into eventual vanishing. Newton interpolation then expresses $C_{n}$ as a rational polynomial of degree at most three. Since its difference from $A F_{n}$ is $o (n)$ , the cubic, quadratic and linear coefficients agree; only a constant can remain:

\begin{matrix} (4) & C_{n} = A n (n + 1) (n + 2) + B, A \in Q_{> 0}, B \in Q . \end{matrix}

The precision matters at the subtraction step. The integer sequence $F_{n} + (- 1)^{n}$ has ratio $1 + 3 / n + O (n^{- 3})$ and never agrees eventually with a polynomial; its error has an oscillating first difference. This example concerns polynomial extraction alone. It is not asserted to satisfy the denominator recurrence.

Reduction and the constant term

We now use the denominator recurrence. Both updates preserve common divisors, so $G_{n} = gcd (C_{n}, D_{n})$ divides $G_{n + 1}$ and every later numerator. On the polynomial tail it therefore divides the third difference $6 A$ , a fixed positive integer. The fourth difference gave polynomiality; the nonzero third difference now bounds cancellation. Thus $G_{n}$ stabilises at a positive integer $g$ .

Dividing by this fixed $g$ gives $u_{n} = C_{n} / g$ , $v_{n} = D_{n} / g$ in lowest terms without changing the recurrences. Their coprimality persists as follows.

Proposition 3.1 (persistent coprimality). Let $a_{n}, u_{n}, v_{n}$ be integer sequences with $u_{n} > 0$ , $v_{n} \geq 0$ and $gcd (u_{n}, v_{n}) = 1$ satisfying

u_{n + 1} = a_{n} u_{n} - v_{n}, v_{n + 1} = a_{n} v_{n} .

Then $gcd (a_{n}, v_{n}) = 1$ . The $a_{n}$ are pairwise coprime, and $gcd (a_{i}, u_{t}) = 1$ whenever $i < t$ .

Proof. A prime dividing both $a_{n}$ and $v_{n}$ would divide $u_{n + 1}$ and $v_{n + 1}$ , contrary to reducedness. For $i < t$ , the factor $a_{i}$ divides $v_{t}$ . Reducedness gives $gcd (a_{i}, u_{t}) = 1$ , and $gcd (a_{t}, v_{t}) = 1$ gives $gcd (a_{i}, a_{t}) = 1$ . ◻

In the cubic case, adjacent numerators are also coprime, since $gcd (u_{n}, u_{n + 1}) = gcd (u_{n}, v_{n}) = 1$ . Write the polynomial for $u_{n}$ as

\begin{matrix} (5) & Q (n) = \frac{m}{6} n (n + 1) (n + 2) + c . \end{matrix}

The third difference $m = 6 A / g$ is a positive integer. Since $n (n + 1) (n + 2) / 6 = (\binom{n + 2}{3})$ is an integer, any sufficiently late value $u_{n} = Q (n)$ gives

c = u_{n} - m (\binom{n + 2}{3}) \in Z .

Adjacent coprimality now restricts this integer $c$ . If a prime $ℓ$ divides $c$ , choose an arbitrarily late $n \equiv - 1 (\mod 6 ℓ)$ . Both three-factor products contain $n + 1$ , so division by $6$ leaves a factor $ℓ$ , even for $ℓ = 2, 3$ . Thus $ℓ$ divides both $Q (n)$ and $Q (n + 1)$ , contradicting adjacent coprimality. This also excludes $c = 0$ . Thus

m \in N_{> 0}, c \in {1, - 1} .

Irreducibility follows from persistence of denominator primes. The pairwise coprime multipliers $a_{n} > 1$ supply infinitely many distinct primes; each divides every later $v_{t}$ and no later $u_{t}$ . A rational root of $Q$ would reduce to a root modulo all but finitely many primes. Choose a persistent prime outside those exceptions. Every sufficiently late index in the root’s residue class would give $ℓ ∣ Q (t) = u_{t}$ , contradicting reducedness. Thus $Q$ has no rational root and, being cubic, is irreducible.

Set $κ = m / 6$ , $η = 6 c / m$ , and

f (T) = T^{3} - T + η, Q (n) = κ f (n + 1) .

A square forced by a zero numerator

At a zero of the numerator polynomial modulo a prime, the recurrence must still relate the two neighbouring nonzero numerators. Eliminating $v_{n}$ from two exact updates makes this constraint visible:

\begin{matrix} (6) & u_{n + 2} = (a_{n} + a_{n + 1}) u_{n + 1} - a_{n}^{2} u_{n} . \end{matrix}

Whenever $u_{k} \equiv 0 (\mod ℓ)$ , it follows that

- u_{k - 1} u_{k + 1} \equiv (a_{k - 1} u_{k - 1})^{2} (\mod ℓ) .

Thus the negative product of the neighbouring numerators must be a square. Since our numerator is a polynomial, its roots modulo $ℓ$ tell us exactly where to apply this observation.

Let $ℓ ∤ 6 m$ be prime and let $r \in F_{ℓ}$ satisfy $f (r) = 0$ . The constant $η = 6 c / m$ is nonzero modulo $ℓ$ , so $r \notin {0, 1, - 1}$ . Choose a sufficiently late $k$ with $k + 1 \equiv r (\mod ℓ)$ . Then $u_{k} = κ f (k + 1) \equiv 0$ , whereas

f (r - 1) = - 3 r (r - 1), f (r + 1) = 3 r (r + 1) .

Consequently, in $F_{ℓ}$ ,

(a_{k - 1} u_{k - 1})^{2} = - u_{k - 1} u_{k + 1} = 9 κ^{2} r^{2} (r^{2} - 1) .

Dividing by the nonzero square $9 κ^{2} r^{2}$ gives

\begin{matrix} (7) & ℓ ∤ 6 m, r \in F_{ℓ}, f (r) = 0 ⟹ r^{2} - 1 \in (F_{ℓ}^{\times})^{2} (ℓ prime) . \end{matrix}

The condition holds for every root; primes with no root impose no condition. This quantifier matters in passing to a number field.

Let $α$ be a root of $f$ and put $K = Q (α)$ , a cubic field. Suppose $α^{2} - 1$ is a nonsquare in $K$ , and choose $β$ with $β^{2} = α^{2} - 1$ . To contradict the modular condition, we seek a Frobenius that fixes $α$ but exchanges $β$ and $- β$ . The nontrivial automorphism of $K (β) / K$ does exactly this. Extend it to $σ \in Gal (M / Q)$ , where $M$ is a Galois closure of $K (β) / Q$ .

Chebotarev’s density theorem [9] supplies infinitely many unramified rational primes with Frobenius conjugate to $σ$ ; choosing a prime of $M$ above each makes it equal to $σ$ . Omit residue characteristic two, primes dividing $6 m$ , and the finitely many primes where $α$ or $β$ is nonintegral or $β$ reduces to zero. Frobenius acts by the $ℓ$ -th power on the residue field, so

{\bar{α}}^{ℓ} = \bar{α}, {\bar{β}}^{ℓ} = - \bar{β} \neq \bar{β} .

Thus $r = \bar{α}$ lies in $F_{ℓ}$ and satisfies $f (r) = 0$ , but neither root $\pm \bar{β}$ of $X^{2} - (r^{2} - 1)$ lies in that field. The condition for every root in (7) applies to this $r$ , giving the contradiction. Hence some $β \in K$ satisfies $β^{2} = α^{2} - 1$ .

Traces in the cubic field

We now need the square relation to constrain the coefficient $η$ . Factoring it produces reciprocal elements, avoiding a separate expansion of the square root in a basis of $K$ :

(α + β) (α - β) = 1.

Put $z = α + β$ . Then $z^{- 1} = α - β$ and $2 α = z + z^{- 1}$ . Since $z \in K$ and $α \in Q (z)$ , we have $Q (z) = K$ . Write the minimal polynomial of $z$ as

p (T) = T^{3} + b T^{2} + d T + w, b, d, w \in Q, w \neq 0.

The minimal polynomial of $z^{- 1}$ is the monic reciprocal polynomial

\frac{T^{3} p (T^{- 1})}{w} = T^{3} + \frac{d}{w} T^{2} + \frac{b}{w} T + \frac{1}{w} .

We compute the same three traces from $f$ and from the reciprocal pair $z, z^{- 1}$ . All traces are from $K$ to $Q$ . The cubic for $α$ gives:

Tr (α) = 0, Tr (α^{2}) = 2, Tr (α^{3}) = - 3 η .

Newton’s identities for $p$ and its reciprocal give

\begin{matrix} (8) & d = - b w, b^{2} + b (w - w^{- 1}) = 1, η = \frac{(b^{2} + 1) (w + w^{- 1})}{8} . \end{matrix}

For completeness, the first equality follows from $0 = 2 Tr (α) = - b - d / w$ . After substituting $d = - b w$ , Newton’s identities give

\begin{aligned} Tr (z^{2}) + Tr (z^{- 2}) & = 2 b^{2} + 2 b (w - w^{- 1}), \\ Tr (z^{3}) + Tr (z^{- 3}) & = - 3 (b^{2} + 1) (w + w^{- 1}) . \end{aligned}

The first line is $4 Tr (α^{2}) - 6 = 2$ . The second is $8 Tr (α^{3}) = - 24 η$ , because the mixed terms in $(z + z^{- 1})^{3}$ have trace $3 Tr (z + z^{- 1}) = 0$ . These give the other two equalities in (8).

Multiplying the middle equation by $w$ and bringing all terms to one side gives $(b w - 1) (b + w) = 0$ . Write $w = r / s$ in lowest terms, with $r \neq 0$ , $s > 0$ . Substituting $b = - w$ or $b = 1 / w$ into the last equation and using $η = 6 c / m$ gives respectively

m = \frac{48 c r s^{3}}{(r^{2} + s^{2})^{2}} or m = \frac{48 c r^{3} s}{(r^{2} + s^{2})^{2}} .

Here the integer scale $m$ is decisive: coprimality $gcd (r^{2} + s^{2}, r s) = 1$ prevents cancellation with the variable factors in either numerator, so $(r^{2} + s^{2})^{2}$ divides $48$ . Hence $r^{2} + s^{2}$ is $1$ , $2$ or $4$ . Both $r$ and $s$ are nonzero, which leaves only $2$ : a sum of two nonzero integer squares cannot equal $1$ or $4$ . Thus $| r | = s = 1$ , and positivity of $m$ gives $m = 12$ . The only remaining numerators are

Q (n) = 2 n (n + 1) (n + 2) + 1 and Q (n) = 2 n (n + 1) (n + 2) - 1.

The contradiction modulo seven

The three-term square condition has reduced the possibilities to two cubics. We now use one more term: the denominator at the middle zero must also come from the preceding exact update. In the plus case, choose a late block starting at $n \equiv 0 (\mod 7)$ ; in the minus case, start at $n \equiv 1 (\mod 7)$ . The four successive numerators have residues

(u_{n}, u_{n + 1}, u_{n + 2}, u_{n + 3}) \equiv {\begin{cases} (1, 6, 0, 2) & (c = 1), \\ (4, 5, 0, 1) & (c = - 1) . \end{cases}

Write $d_{0}, d_{1}$ for the residues of $v_{n}, v_{n + 1}$ and $c_{0}, c_{1}, 0, c_{3}$ for the displayed numerator residues. From $0 = a_{n + 1} c_{1} - d_{1}$ and $c_{3} = - a_{n + 1} d_{1}$ we get $d_{1}^{2} = - c_{1} c_{3} = 2$ . Thus $d_{1} \in {3, 4}$ . The first update, however, gives

d_{1} = a_{n} d_{0} = \frac{d_{0} (d_{0} + c_{1})}{c_{0}} .

Completing the square in these two cases gives, in $F_{7}$ ,

d_{1} + 2 = {\begin{cases} (d_{0} + 3)^{2} & (c = 1), \\ 2 (d_{0} - 1)^{2} & (c = - 1) . \end{cases}

Since $2 = 3^{2}$ in this field, $d_{1} + 2$ must be a square in either case. But $d_{1} \in {3, 4}$ would give $d_{1} + 2 \in {5, 6}$ , both nonsquares. The middle three terms admit $d_{1} = 3$ or $4$ ; neither extends backwards through the preceding exact update. Both cubics are excluded, proving Theorem 1.2.

Section 2 of the companion proves positive lower density of disagreement with each rational cubic of this form. That lower bound depends on the orbit and the cubic. For Theorem 1.2, exclusion of eventual equality suffices.

Bounded increases

We return to the rational tails of Section 2. The Sylvester example had a constant integer numerator. To measure departure from this behaviour, put

E_{n} = D_{n} - (a_{n} - 1) C_{n} = C_{n} - C_{n + 1} .

Negative errors are rises of $C_{n}$ ; zero error gives the tail $1 / (a_{n} - 1)$ . Instead of prescribing a polynomial, we now bound the rises. Quadratic growth makes all steps small relative to $C_{n}$ ; the additional absolute bound applies only to rises, not decreases.

Theorem 4.1 (bounded negative part). Let $a, C, D : N \to N$ satisfy $a_{n} > 1$ , $C_{n} > 0$ , and

C_{n + 1} + D_{n} = a_{n} C_{n}, D_{n + 1} = a_{n} D_{n} (n \geq 0) .

Put $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ . If

\frac{E_{n}}{C_{n}} ⟶ 0 and E_{n} \geq - B for all sufficiently large n

for some integer $B \geq 0$ , then $E_{n} = 0$ for all sufficiently large $n$ .

The linked theorem uses the equivalent division-free condition: for every $K \in N$ , eventually $K | E_{n} | < C_{n}$ . Under this condition, absorption either settles the theorem or leaves $C_{n} \to \infty$ . A stable gcd and a forbidden block will exclude the latter alternative.

Zero errors and descent

Write $z_{+} = max (z, 0)$ . The identities below use (1); positivity and $| E_{n} | < C_{n}$ are imposed only where stated.

Proposition 4.2 (error identities). For integer sequences satisfying (1),

C_{n + 1} = C_{n} - E_{n}, (a_{n + 1} - a_{n}^{2} + a_{n} - 1) C_{n + 1} = a_{n}^{2} E_{n} - E_{n + 1} .

Proof. The first identity follows by substituting $D_{n} = E_{n} + (a_{n} - 1) C_{n}$ into the numerator recurrence. Substituting this expression at the next index and using $D_{n + 1} = a_{n} D_{n}$ gives the second. ◻

Equation (2) now gives $E_{n} / C_{n} = 1 - C_{n + 1} / C_{n} \to 0$ , so $| E_{n} | < C_{n}$ for all sufficiently large $n$ . Koizumi proves this relative-gap limit for an eventual pseudo-greedy tail [10]. His rounding convention also gives $- C_{n} / 2 \leq E_{n} < C_{n} / 2$ , a stronger bound than we need.

Koizumi’s Lemma 3 gives zero absorption for pseudo-greedy tails, and Proposition 1(2) uses descent when their gaps are eventually nonnegative [10]. The following form separates what the two arguments require.

Theorem 4.3 (absorption and descent). Let $a, C, D : N \to N$ satisfy $a_{n} > 1$ , $C_{n} > 0$ and (1). If $| E_{n} | < C_{n}$ for every $n$ , then $E_{n} = 0$ implies $E_{n + 1} = 0$ . For any positive integer sequence $C_{n}$ with $C_{n + 1} = C_{n} - E_{n}$ , eventual nonnegativity of $E_{n}$ implies its eventual vanishing.

Proof. When $E_{n} = 0$ , the second identity in Proposition 4.2 shows that $C_{n + 1}$ divides $E_{n + 1}$ . The inequality $| E_{n + 1} | < C_{n + 1}$ then forces $E_{n + 1} = 0$ . For the second assertion, $C_{n + 1} = C_{n} - E_{n}$ makes the positive integer sequence $C_{n}$ eventually nonincreasing, hence constant. ◻

Corollary 4.4 (two zero errors). For integer sequences satisfying (1), if $E_{n} = E_{n + 1} = 0$ and $C_{n + 1} \neq 0$ , then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ . In particular, if $a, C, D : N \to N$ also satisfy $a_{n} > 1$ and $C_{n} > 0$ , eventual zero error implies the eventual Sylvester recurrence.

Proof. Cancel the nonzero factor $C_{n + 1}$ in the second error identity. ◻

Thus a late zero is absorbing. Without late zeros, $| E_{n} | \geq 1$ and $| E_{n} | / C_{n} \to 0$ force $C_{n} \to \infty$ . The scalar update permits $C_{n} = n + 1$ , $E_{n} = - 1$ forever; excluding this behaviour requires the denominator recurrence.

A stable gcd and a forbidden block

Proposition 4.5 (gcd stabilisation). Let $a, C, D : N \to N$ satisfy $a_{n} > 1$ , $C_{n} > 0$ and (1). If some fixed integer $B \geq 1$ satisfies $- B \leq E_{n} < 0$ at infinitely many indices, then $G_{n} = gcd (C_{n}, D_{n})$ is eventually constant. Dividing $C_{n}, D_{n}$ by its eventual value gives coprime sequences satisfying the same recurrences.

Proof. We have $G_{n} ∣ G_{n + 1}$ and $G_{n} ∣ E_{n}$ . Given $n$ , choose $t \geq n$ with $- B \leq E_{t} < 0$ . Then $G_{n} \leq G_{t} \leq - E_{t} \leq B$ . Hence the positive divisibility chain stabilises. Division by its stable value preserves the recurrences and gives coprime numerators and denominators. ◻

There are two distinct uses of the bound. Arbitrarily late negative errors in a fixed interval suffice to stabilise the gcd. The crossing argument below needs every sufficiently late upward step bounded; otherwise a single large rise could jump over the forbidden block.

A sequence avoiding multiples of $2$ and $3$ cannot cross the pair $6 k + 2, 6 k + 3$ from below with upward steps at most two: its first value at least $6 k + 2$ would be one of those two integers. Decreases before that crossing do not help. For a general step bound $B$ , the Chinese remainder theorem supplies a forbidden block of length $B$ .

Lemma 4.6 (consecutive multiples). For pairwise coprime integers $m_{0}, \dots, m_{B - 1} \geq 2$ and every lower bound, there is a larger $t$ such that $m_{i} ∣ t + i$ for each $i < B$ .

Proof. Solve $t \equiv - i (\mod m_{i})$ by the Chinese remainder theorem and add multiples of $\prod_{i} m_{i}$ to exceed the prescribed bound. ◻

Theorem 4.7 (Chinese remainder theorem and first crossing). Let $u : N \to N$ tend to infinity and let $B \geq 1$ be an integer with $u_{n + 1} \leq u_{n} + B$ for every $n$ . There is no sequence of pairwise coprime integers $m_{i} \geq 2$ for which $gcd (m_{i}, u_{t}) = 1$ whenever $i < t$ .

Proof. Apply Lemma 4.6 to $m_{0}, \dots, m_{B - 1}$ , choosing $t > max (u_{0}, \dots, u_{B})$ . There is a first $n > B$ with $u_{n} \geq t$ . Then

t \leq u_{n} \leq u_{n - 1} + B < t + B .

Thus $u_{n} = t + i$ for some $i < B < n$ , and $m_{i} ∣ u_{n}$ , contrary to $gcd (m_{i}, u_{n}) = 1$ . ◻

Bado proves a two-sided bounded-error criterion by this forbidden-block argument [7]. The gcd stabilisation above allows us to use only the lower error bound.

Proof of Theorem 4.1. Suppose the conclusion fails. Absorption excludes late zeros; $| E_{n} | \geq 1$ and the relative limit then give $C_{n} \to \infty$ . Integer descent forces infinitely many late negative errors, where $1 \leq - E_{n} \leq B$ . Thus $B \geq 1$ and Proposition 4.5 gives a stable gcd $g$ . Restrict to a tail on which the gcd is $g$ and $E_{n} \geq - B$ , then reindex that tail. Dividing by $g$ gives $u_{n} = C_{n} / g \to \infty$ and

u_{n + 1} - u_{n} = - E_{n} / g \leq B .

Proposition 3.1 makes the multipliers $a_{i} \geq 2$ pairwise coprime and coprime to every later numerator, contradicting Theorem 4.7. ◻

Corollary 4.8. Under Theorem 4.1, the multipliers satisfy $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ eventually.

Proof. Theorem 4.1 gives eventual zero error; positivity of $C_{n}$ and Corollary 4.4 give the recurrence. ◻

The condition in the original sequence

Let $γ_{n} = a_{n}^{2} / a_{n + 1} - 1$ . For $t_{n} = P_{n} / a_{n}$ ,

t_{n + 1} - t_{n} = t_{n} γ_{n} .

We bound upward increments, not values or decreases. The relation $C_{n} \sim q t_{n}$ does not control increments; instead an exact identity will give $E_{n} > - q t_{n} γ_{n}$ , turning an upper increment bound into a lower error bound.

Corollary 4.9 (bounded increments of $P_{n} / a_{n}$ ). Let $a_{1} < a_{2} < \dots$ be positive integers, $a_{n + 1} / a_{n}^{2} \to 1$ , and $\sum_{n \geq 1} 1 / a_{n} \in Q$ . Put $P_{n} = \prod_{j < n} a_{j}$ . If

\underset{n \to \infty}{lim sup} \frac{P_{n}}{a_{n}} (\frac{a_{n}^{2}}{a_{n + 1}} - 1) < + \infty,

then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ for all sufficiently large $n$ .

Proof. For the canonical integer tail, direct substitution gives

\begin{matrix} (9) & E_{n} + q \frac{P_{n}}{a_{n}} γ_{n} = q P_{n} (\frac{1}{a_{n + 1}} - (a_{n} - 1) \sum_{k \geq n + 2} \frac{1}{a_{k}}) . \end{matrix}

The tail estimate bounds the subtracted term by $4 (a_{n} - 1) / a_{n + 1}^{2} < 1 / a_{n + 1}$ eventually. The positive remainder gives $E_{n} > - q t_{n} γ_{n}$ , so the assumed upper bound bounds $E_{n}$ below. Only the remainder’s sign is needed here. The canonical tails satisfy the exact recurrences and, by (2), $E_{n} / C_{n} \to 0$ . Theorem 4.1 and Corollary 4.8 finish. ◻

Koizumi’s proof of Corollary 4(1) uses this product-weighted comparison [10]; that corollary assumes a nonpositive upper limit, whereas the argument here allows any finite upper limit. A corresponding LCM comparison appears below. For $a_{n} = b^{2^{n - 1}}$ , $b \geq 2$ , the increments of $P_{n} / a_{n}$ are zero. Since the sequence does not eventually satisfy the Sylvester recurrence, the corollary gives irrationality. For a Sylvester sequence starting at $a_{1} > 1$ , $a_{n} - 1 = (a_{1} - 1) P_{n}$ and the increments tend to zero.

Dividing by $n$ removes the nonsummable $1 / n$ term. A summable upper error then suffices, without a lower bound on $γ_{n}$ .

Corollary 4.10 (an inclusive one-sided $1 / n$ bound). Let $a_{1} < a_{2} < \dots$ be positive integers with $a_{n + 1} / a_{n}^{2} \to 1$ and $\sum_{n} 1 / a_{n} \in Q$ . Suppose that for some $K \geq 0$ and $ε > 0$ ,

γ_{n} := a_{n}^{2} / a_{n + 1} - 1 \leq \frac{1}{n} + \frac{K}{n^{1 + ε}} for all large n .

Then the sequence is eventually Sylvester. In particular, the conclusion holds under the pointwise eventual bound $γ_{n} \leq 1 / n$ .

Proof. The exact model $n$ has successive ratio $1 + 1 / n$ . Thus $(t_{n + 1} / (n + 1)) / (t_{n} / n) = (1 + γ_{n}) / (1 + 1 / n) \leq 1 + K / [n^{ε} (n + 1)]$ . The convergent product of these upper bounds bounds $t_{n} / n$ above; no positive limit is needed. Hence $t_{n} = O (n)$ and $t_{n} γ_{n} \leq t_{n} (γ_{n})_{+} = O (1)$ , so Corollary 4.9 applies. ◻

The weaker condition $lim sup n (γ_{n})_{+} \leq 1$ does not suffice for the estimate $t_{n} = O (n)$ . For example, the scalar ratios $1 + γ_{n} = 1 + (1 + 1 / \log n) / n$ give a product of order $n \log n$ . This scalar product refutes the intermediate linear estimate under the weaker rate, not the Sylvester conclusion for reciprocal tails.

For positive limiting increments, take $a_{1} = 4$ and $a_{n + 1} = ⌈ n a_{n}^{2} / (n + 1) ⌉$ , beginning $4, 8, 43, 1387$ . Here $a_{n} \geq 2 \cdot 2^{2^{n - 1}}$ and

0 \leq 1 + \frac{1}{n} - \frac{a_{n}^{2}}{a_{n + 1}} < \frac{4}{a_{n}^{2}} .

Consequently $t_{n} \sim K n$ and $t_{n + 1} - t_{n} \to K > 0$ . The corollary proves irrationality because $γ_{n} \sim 1 / n$ is incompatible with the eventual Sylvester recurrence.

For the introduction’s $3 / n$ ceiling example, division by $n (n + 1) (n + 2)$ and summability of the rounding errors give $t_{n} \sim K_{3} n^{3}$ and $t_{n + 1} - t_{n} \sim 3 K_{3} n^{2}$ , with $K_{3} > 0$ . Its irrationality follows from Theorem 1.2, beyond the bounded-increase criterion.

Finite total relative increase

Summable relative increases first bound $C_{n}$ by an infinite product, then allow only finitely many rises; integer descent finishes. No denominator recurrence is needed. Relative increases tending merely to zero still allow $C_{n} = n + 1$ or $C_{n} = (n + 1)^{2}$ .

Theorem 5.1 (a convergent sum of relative increases). Let $C_{n}$ be positive integers and $E_{n}$ integers satisfying $C_{n + 1} = C_{n} - E_{n}$ . If

\sum_{n} \frac{(- E_{n})_{+}}{C_{n}} < \infty,

then $E_{n} = 0$ eventually. Neither denominator dynamics nor vanishing relative error is required.

Proof. Set $δ_{n} = (- E_{n})_{+} / C_{n}$ . Then

C_{N} \leq C_{0} \prod_{n < N} (1 + δ_{n}) \leq C_{0} \exp (\sum_{n} δ_{n}) .

Choose an integer $K$ above this bound. A strict rise of the integer sequence has size at least one, so it contributes at least $1 / K$ to $\sum δ_{n}$ . Hence only finitely many rises occur. Thereafter $C_{n}$ is a nonincreasing positive integer sequence, and its eventual constancy gives $E_{n} = 0$ . ◻

The proof also allows positive real $C_{n}$ with integer $E_{n}$ : the values lie in $C_{0} + Z$ , whose bounded positive part is finite. Discrete increments are essential to this argument. With real errors, $C_{n} = 1 + 1 / (n + 1)$ decreases forever with zero relative-increase sum; without positivity, $C_{n} = - n - 1$ , $E_{n} = 1$ does so too. The companion’s Section 13 gives the details.

On an exact reciprocal-tail orbit the conclusion gives the Sylvester recurrence. For the gap sequence of the pseudo-greedy expansion, the same criterion, with the same product bound and integer descent, appears in the Erdős Problem a Day working report on Problem #243, dated 12 August 2026 [8]; the statement above is for any positive integer sequence with $C_{n + 1} = C_{n} - E_{n}$ . This summability condition and the bound in Theorem 4.1 are different estimates. For exact reciprocal tails with $| E_{n} | / C_{n} \to 0$ , each is equivalent to eventual vanishing of $E_{n}$ ; neither estimate has been derived here from the unrestricted problem.

New maxima of an LCM numerator

The least common multiple retains only the largest power of each prime among $q, a_{1}, \dots, a_{n - 1}$ . It preserves integrality, not coprimality: a numerator may now take values forbidden in Section 4.2. The recurrence will instead forbid short positive jumps from selected multiples. Put

L_{n} = lcm (q, a_{1}, \dots, a_{n - 1}), M_{n} = D_{n} / L_{n}, U_{n} = L_{n} x_{n} = C_{n} / M_{n}, V_{n} = E_{n} / M_{n} .

The denominator of $x_{n}$ divides $L_{n}$ , so $U_{n} \in Z$ and $V_{n} = L_{n} - (a_{n} - 1) U_{n} \in Z$ . The fraction $U_{n} / L_{n}$ need not be reduced. With $ρ_{n} = gcd (L_{n}, a_{n})$ , the exact updates are

M_{n + 1} = M_{n} ρ_{n}, ρ_{n} U_{n + 1} = U_{n} - V_{n}, V_{n} = L_{n} - (a_{n} - 1) U_{n} .

These coordinates and updates also appear in Bado’s September 2026 preprint. With his denominator parameter equal to $q$ , his $M_{n - 1}$ , $Δ_{n - 1}$ , $K_{n - 1}$ , $u_{n}$ and $g_{n}$ are respectively our $L_{n}$ , $M_{n}$ , $U_{n}$ , $V_{n}$ and $ρ_{n}$ ; his (19) is the middle update above [7].

Since $L_{n} ∣ q P_{n}$ and $V_{n} = (L_{n} / (q P_{n})) E_{n}$ , multiplying (9) by $L_{n} / (q P_{n})$ gives, eventually,

\begin{matrix} (10) & 0 < V_{n} + \frac{L_{n}}{a_{n}} (\frac{a_{n}^{2}}{a_{n + 1}} - 1) \leq \frac{L_{n}}{a_{n + 1}} . \end{matrix}

The lower bound transfers an upper bound on the growth defect to a lower bound on $V_{n}$ . The upper bound will let us compare weighted series with a summable error.

Write $R_{n} = max_{j \leq n} U_{j}$ and $R = {n : U_{n + 1} > R_{n}}$ . Since $V_{n} / U_{n} = E_{n} / C_{n} \to 0$ , eventually $| V_{n} | < U_{n}$ and $- U_{n} \leq 2 V_{n}$ . When $ρ_{n} \geq 2$ , the first bound gives $U_{n + 1} < U_{n}$ ; the second sharpens this to $U_{n + 1} \leq 3 U_{n} / 4$ . Thus every late rise, in particular every record, has $ρ_{n} = 1$ : its multiplier is coprime to $L_{n}$ . At such a record write the full jump as $d_{n} = U_{n + 1} - U_{n} = - V_{n} > 0$ ; at a contracting step that equality need not hold.

Theorem 6.1 (a convergent weighted sum over new maxima). Assume the growth and rationality hypotheses of Problem 1.1. Let $f : [1, \infty) \to [0, \infty)$ be finite and nonincreasing, with $\int_{1}^{\infty} f (t) d t = \infty$ . Then the sequence is eventually Sylvester if and only if, for some integer $B \geq 0$ ,

\sum_{n \in R} (- V_{n} - B)_{+} f (U_{n}) < \infty .

At a late record, the summand is $(d_{n} - B)_{+} f (U_{n})$ , where $d_{n} = U_{n + 1} - U_{n}$ .

The full jump matters: with previous record $10$ , a step from $5$ to $12$ first crosses $11$ . Its jump is $7$ , but the record increases by only $2$ . This illustrates the two increments, not a denominator sequence satisfying (1).

For $B = 0$ , the integral comparison

\int_{R_{n}}^{R_{n + 1}} f (t) d t \leq (R_{n + 1} - R_{n}) f (U_{n}) \leq d_{n} f (U_{n})

already charges for every newly reached height. The arithmetic is needed to retain divergence after subtracting a fixed $B$ at each record. We shall find a progression of heights whose first crossings still cost at least one unit of excess jump.

The weights $1 / t$ and $1 / [t \log (e t)]$ are allowed; $1 / t^{2}$ is not. One admissible weight and one fixed $B$ suffice; $B$ cannot grow with the record. The limit $V_{n} / U_{n} \to 0$ alone gives no summability.

Proof. Suppose the sequence is not eventually Sylvester. Absorption excludes late zeros of $E_{n}$ , so $V_{n} = E_{n} / M_{n}$ is eventually a nonzero integer. Hence

\frac{1}{U_{n}} \leq \frac{| V_{n} |}{U_{n}} = \frac{| E_{n} |}{C_{n}} ⟶ 0.

Thus $U_{n} \to \infty$ . Infinitely many late records supply pairwise coprime multipliers: each is coprime to its $L_{n}$ , which is divisible by every earlier multiplier. Since $a_{n} \to \infty$ , for any fixed $B \geq 1$ choose $B$ of them, $m_{0}, \dots, m_{B - 1} > B$ . Take $T$ beyond their indices and the threshold for $ρ_{n} = 1$ at records.

Put $P = \prod_{i} m_{i}$ and choose $x$ with $m_{i} ∣ x + i$ by the Chinese remainder theorem. We select the heights $τ = x + B + k P > R_{T}$ , $k \in Z$ . They are spaced $P$ apart.

At the first crossing of a selected height, $U_{n} \leq R_{n} < τ \leq U_{n} + d_{n}$ . In particular this is a record step. If $d_{n} \leq B$ , then $U_{n} \in [τ - B, τ)$ , so

U_{n} = τ - B + i = x + k P + i for some 0 \leq i < B .

The choice of $x$ gives $m_{i} ∣ U_{n}$ . This is allowed: $U_{n} / L_{n}$ need not be reduced. But $m_{i} ∣ L_{n}$ too, so $m_{i} ∣ d_{n} = (a_{n} - 1) U_{n} - L_{n}$ , contradicting $0 < d_{n} \leq B < m_{i}$ . It is the short positive jump, not the numerator value, that is impossible.

A jump may first cross several selected heights. To charge all of them to its single excess $d_{n} - B$ , let their number be $h \geq 1$ . Their spacing gives $(h - 1) P < d_{n}$ . Write $r = d_{n} - B \geq 1$ . Since $P \geq B + 1$ , $d_{n} = B + r \leq P r$ , and hence $h \leq r$ . Each of those heights exceeds $U_{n}$ , so monotonicity gives

\sum_{\begin{matrix} τ first crossed \\ at step n \end{matrix}} f (τ) \leq (d_{n} - B) f (U_{n}) .

Each selected height above $R_{T}$ has one first crossing. The heights are $P$ apart, with the first at most $R_{T} + P$ . For $R_{N} \geq R_{T} + P$ , the intervals $[τ, min {τ + P, R_{N}}]$ with $τ \leq R_{N}$ cover $[R_{T} + P, R_{N}]$ . Monotonicity bounds each integral by $P f (τ)$ , so the crossing bounds give

\begin{matrix} (11) & \sum_{\begin{matrix} T \leq n < N \\ n \in R \end{matrix}} (- V_{n} - B)_{+} f (U_{n}) \geq \frac{1}{P} \int_{R_{T} + P}^{R_{N}} f (t) d t . \end{matrix}

Since $R_{n} \to \infty$ , the right side diverges for every $B \geq 1$ ; $B = 0$ follows by domination. Conversely, the eventual Sylvester recurrence gives by telescoping $x_{n} = 1 / (a_{n} - 1)$ , so $V_{n} = 0$ eventually. ◻

For example, $f (t) = 1 / [t \log (e t)]$ gives the sufficient condition

\sum_{n \in R} \frac{(- V_{n} - B)_{+}}{U_{n} \log (e U_{n})} < \infty .

Its finite lower bound in (11) is $P^{- 1} \log (\log (e R_{N}) / \log (e (R_{T} + P)))$ . Further fixed iterated logarithmic factors are allowed whenever the integral still diverges. All these weights use the same crossing theorem.

For a series, sign control alone is not enough: we bound the total change in its summands. Put $γ_{n} = a_{n}^{2} / a_{n + 1} - 1$ and $θ_{n} = E_{n} / C_{n}$ . The defect identity gives

γ_{n} + θ_{n} = \frac{(1 - θ_{n}) (a_{n} - 1 + θ_{n + 1})}{a_{n + 1}}, 0 < γ_{n} + θ_{n} < 3 / a_{n}

eventually. Positive parts do not increase absolute differences. Since $V_{n} = U_{n} θ_{n}$ , the summands $U_{n} f (U_{n}) (γ_{n} - B / U_{n})_{+}$ and $(- V_{n} - B)_{+} f (U_{n})$ differ by at most $3 U_{n} f (U_{n}) / a_{n} \leq 3 f (1) C_{n} / a_{n}$ . This is the error after weighting. Now $C_{n} / a_{n} \sim q P_{n} / a_{n}^{2}$ , since $a_{n} x_{n} \to 1$ , and

\frac{P_{n + 1} / a_{n + 1}^{2}}{P_{n} / a_{n}^{2}} = \frac{a_{n}^{3}}{a_{n + 1}^{2}} ⟶ 0.

The ratio test therefore makes the weighted error summable, even over all indices. The remainders in (9) and (10) are likewise absolutely summable: each is eventually between zero and $q P_{n} / a_{n + 1} = O (P_{n} / a_{n}^{2})$ . Thus Theorem 6.1 is equivalent to finiteness of

\begin{matrix} (12) & \sum_{n \in R} U_{n} f (U_{n}) {(\frac{a_{n}^{2}}{a_{n + 1}} - 1 - \frac{B}{U_{n}})}_{+} \end{matrix}

for some $B$ . This is a reformulation of the extra hypothesis, not a proof of it from quadratic growth. Both series use the full jump $U_{n + 1} - U_{n}$ , including recovery from earlier decreases. Replacing it by $R_{n + 1} - R_{n}$ , or merely proving that individual summands tend to zero, would not establish the required finiteness.

Corollary 6.2 (a bound using the least common multiple). Assume the hypotheses of Problem 1.1. Write $A_{n} = lcm (a_{1}, \dots, a_{n - 1})$ with $A_{1} = 1$ . If

\underset{n \to \infty}{lim sup} \frac{A_{n}}{a_{n}} (\frac{a_{n}^{2}}{a_{n + 1}} - 1) < \infty,

then the sequence is eventually Sylvester.

Proof. Since $L_{n} / A_{n} = q / gcd (q, A_{n})$ lies in $[1, q]$ , an upper bound on the expression in the corollary gives an upper bound on $(L_{n} / a_{n}) (a_{n}^{2} / a_{n + 1} - 1)$ ; negative terms remain negative. Equation (10) therefore bounds the negative part of $V_{n}$ . Choose an integer $B$ above that eventual bound. The record series then vanishes after a finite prefix, so Theorem 6.1 applies. ◻

The expression in Erdős and Straus’s Theorem 3 is

\frac{[a_{1}, \dots, a_{k}]}{a_{k + 1}} (\frac{a_{k + 1}^{2}}{a_{k + 2}} - 1),

with a nonpositive upper limit [1]. Setting $n = k + 1$ gives exactly $(A_{n} / a_{n}) γ_{n}$ : the prefix ends before $a_{n}$ , and the growth ratio begins at $a_{n}$ . Tijdeman and Yuan extend this type of criterion to positive numerators [4]. Here any finite upper bound suffices under the quadratic-limit assumption. Since $A_{n} ∣ P_{n}$ , the LCM hypothesis is no stronger than the product hypothesis in Corollary 4.9: if the product expression is at most $B$ , the LCM expression is at most $max (B, 0)$ . When the earlier terms are pairwise coprime the two weights agree; repeated prime factors can make the LCM much smaller. This comparison does not assert the existence of a non-Sylvester rational example satisfying one bound but not the other.

The finite upper limit means an eventual upper bound; it does not require $q$ to divide the LCM of the preceding denominators. For positive integer summand numerators $b_{n}$ , the modified error is $V_{n} = b_{n} L_{n} - (a_{n} - 1) U_{n}$ . The companion, Section 6 under “Integer coefficients”, separately proves boundedness from a lower bound on $V_{n}$ and eventual constancy when $V_{n} / U_{n} \to 0$ is also assumed. The latter conclusion must not be read into the first hypothesis alone. The same section links finite examples separating them; compare Badea [3] and Tijdeman–Yuan [4]. The companion’s Section 3 compares Duverney’s signed-series criterion [2], whose printed condition is one-sided, with the stronger absolute-convergence specialisation used there. It also records the different growth hypotheses for irrationality exponents in [14]. Neither comparison is an input to the crossing theorem.

Further questions

Proposition 7.1 (necessary profile). The integer tail of a sequence satisfying Problem 1.1’s hypotheses but not its conclusion has $E_{n} \neq 0$ eventually, $| E_{n} | / C_{n} \to 0$ , unbounded negative magnitudes along negative indices, and

\sum_{n} \frac{(- E_{n})_{+}}{C_{n}} = \infty .

Proof. Absorption excludes late zeros, descent excludes an eventually nonnegative error, and Theorems 4.1 and 5.1 exclude the two finiteness conditions. ◻

For $B \geq 0$ put

F_{B} (X) = \sum_{\begin{matrix} n \in R \\ U_{n} \leq X \end{matrix}} (- V_{n} - B)_{+} .

We count record steps by their starting numerator $U_{n}$ , not by time or the running maximum. Every selected height at most $X$ is first crossed by a jump starting below $X$ , even if it lands above $X$ . Thus a non-Sylvester orbit satisfies $F_{B} (X) \geq X / P_{B} - O_{B} (1)$ , with an orbit-dependent CRT modulus $P_{B}$ ; $U_{n} \to \infty$ also makes $F_{B} (X)$ finite. It would therefore suffice to prove from growth and rationality that, for some fixed integer $B \geq 0$ ,

\begin{matrix} (13) & \underset{X \to \infty}{lim inf} \frac{F_{B} (X)}{X} = 0. \end{matrix}

The next lemma constructs an admissible weight from this vanishing lower ratio: enumerate records by $j$ and put $u_{j} = U_{n}$ , $w_{j} = (- V_{n} - B)_{+}$ . The resulting weighted series is finite, contradicting Theorem 6.1. The estimate remains unproved; the lemma changes what one must estimate, not the hypotheses available.

Lemma 7.2 (weights and linear density). Let $u_{j}$ be positive integers, let $w_{j} \geq 0$ , and put $F (X) = \sum_{u_{j} \leq X} w_{j}$ , with the sum allowed a priori to be $+ \infty$ . Then $\underset{X \to \infty}{lim inf} F (X) / X = 0$ if and only if there is a finite nonincreasing $f : [1, \infty) \to [0, \infty)$ with $\int_{1}^{\infty} f (t) d t = \infty$ and $\sum_{j} w_{j} f (u_{j}) < \infty$ .

Proof. Suppose the lower limit vanishes. Since $F$ is constant on $[m, m + 1)$ , choose integers $X_{1} < X_{2} < \dots$ with $X_{k} \geq 2^{k}$ and $F (X_{k}) \leq 2^{- k} X_{k}$ . Set

f (t) = \sum_{k \geq 1} \frac{1_{[1, X_{k}]} (t)}{X_{k}} .

This function is nonincreasing and bounded by $\sum_{k} 2^{- k}$ . Each cutoff contributes $1 - 1 / X_{k}$ to its integral, but at most $2^{- k}$ to the weighted sum. Interchanging nonnegative sums therefore gives

\int_{1}^{\infty} f (t) d t = \sum_{k} (1 - 1 / X_{k}) = \infty, \sum_{j} w_{j} f (u_{j}) = \sum_{k} \frac{F (X_{k})}{X_{k}} \leq 1.

Conversely, suppose $f$ is such a weight and $F (m) \geq c m$ for some $c > 0$ and all integers $m \geq M$ . Monotonicity and the divergent integral force $f (X) > 0$ , so $F (X) \leq f (X)^{- 1} \sum_{j} w_{j} f (u_{j}) < \infty$ . Thus partial summation applies; the nonnegative differences $f (m) - f (m + 1)$ preserve the lower bound on $F$ . For $N > M$ ,

\sum_{u_{j} \leq N} w_{j} f (u_{j}) = F (N) f (N) + \sum_{m = 1}^{N - 1} F (m) (f (m) - f (m + 1)) \geq c (M f (M) + \sum_{m = M + 1}^{N} f (m)),

every term being nonnegative. The right side diverges as $N \to \infty$ , because $\sum_{m \geq 1} f (m) \geq \int_{1}^{\infty} f (t) d t = \infty$ . ◻

Arithmetic compatibility

The remaining estimate requires the denominator recurrence as well as control of the error. For example, $C_{n} = n^{2} + 1$ , $E_{n} = - (2 n + 1)$ has vanishing relative error and the necessary scalar pattern. But at $n = 2, 3, 4$ its numerators are $5, 10, 17$ . The update $10 = 5 a_{2} - D_{2}$ forces $5 ∣ D_{2}$ , hence $5 ∣ D_{3} = a_{2} D_{2}$ ; the next update would force $5 ∣ 17$ . Thus these numerators cannot satisfy (1). The companion’s Section 14 also constructs sequences avoiding sparse fixed moduli and distinguishes that avoidance from compatibility with all later denominators. Neither property alone supplies (13).

Conversely, suppose integer sequences indexed from zero satisfy (1), with $a_{n} > 1$ , $C_{n} > 0$ , $D_{n} \geq 0$ and $E_{n} / C_{n} \to 0$ . Section 4 of the companion proves that $D_{n} > 0$ , $C_{n} / D_{n} \to 0$ , $\sum_{n} 1 / a_{n} = C_{0} / D_{0}$ and $a_{n + 1} / a_{n}^{2} \to 1$ . The vanishing remainder $C_{n} / D_{n} \to 0$ turns the finite reciprocal identities into an infinite series. A scalar profile or finite prefix does not supply it.

Problem 7.3 (growth of repeated denominator factors). For every rational-tail orbit satisfying the hypotheses but not the conclusion of Problem 1.1, must

\underset{n \to \infty}{lim sup} \frac{\log M_{n}}{n} > 0 ?

Equivalently, must there be a $K \geq 1$ for which

2^{n} \leq M_{n}^{K}

at infinitely many indices?

Section 2 gives $C_{n + 1} / C_{n} \to 1$ ; averaging logarithms therefore gives $\log C_{n} = o (n)$ . Since $1 \leq M_{n} \leq C_{n}$ , every such orbit already satisfies $\log M_{n} / n \to 0$ . A positive answer therefore holds exactly when no such orbit exists: proving it from failure of Sylvester behaviour would exclude every counterexample.

A factorial modulus for integral recursion

A constant-negative error $E_{n} = - m$ with $C_{0} = c$ gives $C_{n} = c + n m$ and the identity

\begin{matrix} (14) & D_{n} + m = (a_{n} - 1) C_{n} . \end{matrix}

In the case $m = c = 1$ , where (14) reads $D_{n} + 1 = (a_{n} - 1) (n + 1)$ , each multiplier is determined by its predecessor. The recursion is $a_{n + 1} = num (n, a_{n}) / (n + 2)$ , where

num (n, a) = (n + 1) a^{2} - (n + 2) a + (n + 3),

the forced numerator. We stop at the first nonintegral quotient. This procedure checks divisibility only; it does not impose the positivity conditions required of an infinite reciprocal-tail sequence. The formal exact-division condition requires exact division at each step.

Example A.1 (a nonintegral second step). Starting from $a_{0} = 3$ , the first numerator $num (0, 3) = 6$ is divisible by $2$ , giving $a_{1} = 3$ . The next numerator $num (1, 3) = 13$ is not divisible by $3$ , so the recursion stops.

Direct iteration can produce very large intermediate integers. To decide whether the first $h$ divisions are exact, however, it suffices to know the initial value modulo $(h + 1)!$ . Computing a pseudo-greedy orbit through residues modulo a shrinking product modulus is Koizumi’s method [10]; for the forced numerator that product is a factorial.

Theorem A.2 (factorial residue reduction). Let $h$ be a nonnegative integer and let $a, b$ be integers with $a \equiv b (\mod (h + 1)!)$ . The first $h$ steps of the recursion $a_{n + 1} = num (n, a_{n}) / (n + 2)$ , starting at index zero, are integral for $a_{0} = a$ if and only if they are integral for $a_{0} = b$ .

Proof. Division by $i + 2$ consumes that factor of the modulus; no modular inverse is required. Define $M (0, i) = 1$ and $M (h + 1, i) = (i + 2) M (h, i + 1)$ . Induct on $h$ , allowing any starting index $i$ : inputs congruent modulo $M (h, i)$ either both complete $h$ integral steps or neither does. The case $h = 0$ is immediate.

If $a \equiv b (\mod (i + 2) M (h, i + 1))$ , the integer polynomial $num (i, \cdot)$ preserves this congruence. Its values are therefore either both divisible by $i + 2$ or neither is. In the latter case both recursions stop. In the former, exact division leaves the quotients congruent modulo $M (h, i + 1)$ , and induction supplies the remaining $h$ steps. Finally $M (h, 0) = (h + 1)!$ . ◻

For $h = 1$ , the condition is $2 ∣ a^{2} - 2 a + 3$ , or equivalently that $a$ is odd. This illustrates Theorem A.2 with modulus $2! = 2$ .

The enumeration in Example 9.1 of the companion, over $2 \leq a_{0} < 5000$ , gives at most $17$ successful updates ( $18$ values including $a_{0}$ ). The seed $a_{0} = 1$ is excluded because it is fixed and violates $a_{n} \geq 2$ . This finite calculation establishes only the stated range. The infinite constant-negative exclusion requires the separate argument under the hypotheses given there.

Sources and related work

The companion Reciprocal Sums and the Sylvester Recurrence: Further Results and Proofs supplies full proofs and fixed-revision links: Section 2 for regular rates and cubic disagreement; Sections 4–5 for integer tails; Section 12 for the gcd and bounded-increment arguments; Section 6 for LCM results; Section 13 for scalar summability; and Section 14 for open estimates and failed constructions. A final map records dependencies. The auxiliary constructions satisfy only their stated hypotheses, not necessarily those of a rational reciprocal series.

For the earlier integer-remainder method see Erdős–Straus [12]. The companion’s Section 3 distinguishes polynomial Cantor series [13] and the freely selectable series of Problem #270 [15] from the present setting. The Isabelle/HOL work [16] formalises older Erdős–Straus criteria, not Problem #243. General-rate extraction uses the Gamma-ratio asymptotics in [17]; the cubic case uses the explicit $F_{n}$ .

Indexing of the canonical tails.

Section 2 starts with $C_{1} = p$ , $D_{1} = q$ . Setting $a_{0} = 1$ , $D_{0} = q$ , $C_{0} = p + q$ extends the recurrences by one update, but gives neither $a_{0} > 1$ nor strict increase at that step. The zero-based formal cubic theorem instead uses $N$ with $a_{N} > N$ , $b_{n} = n + 1$ for $0 \leq n < N$ and $b_{n} = a_{n}$ thereafter. This sequence is strictly increasing and changes the reciprocal sum by a rational finite sum without shifting $n$ or $3 / n$ on the tail. See the companion’s indexing subsection.

Verification and reproducibility

The links identify fixed-revision Lean declarations and recorded Comparator checks. The printed cubic argument uses Chebotarev; the formal square-specialisation proof uses a Dedekind-zeta pole comparison. Their common conclusion does not check each step of the printed proof. This revision includes no new Lean build, Comparator replay or independent review. The evidence record retains source-pin and index gaps, and the estimate in Section 7 remains open.

The formal factorial residue reduction uses the shrinking-modulus induction, polynomial congruence, and cancellation after exact division. Its modulus is identified by the ascending-factorial formula and its factorial value at the initial index.

References

P. Erdős and E. G. Straus, On the irrationality of certain Ahmes series, J. Indian Math. Soc. (N.S.) 27 (1964), 129–133. MR 175848.
D. Duverney, Irrationality of fast converging series of rational numbers, J. Math. Sci. Univ. Tokyo 8 (2001), 275–316. MR 1837165.
C. Badea, A theorem on irrationality of infinite series and applications, Acta Arith. 63 (1993), no. 4, 313–323, doi:10.4064/aa-63-4-313-323.
R. Tijdeman and P. Yuan, On the rationality of Cantor and Ahmes series, Indag. Math. (N.S.) 13 (2002), no. 3, 407–418, doi:10.1016/S0019-3577(02)80018-0.
P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, Monogr. Enseign. Math. 28, Geneva, 1980, p. 64.
P. Erdős, On the irrationality of certain series: problems and results, in A. Baker (ed.), New Advances in Transcendence Theory, Cambridge UP, 1988, pp. 102–109, doi:10.1017/CBO9780511897184.009.
I. O. Bado, Prime-Support Rigidity and Primitive Pseudo-Greedy Dynamics: Partial Progress on Erdős Problem #243, preprint posted September 2026, doi:10.13140/RG.2.2.36612.08325.
P. White with Claude (Anthropic), Erdős #243: working report, Erdős Problem a Day, page dated 12 August 2026. AI-assisted, unrefereed working report.
P. Stevenhagen and H. W. Lenstra, Jr., Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, 26–37, doi:10.1007/BF03027290. Page references are to the linked author version dated 23 March 1995.
J. Koizumi, Irrationality of the reciprocal sum of doubly exponential sequences, Integers 26 (2026), Paper No. A28, 17 pp., doi:10.5281/zenodo.18714404. Locators refer to this published version.
T. F. Bloom, Erdős Problem #243, accessed 28 July 2026.
P. Erdős and E. G. Straus, On the irrationality of certain series, Pacific J. Math. 55 (1974), no. 1, 85–92.
J. Hančl and R. Tijdeman, On the irrationality of polynomial Cantor series, Acta Arith. 133 (2008), no. 1, 37–52, doi:10.4064/aa133-1-3. Locators refer to the published version.
D. Duverney, T. Kurosawa and I. Shiokawa, Irrationality exponents of certain fast converging series of rational numbers, Tsukuba J. Math. 44 (2020), no. 2, 235–250, doi:10.21099/tkbjm/20204402235. Theorem locators follow the linked 14-page author version.
T. Crmarić and V. Kovač, On the irrationality of certain super-polynomially decaying series, Colloq. Math. 179 (2025), 55–68, doi:10.4064/cm9628-5-2025. Theorem locators follow arXiv:2504.18712v1.
A. Koutsoukou-Argyraki and W. Li, Irrationality Criteria for Series by Erdős and Straus, Archive of Formal Proofs, 12 May 2020. An Isabelle/HOL formalisation; the archive entry identifies the results formalised.
National Institute of Standards and Technology, Digital Library of Mathematical Functions, §5.11(iii), formula 5.11.12, accessed 16 September 2026.

Long paper, 61 pages

Reciprocal Sums and the Sylvester Recurrence: Further Results and Proofs

PDFOpen the PDF, 61 pages Open as its own page Current source

PDF and source links follow the latest files on GitHub. The web reader shows the edition published here.

Lean source files

151 source files: 147 programme or result files and 4 imported dependencies. See them in the Lean map.

The programme directory, linked result sources and their local imports. Shared files can appear in more than one programme.

GitHub lean/ErdosProblems/Erdos243/CoefficientDivisorFence.lean
GitHub lean/ErdosProblems/Erdos243/CubicNeighbourIdentity.lean
GitHub lean/ErdosProblems/Erdos243/CumulativeLcmTransfer.lean
GitHub lean/ErdosProblems/Erdos243/DynamicCancellation.lean
GitHub lean/ErdosProblems/Erdos243/FeedbackRealizability.lean
GitHub lean/ErdosProblems/Erdos243/FiniteHorizonResidue.lean
GitHub lean/ErdosProblems/Erdos243/GlobalLcmHeight.lean
GitHub lean/ErdosProblems/Erdos243/LcmCriticalBoundary.lean
GitHub lean/ErdosProblems/Erdos243/LcmRecordCrossing.lean
GitHub lean/ErdosProblems/Erdos243/LcmRecordDivergence.lean
GitHub lean/ErdosProblems/Erdos243/LcmRecordExcess.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV6/RegularRateExtractionSpec.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV8/Discrete.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV8/GeneralRateExtractionBridge.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV8/NewtonClassification.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV8/NewtonClassificationAudit.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV8/RisingQuotients.lean
GitHub lean/ErdosProblems/Erdos243/NewtonV8/SharpRegularRateGrowth.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/ArithmeticWeightedRecord.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CRTObstructionDensity.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CanonicalGrowthBounds.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CanonicalRecords.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CoprimeCores.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicDivisorObstruction.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicFieldCoordinates.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicFieldScale.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicGcdFence.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicIntegralNormalisation.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicModularDensity.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicPrimitiveNormalisation.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicQuarticCertificates.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicQuarticWindows.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicRationalRoots.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicRationalScale.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicScaleArithmetic.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicSquareCoordinates.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicWindowTransport.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/CubicZeroDensityShape.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/DensityTransport.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/FrobeniusDescent.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/GroupAPaperEndpointsAudit.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/GrowthRecordEquivalence.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/InclusiveBoundaryFinite.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/InclusiveLimsup.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/InclusiveRecordAssembly.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/InclusiveTowerBlocks.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/IntegralWeights.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/LogLogNormaliser.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/OrbitBlockArithmetic.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/PresievedCRT.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/PrimitiveMultiplierSupply.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/PrimitiveRecordBoundary.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/QuantitativeRecordDichotomy.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/ReciprocalProductAmplification.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/RecordDivisibility.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/RecordGcdReduction.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/SubcriticalRecordBoundary.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/UncentredFinite.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/UncentredSeries.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR11/WindowIncidence.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicArithmeticAudit.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicModularSquareSpecialisation.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateCanonicalBridge.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateDefect.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateDifferenceLimits.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateFiniteDifference.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateNormalisation.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRatePositiveRationalProfile.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateProductAsymptotic.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateProductEndpoint.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateQuotientBounded.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateQuotientIncrement.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateRationalProfile.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateResidualConstant.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateResidualStep.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRateSummableTail.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicRecoveryAudit.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CubicSquareSpecializationAssembly.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CutoffWeightAnalytic.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CutoffWeightConstruction.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CutoffWeightCriterion.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CutoffWeightForward.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/CutoffWeightReverse.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/InclusiveOne.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/PowerPersistence.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/RealCutoffCriterion.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/ScaleTwelve.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR20/TwoForbiddenWords.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/AmplifiedRecordEquivalence.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ChebotarevSquareSpecialisation.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ClassicalHalfspaceSigns.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/CubicProfileGcdShape.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/CubicRateExclusionChain.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/DoubleLogOrbitBound.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ExactOrbitRecordDichotomy.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ForbiddenBlockCrossing.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ForcedOrbitResidueHorizon.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/GaloisSignFlipClosure.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/MaximalGapConstant.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/NegativeMagnitudeExclusions.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/NonintegralRegularRate.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ProductDefectThresholds.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ProtectedEpochBarrierCount.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/RecordJumpEnergySeries.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ReducedDenominatorPrimePowers.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ReducedStepLocalArithmetic.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/RegularRateExtraction.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/ShiftedSignComparison.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/SlowGrowthProductIncrements.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/SlowNegativePartRecord.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/SquareSpecialisationDedekind.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/SquareSpecialisationUnconditional.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR21/WindowAvoidance.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/Arithmetic.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/CanonicalState.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/Frontier.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/LcmDefect.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/LcmStationarity.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/Limits.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/ProductDefect.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/QuantitativeTail.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/RealTail.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR7/Reduction.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR8/CanonicalNegativeMass.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR8/CanonicalWeightedRecords.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR8/Foundation.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR8/GrowthDebtSummability.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR8/WeightAnalysis.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR8/WeightedRecords.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR9/AdaptiveCoefficients.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR9/CoefficientHeight.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR9/PolynomialCorrections.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR9/ValuationPayment.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR9/WeightedRecurrence.lean
GitHub lean/ErdosProblems/Erdos243/PaperCompleteR9Packets.lean
GitHub lean/ErdosProblems/Erdos243/PaperCorrespondenceAudit.lean
GitHub lean/ErdosProblems/Erdos243/PrimitivePrefixRigidity.lean
GitHub lean/ErdosProblems/Erdos243/PrimitiveRecordBarrier.lean
GitHub lean/ErdosProblems/Erdos243/ProtectedEpochEnergy.lean
GitHub lean/ErdosProblems/Erdos243/ReciprocalTailRigidity.lean
GitHub lean/ErdosProblems/Erdos243/RecordIncrementBarrier.lean
GitHub lean/ErdosProblems/Erdos243/RepairEntropy.lean
GitHub lean/ErdosProblems/Erdos243/SaturatedSquareTransport.lean
GitHub lean/ErdosProblems/Erdos243/SlowRiseBarrier.lean
GitHub lean/ErdosProblems/Erdos243/SparseResetRecovery.lean
GitHub lean/ErdosProblems/Erdos243/UncentredRecordCharge.lean
GitHub lean/ErdosProblems/Erdos243/WeightedCRTRepair.lean
GitHub lean/ErdosProblems/Shared/DirichletPoleComparison.lean
GitHub lean/ErdosProblems/Shared/IdealCountingEuler.lean
GitHub lean/ErdosProblems/Shared/NonsquareModuloPrimes.lean
GitHub lean/ErdosProblems/Shared/QuadraticSplitPrimes.lean

Statements with Lean proofs

Lean is software that verifies a formal proof against its theorem statement and assumptions. These proofs establish only the statements listed here.

Lean proves cubic_rate_irrationality_unconditional for positive StrictMono zero-indexed $a_{n}$ with $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ . The one-based paper uses a finite-prefix bridge; general #243 remains open.
Lean proves nonintegral_regular_rate_irrational for positive StrictMono zero-indexed $a_{n}$ whenever the real coefficient lambda is greater than one and nonintegral, with $a_{n}^{2} / a_{n + 1} = 1$ + lambda/n + $o (n^{- λ})$ . Summability is derived. The one-based paper uses the same finite-prefix bridge; the unrestricted problem remains open.
The exact product-cleared tail dynamics and the defect identity, as identities in the integer state variables.
That a vanishing centred state is absorbing under strict centring, so the state is either eventually zero or nowhere zero.
That eventual vanishing of the centred state, with the next tail state nonvanishing, forces the Sylvester recurrence eventually.
That a nonnegative centred state vanishes eventually, by descent.
That the centred state cannot be eventually constant and negative, at any magnitude and any common scale.
That the negative magnitude cannot be eventually periodic with positive drift, in the regime where each magnitude is below its multiplier.
A coprimality barrier: a sequence tending to infinity with uniformly bounded upward increments cannot permanently avoid infinitely many fresh pairwise coprime moduli.
That a reduced exact tail has pairwise coprime multipliers which its numerator permanently avoids, so no such tail has a divergent numerator with bounded rise.
That the tail gcd stabilises under cofinally bounded negative magnitudes.
Conditionally: exact dynamics, eventual strict centring, an eventually bounded negative part, and normalised vanishing together force the centred state to vanish eventually.
That survival through a fixed number of forced updates depends only on the initial state modulo a factorial of the horizon.
From a strictly increasing positive integer sequence, a rational reciprocal sum and $a_{n + 1} / a_{n}^{2}$ tending to one, canonical_integer_tail_normalized derives eventual strict centring and normalised vanishing of the exact integer tail.

What these proofs do not establish

The unrestricted problem.
A uniform lower bound on the centred error for every sequence in the original problem; the canonical tail transfer does not supply this additional hypothesis.
Any exclusion of negative excursions whose magnitudes are unbounded along a cofinal set.
The Erdős–Straus weighted criterion and Duverney's conditional characterisation, which are cited rather than formalised here.

The formal record: 4 main results, 3 open obligations, 9 selected result modules, finite search evidence, Comparator review

Main results

Statements and their limits are copied from the public research record. Recorded status: registered_declarations

conditional reduction and no-go result family: bounded_negative_exclusion

Normalised vanishing and bounded rise exclude a cofinally bounded negative part.

All dynamics, bounded-rise, positivity, and vanishing hypotheses remain explicit.

ErdosProblems.Erdos243.no_cofinallyBoundedNegative_of_normalizedVanishes

locally proved signed recovery/rigidity theorem; novelty unassessed family: centered_state_dynamics

Under exact natural C/D dynamics with $a > 1, C > 0, E = D$ - (a - 1)C, strict |E| $< C$ , a uniform lower bound on E, and division-free normalized vanishing, boundedNegativePart_eventually_zero forces $E = 0$ eventually; centered-zero plus an eventually nonzero next tail recovers eventual Sylvester recurrence.

The signed theorem has a C D : ℕ → ℕ, E : ℕ → ℤ, and B : ℕ with all exact hypotheses explicit: $a > 1, C > 0$ , C(n + 1) + D(n) = a(n) · C(n), D(n + 1) = a(n) · D(n), E is the centered state D − (a − 1)C, |E| $< C$ , a uniform lower bound on E, and division-free normalized vanishing. It excludes persistent bounded negative behaviour and forces eventual centered defect zero; centered-zero plus an eventually nonzero next tail recovers Sylvester, but no reciprocal-tail irrationality follows. The unbounded negative mixed-sign branch and the prime-specific producer remain open. This is distinct from the periodic negative-orbit and cofinally bounded-negative no-go families; no novelty, priority, significance, or external-review claim is made, and no unrestricted #243 solution follows.

ErdosProblems.Erdos243.boundedNegativePart_eventually_zero

conditional analytic recovery criterion; novelty unassessed family: negative_mass_recovery

Under exact next-denominator and next-tail C/D dynamics with a, D : ℕ → ℤ, C : ℕ → ℕ, $C > 0$ , the strict centered step equation, division-free normalized vanishing, and Summable normalized negative centered mass, the centered state vanishes eventually and a follows the Sylvester recurrence eventually.

This is a conditional recovery criterion: the source theorem assumes every displayed dynamics, positivity, strict centered-step, normalized-vanishing, and summability hypothesis, and does not prove them for the original Erdős #243 orbit. Any surviving canonical orbit must have divergent normalized negative mass. It supplies no prime-specific producer, unconditional #243 endpoint, or reciprocal-tail irrationality, and makes no novelty, priority, significance, or external-review claim. It is distinct from centered_state_dynamics, which uses a uniform lower-bound hypothesis rather than summability of normalized negative mass.

ErdosProblems.Erdos243.sylvesterNext_eventually_of_summable_negativeRelativeMass

no-go result family: negative_orbit_no_go

An eventually periodic negative-error orbit with positive phase growth is impossible.

The theorem does not cover arbitrary unbounded negative behaviour.

ErdosProblems.Erdos243.no_eventuallyPeriodicNegative_orbit

Assumptions still needing proofs

Prove any one of these and the corresponding reduction above becomes unconditional.

unbounded_negative_excursions Exclude or construct exact orbits with infinitely many unbounded negative centred excursions. Checked exclusions assume bounded negative part, a fixed period, or fixed prime divisors.
derive_negative_part_bound Derive a lower bound on centred error from the original growth and rational-sum hypotheses, control unbounded negative excursions another way, or construct a counterexample.
formalise_the_published_criteria Kernel-check the Erdos-Straus weighted criterion and Duverney's conditional characterisation under explicit analytic hypotheses.

Finite search evidence

An exact search over initial states below five thousand produced forced prefixes of length seventeen and no longer. It is superseded: the constant-negative template is now excluded outright, for every seed and at every scale.

Selected Lean proof files

The public result record selects 9 modules. Browse all 151 source files in this programme’s source map, including shared result sources and local imported dependencies.

Module	Lines	Declarations	Theorems
`ErdosProblems.Erdos243.ReciprocalTailRigidity`	2441	78	68
`ErdosProblems.Erdos243.FiniteHorizonResidue`	141	10	7
`ErdosProblems.Erdos243.SparseResetRecovery`	720	23	18
`ErdosProblems.Erdos243.DynamicCancellation`	624	21	21
`ErdosProblems.Erdos243.FeedbackRealizability`	165	7	7
`ErdosProblems.Erdos243.GlobalLcmHeight`	152	13	9
`ErdosProblems.Erdos243.LcmCriticalBoundary`	388	15	14
`ErdosProblems.Erdos243.PrimitivePrefixRigidity`	136	6	4
`ErdosProblems.Erdos243.WeightedCRTRepair`	333	17	11

Comparator review

Comparator runs selected Lean proofs against separately supplied theorem statements using recorded software versions. A successful run establishes that those proofs satisfy those statements; it does not prove the unanswered questions above.

Replayed by the Comparator

Statement and type parity replayed against the pinned toolchain.

Under exact natural C/D dynamics with $a > 1, C > 0, E = D$ - (a - 1)C, strict |E| $< C$ , a uniform lower bound on E, and normalized vanishing, boundedNegativePart_eventually_zero forces $E = 0$ eventually. centeredState_eventually_zero supplies the nonnegative stabilization mechanism, and sylvesterNext_eventually_of_centered_zero recovers eventual Sylvester recurrence when the next tail is nonzero.

The signed theorem has a C D : ℕ → ℕ, E : ℕ → ℤ, and B : ℕ with all exact hypotheses explicit: $a > 1, C > 0$ , C(n + 1) + D(n) = a(n) · C(n), D(n + 1) = a(n) · D(n), E is the centered state D − (a − 1)C, |E| $< C$ , a uniform lower bound on E, and division-free normalized vanishing. It excludes persistent bounded negative behaviour and forces eventual centered defect zero; centered-zero plus an eventually nonzero next tail recovers Sylvester, but no reciprocal-tail irrationality follows. The unbounded negative mixed-sign branch and the prime-specific producer remain open. This is distinct from the periodic negative-orbit and cofinally bounded-negative no-go families; no novelty, priority, significance, or external-review claim is made, and no unrestricted #243 solution follows.

centered_state_dynamics: targeted
Constant, eventually constant, periodic, and eventually periodic negative-error orbits are excluded in their stated regimes.

The exclusions do not cover arbitrary unbounded negative behaviour.

negative_orbit_no_go: targeted_representative_periodic_theorem
Normalised vanishing excludes a cofinally bounded negative part and forces eventual Sylvester behaviour.

Every positivity, dynamics, bounded-rise, and vanishing hypothesis remains explicit.

bounded_negative_exclusion: targeted
Under exact reciprocal-tail C/D dynamics, positive tail, the strict centered-step equation, and division-free normalized vanishing, summability of the normalized negative centered mass forces centeredState to vanish eventually and recovers the Sylvester recurrence. The load-bearing theorem is supported by the exact tail-growth bound and the finite-negative-mass stabilization theorem.

The exact criterion assumes a, D : ℕ → ℤ and C : ℕ → ℕ with the declared next-denominator and next-tail dynamics, $C > 0$ , the strict centered step equation, division-free normalized vanishing, and Summable (negativeRelativeMass C (fun n ↦ centeredState (a n) (D n) (C n))). It does not prove these hypotheses for the original Erdős #243 orbit, supply a prime-specific producer, or establish an unconditional #243 endpoint or reciprocal-tail irrationality. Any surviving canonical orbit must have divergent normalized negative mass. This is distinct from centered_state_dynamics, whose recovery criterion uses a uniform lower-bound hypothesis; no novelty, priority, significance, or external-review claim is made.

negative_mass_recovery: targeted

Represented indirectly

Covered through a neighbouring selected interface, not replayed one-to-one.

A bounded-rise sequence cannot remain coprime to fresh pairwise-coprime moduli; reduced tails inherit this obstruction.

The required bounded-rise input is not automatic for the original sequence.

bounded_rise_coprimality: represented_by_stronger_selected_boundary_theorem

The result statements, their limits and the counts are copied from the public Lean repository’s published records identified by b0ebeb9add157584. These records are copied into the page when the website is built. Introductory explanations and labels are written for this site. The diagram at the top is the exception: a program draws it from numbers the papers print and tests the numerical relationships shown. Its caption and explanation are written for this site.