Reciprocal-Tail Rigidity: Theorems, Proofs and Questions

Introduction

Sylvester’s sequence $2, 3, 7, 43, 1807, \dots$ is generated by $a_{n} = a_{n - 1}^{2} - a_{n - 1} + 1$ and has reciprocal sum $1$ ; the recurrence is equivalent to the telescoping identity

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

Consequently the tail beginning with $1 / 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:

Problem 1.1 (Erdős #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$ .

See [5] and [6]. The supplied catalogue snapshot lists the problem as open [13]. 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. The polynomial $a^{2} - a + 1$ is called the Sylvester successor.

The hypothesis is asymptotic and the conclusion is exact. Clearing a rational tail as $C_{n} / D_{n}$ exposes that distinction in the integer $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ : a Sylvester tail has $E_{n} = 0$ , while quadratic growth only gives $E_{n} / C_{n} \to 0$ . Integrality alone cannot turn this relative estimate into $E_{n} = 0$ when $C_{n}$ grows. The exact dynamics retain extra information: divisors persist in the unreduced denominator $D_{n}$ , and coprimality restricts the later reduced numerators once the gcd has stabilised. When cancellation continues, persistence in the reduced denominator must be proved separately. These are the divisibility properties used by the bounded-negative and record-crossing arguments.

The cubic proof is independent of the arguments about bounded increments. For the bounded-increment proof accompanying the short note, Sections 4 and 5 give the recurrences and zero-error argument; Sections 11 and 12 supply the gcd stabilisation and CRT contradiction. Sections 6 and 7 use two different integer numerators, respectively obtained by clearing denominators with an LCM and by reducing a fraction to lowest terms. Section 13 gives the independent, elementary argument for a convergent sum of relative increases. The constant and periodic cases appear in Sections 9 and 10.

Section 3 compares the results with prior work and identifies their formalisation status. Section 14 separates questions about reciprocal tails from examples that merely avoid prescribed moduli. Appendices A and B give source locations and a finite residue calculation.

We use $z_{+} = max (z, 0)$ . Deleting a finite prefix is harmless for an eventual recurrence, but not for the coefficients in a higher-order rate. In particular, the index $n$ in $1 + 3 / n + o (n^{- 3})$ is kept fixed throughout the cubic proof. The recurrence sections also use zero-based indexing, with that convention stated where the integer sequences are introduced.

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

Irrationality at the cubic rate

The rate in the next theorem is much more specific than $a_{n + 1} / a_{n}^{2} \to 1$ : both the coefficient $3 / n$ and the error $o (n^{- 3})$ are required. It excludes a Sylvester tail, whose deviation from $1$ is $O (1 / a_{n})$ . The coefficient $3$ also puts it outside the bounded-increment criterion: the increments of the product ratio grow like a positive multiple of $n^{2}$ . We first construct the integer numerators that rationality would require, and then prove that they cannot have the resulting cubic form. The little- $o$ condition is used in the integer finite-difference argument below; it cannot simply be replaced there by $O (n^{- 3})$ .

Theorem 2.1 (cubic-rate irrationality). If strictly increasing positive integers satisfy $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ , then $\sum_{n} 1 / a_{n}$ is irrational.

For a concrete sequence satisfying the hypothesis, take

a_{1} = 8, a_{n + 1} = ⌈ \frac{n a_{n}^{2}}{n + 3} ⌉ (n \geq 1) .

It begins $8, 16, 103, 5305, \dots$ . The inequality $a_{n + 1} \geq a_{n}^{2} / 4$ gives $a_{n} \geq 4 \cdot 2^{2^{n - 1}} \geq 8$ by induction. Hence $a_{n + 1} \geq a_{n}^{2} / 4 \geq 2 a_{n}$ , so the sequence is strictly increasing. Rounding upwards gives

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

Thus its reciprocal sum is irrational. The proof of the theorem uses the following arithmetic obstruction.

Theorem 2.2 (rising-factorial cubic exclusion). Let $a, C, D : N \to Z_{> 0}$ satisfy

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

Then for every $A \in Q_{> 0}$ and every $B \in Q$ ,

\underset{X \to \infty}{lim inf} \frac{# {n \leq X : C_{n} \neq A n (n + 1) (n + 2) + B}}{X} > 0 .

In particular no such orbit satisfies $C_{n} = A n (n + 1) (n + 2) + B$ for all large $n$ .

The irrationality theorem needs only exclusion of eventual equality. Theorem 2.2 proves more: disagreement with the proposed cubic has positive lower density. The lower bound may depend on the orbit and the cubic; it is not a uniform numerical constant.

The exclusion has three steps. Agreement on arbitrarily late blocks of four consecutive indices gives a uniform bound on the common divisor of numerator and denominator. Dividing out its eventual value reduces the proposed cubic to $m n (n + 1) (n + 2) / 6 + c$ , with $m$ a positive integer and $c = \pm 1$ . Next, the two-step numerator recurrence forces a square condition at primes dividing the middle of three consecutive numerators. Chebotarev’s theorem turns this into a square in a cubic number field, and a trace calculation forces $m = 12$ . Finally, the two remaining cubics fail the exact recurrence modulo seven, at different specified residue classes of the index. The lemmas below carry out these steps in that order.

The integer tail.

Suppose $\sum_{n \geq 1} 1 / a_{n} = p / q$ with positive integers $p, q$ , and write $x_{n} = \sum_{k \geq n} 1 / a_{k}$ for the tail. Put

D_{n} = q \prod_{1 \leq k < n} a_{k}, C_{n} = D_{n} x_{n} .

Then $D_{n}$ is a positive integer, and

C_{n} = D_{n} (\frac{p}{q} - \sum_{1 \leq k < n} \frac{1}{a_{k}}) = p \prod_{1 \leq k < n} a_{k} - q \sum_{1 \leq k < n} \prod_{\begin{matrix} 1 \leq j < n \\ j \neq k \end{matrix}} a_{j}

is a positive integer as well. From $x_{n} = 1 / a_{n} + x_{n + 1}$ ,

C_{n + 1} = D_{n + 1} x_{n + 1} = a_{n} D_{n} (x_{n} - \frac{1}{a_{n}}) = a_{n} C_{n} - D_{n}, D_{n + 1} = a_{n} D_{n},

which is (1). These are the tail variables of Koizumi’s Lemma 4 [12], up to a common positive factor. Section 4 constructs these variables together with the centred error $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ , which this section does not need. The subsequent cubic exclusion uses only these integer recurrences; it does not assume a reciprocal sum. To apply its zero-based statement without shifting the rate hypothesis, adjoin $a_{0} = 1$ , $D_{0} = q$ and $C_{0} = p + q$ . The recurrences at $0$ then give $D_{1} = q$ and $C_{1} = p$ , while every original index $n \geq 1$ is unchanged. The auxiliary term $a_{0}$ need not satisfy the increasing-sequence hypothesis of the irrationality theorem: the exclusion requires only positive multipliers.

Reduction under the zero lower-density assumption

For $S \subseteq N$ write $\underset{―}{d} (S) = \underset{X}{lim inf} # (S \cap [1, X]) / X$ . The condition $\underset{―}{d} (S) = 0$ only requires these proportions to approach zero along a sequence of cutoffs; it does not require their limit to exist. The argument below uses exactly this weaker assumption. For a sequence $F$ , let $Δ F_{n} = F_{n + 1} - F_{n}$ ; higher powers of $Δ$ mean repeated forward differences. This operator is distinct from the later indexed quantity $Δ_{n}$ , the Sylvester defect.

Lemma 2.3 (periodic obstruction principle). Let $h, L$ be positive integers and let $j_{1}, \dots, j_{L}$ be fixed integer offsets. Suppose that for every sufficiently large $n$ in one residue class modulo $h$ at least one of $n + j_{1}, \dots, n + j_{L}$ lies in $S$ . Then $\underset{―}{d} (S) \geq 1 / (L h)$ .

Proof. There are $X / h + O (1)$ relevant starting indices below $X$ . Their witnesses lie below $X + O (1)$ because the offsets are fixed, and each element of $S$ serves as a witness for at most $L$ starting indices. Hence $L # (S \cap [1, X]) \geq X / h - O (1)$ , which gives the claimed lower density. ◻

Fix $A \in Q_{> 0}$ , $B \in Q$ , and suppose for contradiction that

P (n) = A n (n + 1) (n + 2) + B, S = {n : C_{n} \neq P (n)}, \underset{―}{d} (S) = 0 .

Everything through the end of Section 2.4 runs under that assumption.

Lemma 2.4 (gcd stabilisation and the primitive shape). Write $G_{n} = gcd (C_{n}, D_{n})$ . Then $6 A$ is a positive integer, $G_{n}$ divides $6 A$ for every $n$ , and $G_{n}$ is eventually equal to a positive integer $g$ . On the tail where $G_{n} = g$ , put $u_{n} = C_{n} / g$ , $v_{n} = D_{n} / g$ and $Q (n) = P (n) / g$ . Then

\begin{matrix} (2) & u_{n + 1} = a_{n} u_{n} - v_{n}, v_{n + 1} = a_{n} v_{n}, gcd (u_{n}, v_{n}) = 1, gcd (u_{n}, u_{n + 1}) = 1, \end{matrix}

and there are $m \in Z_{> 0}$ and $c \in {- 1, 1}$ with

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

Proof. Equation (1) gives $G_{n} ∣ G_{n + 1}$ and $G_{n} ∣ C_{t}$ for every $t \geq n$ . Since $\underset{―}{d} (S) = 0$ , beyond every threshold there is a block of four consecutive indices disjoint from $S$ : otherwise every block of four would meet $S$ and $\underset{―}{d} (S) \geq 1 / 4$ . On such a block $Δ^{3} C_{t} = Δ^{3} P (t) = 6 A$ , and $G_{n}$ divides each of the four values, hence divides $6 A$ . So $6 A$ is a positive integer and the divisibility chain $(G_{n})$ is bounded and stabilises at some $g$ .

On the primitive tail, $gcd (u_{n}, v_{n}) = 1$ by construction, and a prime dividing $u_{n}$ and $u_{n + 1}$ would divide $v_{n} = a_{n} u_{n} - u_{n + 1}$ , which gives $gcd (u_{n}, u_{n + 1}) = 1$ .

The polynomial $Q$ is integer-valued: it takes an integer value at every integer argument, although its coefficients need not all be integers. Indeed, let $N$ clear the denominators of its coefficients, so $N Q \in Z [X]$ and $Q (n + N) - Q (n) \in Z$ for every $n$ . A non-integral value at one argument would therefore force an exception at every late argument in one residue class modulo $N$ , and Lemma 2.3 with $L = 1$ would contradict $\underset{―}{d} (S) = 0$ . Now $Q (- 1) = Q (0) = B / g$ , so $c := B / g \in Z$ , and $m := Q (1) - Q (0) = 6 A / g$ is a positive integer, which is (3) with $c \in Z$ .

It remains to exclude $c = 0$ and every $c$ with a prime factor. Let $ℓ$ be a prime dividing $c$ , or any prime if $c = 0$ . For $n \equiv - 1 (\mod 6 ℓ)$ , write $n + 1 = 6 ℓ k$ ; then

\frac{n (n + 1) (n + 2)}{6} = ℓ k (6 ℓ k - 1) (6 ℓ k + 1), \frac{(n + 1) (n + 2) (n + 3)}{6} = ℓ k (n + 2) (n + 3),

so $ℓ$ divides both $Q (n)$ and $Q (n + 1)$ . Agreement at both indices would give $ℓ ∣ gcd (u_{n}, u_{n + 1}) = 1$ . Hence one of $n, n + 1$ lies in $S$ for every late $n \equiv - 1 (\mod 6 ℓ)$ , and Lemma 2.3 with $L = 2$ , $h = 6 ℓ$ gives $\underset{―}{d} (S) \geq 1 / (12 ℓ)$ . This contradiction leaves $c = \pm 1$ . ◻

Lemma 2.5 (the multiplier supply, and the reducible case). On the primitive tail, $gcd (a_{n}, v_{n}) = 1$ , the multipliers at distinct indices are pairwise coprime, infinitely many of them exceed $1$ , and the cubic $Q_{m, c}$ of (3) is irreducible over $Q$ .

Proof. A prime dividing $a_{n}$ and $v_{n}$ would divide $u_{n + 1}$ and $v_{n + 1}$ , against $gcd (u_{n + 1}, v_{n + 1}) = 1$ ; and every earlier multiplier divides every later $v_{n}$ , so distinct multipliers are coprime. If $a_{n} = 1$ for all large $n$ then $v_{n}$ is eventually a positive constant and $u_{n + 1} = u_{n} - v_{n}$ decreases without bound, against positivity. So infinitely many distinct primes divide late multipliers.

Suppose $Q_{m, c}$ had a rational root. Choose a prime $ℓ ∤ 6 m$ dividing a late multiplier $a_{N}$ , large enough that the root reduces modulo $ℓ$ . Then $Q_{m, c}$ vanishes modulo $ℓ$ on a full residue class, while $ℓ ∣ v_{n}$ and therefore $ℓ ∤ u_{n}$ for every $n > N$ . Agreement at any late index of that class is impossible, and Lemma 2.3 with $L = 1$ , $h = ℓ$ gives $\underset{―}{d} (S) \geq 1 / ℓ$ . ◻

A square condition from three consecutive numerators

At a prime dividing a middle numerator, the two-step recurrence forces the negative product of its neighbours to be a square. For the proposed cubic this becomes a square condition on $r^{2} - 1$ at every root of a polynomial modulo almost every prime. The next lemma turns that condition into a square in the cubic number field.

Lemma 2.6 (square specialisation). Let $f \in Q [T]$ be irreducible with root $α$ , and let $H \in Q [T]$ satisfy $H (α) \neq 0$ . If for all but finitely many primes $ℓ$ every root $r \in F_{ℓ}$ of the reduction of $f$ has $H (r)$ a square in $F_{ℓ}^{\times}$ , then $H (α)$ is a square in $Q (α)^{\times}$ .

Proof. Suppose not. Put $K = Q (α)$ and choose $β$ with $β^{2} = H (α)$ , so $K (β) / K$ is quadratic. Take a finite Galois extension $L / Q$ containing $K (β)$ and $σ \in Gal (L / K)$ restricting nontrivially to $K (β)$ , so that $σ α = α$ and $σ β = - β$ . By the Chebotarev density theorem in the form stated by Stevenhagen and Lenstra , there are infinitely many unramified rational primes whose Frobenius class in $Gal (L / Q)$ is that of $σ$ ; only the infinitude is used. Discard the finitely many primes dividing denominators or the discriminant, the prime $2$ , and those at which $β$ reduces to zero. The Frobenius elements at the primes of $L$ above a fixed $ℓ$ form that conjugacy class, so one of those primes has Frobenius exactly $σ$ . At this prime the residue field satisfies ${\overset{―}{α}}^{ℓ} = \overset{―}{α}$ and ${\overset{―}{β}}^{ℓ} = - \overset{―}{β}$ , so $\overset{―}{α} \in F_{ℓ}$ while $\overset{―}{β} \notin F_{ℓ}$ . Then $H (\overset{―}{α}) = {\overset{―}{β}}^{2}$ is a nonsquare in $F_{ℓ}$ at a root of the reduction of $f$ , against the hypothesis. ◻

The hypothesis is needed at every root and at all but finitely many primes. A favourable finite set of tested primes would not suffice.

Proposition 2.7 (the square forced by the numerator recurrence). Write $κ = m / 6$ and $η = 6 c / m$ , so that $Q_{m, c} (n) = κ f (n + 1)$ for $f (T) = T^{3} - T + η$ . Then $α^{2} - 1$ is a square in $Q (α)^{\times}$ for a root $α$ of $f$ .

Proof. Eliminating $v_{n}$ from (2) gives

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

Let $ℓ$ be a prime and $k$ an index with $ℓ ∣ u_{k}$ . Reading (4) at $n = k - 1$ modulo $ℓ$ gives $u_{k + 1} \equiv - a_{k - 1}^{2} u_{k - 1}$ , hence

\begin{matrix} (5) & - u_{k - 1} u_{k + 1} \equiv (a_{k - 1} u_{k - 1})^{2} (\mod ℓ), \end{matrix}

so $- u_{k - 1} u_{k + 1}$ is a square modulo $ℓ$ .

Let $ℓ ∤ 6 m$ and let $r \in F_{ℓ}$ be a root of $f$ . Then $r \neq 0$ and $r \neq \pm 1$ , since $f (0) = η \neq 0$ and $f (\pm 1) = η$ . Using $η = r - r^{3}$ ,

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

so at an index $k \equiv r - 1 (\mod ℓ)$ we may reduce the polynomial values in $F_{ℓ}$ . All equalities in the following calculation are in that field: $Q (k) = 0$ , $Q (k - 1) = - 3 κ r (r - 1)$ , $Q (k + 1) = 3 κ r (r + 1)$ , and

\begin{matrix} (6) & - Q (k - 1) Q (k + 1) = 9 κ^{2} r^{2} (r^{2} - 1) . \end{matrix}

If $r^{2} - 1$ were a nonsquare modulo $ℓ$ , then so would be the right side of (6), because $9 κ^{2} r^{2}$ is a nonzero square; agreement at all three of $k - 1, k, k + 1$ would then contradict (5). That prohibition recurs at every index of the class $r - 1$ modulo $ℓ$ , and Lemma 2.3 with $L = 3$ , $h = ℓ$ would give $\underset{―}{d} (S) \geq 1 / (3 ℓ)$ . So $r^{2} - 1$ is a square in $F_{ℓ}^{\times}$ at every root of every good reduction, and Lemma 2.6 applies with $H (T) = T^{2} - 1$ . ◻

The square condition forces $m = 12$

Lemma 2.8 (classification of the scales). Let $m$ be a positive integer, let $c \in {- 1, 1}$ and $η = 6 c / m$ , and suppose $T^{3} - T + η$ is irreducible over $Q$ with a root $α$ such that $α^{2} - 1$ is a square in $Q (α)^{\times}$ . Then $m = 12$ .

Proof. Choose $β \in Q (α)$ with $β^{2} = α^{2} - 1$ . The substitution $z = α + β$ is useful because its inverse is already in the same field and expresses $α$ symmetrically in $z, z^{- 1}$ . Then $(α + β) (α - β) = 1$ , so

\begin{matrix} (7) & z^{- 1} = α - β, α = \frac{1}{2} (z + z^{- 1}), \end{matrix}

and $z$ generates $Q (α)$ . Write its minimal polynomial as $Z^{3} + b Z^{2} + d Z + w$ with $b, d, w \in Q$ and $w \neq 0$ . We use the first two traces of $α$ to restrict these coefficients, then the third trace to impose $η = 6 c / m$ . All traces below are from $Q (α)$ to $Q$ . The polynomial $T^{3} - T + η$ gives

\begin{matrix} (8) & Tr α = 0, Tr α^{2} = 2, Tr α^{3} = - 3 η . \end{matrix}

Newton’s identities give $Tr z = - b$ and $Tr z^{- 1} = - d / w$ , so the first equation in (8) and (7) give

\begin{matrix} (9) & d = - b w . \end{matrix}

For the second trace, Newton’s identities and $d = - b w$ give

Tr z^{2} = b^{2} + 2 b w, Tr z^{- 2} = b^{2} - 2 b / w .

Since the trace of $1$ is $3$ , squaring (7) yields $4 Tr α^{2} = Tr z^{2} + 6 + Tr z^{- 2}$ . Substituting $Tr α^{2} = 2$ gives $b^{2} + b (w - w^{- 1}) = 1$ . Multiplication by $w$ factors this equation:

\begin{matrix} (10) & (b w - 1) (b + w) = 0 . \end{matrix}

For the third trace, the same identities give

\begin{aligned} Tr z^{3} & = - b^{3} - 3 b^{2} w - 3 w, \\ Tr z^{- 3} & = b^{3} - 3 b^{2} / w - 3 / w . \end{aligned}

The cross terms in $(z + z^{- 1})^{3}$ have trace $3 (Tr z + Tr z^{- 1}) = 0$ by (9). Thus $8 Tr α^{3} = Tr z^{3} + Tr z^{- 3}$ . Using $Tr α^{3} = - 3 η$ now gives

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

By (10), either $b = - w$ or $b = w^{- 1}$ , and (11) becomes

η = \frac{(w^{2} + 1)^{2}}{8 w} or η = \frac{(w^{2} + 1)^{2}}{8 w^{3}} .

Write $w = r / s$ with $r \in Z \ {0}$ , $s \in Z_{> 0}$ and $gcd (r, s) = 1$ . Since $η = 6 c / m$ ,

\begin{matrix} (12) & 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}} . \end{matrix}

Now $gcd (r^{2} + s^{2}, r s) = 1$ , so integrality of $m$ and $| c | = 1$ force $(r^{2} + s^{2})^{2} ∣ 48$ , hence $r^{2} + s^{2} \in {1, 2, 4}$ . With $r \neq 0$ and $s \geq 1$ the value $1$ is too small, and $4$ is not a sum of two nonzero squares, so $r^{2} + s^{2} = 2$ and $| r | = s = 1$ . Then (12) gives $m = 12 c r$ , and $m > 0$ gives $m = 12$ . ◻

The square condition leaves the two possible cubics

\begin{matrix} (13) & Q_{12, \pm 1} (n) = 2 n (n + 1) (n + 2) \pm 1 . \end{matrix}

The square condition uses three consecutive numerators. The last step also uses the preceding denominator update, so it tests four consecutive numerators instead.

The two remaining cubics fail modulo seven

Lemma 2.9 (the two forbidden words). For $Q_{12, 1}$ , every sufficiently late four-index window beginning at $n \equiv 0 (\mod 7)$ contains an exceptional index. For $Q_{12, - 1}$ , the same holds for windows beginning at $n \equiv 1 (\mod 7)$ . In either case, $\underset{―}{d} (S) \geq 1 / 7$ . No phase-free four-index obstruction is asserted.

Proof. Reduce modulo $7$ . For $c = 1$ the values of $Q_{12, 1}$ at $n = 0, 1, 2, 3$ are $1, 13, 49, 121$ , that is

\begin{matrix} (14) & (1, 6, 0, 2), \end{matrix}

and for $c = - 1$ the values at $n = 1, 2, 3, 4$ are $11, 47, 119, 239$ , that is

\begin{matrix} (15) & (4, 5, 0, 1) . \end{matrix}

Each four-term pattern recurs with period $7$ .

Index a proposed occurrence locally by $0, 1, 2, 3$ , and use $a_{i}$ for the multiplier at local index $i$ . Let $(c_{0}, c_{1}, 0, c_{3})$ be the residues of $u$ and $(d_{0}, d_{1}, d_{2}, d_{3})$ those of $v$ . Thus $c_{i + 1} = a_{i} c_{i} - d_{i}$ and $d_{i + 1} = a_{i} d_{i}$ modulo $7$ . The middle zero gives $a_{1} c_{1} = d_{1}$ , then $d_{2} = a_{1} d_{1}$ and $c_{3} = - d_{2}$ , so

\begin{matrix} (16) & d_{1}^{2} = c_{1} a_{1} d_{1} = c_{1} d_{2} = - c_{1} c_{3} . \end{matrix}

For (14) this is $- 6 \cdot 2 = 2$ , and for (15) it is $- 5 \cdot 1 = 2$ . The square roots of $2$ modulo $7$ are $3$ and $4$ , so $d_{1} \in {3, 4}$ in both cases.

The first step gives $a_{0} = (c_{1} + d_{0}) / c_{0}$ and hence $d_{1} = d_{0} (d_{0} + c_{1}) / c_{0}$ , which is legitimate because $c_{0} \in {1, 4}$ is invertible. For (14) this is $d_{1} = d_{0} (d_{0} + 6)$ , with values

(0, 0, 2, 6, 5, 6, 2) at d_{0} = 0, 1, \dots, 6,

and for (15) it is $d_{1} = 2 d_{0} (d_{0} + 5)$ , with values

(0, 5, 0, 6, 2, 2, 6) .

Both images are ${0, 2, 5, 6}$ , which misses ${3, 4}$ . All seven initial denominator residues have been displayed, so the calculation is exhaustive and rests on no unreported search.

Hence every sufficiently late window $[7 k, 7 k + 3]$ for the plus profile, and every sufficiently late window $[1 + 7 k, 4 + 7 k]$ for the minus profile, contains an element of $S$ . Windows within each family are pairwise disjoint. There are $X / 7 + O (1)$ such windows contained in $[0, X]$ , so choosing one exceptional index in each gives $# (S \cap [0, X]) \geq X / 7 - O (1)$ and therefore $\underset{―}{d} (S) \geq 1 / 7$ . This stronger local bound is not promoted to a uniform lower bound for arbitrary cubic profiles. ◻

Proof of Theorem 2.2. Assume $\underset{―}{d} (S) = 0$ . Lemmas 2.4 and 2.5 put the primitive tail in the shape (3) with $c = \pm 1$ and $Q_{m, c}$ irreducible. Each excluded branch already contradicts the assumption by producing a positive, branch-dependent lower density, namely $1 / (12 ℓ)$ or $1 / ℓ$ for the relevant prime $ℓ$ . Proposition 2.7 and Lemma 2.8 force $m = 12$ , and Lemma 2.9 then gives $\underset{―}{d} (S) \geq 1 / 7$ , the final contradiction. ◻

From an asymptotic ratio to an exact polynomial

We now connect the arithmetic exclusion to the rate in the original sequence. First compare $C_{n}$ with a sequence whose consecutive ratio is exactly $1 + λ / n$ . The remainder will have every positive-order forward difference tending to zero. A sufficiently high difference of $C_{n}$ then tends to zero as well; because it is an integer, it must vanish eventually. This is the step that turns the asymptotic estimate into a polynomial identity.

Lemma 2.10 (integer extraction at a regular rate). Let $λ > 1$ and let $C_{n}$ be positive integers with

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

Then $λ$ is an integer $d \geq 2$ , and there are $A \in Q_{> 0}$ and $B \in Q$ with $C_{n} = A n (n + 1) \dots (n + d - 1) + B$ for all large $n$ .

Proof. Put $F_{n} = Γ (n + λ) / Γ (n)$ , so that $F_{n + 1} / F_{n} = 1 + λ / n$ exactly and $F_{n} \sim n^{λ}$ by the gamma-ratio asymptotic [20]. Write $ε_{n} = o (n^{- λ})$ for the error in (17) and $z_{n} = C_{n} / F_{n}$ , so that $z_{n + 1} / z_{n} = 1 + ε_{n} / (1 + λ / n)$ . Since $λ > 1$ the errors are absolutely summable, so the product converges and $z_{n} \to K$ for some $K > 0$ , with $z_{n} - K = o (n^{1 - λ})$ . To see the stated error, put $η_{n} = sup_{k \geq n} k^{λ} | ε_{k} | \to 0$ ; the tail of the logarithmic product has absolute value at most $O (η_{n} \sum_{k \geq n} k^{- λ}) = o (n^{1 - λ})$ . The factors are positive eventually, so the limiting product is nonzero. Hence

\begin{matrix} (18) & δ_{n} := C_{n} - K F_{n} = F_{n} (z_{n} - K) = o (n) . \end{matrix}

The recurrence gives $δ_{n + 1} - δ_{n} = (λ / n) δ_{n} + ε_{n} C_{n}$ , in which the first term is $o (1)$ by (18) and the second is $o (1)$ because $C_{n} = O (n^{λ})$ . So $Δ δ_{n} \to 0$ , and therefore $Δ^{j} δ_{n} \to 0$ for every $j \geq 1$ .

For the comparison sequence, the Gamma recurrence gives

Δ F_{n} = \frac{Γ (n + 1 + λ)}{Γ (n + 1)} - \frac{Γ (n + λ)}{Γ (n)} = λ \frac{Γ (n + λ)}{Γ (n + 1)} .

Iterating this identity gives

Δ^{j} F_{n} = λ (λ - 1) \dots (λ - j + 1) \frac{Γ (n + λ)}{Γ (n + j)},

whose right side is $O (n^{λ - j})$ . Choose an integer $j > λ$ ; then $Δ^{j} F_{n} \to 0$ , so $Δ^{j} C_{n} \to 0$ . These are integers, so $Δ^{j} C_{n} = 0$ for all large $n$ . Choose $N$ beyond this threshold. The Newton forward-difference formula gives

C_{N + t} = \sum_{i = 0}^{j - 1} (\binom{t}{i}) Δ^{i} C_{N} (t \geq 0),

so $C_{n}$ agrees eventually with a polynomial with rational coefficients. Its growth $C_{n} ≍ n^{λ}$ forces the degree to be $λ$ , so $λ = d$ is an integer, and $d \geq 2$ because $λ > 1$ . For that integer $F_{n} = n (n + 1) \dots (n + d - 1)$ exactly, so (18) says that the difference of two polynomials of degree $d$ is $o (n)$ , hence constant. The leading coefficient of the rational polynomial is $K$ , so $K \in Q_{> 0}$ ; the constant difference is rational as well. This gives the stated shape with $A = K$ and $B \in Q$ . ◻

The precision in (17) carries weight. The positive integers $C_{n} = n (n + 1) (n + 2) + (- 1)^{n}$ satisfy $C_{n + 1} / C_{n} = 1 + 3 / n + O (n^{- 3})$ and are not eventually polynomial, so the little- $o$ remainder cannot in general be replaced by a big- $O$ remainder at the same exponent. That countermodel is a scalar sequence rather than an exact orbit, and it bears on Lemma 2.10 alone.

Lemma 2.11 (the tail ratio reads the growth defect). Let $a_{n}$ be strictly increasing positive integers with $a_{n + 1} / a_{n}^{2} \to 1$ and $\sum_{n} 1 / a_{n}$ rational, and let $(C_{n}, D_{n})$ be the integer tail. Write $γ_{n} = a_{n}^{2} / a_{n + 1} - 1$ . Then

\frac{C_{n + 1}}{C_{n}} = 1 + γ_{n} + O (a_{n}^{- 1}), a_{n} \geq \exp (c 2^{n}) eventually for some c > 0 .

Proof. Since $a_{n + 1} / a_{n}^{2} \to 1$ and $a_{n} \to \infty$ , there is an $N$ with $a_{n + 1} \geq a_{n}^{2} / 2 \geq 2 a_{n}$ for $n \geq N$ . Iterating $a_{n + 1} \geq a_{n}^{2} / 2$ from an index where $a_{n} > 2$ gives $a_{n} \geq \exp (c 2^{n})$ eventually. The same doubling gives, for $m > N$ ,

\frac{1}{a_{m}} \leq x_{m} = \sum_{k \geq m} \frac{1}{a_{k}} \leq \frac{2}{a_{m}},

so $x_{m} = (1 + ρ_{m}) / a_{m}$ with $0 \leq ρ_{m} = a_{m} x_{m + 1} \leq 2 a_{m} / a_{m + 1} \leq 4 / a_{m}$ , using $a_{m + 1} \geq a_{m}^{2} / 2$ . Hence

\frac{C_{n + 1}}{C_{n}} = \frac{a_{n} D_{n} x_{n + 1}}{D_{n} x_{n}} = a_{n} \cdot \frac{(1 + ρ_{n + 1}) / a_{n + 1}}{(1 + ρ_{n}) / a_{n}} = \frac{a_{n}^{2}}{a_{n + 1}} \cdot \frac{1 + ρ_{n + 1}}{1 + ρ_{n}} .

The last factor is $1 + O (1 / a_{n})$ and $a_{n}^{2} / a_{n + 1}$ is bounded, so the product is $a_{n}^{2} / a_{n + 1} + O (a_{n}^{- 1})$ . ◻

The exact identity in Section 6 gives the same estimate: $C_{n + 1} / C_{n} = 1 - E_{n} / C_{n}$ , while $0 < γ_{n} + E_{n} / C_{n} < 3 / a_{n}$ eventually. The identity follows from Theorem 5.1; its bound also uses vanishing relative error and near-quadratic growth. Equation (20) is the resulting weighted-sum application, not the identity itself.

Proof of Theorem 2.1. The hypothesis $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ gives $a_{n + 1} / a_{n}^{2} \to 1$ . Suppose $\sum_{n} 1 / a_{n}$ were rational and pass to the integer tail, so that $(a, C, D)$ satisfies (1) with every $C_{n}$ and $D_{n}$ a positive integer. By Lemma 2.11 and $a_{n} \geq \exp (c 2^{n})$ , the error term $O (a_{n}^{- 1})$ is $o (n^{- 3})$ , so

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

Lemma 2.10 at $λ = 3$ gives $C_{n} = A n (n + 1) (n + 2) + B$ for all large $n$ , with $A \in Q_{> 0}$ and $B \in Q$ . That contradicts Theorem 2.2. ◻

No restriction on the rational normalisation was assumed: the proof derives the permitted primitive leading coefficient. The two residue patterns (14) and (15), the image ${0, 2, 5, 6}$ modulo $7$ and the condition $(r^{2} + s^{2})^{2} ∣ 48$ have been calculated above. The public checkpoint also contains formalised polynomial extraction, primitive cubic normalisation and finite transport results, including the primitive-shape theorem. These are components, not an assembled proof of Theorem 2.1. No declaration of that complete irrationality implication has been identified in the supplied source index. Lemma 2.6 uses the classical finite-Galois Chebotarev theorem; its use must be justified by the number-field argument, not by finite residue computations.

Theorem 2.1 assumes neither rationality nor an integer orbit: these enter only under the supposition that the reciprocal sum is rational. Its rate implies $a_{n + 1} / a_{n}^{2} \to 1$ , so it treats a subclass of the growth sequences in Problem 1.1. It proves irrationality on that subclass, rather than constructing a Sylvester recurrence. Sylvester tails have the much smaller deviation $O (1 / a_{n})$ and do not belong to it.

Writing $P_{n} = \prod_{k < n} a_{k}$ , at the cubic rate $P_{n} / a_{n}$ grows like $n^{3}$ and its increment like $n^{2}$ . Thus neither the bounded-increment criterion nor Koizumi’s nonpositive upper-limit criterion applies. The rate also fails his $1 + o (1 / n)$ condition, and Duverney’s signed defect series diverges. We do not decide whether the LCM-weighted criteria apply; that requires information about the repeated factors in the prefix product. Conversely, Theorem 2.2 assumes only positive integer $a_{n}, C_{n}, D_{n}$ and the recurrences (1), not the near-quadratic growth limit. The two arguments therefore retain distinct hypotheses.

In familiar approximation notation, $C_{n} = q (\prod_{k < n} a_{k} \cdot \sum_{m} 1 / a_{m} - \sum_{k < n} \prod_{j < n, j \neq k} a_{j})$ is a linear form in the reciprocal sum with integer coefficients. Here these integer remainders grow like $n^{3}$ instead of tending to zero. The precision $o (n^{- 3})$ lets finite differences identify their exact polynomial form; the recurrence then excludes it. The integer example $n (n + 1) (n + 2) + (- 1)^{n}$ above explains why an $O (n^{- 3})$ error alone does not justify that polynomial conclusion.

Prior work and formalisation

Classical criteria and pseudo-greedy expansions.

The rational-tail method predates these coordinates. Erdős and Straus [15] use eventual integer remainders under a small-numerator hypothesis. In polynomial Cantor series, Hančl and Tijdeman split the numerator into finitely many shifted products. Rationality is then characterised by the vanishing of the resulting polynomial sum [16]. Their theorem provides methodological context, not a result for arbitrary arrays of signed integer coefficients: the rearrangement of the infinite sum needs boundary control, supplied there by the polynomial hypothesis. Neither result supplies the first-crossing argument for a lower error bound proved below.

Several classical results give sufficient conditions directly on the sequence $(a_{n})$ . Their hypotheses use different quantities, so the comparisons must be made separately. Koizumi’s product criterion is implied by eventual nonnegativity of the integer error $E_{n}$ , under the identification of coordinates given below. It therefore already covers the descent argument in Section 8 (see ). The original Erdős–Straus criterion instead uses a least common multiple. Erdős and Straus proved that if $lim a_{n} / a_{n - 1}^{2} = 1$ , the reciprocal sum is rational, and $(a_{n})$ has no Sylvester tail, then

\underset{n \to \infty}{lim sup} \frac{[a_{1}, \dots, a_{n}]}{a_{n + 1}} (\frac{a_{n + 1}^{2}}{a_{n + 2}} - 1) > 0,

where $[a_{1}, \dots, a_{n}]$ is the least common multiple [1]. This is the indexing in the original theorem. With $A_{r} = lcm (a_{1}, \dots, a_{r - 1})$ and $r = n + 1$ , its expression is exactly $(A_{r} / a_{r}) (a_{r}^{2} / a_{r + 1} - 1)$ , the LCM quantity in the short note. The index change is not an additional difference between those two criteria. Erdős’s 1988 survey, followed by the supplied 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 [6][13]. 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 [12]. Tijdeman and Yuan give a criterion of the same kind for Ahmes series with positive integer numerators, weighted by the least common multiple of the earlier denominators .

Duverney’s signed criterion gives a further comparison. Let $(a_{n})$ be positive integers tending to infinity and $ϵ_{n} \in {- 1, 1}$ . Under the sufficient hypothesis $\sum_{n \geq 0} | a_{n + 1} / a_{n}^{2} - 1 | < \infty$ , the sum $\sum_{n \geq 0} ϵ_{n} / a_{n}$ is rational if and only if

a_{n + 1} = a_{n}^{2} - (ϵ_{n + 1} / ϵ_{n}) a_{n} + ϵ_{n + 2} / ϵ_{n + 1}

for all large $n$ [2]. The all-positive specialisation is the form relevant here.

There is a qualification concerning the convergence assumption. Display (3.6) in that corollary has no absolute values. In the proof on pp. 299–300, the reduced auxiliary fractions $p_{n}^{'} / q_{n}^{'}$ satisfy $p_{n + 1}^{'} ∣ q_{n}^{'}$ and

p_{n}^{'} \leq p_{N}^{'} \prod_{k = N}^{n - 1} \frac{q_{k}^{'}}{p_{k}^{'}} .

The required boundedness follows if $\prod_{k \geq N} (p_{k}^{'} / q_{k}^{'})$ has a positive limit. Absolute convergence of the growth-defect series ensures this, using the summable error in Duverney’s estimate (3.3). Signed convergence alone does not justify that product step, even for positive rational factors. For each integer $m \geq 2$ , take the pair $1 + 1 / m$ , $1 - 1 / m$ successively $m$ times. The deviations cancel after every pair, and the intervening partial sums are $1 / m \to 0$ , so their series converges. But the product through the block $m = N$ is

\prod_{m = 2}^{N} {(1 - \frac{1}{m^{2}})}^{m} = \frac{(N + 1)^{N}}{2 N^{N + 1}} \sim \frac{e}{2 N} ⟶ 0;

the equality follows by cancelling powers of consecutive integers. This example does not impose $p_{n + 1}^{'} ∣ q_{n}^{'}$ . It refutes only the general product inference, not Duverney’s arithmetic criterion. We therefore use only the absolute-convergence form; the interpretation with merely signed convergence is not needed in any proof here.

In the all-positive case $ϵ_{n} = 1$ , absolute convergence also gives a direct comparison with the classical product criterion. With the one-based notation $P_{n} = \prod_{1 \leq j < n} a_{j}$ used above,

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

The ratios on the right have an absolutely convergent sum of deviations from $1$ , because the same is true of their reciprocals and those reciprocals tend to $1$ . Thus $P_{n} / a_{n}$ has a positive finite limit, and its increments tend to zero. This case already satisfies the classical nonpositive-upper-limit condition; the bounded-increment result allows a larger class of sequences.

A different quantitative question is treated by Duverney, Kurosawa and Shiokawa [17]. For rational $x_{n} > 1$ , their result assumes eventual $x_{n + 1} \geq x_{n}^{2}$ and control of the accumulated denominators of $x_{n + 1} / x_{n}^{2}$ ; it computes the irrationality exponent of a signed reciprocal series. We use it only as a restricted comparison. In particular, a Sylvester tail and the cubic rate considered here approach quadratic growth from the other side.

Badea’s positive-term criterion is adjacent but different. For a convergent series $\sum_{n} b_{n} / a_{n}$ with $a_{n}, b_{n}$ positive integers, eventual strict inequality

a_{n + 1} > \frac{b_{n + 1}}{b_{n}} a_{n}^{2} - \frac{b_{n + 1}}{b_{n}} a_{n} + 1

forces irrationality, while rationality under the corresponding non-strict inequality forces eventual equality [3]. For $b_{n} = 1$ , its hypothesis is $a_{n + 1} \geq a_{n}^{2} - a_{n} + 1$ , an inequality between consecutive denominators, not the one-step sign condition $E_{n} \geq 0$ used in integer descent. Under the standing rational-tail and growth hypotheses, however, either inequality imposed eventually forces a Sylvester tail and hence the other. Their eventual forms are equivalent in this setting; that fact does not supply either condition for a general signed error. The general positive-coefficient criterion is not identified as a checked theorem in the supplied evidence.

Koizumi’s pseudo-greedy expansion [12] chooses $a_{n}$ by rounding $x_{n}^{- 1} + 1$ to the nearest integer, with a half-integer rounded upwards. Here $x_{n}$ is the remaining sum before subtracting $1 / a_{n}$ . Thus $a_{n} = ⌊ x_{n}^{- 1} + 3 / 2 ⌋$ , and the gap $ε_{n} = x_{n}^{- 1} + 1 - a_{n}$ is the signed rounding error. Write the rational initial sum as $r = p / q$ with positive integers $p, q$ . His Lemma 4 [12] produces integers $c_{n} > 0$ , $d_{n}$ and $e_{n}$ with $x_{n} = c_{n} / d_{n}$ and $ε_{n} = e_{n} / c_{n}$ , satisfying

a_{n} = \frac{d_{n} - e_{n}}{c_{n}} + 1, c_{n + 1} = c_{n} - e_{n}, d_{n + 1} = a_{n} d_{n},

and the proof of that lemma also gives $c_{n + 1} = a_{n} c_{n} - d_{n}$ . These are the recurrences of Section 4, after matching the starting index and the initial normalization. For a sequence satisfying the hypotheses of Problem 1.1, the rounding rule is guaranteed only after a finite restart [12]. Restarting there with the tail in lowest terms gives $(c_{n}, d_{n}, e_{n})$ ; the original $(C_{n}, D_{n}, E_{n})$ on that tail is a fixed positive integer multiple of this triple, with the indices matched. Thus $E_{n} / C_{n} = ε_{n}$ is unchanged by the restart. The integer $E_{n}$ is not necessarily a numerator in lowest terms, and the rounding range is not asserted before the restart. The first identity above gives $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ ; the remaining identities are exactly the numerator and denominator recurrences, including Proposition 4.1. On an all-negative tail we later write $e_{n} = - E_{n} > 0$ for the magnitude. That local use of lower-case $e_{n}$ has the opposite sign to Koizumi’s signed integer $e_{n}$ .

His Theorem 3 [12] proves the equivalence of two assertions. Conjecture 1 asks whether, for a positive rational $r$ , the condition $ε_{n} \to 0$ forces $ε_{n} = 0$ eventually. Question 1 [12] is the question of Erdős and Graham stated as Problem 1.1 above. Two implications used below already appear in these coordinates: his Lemma 3, that $ε_{n} = 0$ forces $ε_{n + 1} = 0$ , is the absorption of Theorem 5.8, and his Proposition 1(2), that $ε_{n} \geq 0$ for all large $n$ forces $ε_{n} = 0$ for all large $n$ , is the descent of Theorem 8.1. Both statements are given in [12]. Koizumi attributes Proposition 1(2) to Badea. Its contrapositive says that a counterexample must have negative errors infinitely often; it assumes the sign is eventually nonnegative, while Theorem 12.1 below assumes only that the negative part is eventually bounded. It permits negative errors between $- B$ and $0$ and imposes no independent upper bound on positive errors; the relative-error limit is still required.

The growth hypothesis in Problem 1.1 is calibrated by two facts about Sylvester’s sequence. With $a_{1} = 2$ , it satisfies $a_{n} \sim c_{0}^{2^{n}}$ with $c_{0} = 1.2640847 \dots$ . Deleting initial terms and reindexing produces sequences with $a_{n} \sim C^{2^{n}}$ for arbitrarily large $C$ whose reciprocals still sum to a rational number [7]. 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 [7]; they attribute the sharpness observation to Erdős (1975). A sequence with $a_{n} / a_{n - 1}^{2} \to 1$ has $a_{n}^{1 / 2^{n}}$ convergent, so that criterion says nothing about the sequences of Problem 1.1, and rationality is genuinely possible there. Sylvester’s sequence is A000058 in the OEIS; A129871 is the variant $1, 2, 3, 7, 43, \dots$ with an initial $1$ prepended. For the recent literature on irrationality of Ahmes series we refer to Kovač and Tao [7], 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.

Crmarić and Kovač [18] address the neighbouring Problem #270, not Problem #243. Allowing integer $f (n) \to \infty$ in $\sum_{n} (\prod_{j = 1}^{f (n)} (n + j))^{- 1}$ gives every positive real value; imposing nondecreasing $f$ gives a measure-zero value set. The latter assertion does not rule out individual rational values. Their extension of Kakeya’s subsum argument explains why decay alone need not force irrationality when the summands remain freely selectable. The present exact denominator recurrence imposes additional compatibility, so neither direction is an implication between their theorem and ours.

The Formal Conjectures collection contains a mathematically equivalent unproved declaration, up to its zero-based indexing . Its summand is $Q$ -valued, so Lean’s Summable hypothesis asserts the existence of a sum in $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. Its role here is statement-level prior art; it supplies no proof authority, and the development in this note is independent of it. The checked results in this project include the state implications and the specified theorems about the reciprocal sequence; they are not confined to the state system. Earlier formal work on the remainder method should also be distinguished from a solution of this problem: Koutsoukou-Argyraki and Li’s Archive of Formal Proofs entry [19] records an Isabelle/HOL formalisation of Erdős–Straus (1974), Theorem 2.1, Corollary 2.10 and Theorem 3.1. That is formal prior art for those classical criteria, not an existing formal proof of Erdős #243.

Results and proof status.

The cubic-rate theorem (Theorem 2.1) is an ordinary irrationality proof with formalised components. The bounded-negative theorem (Theorem 12.1) and the scalar summability theorem (Theorem 13.1) have checked declarations. The checked theorems using a product or a least common multiple include the estimates for rational tails. The complete weighted-record statement has a proof source in the separate release; that source is not part of the main-repository build documented here. For the further record criteria, each evidence paragraph identifies the ordinary argument and the checked lemma it uses. In particular, Lemma 7.7 below proves the existence of large odd prime powers on the page; its written proof is not included in the inherited Lean receipt. The static-model conclusions in Section 14 are likewise ordinary results.

The additional bound or convergence assumption is not derived from the problem’s hypotheses. An equivalence between convergence and the desired recurrence does not prove either of them. In the stable-gcd case the record-increment theorem gives a positive lower bound for the log-log coefficient, not necessarily an infinite coefficient. All conclusions about nonzero tails retain failure of eventual Sylvester behaviour as a hypothesis.

The lower-error-bound proof is independent of the cubic argument: it uses exact updates, absorption, gcd stabilisation and a CRT first crossing. The scalar proof uses a product bound and integer descent. Section 14 states the resulting necessary conditions on a counterexample; it does not classify mixed-sign tails.

Integer numerators, denominators and errors

Write a rational reciprocal tail as $C_{n} / D_{n}$ , without requiring the fraction to be reduced. Removing $1 / a_{n}$ and clearing its denominator gives

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

We measure the difference from a Sylvester tail by $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ . These are Koizumi’s recurrences [12]; their formal definitions are the denominator update, the numerator update, and the error.

We also study these identities for arbitrary integer sequences, before constructing any reciprocal series. An exact orbit means sequences $a_{n}, C_{n}, D_{n}$ satisfying the two displayed recurrences at every index; $E_{n}$ always denotes the error just defined. Here and in the following recurrence sections the indices may start at $0$ . The terms $a_{n}$ are the multipliers, and $C_{n}, D_{n}$ are the numerator and denominator, not necessarily coprime. An exact orbit need not obey the pseudo-greedy rounding rule. That rule gives $- C_{n} / 2 \leq E_{n} < C_{n} / 2$ , whereas the absorption argument below needs only $| E_{n} | < C_{n}$ . At a negative error we write $e_{n} = - E_{n} > 0$ . For an isolated step we use $a, D, C \in Z$ without subscripts.

Proposition 4.1 (update law). For all $a, D, C \in Z$ ,

a C - D = C - (D - (a - 1) C) .

Consequently, every exact orbit satisfies $C_{n + 1} = C_{n} - E_{n}$ .

Proof. $C - (D - (a - 1) C) = a C - D$ . ◻

The identity is formalised as the update law. Thus $C_{n}$ decreases when $E_{n} > 0$ , increases when $E_{n} < 0$ , and stays unchanged when $E_{n} = 0$ . This is why bounds on the negative error become bounds on upward increments.

Example 4.2 (the Sylvester orbit). Take $a_{n} = 2, 3, 7, 43, 1807, \dots$ with $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ , and start the state at $D_{0} = C_{0} = 1$ . The two updates give

$n$	$a_{n}$	$D_{n}$	$C_{n}$	$E_{n}$
$0$	$2$	$1$	$1$	$0$
$1$	$3$	$2$	$1$	$0$
$2$	$7$	$6$	$1$	$0$
$3$	$43$	$42$	$1$	$0$
$4$	$1807$	$1806$	$1$	$0$

and $D_{n} = a_{n} - 1$ with $C_{n} = 1$ at every index: if $D_{n} = a_{n} - 1$ and $C_{n} = 1$ then $C_{n + 1} = a_{n} - (a_{n} - 1) = 1$ and $D_{n + 1} = a_{n} (a_{n} - 1) = a_{n + 1} - 1$ . Hence $E_{n} = D_{n} - (a_{n} - 1) C_{n} = 0$ throughout and the numerator never moves, which is Proposition 4.1 in the stationary case.

Construction from the reciprocal sum.

Let $T_{n} = \sum_{k \geq n} 1 / a_{k}$ and suppose $T_{0} \in Q$ . Put $D_{0}$ equal to a common denominator and $D_{n} = D_{0} a_{0} \dots a_{n - 1}$ , and set $C_{n} = D_{n} T_{n}$ . Then $C_{n} \in Z$ for every $n$ , and from $T_{n} = 1 / a_{n} + T_{n + 1}$ one gets $C_{n + 1} = a_{n} C_{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 error measures deviation from the Sylvester tail identity, and it vanishes identically on the Sylvester orbit.

The elementary identities in ReciprocalTailRigidity.lean are stated for an abstract integer system. Their reciprocal-tail interpretation is supplied separately by the checked PaperCompleteR7 modules, including the product condition for a rational reciprocal sum. The natural-state identities used in this passage include the tail realisation, the denominator realisation, and the signed update. Thus the abstract integer identities and their application to a rational reciprocal sum have separate formal statements.

Conversely, the recurrences identify a reciprocal sum when the ratio $C_{n} / D_{n}$ tends to zero. Regard that ratio as a real number, the tail ratio. Assume $a_{n} > 0$ , $D_{n} > 0$ , $C_{n + 1} + D_{n} = a_{n} C_{n}$ and $D_{n + 1} = a_{n} D_{n}$ . Dividing the numerator update by $a_{n} D_{n}$ gives $C_{n} / D_{n} = 1 / a_{n} + C_{n + 1} / D_{n + 1}$ , the one-step reciprocal identity. Iterating gives

\frac{C_{0}}{D_{0}} = \sum_{n < N} \frac{1}{a_{n}} + \frac{C_{N}}{D_{N}},

as in the finite telescoping identity. If $C_{N} / D_{N} \to 0$ , taking the limit identifies $\sum_{n} 1 / a_{n} = C_{0} / D_{0}$ , the series realisation. No growth, error bound or separate rationality hypothesis is used in these three identities. Positivity and the stated limit of $C_{n} / D_{n}$ are still required. They prove the direction from recurrences to a series; the construction from a rational reciprocal sum was given above and is also formalised in separate declarations.

Under the relative-error hypothesis used below, the required limit is automatic. Suppose $a_{n} > 1$ , $C_{n} > 0$ , $D_{n} \geq 0$ and $E_{n} / C_{n} \to 0$ on an exact integer orbit. If $D_{0} = 0$ , then $D_{n} = 0$ and $E_{n} / C_{n} = 1 - a_{n} \leq - 1$ at every index, a contradiction. Thus $D_{0} \geq 1$ and $D_{n} \geq D_{0} 2^{n}$ . For each $ε > 0$ , the update gives $C_{n + 1} \leq (1 + ε) C_{n}$ eventually. Taking $0 < ε < 1$ shows that $C_{n} / D_{n} \to 0$ , so the telescoping identity realises the reciprocal sum as $C_{0} / D_{0}$ .

The same assumptions also imply the quadratic growth limit. Put $θ_{n} = E_{n} / C_{n}$ . Then $a_{n} = D_{n} / C_{n} + 1 - θ_{n} \to \infty$ , and the exact recurrences give

\frac{a_{n + 1}}{a_{n}^{2}} = \frac{1}{1 - θ_{n}} - \frac{1}{a_{n}} + \frac{1 - θ_{n + 1}}{a_{n}^{2}} ⟶ 1.

In particular, the multipliers are strictly increasing eventually. Thus a global orbit with these positivity and relative-error assumptions already gives a sequence of the type in Problem 1.1 after deletion of a finite prefix. No separate tail-limit estimate is needed for such an orbit; without the relative-error assumption, that estimate remains a condition of the general telescoping argument.

Proposition 4.3 (scaling the numerator and denominator). For every $s, a, D, C \in Z$ ,

a (s D) = s (a D), a (s C) - s D = s (a C - D),

s D - (a - 1) s C = s [D - (a - 1) C] .

The three identities are formalised for the denominator, numerator and error. Multiplying the numerator and denominator by the same factor therefore preserves the recurrence and scales the error by that factor. When the factor divides all entries, we can divide it out instead. This is used in the finite calculation of Appendix B and in the induction in Theorem 10.1.

When a zero error forces the Sylvester recurrence

The converse to the Sylvester example follows by eliminating $D_{n}$ from two successive updates. Define

Δ_{n} = a_{n + 1} - (a_{n}^{2} - a_{n} + 1),

the Sylvester defect. The identity below relates $Δ_{n}$ to two consecutive errors. It will show both that eventual zero error forces the recurrence and that, under $| E_{n} | < C_{n}$ , a single zero error forces the next one to vanish.

Theorem 5.1 (defect identity). For all $a, a^{'}, D, C \in Z$ ,

\begin{aligned} [a^{'} - (a^{2} - a + 1)] (a C - D) & = a^{2} [D - (a - 1) C] \\ - [a D - (a^{'} - 1) (a C - D)], \end{aligned}

that is, $Δ_{n} C_{n + 1} = a_{n}^{2} E_{n} - E_{n + 1}$ .

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

The identity is formalised as the defect identity. No sign or growth hypothesis is needed for the identity itself. Such hypotheses enter only in its consequences below.

Example 5.2 (one defect and the error it creates). Continue Example 4.2 but replace $a_{3} = 43$ by $a_{3} = 44$ . The states $D_{3} = 42$ and $C_{3} = 1$ are unchanged, since they depend only on $a_{0}, a_{1}, a_{2}$ , and $E_{2} = 0$ still. The defect is $Δ_{2} = a_{3} - (a_{2}^{2} - a_{2} + 1) = 44 - 43 = 1$ , and $E_{3} = D_{3} - (a_{3} - 1) C_{3} = 42 - 43 = - 1$ , so the identity reads

Δ_{2} C_{3} = 1 \cdot 1 = 1 = 49 \cdot 0 - (- 1) = a_{2}^{2} E_{2} - E_{3} .

By Proposition 4.1 the numerator then rises, $C_{4} = C_{3} - E_{3} = 2$ . A single unit of defect at one index has produced a negative error of magnitude $1$ at the next, increasing the numerator from $1$ to $2$ .

Theorem 5.3 (two vanishing errors force the step). Let $a, a^{'}, D, C \in Z$ with $a C - D \neq 0$ . If

D - (a - 1) C = 0, a D - (a^{'} - 1) (a C - D) = 0,

then $a^{'} = a^{2} - a + 1$ .

Proof. Theorem 5.1 gives $[a^{'} - (a^{2} - a + 1)] (a C - D) = 0$ . The second factor is nonzero, so the first factor must vanish. ◻

The conclusion is formalised as the local rigidity step. The hypothesis $C_{n + 1} \neq 0$ is not removable: at $C_{n + 1} = 0$ the identity gives no information about $a^{'}$ .

Relations among three consecutive numerators

Eliminating the denominator from two successive steps gives a relation among three reduced numerators. Write $u, u_{1}, u_{2}$ for the reduced numerator coordinates, $v, v_{1}$ for the corresponding denominator coordinates, and $h, h_{1}$ for the two common factors removed in reduction. If the two steps have multipliers $a, a_{1}$ , then the exact hypotheses are

h u_{1} + v = a u, h v_{1} = a v, h_{1} u_{2} + v_{1} = a_{1} u_{1} .

Theorem 5.4 (eliminating the denominator from two steps). Let $a, a_{1}, u, u_{1}, u_{2}, v, v_{1}, h, h_{1}$ be integers satisfying

h u_{1} + v = a u, h v_{1} = a v, h_{1} u_{2} + v_{1} = a_{1} u_{1} .

Then $a^{2} u + h h_{1} u_{2} = h (a + a_{1}) u_{1}$ .

Proof. Multiply the first equation by $a$ , replace $a v$ using the second equation, and then replace $h_{1} u_{2} + v_{1}$ using the third. The remaining terms factor as the displayed right-hand side. ◻

This is the recurrence obtained by eliminating the denominator. Both cancellation factors remain in the formula. The identity adds no assumption to the two exact steps, but it still contains both multipliers and cannot by itself force $a_{1} = a^{2} - a + 1$ ; Lemma 5.6 specifies what it forgets modulo a fixed old denominator.

When neither step cancels a common factor, the same recurrence gives a square identity. Write $p, p_{1}, p_{2}$ for three consecutive numerators, $q = a p - p_{1}$ for the denominator before the first step, and $a, a_{1}$ for the two multipliers. Then

p_{2} + a^{2} p = (a + a_{1}) p_{1} .

The resulting square identity is as follows.

Theorem 5.5 (a square identity without cancellation). Let $a, a_{1}, p, p_{1}, p_{2}, q$ be integers with $q = a p - p_{1}$ and $p_{2} + a^{2} p = (a + a_{1}) p_{1}$ . Then

q^{2} + (p p_{2} - p_{1}^{2}) = (a_{1} - a) p p_{1} .

Proof. Substitute $q = a p - p_{1}$ and $p_{2} = (a + a_{1}) p_{1} - a^{2} p$ :

\begin{aligned} q^{2} + p p_{2} - p_{1}^{2} & = (a p - p_{1})^{2} + p ((a + a_{1}) p_{1} - a^{2} p) - p_{1}^{2} \\ = (a_{1} - a) p p_{1} . \end{aligned}

◻

The term $q^{2}$ is nonnegative, while $p p_{2} - p_{1}^{2}$ measures the difference between the product of the outer numerators and the square of the middle one. The right side records the change in multiplier, so the identity gives a necessary algebraic constraint without asserting a sign or a global monotonicity. It is checked as the square identity when no factor is cancelled; no global exclusion of approximate solutions is claimed.

The reduced error update must also be compatible with the denominator recurrence. The following calculation gives the exact compatibility condition. Here $e, e_{1}$ are signed errors in reduced coordinates, not the positive magnitudes denoted by $e_{n}$ in the all-negative case. Let $Δ$ be a proposed value of the Sylvester defect. If

h u_{1} = u - e, h e_{1} = a^{2} e - Δ (u - e),

then the denominator equality

h ((a_{1} - 1) u_{1} + e_{1}) = a ((a - 1) u + e)

holds precisely when the following difference vanishes:

\begin{aligned} h ((a_{1} - 1) u_{1} + e_{1}) - a ((a - 1) u + e) \\ = [a_{1} - (a^{2} - a + 1) - Δ] (u - e) . \end{aligned}

Consequently, when $u - e \neq 0$ ,

h ((a_{1} - 1) u_{1} + e_{1}) = a ((a - 1) u + e) ⟺ a_{1} = a^{2} - a + 1 + Δ .

The equivalence with the denominator recurrence is formalised using the factored difference between the two recurrences. The hypothesis $u - e \neq 0$ is essential: if $u - e = 0$ , the factorised mismatch cannot identify $a_{1}$ .

The identities hold under the local hypotheses displayed in their statements. It is their proposed global applications, not the identities, that would need additional information, such as control of cancellation or a sign estimate for $p p_{2} - p_{1}^{2}$ . No such information is deduced here for an arbitrary rational near-quadratic tail.

Lemma 5.6 (saturation modulo an old denominator). Let $M \geq 2$ . Any finite word $r_{0}, \dots, r_{k}$ of units modulo $M$ is compatible with the cancellation-free recurrences modulo $M$ , with all reduced denominator residues equal to zero. Consequently the eliminated two-step identity alone imposes no further restriction on such unit words when the multiplier residues are free.

Proof. Set $v_{i} \equiv 0 (\mod M)$ and choose $a_{i} \equiv r_{i + 1} r_{i}^{- 1} (\mod M)$ . Then $r_{i + 1} + v_{i} \equiv a_{i} r_{i}$ and $v_{i + 1} \equiv a_{i} v_{i}$ . Eliminating $v_{i}$ gives the two-step identity automatically. ◻

This is finite residue compatibility, not existence of a positive integer orbit, much less a rational tail with near-quadratic growth. For $M ∣ v_{T}$ on a tail with no further common-factor cancellation, the actual $u_{n}$ are indeed units modulo $M$ . Useful further restrictions must therefore retain information discarded here: for example multiplier size, changing moduli, or primes outside the old denominator. The square restriction used in the cubic proof concerns precisely a prime at which a middle numerator vanishes.

Theorem 5.7 (sequence form). Let $a, D, C : N \to Z$ satisfy $D_{n + 1} = a_{n} D_{n}$ and $C_{n + 1} = a_{n} C_{n} - D_{n}$ . If $E_{n} = 0$ for all sufficiently large $n$ and $C_{n + 1} \neq 0$ for all sufficiently large $n$ , then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ for all sufficiently large $n$ .

The sequence form is formalised as the eventual Sylvester recurrence. Take the larger of the two thresholds and apply Theorem 5.3 at each later index. This is the final step of the criteria below that force $E_{n}$ to vanish eventually.

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

Theorem 5.8 (zero is absorbing). Let $a, C, D : N \to N$ be an exact orbit of natural numbers, so $C_{n + 1} + D_{n} = a_{n} C_{n}$ and $D_{n + 1} = a_{n} D_{n}$ , and let $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ . Suppose the centring is strict, $| E_{n} | < C_{n}$ for every $n$ . If $E_{n} = 0$ then $E_{n + 1} = 0$ .

Proof. Putting $E_{n} = 0$ in Theorem 5.1 gives $Δ_{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. ◻

The conclusion is formalised as the absorption of a vanishing error, with the companion contrapositive along a tail: if zero is absorbing beyond some index and $E$ does not vanish eventually, then $E$ is nowhere zero beyond that index.

Beyond an eventual centring threshold, either $E$ reaches zero and stays there, or it is nowhere zero. A zero before that threshold need not persist, as Example 5.2 shows: the altered multiplier creates $E_{3} = - 1$ with $C_{3} = 1$ , exactly where strict centring fails. Sections 9 and 10 address the special all-negative case. The mixed-sign analysis in Sections 12 and 13 separates arbitrarily late negative errors from an eventually nonnegative tail.

A criterion using new maxima of an LCM numerator

Clear each rational tail with a least common multiple rather than a product. The resulting numerator is a positive integer. We will show that the Sylvester recurrence is equivalent to convergence of a weighted sum over steps at which this numerator exceeds all its previous values. The first-crossing proof permits a fixed amount to be subtracted from each such increase. The equivalence is not a proof of convergence under the original hypotheses.

Formalisation.

The proof below is ordinary mathematics. The first-crossing arithmetic has formalised components in LcmRecordExcess.lean. In addition, the separate release contains the complete criterion for real-valued weights and its natural-weight version. These release sources contain proof bodies, but they are outside the supplied successful main-repository build; a Comparator configuration alone is not a replay receipt. The finite-orbit data retained with the source are diagnostic examples, not a proof of termination for all rational seeds.

The sum counts only steps setting new maxima and subtracts the same fixed amount from each actual jump. Unlike Koizumi’s eventual-nonnegative case in Proposition 1(2), it permits both signs of the error. The weaker model in Proposition 7.15 assumes only nondivisibility by whole moduli. It omits both coprimality to their prime factors and the denominator recurrence, so its counterexamples do not refute an argument using those additional properties.

In this section the indices start at $0$ . Write the full reciprocal sum as $p / q$ , with positive integers $p, q$ , put $x_{n} = \sum_{k \geq n} 1 / a_{k}$ , and take $D_{0} = q$ . Set

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

The rational tail has denominator dividing $L_{n}$ , so $U_{n} = L_{n} x_{n}$ and $V_{n}$ are integers. This clears the denominator but need not reduce the fraction: $U_{n}$ and $L_{n}$ may still have common factors. 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 are Bado’s LCM coordinates, with the indexing translated explicitly. Take his denominator parameter to be $q$ and identify his $a_{n + 1}$ with our $a_{n}$ . Then his $M_{n}$ , $Δ_{n}$ , $K_{n}$ , $u_{n + 1}$ and $g_{n + 1}$ are respectively our $L_{n}$ , $M_{n}$ , $U_{n}$ , $V_{n}$ and $ρ_{n}$ . His (19) becomes the middle update above [8].

Write $R_{n} = max_{j \leq n} U_{j}$ and $R = {n : U_{n + 1} > R_{n}}$ . Strict centring already gives $U_{n + 1} < U_{n}$ when $ρ_{n} \geq 2$ , so every sufficiently late strict rise has $ρ_{n} = 1$ . The stronger eventual bound $- U_{n} \leq 2 V_{n}$ , supplied by $V_{n} / U_{n} = E_{n} / C_{n} \to 0$ , gives the quantitative estimate $U_{n + 1} \leq 3 U_{n} / 4$ when $ρ_{n} \geq 2$ . At a sufficiently late LCM record, $ρ_{n} = 1$ and the actual jump is $d_{n} = U_{n + 1} - U_{n} = - V_{n} > 0$ . At a contracting step with $ρ_{n} \geq 2$ this identity need not hold.

Theorem 6.1 (boundedness and a weighted sum over new maxima). Let $a_{n}, L_{n}, U_{n}$ be positive integers and $V_{n}$ integers satisfying

\begin{matrix} L_{n + 1} = lcm (L_{n}, a_{n}), ρ_{n} = gcd (L_{n}, a_{n}), \\ ρ_{n} U_{n + 1} = U_{n} - V_{n}, V_{n} = L_{n} - (a_{n} - 1) U_{n}, - U_{n} \leq 2 V_{n} . \end{matrix}

Let $f : [1, \infty) \to [0, \infty)$ be finite and nonincreasing, with $\int_{1}^{\infty} f (t) d t = \infty$ . For each fixed integer $B \geq 0$ ,

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

Proof. A bounded integer running maximum increases only finitely many times, so bounded $U_{n}$ gives a finite sum. Suppose instead that $U_{n}$ is unbounded. There are infinitely many record rises, each with $ρ_{n} = 1$ . Its multiplier is greater than one because $d_{n} = (a_{n} - 1) U_{n} - L_{n} > 0$ . If $r < s$ are record indices, then $a_{r} ∣ L_{s}$ and $gcd (a_{s}, L_{s}) = 1$ , hence $gcd (a_{r}, a_{s}) = 1$ . The record multipliers are therefore distinct and pairwise coprime. For any fixed $B \geq 1$ , choose $B$ of them greater than $B$ , and take $T$ after their indices. These earlier multipliers $m_{0}, \dots, m_{B - 1}$ all divide $L_{T}$ .

Put $P = \prod_{i} m_{i}$ and choose $x$ by the Chinese remainder theorem with $m_{i} ∣ x + i$ . Consider the heights $τ = x + B + k P > R_{T}$ , $k \in Z$ . We first show that a crossing requires $d_{n} > B$ , then count how many heights one jump can cross. A first crossing $U_{n} \leq R_{n} < τ \leq U_{n} + d_{n}$ is a record step. If $d_{n} \leq B$ , then $U_{n} \in [τ - B, τ)$ , so some $m_{i}$ divides $U_{n}$ . It also divides $L_{n}$ , hence divides $d_{n} = (a_{n} - 1) U_{n} - L_{n}$ , contradicting $0 < d_{n} \leq B < m_{i}$ .

If the step first crosses $h \geq 1$ such heights, their spacing gives $(h - 1) P < d_{n}$ . With $r = d_{n} - B \geq 1$ and $P \geq B + 1$ , we have $d_{n} = B + r \leq P r$ , whence $h \leq r$ . Monotonicity of $f$ now gives

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

Each selected height has one first crossing, and the first selected height is at most $R_{T} + P$ . Summing and comparing each interval of length $P$ with its left endpoint gives, for $R_{N} \geq R_{T} + P$ , the finite bound

\begin{matrix} (19) & \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$ . The case $B = 0$ follows by domination. ◻

Only the lower centring bound was used. In particular, neither vanishing relative error nor a growth estimate for $C_{n}$ supplies the CRT moduli: the record multipliers themselves do so. Vanishing relative error enters in the following application to the original sequence.

Theorem 6.2 (a convergent weighted sum over new maxima). Assume the growth and rationality hypotheses of Problem 1.1, and let $f$ be as in Theorem 6.1. 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 .

Proof. If the sequence is not eventually Sylvester, zero error is never reached on a sufficiently late tail. Integrality gives $1 / U_{n} \leq | V_{n} | / U_{n} = | E_{n} | / C_{n} \to 0$ , so $U_{n}$ is unbounded. Theorem 6.1, applied after the centring threshold, forces divergence for every $B$ . Once the running maximum of the retained tail exceeds the omitted prefix maximum, deleting that prefix no longer changes which steps set new records. Unboundedness ensures that this crossing occurs. Conversely, a Sylvester tail telescopes to $x_{n} = 1 / (a_{n} - 1)$ , so $V_{n} = 0$ eventually. ◻

The weights $f (t) = 1 / t$ and $f (t) = 1 / [t \log (e t)]$ are admissible: they are nonnegative and nonincreasing, but their integrals diverge. The faster-decaying weight $1 / t^{2}$ is not admissible. The divergence requirement is used at the last line of the crossing argument; without it, unbounded numerators need not make the lower bound diverge. 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 (19) 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. These are specialisations of one crossing theorem.

The criterion also has an exact expression in the original growth defect. 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. Thus the two nonnegative 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}$ . To see summability directly, put $P_{n} = \prod_{j < n} a_{j}$ . The tail estimate $x_{n} \sim 1 / a_{n}$ gives $C_{n} / a_{n} \sim q P_{n} / a_{n}^{2}$ , and

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

Thus $\sum_{n} C_{n} / a_{n} < \infty$ by the ratio test. Since $U_{n} \leq C_{n}$ and $f (U_{n}) \leq f (1)$ , the comparison error is summable. Consequently Theorem 6.2 is equivalent to finiteness of

\begin{matrix} (20) & \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$ . The original hypotheses do not currently supply this finiteness. In particular, termwise convergence to zero is insufficient. The corresponding formal comparison starts from the same positive, strictly increasing integer sequence, its rational reciprocal sum and the near-quadratic growth limit. It uses the summand in (20) at record indices and zero elsewhere, with the same class of weights and existential choice of $B$ . The formal estimate uses the same ratio-test argument, with the sufficient constant $16$ in place of $3$ . This transfers the criterion; it does not supply the required finiteness from the original hypotheses. The separate-release source GrowthDebtSummability.lean contains the factored-growth formulation. It is outside the documented main-repository build. The on-page comparison above is an ordinary proof; this prose revision does not constitute a new Lean check of that release.

The crossed heights lie above $R_{n}$ , but the divisibility argument uses the starting numerator $U_{n}$ and the full jump $U_{n + 1} - U_{n}$ . Replacing this by $R_{n + 1} - R_{n}$ would discard the recovery from an earlier decrease.

Integer coefficients.

The following extension is not used in either the bounded-increment proof or the cubic-rate argument. We give the proof here to keep the short note’s comparison separate from its main unit-fraction argument.

The first-crossing argument also works when the summand has an integer numerator $b_{n}$ . In that case

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

Assume that $a_{n} \geq 2$ , that $L_{n}, U_{n}$ are positive integers, and that $L_{n + 1} = lcm (L_{n}, a_{n})$ , with $ρ_{n} = gcd (L_{n}, a_{n})$ . Suppose $V_{n} \geq - B$ eventually, with an integer $B \geq 0$ . Then $U_{n + 1} \leq U_{n} + B$ ; if $B = 0$ , boundedness follows at once. For $B \geq 1$ , a record step with $R_{n} > B$ must have $ρ_{n} = 1$ , since $ρ_{n} \geq 2$ would give

U_{n + 1} \leq \frac{U_{n} + B}{2} \leq \frac{R_{n} + B}{2} < R_{n} .

Thus an unbounded sequence would supply infinitely many pairwise coprime record multipliers. Choose $B$ of them larger than $B$ , and then a CRT block of $B$ consecutive integers above the previous maximum, each divisible by one of the chosen multipliers. The first step past the upper end of the block is a high record step, so $ρ_{n} = 1$ . Its positive jump is at most $B$ , hence the preceding numerator $U_{n}$ lies in the block. The corresponding multiplier divides both $U_{n}$ and $L_{n}$ , hence divides the jump $(a_{n} - 1) U_{n} - b_{n} L_{n}$ . A positive jump at most $B$ cannot have a divisor larger than $B$ . This also explains why no growth assumption on $a_{n}$ , centring, or relative-error limit is needed for boundedness.

With the additional limit $V_{n} / U_{n} \to 0$ , choose an integer $K$ bounding $U_{n}$ . Eventually $| V_{n} | < U_{n} / K \leq 1$ , so the integer $V_{n}$ is zero. The recurrence becomes $ρ_{n} U_{n + 1} = U_{n}$ ; the positive integer sequence $U_{n}$ is then nonincreasing and hence eventually constant. For positive $b_{n}$ , the classical comparisons are Badea’s Corollary 2.2 [3] and the criterion of Tijdeman and Yuan [4]. Further finite examples separating boundedness from stationarity are in the coefficient proof supplement.

New maxima of reduced numerators

In Section 6, a prime divisor of $L_{n}$ continues to divide every later $L_{j}$ . This section instead writes the reciprocal tail in lowest terms as $u_{n} / v_{n}$ . Cancellation can then remove prime factors from $v_{n}$ , so their persistence needs a separate proof. The criteria below use the size of new maxima of $u_{n}$ and the prime powers that remain in its denominator. They do not identify $u_{n}$ with the LCM numerator $U_{n}$ .

Fractions in lowest terms.

Put

G_{n} = gcd (C_{n}, D_{n}), u_{n} = C_{n} / G_{n}, v_{n} = D_{n} / G_{n}, {\tilde{e}}_{n} = E_{n} / G_{n} .

Thus $gcd (u_{n}, v_{n}) = 1$ and ${\tilde{e}}_{n}$ is a signed integer. The factor $h_{n} = G_{n + 1} / G_{n}$ records the common factor removed at the next step. The relation to the preceding section is exact:

\frac{G_{n}}{M_{n}} = gcd (U_{n}, L_{n}), u_{n} = \frac{U_{n}}{gcd (U_{n}, L_{n})}, v_{n} = \frac{L_{n}}{gcd (U_{n}, L_{n})} .

Indeed, $C_{n} = M_{n} U_{n}$ and $D_{n} = M_{n} L_{n}$ . Clearing with an LCM and reducing to lowest terms are different operations. For example, the exact step $(C, D, a) = (3, 6, 3)$ has $E = 0$ and gives $(C^{'}, D^{'}) = (3, 18)$ . With $L = 6$ , its LCM numerator falls from $3$ to $1$ , while the reduced numerator stays $1$ : the LCM factor is $ρ = 3$ , but the reduction factor is $h = 1$ . This step begins a Sylvester tail.

In general, before reduction the next numerator is $w_{n} = a_{n} u_{n} - v_{n} = u_{n} - {\tilde{e}}_{n}$ , so

h_{n} u_{n + 1} = w_{n}, h_{n} v_{n + 1} = a_{n} v_{n}, gcd (u_{n}, u_{n + 1}) = 1.

The negative magnitude $e_{n} = - E_{n}$ used earlier is not ${\tilde{e}}_{n}$ ; neither is Koizumi’s real gap $ε_{n}$ .

For the maxima and their increments write

R_{n} = max_{k \leq n} u_{k}, H_{n} = max_{j \leq n} C_{j}, s_{n} = R_{n + 1} - R_{n} .

At a strict rise let $d_{n} = u_{n + 1} - u_{n}$ . Then $s_{n} = (d_{n} - (R_{n} - u_{n}))_{+}$ . Thus the actual jump includes recovery of the earlier decrease $R_{n} - u_{n}$ , whereas the record increment does not. For example, if $R_{n} = 10$ , $u_{n} = 5$ and $u_{n + 1} = 12$ , then $s_{n} = 2$ but $d_{n} = 7$ . This illustrates the definitions, not a claimed reciprocal-tail orbit. We will use

m_{n} = (- {\tilde{e}}_{n})_{+}, A_{n} = \frac{R_{n}}{u_{n}} m_{n}, δ_{n} = {(\frac{a_{n}^{2}}{a_{n + 1}} - 1)}_{+}, ℓ (x) = \log_{2} \log_{2} max (4, x) .

The factor $R_{n} / u_{n}$ in $A_{n}$ measures how far the current numerator has fallen below its previous maximum. It equals one at a maximum and can be large after a decrease. The symbol $A_{n}$ is distinct from the prefix product $A_{n}$ used later.

Unless a statement in this section specifies an abstract recurrence, we assume the hypotheses of Problem 1.1 and use its integer tails, for which $| E_{n} | / C_{n} \to 0$ after a finite shift. We will write out the conclusion $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ eventually rather than give it a separate symbol.

Comparison with Duverney’s reduced parameters.

For the positive reciprocal series, the eventually reduced parameters in Duverney’s Theorem 3.1 and Section 5.2 [2] can be taken as follows. The symbols $p_{n}, q_{n}$ in this comparison are Duverney’s auxiliary integers, not the fixed numerator and denominator of the full reciprocal sum:

p_{n} = u_{n}, q_{n} = w_{n} = a_{n} u_{n} - v_{n} = h_{n} u_{n + 1}, E_{n} = G_{n} (p_{n} - q_{n}) .

Indeed, $gcd (u_{n}, w_{n}) = gcd (u_{n}, v_{n}) = 1$ . Since $a_{n} v_{n} = a_{n}^{2} u_{n} - a_{n} w_{n}$ , reduction of the next tail gives

h_{n} = gcd (w_{n}, a_{n} v_{n}) = gcd (w_{n}, a_{n}^{2}), p_{n + 1} ∣ q_{n} .

For the gcd equality, subtract the multiple $a_{n} w_{n}$ and use the coprimality of $u_{n}, w_{n}$ ; the divisibility follows from $q_{n} = h_{n} p_{n + 1}$ . Eliminating $v_{n + 1}$ then gives Duverney’s recurrence:

a_{n + 1} = \frac{p_{n}}{q_{n}} a_{n}^{2} - a_{n} + \frac{q_{n + 1}}{p_{n + 1}} .

Thus $q_{n} / p_{n + 1} = h_{n}$ is precisely the cancellation factor, and $q_{n} / p_{n} \to 1$ . This identifies the reduced parameters, not every possible unreduced choice in the original theorem. An upper bound on $q_{n} - p_{n}$ controls the increase before cancellation in the reduced coordinates. To transfer that bound directly to $(- E_{n})_{+} = G_{n} (q_{n} - p_{n})_{+}$ would also require control of $G_{n}$ .

The source references distinguish complete Lean proofs from written arguments that use formalised lemmas. The supplied index records a build of the listed public modules at revision 6b78209ab63a; the links below retain their original revisions. It separately records successful Comparator checks for specified theorems in the release, not a build of that release as a whole. A challenge statement containing sorry is not a proof, and a configuration entry alone does not record a successful check. Citing a formalised lemma does not discharge the extra hypotheses or steps of the written argument using it.

Lemma 7.1 (the denominator valuation transition). Let $u, v, a$ be positive integers, $gcd (u, v) = 1$ , and $w = a u - v > 0$ . Put $h = gcd (w, a v)$ and $v^{'} = a v / h$ . For a prime $p$ , write $r = ν_{p} (a)$ , $s = ν_{p} (v)$ and $t = ν_{p} (w)$ . Then

ν_{p} (v^{'}) = {\begin{cases} max (r, s), & r \neq s, \\ max (0, 2 s - t), & r = s . \end{cases}

In particular $ν_{p} (v^{'}) \leq max (r, s)$ . A strict loss relative to $s$ requires $r = s \geq 1$ and $t > s$ .

Proof. Always $ν_{p} (v^{'}) = r + s - min (t, r + s)$ . If $r \neq s$ , primitivity implies $t = min (r, s)$ : when $s > 0$ , $u$ is a $p$ -adic unit, and when $s = 0 < r$ , $v$ is a unit. If $r = s > 0$ , both terms in $a u - v$ are divisible by $p^{s}$ , so $t \geq s$ ; substituting gives the second case. If $r = s = 0$ , the same formula gives zero without needing $u$ to be a unit. ◻

Cancellation is not the same as a fall in the reduced denominator valuation. For example, $(u, v, a) = (2, 15, 9)$ gives $w = 3$ , $h = 3$ and $(u^{'}, v^{'}) = (1, 45)$ . The numerator before cancellation exceeds $u$ by only $w - u = 1$ , yet the $3$ -adic valuation of the reduced denominator rises from $1$ to $2$ . This is a finite exact step, not an infinite counterexample.

Corollary 7.2 (persistence of a prime power). Suppose $p^{k} ∣ v_{s}$ . If $w_{n} < p^{k + 1}$ at every step from $s$ through $t - 1$ , then $p^{k} ∣ v_{t}$ .

Proof. At a first loss of divisibility by $p^{k}$ , the current exponent is some $j \geq k$ and the valuation lemma forces $ν_{p} (w_{n}) > j$ . This would give $w_{n} \geq p^{j + 1} \geq p^{k + 1}$ , contrary to the hypothesis. ◻

These are ordinary local calculations. They explain the persistence threshold used below without identifying any new Lean declaration.

How fast the running maximum must increase

Theorem 7.3 (increments of the running maximum). Let $Θ = \underset{n}{lim sup} (H_{n + 1} - H_{n}) / ℓ (H_{n})$ on a rational-tail orbit under the standing hypotheses, and suppose $E_{n}$ is not eventually zero. Then either $G_{n}$ is unbounded and $Θ$ is infinite, or $G_{n}$ stabilises at a value $g$ and $Θ \geq g v_{T} / φ (v_{T})$ for every late $T$ , so that $Θ > g \geq 1$ . For any orbit under the standing hypotheses, therefore, $Θ = 0$ or $Θ > 1$ , and $Θ \leq 1$ forces the eventual Sylvester recurrence.

The constant in the next condition is measured against a double logarithm, not against $C_{n}$ . This grows much more slowly than any positive power of $C_{n}$ . Every fixed bound on $(- E_{n})_{+}$ satisfies it on a nonzero tail because $C_{n} \to \infty$ ; it also permits unbounded negative parts on the double-logarithmic scale, with the coefficient specified below. In contrast, an error of size $\sqrt{C_{n}}$ has relative size tending to zero but violates the condition. These are comparisons of bounds, not constructions of reciprocal tails.

Corollary 7.4 (the double-logarithmic bound). If

\underset{n}{lim sup} \frac{(- E_{n})_{+}}{ℓ (C_{n})} \leq 1,

then the sequence is eventually Sylvester. Every counterexample therefore satisfies

\underset{n}{lim sup} \frac{(- E_{n})_{+}}{ℓ (C_{n})} > 1.

Proof of Theorem 7.3 and Corollary 7.4. We first prove the auxiliary lower bound $Θ \geq 1$ . This part needs only an exact positive integer orbit with $a_{n} > 1$ , $D_{0} \geq 1$ , $| E_{n} | / C_{n} \to 0$ and error not eventually zero. In particular, it will also apply to the abstract orbit in Theorem 7.11. The key input is that, outside a set of indices of density zero, $a_{n}$ is coprime to the entire preceding denominator $D_{n}$ . This supplies almost one new coprime modulus per step. The denominator growth then places the resulting CRT block at the required double-logarithmic height.

How often a multiplier is coprime to the preceding denominator. We use the LCM factorisation from Section 6. In the present zero-based indexing, put

L_{n} = lcm (D_{0}, a_{0}, \dots, a_{n - 1}), M_{n} = D_{n} / L_{n}, ρ_{n} = gcd (L_{n}, a_{n}) .

The finite telescoping identity gives

\frac{C_{n}}{M_{n}} = L_{n} (\frac{C_{0}}{D_{0}} - \sum_{j < n} \frac{1}{a_{j}}) \in Z_{> 0} .

Thus $M_{n} ∣ C_{n}$ , while $M_{0} = 1$ and $M_{n + 1} = ρ_{n} M_{n}$ . Since $L_{n}$ and $D_{n}$ have the same prime divisors,

# {n < N : gcd (a_{n}, D_{n}) > 1} = # {n < N : ρ_{n} > 1} \leq \log_{2} M_{N} \leq \log_{2} C_{N} = o (N) .

Here the last estimate follows by summing $\log (C_{n + 1} / C_{n}) = \log (1 - E_{n} / C_{n}) = o (1)$ . This is the density-one coprimality argument of Bado , written with the exact-orbit hypotheses used here. Only the finite telescoping identity is needed; no estimate on record increments has entered this count.

Choosing the moduli and controlling their product. Absorption and vanishing relative error give $C_{n} \to \infty$ , hence $H_{n} \to \infty$ . The maximum is still subexponential: for every $ε > 0$ , choose $K_{ε}$ with $C_{j} \leq K_{ε} e^{ε j}$ for every $j$ . Then $H_{n} \leq K_{ε} e^{ε n}$ , so $\log H_{n} = o (n)$ . Since $D_{n} \geq 2^{n}$ and $a_{n} = D_{n} / C_{n} + 1 - E_{n} / C_{n}$ , eventually

a_{n} \geq 2^{n / 2}, a_{n} < 2 D_{n}, ℓ (D_{n}) \leq n + O (1) .

For the last inequality, $D_{n + 1} < 2 D_{n}^{2}$ gives $1 + \log_{2} D_{n + 1} < 2 (1 + \log_{2} D_{n})$ . Iteration from a fixed late index, followed by another logarithm, gives $ℓ (D_{n}) \leq n + O (1)$ .

Suppose $H_{n + 1} - H_{n} \leq c ℓ (H_{n})$ eventually for some $0 < c < 1$ . For a large integer $B$ , take the first $B$ indices at or after $⌈ 3 \log_{2} B ⌉$ for which $gcd (a_{n}, D_{n}) = 1$ . Write the corresponding multipliers as $m_{0}, \dots, m_{B - 1}$ and let $s$ be the index immediately after the last choice. The density estimate just proved gives $s = B + o (B)$ : deleting $O (\log B)$ initial indices and $o (s)$ exceptional indices leaves $B$ choices. Each $m_{i} > 2 B$ for large $B$ , and the chosen multipliers are pairwise coprime, because each earlier one divides the denominator preceding a later one. All divide $D_{s}$ . For $P = \prod_{i} m_{i}$ we therefore have

(2 B)^{B} < P \leq D_{s}, H_{s} < P, B < P, ℓ (3 P) \leq B + o (B) .

The bound on $H_{s}$ uses $\log H_{s} = o (s)$ and $s = B + o (B)$ . Thus the product is large enough to place the block beyond the previous maximum, but small enough that the allowed jump at its height is less than the block length: $c ℓ (3 P) < B$ for all sufficiently large $B$ . Both comparisons are needed; existence of a distant CRT block alone would not control a height-dependent jump bound.

Crossing the block. Choose $x \in [P, 2 P)$ by the Chinese remainder theorem so that $m_{i} ∣ x + i$ for $0 \leq i < B$ . At the first record $C_{t} \geq x$ after $s$ , the preceding maximum is below $x$ and its increase is at most $c ℓ (2 P) < B$ . Thus $x \leq C_{t} < x + B < 3 P$ , so some $m_{i}$ divides both $C_{t}$ and $D_{t}$ . The exact updates preserve this common divisor. At the next record $C_{r}$ we would therefore have

m_{i} ∣ C_{r} - C_{t}, 0 < C_{r} - C_{t} \leq c ℓ (C_{t}) \leq c ℓ (3 P) < B < m_{i},

which is impossible. This proves the auxiliary bound $Θ \geq 1$ .

The integer normalisation matters here. Scaling $(C, D, E)$ by a positive integer $k$ scales the running maximum by $k$ and its limit-superior coefficient by $k$ , since $ℓ (k x) / ℓ (x) \to 1$ . Thus the bound with coefficient $1$ is not invariant under arbitrary clearing of denominators. The next step keeps track of the common factor rather than discarding it.

The common gcd and the sharper coefficient. For any fixed $N$ , divide the tail from $N$ onwards by $G_{N}$ . The resulting integer orbit satisfies the same hypotheses. Its running maximum is eventually $H_{n} / G_{N}$ , and $ℓ (H_{n} / G_{N}) / ℓ (H_{n}) \to 1$ . The auxiliary bound therefore gives $Θ \geq G_{N}$ . If $G_{N}$ is unbounded, then $Θ = + \infty$ .

Otherwise $G_{n} = g$ eventually. Fix a later index $T$ with $v_{T} > 1$ . The reduced exact tail has pairwise coprime multipliers, each coprime to $v_{T}$ . For a large integer $L$ , exactly

k_{L} = \frac{φ (v_{T})}{v_{T}} L + O (v_{T})

of the offsets $0, \dots, L - 1$ are coprime to $v_{T}$ . Assign to those offsets the next $k_{L}$ multipliers, beginning at $T$ . Put $s = T + k_{L}$ and $Q = v_{s} = v_{T} \prod_{T \leq j < s} a_{j}$ . Solve $x \equiv 0 (\mod v_{T})$ and $x \equiv - j$ modulo the multiplier assigned to offset $j$ , and take the solution in $[Q, 2 Q)$ . Every integer in $[x, x + L)$ then fails to be coprime to $v_{s}$ . No later reduced numerator can lie there.

The running maximum $R_{s}$ of the reduced numerator is below $Q$ for large $L$ , by the growth estimates above. The first crossing of $x$ after $s$ must therefore have a record increment at least $L$ . Its preceding maximum is below $2 Q$ , and $ℓ (2 Q) \leq s + O (1) = T + k_{L} + O (1)$ . The corresponding record indices tend to infinity with $L$ , so

\underset{n}{lim sup} \frac{R_{n + 1} - R_{n}}{ℓ (R_{n})} \geq lim_{L \to \infty} \frac{L}{T + k_{L} + O (1)} = \frac{v_{T}}{φ (v_{T})} .

Since $H_{n} = g R_{n}$ eventually, this gives $Θ \geq g v_{T} / φ (v_{T}) > g$ . An eventually Sylvester tail instead has constant $C_{n}$ and $Θ = 0$ . Finally,

H_{n + 1} - H_{n} = (- E_{n} - (H_{n} - C_{n}))_{+} \leq (- E_{n})_{+} .

Together with $ℓ (C_{n}) \leq ℓ (H_{n})$ , this proves the corollary. ◻

Formalisation.

The supplied formal sources contain persistence and pointwise-rise versions of the arithmetic steps: persistence of a common divisor, the bounded CRT block, the slow-rise landing lemma, and the coprime-block exclusion. The growth estimates, the count of usable moduli and the running-maximum argument are proved above in ordinary mathematics. The cited declarations verify their own arithmetic statements, not this assembled theorem. In particular, their landing bound controls increments of $C_{n}$ ; the argument above controls increments of $H_{n}$ and is a written extension, not a direct invocation of that declaration.

No upper bound on $Θ$ is proved. If $G_{n}$ is unbounded, the theorem forces $Θ = + \infty$ . If $G_{n} = g$ eventually, it proves only $Θ \geq g v_{T} / φ (v_{T})$ for every late $T$ . Since $v_{T} ∣ v_{T + 1}$ , the ratios $φ (v_{T}) / v_{T}$ are nonincreasing and have a limit $σ \geq 0$ . If $σ = 0$ , the lower bound again forces $Θ = + \infty$ ; if $σ > 0$ , it gives $Θ \geq g / σ$ but does not determine whether $Θ$ is finite. Replacing $H_{n}$ by the running maximum of $u_{n}$ divides the coefficient by $g$ , since $ℓ (g x) / ℓ (x) \to 1$ .

Bounds that allow for cancellation and earlier decreases

Theorem 7.5 (bounds allowing for previous decreases). Under the standing hypotheses, the following are equivalent: eventual Sylvester behaviour; $\underset{n}{lim sup} A_{n} < \infty$ ; $\underset{n}{lim sup} R_{n} δ_{n} < \infty$ . Each of those two limits superior is $0$ or $+ \infty$ .

Corollary 7.6 (the critical rate). Under the standing hypotheses and $δ_{n} = O (1 / n)$ , with no convergence of $n δ_{n}$ assumed, eventual Sylvester behaviour is equivalent to $u_{n} = O (n)$ and to $(- {\tilde{e}}_{n})_{+} = O (1)$ . A counterexample at the critical rate therefore has $\underset{n}{lim sup} u_{n} / n = \infty$ and $\underset{n}{lim sup} (- {\tilde{e}}_{n})_{+} = \infty$ .

Proof of Theorem 7.5. Suppose the orbit is not eventually Sylvester and $A_{n} \leq K$ eventually, for an integer $K \geq 1$ . Absorption and $| {\tilde{e}}_{n} | / u_{n} \to 0$ give $u_{n} \to \infty$ . Negative reduced errors must occur arbitrarily late, since otherwise $h_{n} u_{n + 1} = u_{n} - {\tilde{e}}_{n}$ would make $u_{n}$ eventually nonincreasing.

The bound controls cancellation as well as upward motion. Fix a late index $s$ , and let $t > s$ be the first subsequent negative-error index. At the intervening steps the reduced numerator is nonincreasing, so $u_{t} \leq u_{s + 1}$ . Since $R_{t} \geq u_{s}$ and $m_{t} = | {\tilde{e}}_{t} | \geq 1$ ,

A_{t} = \frac{R_{t} m_{t}}{u_{t}} \geq \frac{u_{s}}{u_{s + 1}} = \frac{h_{s}}{1 - {\tilde{e}}_{s} / u_{s}} .

Thus $h_{s} \leq 3 K / 2 < 2 K$ after the relative-error threshold. Also $m_{n} \leq A_{n} \leq K$ , since $R_{n} \geq u_{n}$ , and hence $u_{n + 1} \leq u_{n} + K$ .

We can now choose primes too large to be removed by cancellation. The density-one argument in the proof of Theorem 7.3 supplies infinitely many late multipliers $a_{n}$ coprime to $D_{n}$ . These multipliers are pairwise coprime. At each such step, $a_{n}$ is coprime to $v_{n}$ and $gcd (u_{n}, v_{n}) = 1$ , so $a_{n} u_{n} - v_{n}$ is coprime to both $a_{n}$ and $v_{n}$ . Hence $h_{n} = 1$ and $a_{n} ∣ v_{n + 1}$ . Only finitely many of the chosen multipliers can have all their prime divisors at most $2 K$ , since each uses a different prime from that finite set. Choose $K$ distinct primes $p_{0}, \dots, p_{K - 1} > 2 K$ at these steps. Once a chosen prime divides a reduced denominator, it divides every later one: $h_{n} v_{n + 1} = a_{n} v_{n}$ and $h_{n} < 2 K < p_{i}$ prevent its removal. All the primes therefore divide $v_{T}$ at a common later index $T$ .

Consequently every $u_{n}$ with $n \geq T$ is coprime to all the $p_{i}$ . Choose a CRT block of $K$ consecutive integers, one divisible by each $p_{i}$ , above $R_{T}$ . Divergence forces a first crossing, while $u_{n + 1} \leq u_{n} + K$ forces it to land inside the block, a contradiction. This proves that finite $lim sup A_{n}$ forces a Sylvester tail.

The comparison $| δ_{n} - m_{n} / u_{n} | \leq 3 / a_{n}$ gives $| R_{n} δ_{n} - A_{n} | \leq 3 R_{n} / a_{n} \to 0$ . Here $R_{n} \leq H_{n}$ , $\log H_{n} = o (n)$ and $a_{n}$ grows doubly exponentially. Thus the two boundedness conditions are equivalent. On a Sylvester tail, $u_{n} = 1$ and $m_{n} = 0$ eventually, so $A_{n} \to 0$ and $R_{n} δ_{n} \to 0$ . Since both quantities are nonnegative, their limits superior can only be $0$ or $+ \infty$ . ◻

The estimate at the first later negative error is the lemma in the release, negative error scaled by the previous maximum after cancellation: at the first later negative error, $u_{t} \leq u_{s + 1}$ and $u_{s} u_{t} \leq R_{t} | {\tilde{e}}_{t} | u_{s + 1}$ . The supplied index also records this lemma in a built public module. That evidence concerns the lemma, not a formal verification of the complete proof above. The exact example $15 / 134 = 1 / 10 + 1 / 85 + 1 / 5695$ , with steps in reduced fractions $(15, 134) \to (4, 335) \to (1, 5695)$ and $A_{1} = 15 / 4$ , attains equality in the displayed bound.

For Corollary 7.6, the comparison $| δ_{n} - m_{n} / u_{n} | \leq 3 / a_{n}$ and the rate $δ_{n} = O (1 / n)$ give $m_{n} / u_{n} = O (1 / n)$ . If $u_{n} = O (n)$ , then $m_{n} = O (1)$ . Conversely, $m_{n} = O (1)$ gives $u_{n + 1} \leq u_{n} + m_{n}$ , hence $u_{n} = O (n)$ and $R_{n} = O (n)$ . In either case $A_{n} = R_{n} m_{n} / u_{n} = O (1)$ , so Theorem 7.5 gives eventual Sylvester behaviour. A Sylvester tail has $u_{n} = 1$ and $m_{n} = 0$ eventually, which proves the converse implications.

The condition bounds the negative reduced error after multiplying it by $R_{n} / u_{n}$ . At a current maximum this is just $(- {\tilde{e}}_{n})_{+}$ ; after a decrease the multiplier is larger. A bound on $(- {\tilde{e}}_{n})_{+}$ does not directly control this additional factor. Under the critical-rate hypothesis, the preceding corollary supplies the required control. A Sylvester tail satisfies the condition with eventual value zero. We do not derive it for every rational tail satisfying the growth hypothesis.

Lemma 7.7 (large odd prime powers in the reduced denominator). Under the standing hypotheses, for every fixed $A > 0$ and every sufficiently large $n$ , the reduced denominator $v_{n}$ has an odd prime-power divisor $Q = p^{k}$ with

Q > (H_{n} + 2)^{A}, H_{n} = max_{j \leq n} C_{j} .

The prime $p$ may depend on $n$ ; no stable-gcd or prime-arrival assumption is imposed.

Proof. The denominator grows too fast for all its odd prime-power factors to remain small compared with $H_{n}$ . Indeed, the estimate for the rational tail gives $C_{n + 1} / C_{n} \to 1$ , hence $\log H_{n} = o (n)$ . Since $x_{n} = u_{n} / v_{n} \leq 2 / a_{n}$ and $u_{n} \geq 1$ , $v_{n} \geq a_{n} / 2$ . Also $v_{n} ∣ L_{n} = lcm (q, a_{0}, \dots, a_{n - 1})$ , so the $2$ -primary part of $v_{n}$ is at most $max (q, a_{n - 1}) = a_{n - 1}$ for all large $n$ . Its odd part $W_{n}$ therefore satisfies

W_{n} \geq \frac{a_{n}}{2 a_{n - 1}} \geq \frac{a_{n - 1}}{4}, \log W_{n} \geq c 2^{n - 1} - O (1)

for some $c > 0$ . Put $B_{n} = (H_{n} + 2)^{A} = \exp (o (n))$ . If every exact odd prime-power factor of $W_{n}$ were at most $B_{n}$ , then $W_{n} ∣ lcm (1, \dots, ⌊ B_{n} ⌋)$ , giving

\log W_{n} \leq B_{n} \log B_{n} = \exp (o (n)) .

This contradicts the preceding exponential lower bound for all sufficiently large $n$ . An offending exact prime-power factor is the required $Q$ . ◻

The argument compares the logarithm of the odd denominator part with the logarithm of a factorial bound. It needs neither the prime number theorem nor a lower density of new primes, and makes no such claim.

Theorem 7.8 (unit record increments). Under the standing hypotheses, if $R_{n + 1} - R_{n} \leq 1$ for all large $n$ , then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ for all large $n$ . Hence the sequence is eventually Sylvester if and only if $# {n : R_{n + 1} - R_{n} \geq 2}$ is finite. No hypothesis is placed on drawdowns, on record-setting jumps, or on the cancellation factors $h_{n}$ .

Proof. Suppose the orbit is not eventually Sylvester. Absorption gives ${\tilde{e}}_{n} \neq 0$ on a late tail, so vanishing relative error and integrality give $u_{n} \to \infty$ . Choose $s$ beyond the unit-increment and centring thresholds and the threshold in Lemma 7.7 with $A = 3$ . Since $H_{s} \geq R_{s} \geq 1$ , it supplies an odd $Q = p^{k} ∣ v_{s}$ with $Q > (H_{s} + 2)^{3} > 4 (R_{s} + 2)$ and $Q \geq 16$ . Let $Y$ be the least multiple of $p$ above $R_{s}$ . Then $Y \leq R_{s} + p < Q / 4 + p \leq 5 Q / 4$ . At the first $t > s$ with $u_{t} \geq Y$ , the integral unit-record increment forces $u_{t} = Y$ . Before $t$ , one has $w_{n} < 3 u_{n} / 2 < 15 Q / 8 < p Q = p^{k + 1}$ . Corollary 7.2 therefore gives $p^{k} ∣ v_{t}$ . But $p ∣ u_{t} = Y$ , contradicting $gcd (u_{t}, v_{t}) = 1$ . The converse follows because a Sylvester tail has $u_{n} = 1$ eventually. ◻

The separate release contains the unit-increment landing lemma and the one-unit record-increment implication. The supplied index also records these statements in a built public module. Their assumption about the existence of a prime power is proved here by the preceding written lemma. The complete theorem about the rational tail is not thereby an assembled Lean theorem.

The two-unit criterion discussed below bounds the actual jump at each record step, rather than the increase in the running maximum. As numerical bounds on individual steps, neither condition implies the other: the first allows $s_{n} = 2$ , while $s_{n} \leq 1$ permits large jumps after an earlier decrease. This is a comparison of the bounds, not a claim that they remain logically independent under all the standing tail hypotheses; there both criteria force eventual Sylvester behaviour. The finite example $(8, 177) \to (7, 4071) \to (10, 2373393)$ with multipliers $23$ and $583$ has records $8$ and $10$ , increment $2$ , jump $3$ and $gcd (8, 10) = 2$ , which is why the parity argument for crossing an odd level does not transfer from actual jumps to increments of the running maximum.

Counting jumps before a prime power can be lost

Theorem 7.9 (counting crossings before a prime power is lost). Let the orbit satisfy the reduced recurrences of this section, with $2 | {\tilde{e}}_{n} | < u_{n}$ from an index $s$ . Let $p \geq 3$ be prime, $Q = p^{ℓ}$ divide $v_{s}$ with $Q \geq 16$ , put $L = p Q / 2$ , and assume $R_{s} < L / 2$ . Assume that $u_{t} \geq L$ for some $t > s$ , and let $τ$ be the first such index, let $J$ be the set of steps in $[s, τ)$ that first cross at least one odd multiple of $p$ in $(L / 2, L]$ , and put $X = \sum_{n \in J} (d_{n} - 2)$ . Then every $n \in J$ is a record step with $h_{n} = 1$ and $d_{n} \geq 3$ , and $p Q \leq (8 p + 8) | J | + 4 X + 8 p$ .

Proof of Theorem 7.9. For $s \leq n < τ$ , one has $u_{n} < L$ and $w_{n} < 3 u_{n} / 2 < 3 p Q / 4 < p^{ℓ + 1}$ , since $Q = p^{ℓ}$ . Corollary 7.2 gives $Q ∣ v_{t}$ throughout $[s, τ]$ , so $p ∤ u_{t}$ there. A first crossing of a level above $R_{s}$ is a record step. If $h_{n} \geq 2$ then $u_{n + 1} = w_{n} / h_{n} < 3 u_{n} / 4$ , so every such record step has $h_{n} = 1$ . An odd multiple of $p$ cannot be landed on. A jump of size $1$ crossing it would land on it; a jump of size $2$ avoiding the landing would have two even endpoints, contrary to $gcd (u_{n}, u_{n + 1}) = 1$ . Thus every $n \in J$ has $d_{n} \geq 3$ . It remains to count these levels. The interval $(L / 2, L]$ has length $p Q / 4$ , and odd multiples of $p$ are spaced by $2 p$ , so it contains at least $Q / 8 - 1$ of them. The levels first crossed by a step of size $d_{n}$ have the same spacing, so there are at most $1 + d_{n} / (2 p)$ of them. Summing over $J$ gives

Q / 8 - 1 \leq | J | + \frac{2 | J | + X}{2 p},

which rearranges to the asserted inequality. ◻

The next series ignores record jumps of size at most two, apart from finitely many initial terms, and assigns a smaller cost to a large jump when it begins at a large numerator. A Sylvester tail has no late records, so both series converge. The proof shows that a non-Sylvester rational tail contributes a fixed positive amount on arbitrarily late finite intervals. Thus convergence is a genuine additional requirement, not a restatement of the pointwise limit $| E_{n} | / C_{n} \to 0$ .

Theorem 7.10 (two convergence criteria for large record jumps). Under the standing hypotheses, the sum $E = \sum_{n record} (1_{d_{n} \geq 3} u_{n}^{- 1 / 2} + (d_{n} - 2)_{+} u_{n}^{- 1})$ is finite if and only if the sequence is eventually Sylvester; and $\sum_{n record} (d_{n} - 2)_{+} u_{n}^{- 1 / 2}$ is finite if and only if the sequence is eventually Sylvester.

Proof. Assume first that the recurrence is not eventually Sylvester. Then $u_{n} \to \infty$ . For every sufficiently late $s$ , Lemma 7.7 with $A = 3$ gives an odd $Q = p^{k} ∣ v_{s}$ with $Q > (H_{s} + 2)^{3}$ , hence $Q \geq 16$ and $p Q > 4 R_{s}$ . Set $L = p Q / 2$ and take its first crossing. The preceding theorem applies. Because $Q \geq p$ and $p \geq 3$ ,

\frac{8 p}{L} = \frac{16}{Q} \leq 1, \frac{8 p + 8}{\sqrt{L}} \leq 8 \sqrt{2} (1 + 1 / p) < 16.

Dividing the preceding counting inequality by $L$ therefore gives

1 \leq 16 \frac{| J |}{\sqrt{L}} + 4 \frac{X}{L} \leq 16 \sum_{n \in J} (\frac{1}{\sqrt{u_{n}}} + \frac{d_{n} - 2}{u_{n}}),

since $u_{n} < L$ for $n < τ$ and $d_{n} \geq 3$ on $J$ . Thus an arbitrarily late finite window contributes at least $1 / 16$ to $E$ , contradicting convergence. No disjointness of the windows is needed: every window lies in a tail of the nonnegative series. On a Sylvester tail $u_{n} = 1$ eventually, so there are no late records and $E$ is finite. Finally, term by term at a record,

1_{d_{n} \geq 3} u_{n}^{- 1 / 2} + (d_{n} - 2)_{+} u_{n}^{- 1} \leq 2 (d_{n} - 2)_{+} u_{n}^{- 1 / 2} .

Hence finiteness of the second series implies finiteness of the first, and convergence in the converse direction again follows from eventual Sylvester behaviour. ◻

Formalisation.

The separate release contains the integer inequality counting crossings before a prime power is lost and its counting lemmas. The supplied index also records the integer inequality in a built public module. The existence of the required prime power, the real-valued bound and the complete equivalence above have written proofs; the Lean inequality is the checked integer form, not a checked transcription of the whole assembled theorem. The checked main-repository declaration the two-unit record-rise implication retains a supply premise: arbitrarily late $s$ admit an odd $p^{k} ∣ v_{s}$ with $3 R_{s} < p^{k}$ . Lemma 7.7 supplies this premise in ordinary mathematics. The declaration itself has not thereby become a complete checked theorem about rational tails. This distinction is about formal coverage, not an unfilled mathematical supply argument in the text.

Bounds on the error and on the original sequence

Theorem 7.11 (slow negative part). Let $(a, C, D)$ be an exact orbit of natural numbers with $a_{n} > 1$ , $C_{n} > 0$ , $D_{0} \geq 1$ , under vanishing relative error. Suppose that for some $δ \in (0, 1)$ and all large $n$ with $E_{n} < 0$ one has $- E_{n} \leq (1 - δ) ℓ (C_{n})$ . Then $E_{n} = 0$ for all large $n$ , and $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ for all large $n$ .

Theorem 12.1 is the case of a constant bound, since a constant is eventually below $(1 - δ) ℓ (C_{n})$ on a nonzero tail, where $C_{n} \to \infty$ .

Proof. Suppose the error is not eventually zero. The auxiliary lower bound in the proof of Theorem 7.3 applies to this exact integer orbit: it used only $a_{n} > 1$ , $C_{n} > 0$ , $D_{0} \geq 1$ and vanishing relative error. It gives $\underset{n}{lim sup} (H_{n + 1} - H_{n}) / ℓ (H_{n}) \geq 1$ . On the other hand, the hypothesis and $C_{n} \leq H_{n}$ give

H_{n + 1} - H_{n} \leq (- E_{n})_{+} \leq (1 - δ) ℓ (C_{n}) \leq (1 - δ) ℓ (H_{n})

for all large $n$ , a contradiction. Thus $E_{n} = 0$ eventually, and Theorem 5.7 gives the Sylvester recurrence. ◻

Formalisation.

The corresponding pointwise-rise argument has formalised arithmetic lemmas: persistence of a common divisor, the overlap transport, the landing lemma and the coprime-block exclusion. The count of indices and the simultaneous choice of constants are written out in the earlier proof; no end-to-end Lean verification of this consequence is claimed. Corollary 7.4 includes the boundary coefficient $1$ , while the preceding theorem on the running maximum also discounts rises that recover an earlier decrease. The present statement is retained for its direct bound on $E_{n}$ .

To compare the bounded hypothesis with the classical criteria, number the original sequence from $1$ in this subsection and put $P_{n} = \prod_{1 \leq j < n} a_{j}$ . Then

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

Thus the bound concerns upward increments, not boundedness of $P_{n} / a_{n}$ . The quadratic growth limit controls only the ratio of consecutive terms. Sylvester tails satisfy the bound, as do exact-square sequences $a_{n} = b^{2^{n - 1}}$ with $b \geq 2$ , for which the difference is zero. The latter never satisfies the Sylvester recurrence, so the bounded criterion below recovers irrationality of its reciprocal sum. The rounded examples after Corollary 7.13 show more generally how a term $c / n$ in the ratio produces increments of order $n^{c - 1}$ . The theorem allows a finite positive upper limit where the classical product criterion requires a nonpositive one; neither bound is derived from the original problem alone.

Theorem 7.12 (bounded or slowly growing increments of the product ratio). Let $a_{1} < a_{2} < \dots$ be positive integers with $a_{n + 1} / a_{n}^{2} \to 1$ and $\sum_{n \geq 1} 1 / a_{n} = p / q$ , where $p, q$ are positive integers. Put

Q_{n} = \frac{a_{1} a_{2} \dots a_{n - 1}}{a_{n}} (\frac{a_{n}^{2}}{a_{n + 1}} - 1) .

If $\underset{n}{lim sup} Q_{n} < \infty$ , the sequence is eventually Sylvester. The same conclusion holds if, for some $δ > 0$ and all large $n$ ,

Q_{n} \leq \frac{1 - δ}{q} ℓ (a_{1} \dots a_{n - 1} / a_{n}) .

For the bounded clause, use the stated denominator $q$ , put $P_{n} = \prod_{j < n} a_{j}$ , $x_{n} = \sum_{k \geq n} 1 / a_{k}$ , and form the integer tail $D_{n} = q P_{n}$ , $C_{n} = D_{n} x_{n}$ , $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ . Exact cancellation gives

E_{n} + q Q_{n} = q P_{n} (\frac{1}{a_{n + 1}} - (a_{n} - 1) \sum_{k \geq n + 2} \frac{1}{a_{k}}) .

The expression in parentheses is positive eventually, since $\sum_{k \geq n + 2} 1 / a_{k} \leq 4 / a_{n + 1}^{2}$ and $a_{n + 1} > 4 (a_{n} - 1)$ eventually. Thus $E_{n} \geq - q Q_{n}$ , and $lim sup Q_{n} < \infty$ supplies the eventual lower bound required by Theorem 12.1. This proves the bounded clause without first estimating the absolute size of the comparison error.

For the slow-growth clause and the later summability comparisons, the same exact formula gives

0 < E_{n} + q Q_{n} \leq q P_{n} / a_{n + 1} = O (P_{n} / a_{n}^{2})

eventually. The ratio test in Section 6 shows that these errors have a convergent sum, hence tend to zero. The factor $1 / q$ in the slow-growth clause cancels the factor $q$ in $E_{n} + q Q_{n} = o (1)$ . Suppose the sequence is not eventually Sylvester. Absorption and vanishing relative error give $C_{n} \to \infty$ , and the tail estimate $C_{n} \sim q P_{n} / a_{n}$ implies

\frac{ℓ (C_{n})}{ℓ (P_{n} / a_{n})} ⟶ 1.

For $0 < δ < 1$ , the assumed bound and $E_{n} + q Q_{n} = o (1)$ consequently give $(- E_{n})_{+} \leq (1 - δ / 2) ℓ (C_{n})$ eventually. This contradicts Theorem 7.11. If $δ \geq 1$ , the hypothesis gives $Q_{n} \leq 0$ eventually and the bounded clause already applies. The growth argument used in this deduction is a written argument, not an additional assembled Lean theorem.

The same comparison permits any positive real clearing factor $F_{n} \leq q P_{n}$ : multiplying $E_{n} + q Q_{n} = o (1)$ by $F_{n} / (q P_{n})$ gives

F_{n} - (a_{n} - 1) F_{n} x_{n} + \frac{F_{n}}{a_{n}} (\frac{a_{n}^{2}}{a_{n + 1}} - 1) = o (1) .

Neither $F_{n} x_{n}$ nor $F_{n} - (a_{n} - 1) F_{n} x_{n}$ need be integral. The LCM choice $F_{n} = L_{n}$ makes both integers, but its update includes the factor $ρ_{n}$ of Section 6. The short note uses only this LCM specialisation; no general clearing factor is needed in its bounded-increment proof.

Attribution.

Erdős and Straus require $lim sup \leq 0$ in the corresponding criterion, with the least common multiple in place of the product and the growth factor one index later, so their quantity is $[a_{1}, \dots, a_{n}] a_{n + 1}^{- 1} (a_{n + 1}^{2} / a_{n + 2} - 1)$ ; Koizumi’s Corollary 4(1) uses the product form [12]. The bounded clause follows from Theorem 12.1. For Koizumi’s product expression it replaces a nonpositive upper limit by an arbitrary finite upper limit. The material distinction here is product versus least common multiple. Reindexing $r = n + 1$ makes the classical LCM expression $[a_{1}, \dots, a_{r - 1}] a_{r}^{- 1} (a_{r}^{2} / a_{r + 1} - 1)$ , exactly the expression in the short note’s LCM corollary.

The comparison $E_{n} + q Q_{n} = o (1)$ has its classical predecessor in Koizumi’s proof of Corollary 4(1) . The bounded clause uses the checked rational-tail estimates; the slow-growth deduction above is an ordinary written argument.

Corollary 7.13 (the $1 / n$ threshold). 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$ . If

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

then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ for all large $n$ . The same conclusion holds if, for some $K \geq 0$ and $ε > 0$ ,

\frac{a_{n}^{2}}{a_{n + 1}} - 1 \leq \frac{1}{n} + \frac{K}{n^{1 + ε}} eventually .

In particular the one-sided bound by $1 / n$ is included.

Proof. Put $γ_{n} = a_{n}^{2} / a_{n + 1} - 1$ and $t_{n} = (\prod_{j < n} a_{j}) / a_{n}$ , so that $t_{n + 1} / t_{n} = 1 + γ_{n}$ . Choose $r \in (0, 1)$ and $N$ with $γ_{n}^{+} \leq r / n$ for all $n \geq N$ . Then

t_{n} \leq t_{N} \prod_{k = N}^{n - 1} (1 + \frac{r}{k}) = O (n^{r}),

so $(t_{n} γ_{n})_{+} = t_{n} γ_{n}^{+} = O (n^{r - 1})$ tends to zero and $\underset{n}{lim sup} t_{n} γ_{n} \leq 0$ . Koizumi’s Corollary 4(1) [12] gives the first conclusion. For the second, positivity of $1 + γ_{n}$ and

1 + γ_{n} \leq (1 + 1 / n) (1 + K / n^{1 + ε})

give $t_{n} = O (n)$ , since the second product converges. Consequently $t_{n} (γ_{n})_{+} = O (1)$ , and the criterion bounding the product expression applies. ◻

The inclusive clause requires more than $lim sup n (γ_{n})_{+} \leq 1$ . That weaker condition does not give the product estimate: for example, the scalar sequence $γ_{n} = (1 + 1 / \log n) / n$ has $t_{n} ≍ n \log n$ and $t_{n} γ_{n} ≍ \log n$ . This is a limitation of the estimate, not a counterexample to the original problem.

More generally, if $c > 0$ , $ε > 0$ and

\frac{a_{n}^{2}}{a_{n + 1}} = 1 + \frac{c}{n} + O (n^{- 1 - ε}),

then the consecutive-ratio identity gives $t_{n} \sim K n^{c}$ for some $K > 0$ and $t_{n + 1} - t_{n} \sim K c n^{c - 1}$ . To see the constant, take logarithms and subtract $c \log (1 + 1 / n)$ ; the remainder is absolutely summable. Hence the increments are bounded for $c \leq 1$ and unbounded for $c > 1$ . These rates are realised by increasing integer sequences: set $a_{n + 1} = ⌈ n a_{n}^{2} / (n + c) ⌉$ and choose the seed large enough that $a_{n + 1} \geq a_{n}^{2} / (1 + c) \geq 2 a_{n}$ throughout. The rounding remainder in $[0, 1)$ gives an error in the ratio bounded by $(1 + c)^{2} / a_{n}^{2}$ , smaller than every fixed inverse power of $n$ . This calculation supplies the family comparison behind the two rounded examples retained in the short note. It concerns their growth and does not assume rationality.

The second clause has a concrete application outside Koizumi’s nonpositive-upper-limit product condition. The sequence $a_{1} = 4$ , $a_{n + 1} = ⌈ n a_{n}^{2} / (n + 1) ⌉$ begins $4, 8, 43, 1387, \dots$ and satisfies

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

The lower bound follows from $a_{n + 1} \geq a_{n}^{2} / 2$ ; the upper error bound follows by writing the rounding remainder in $[0, 1)$ . Consequently $t_{n} \sim K n$ and $t_{n} γ_{n} \to K > 0$ by the product comparison above. The corollary proves that the reciprocal sum is irrational, since a Sylvester tail would have $γ_{n} = O (1 / a_{n})$ rather than $γ_{n} \sim 1 / n$ .

The strict clause includes Koizumi’s sufficient rate $1 + o (1 / n)$ [12]; the inclusive clause allows a bounded positive increment rather than requiring a nonpositive upper limit.

Signs of the error and of the growth ratio

We keep the preceding one-based indexing. The growth defect need not have the opposite sign to $E_{n}$ : the next identity displays the correction, including its sign on a Sylvester tail.

Proposition 7.14 (comparison of the two signs). The factor $M_{n} = D_{n} / L_{n}$ divides $G_{n} = gcd (C_{n}, D_{n})$ . Thus $G_{n} / M_{n}$ is a positive integer and $E_{n} / M_{n} = (G_{n} / M_{n}) {\tilde{e}}_{n}$ is an integer with the same sign as $E_{n}$ . The sign of the growth ratio minus one also depends on a correction term. The exact recurrences give, whenever $a_{n + 1} C_{n} C_{n + 1} \neq 0$ ,

\begin{matrix} (21) & \frac{a_{n}^{2}}{a_{n + 1}} - 1 = - \frac{E_{n}}{C_{n}} + Λ_{n}, Λ_{n} = \frac{(1 - E_{n} / C_{n}) (a_{n} - 1 + E_{n + 1} / C_{n + 1})}{a_{n + 1}}, \end{matrix}

and, under the standing positive rational-tail hypotheses, $0 < Λ_{n} < 3 / a_{n}$ for all sufficiently large $n$ . The Erdős–Straus quantity of Theorem 3 is

Z_{n}^{ES} = \frac{[a_{1}, \dots, a_{n}]}{a_{n + 1}} (\frac{a_{n + 1}^{2}}{a_{n + 2}} - 1) .

Its least common multiple includes $a_{n}$ but not the clearing denominator $q$ . It is not $Q_{n} = (P_{n} / a_{n}) γ_{n}$ from the preceding subsection, nor $L_{n} γ_{n + 1} / a_{n + 1}$ under our convention $L_{n} = lcm (q, a_{1}, \dots, a_{n - 1})$ . Being a positive multiple of the next growth defect, $Z_{n}^{ES}$ has the sign of $Λ_{n + 1} - E_{n + 1} / C_{n + 1}$ . For all sufficiently large $n$ , it is positive when $E_{n + 1} \leq 0$ ; for $E_{n + 1} > 0$ , it is negative precisely when $E_{n + 1} / C_{n + 1} > Λ_{n + 1}$ . On a Sylvester tail $E_{n} = 0$ and $Λ_{n} = (a_{n} - 1) / a_{n + 1} > 0$ .

Proof. Since both $C_{n} = D_{n} x_{n}$ and $L_{n} x_{n}$ are integers, $M_{n} = D_{n} / L_{n}$ divides $C_{n}$ as well as $D_{n}$ . It therefore divides $G_{n}$ . For (21), write $θ_{n} = E_{n} / C_{n}$ ; Proposition 4.1 gives $C_{n + 1} = C_{n} (1 - θ_{n})$ and $D_{n} / C_{n} = a_{n} - 1 + θ_{n}$ , so $a_{n + 1} - 1 + θ_{n + 1} = a_{n} D_{n} / C_{n + 1} = a_{n} (a_{n} - 1 + θ_{n}) / (1 - θ_{n})$ . Multiplying the asserted identity by $a_{n + 1}$ and substituting reduces it to $a_{n + 1} + a_{n} - 1 + θ_{n + 1} = a_{n}^{2} / (1 - θ_{n})$ , which is the displayed relation with $a_{n}$ added to both sides. The bound follows from $θ_{n} \to 0$ and $a_{n + 1} \geq a_{n}^{2} / 2$ . On Sylvester’s sequence $θ_{n} = 0$ and $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ , so $a_{n}^{2} / a_{n + 1} - 1 = (a_{n} - 1) / a_{n + 1} = Λ_{n} > 0$ . ◻

A nonpositive upper limit admits positive values tending to zero; it is not an eventual pointwise sign condition. For the product quantity $Q_{n} = (P_{n} / a_{n}) γ_{n}$ , the identity $E_{n} + q Q_{n} = o (1)$ shows that eventual $E_{n} \geq 0$ implies $lim sup Q_{n} \leq 0$ , as in Koizumi’s Corollary 4(1) [12]. For the classical LCM expression $Z_{n}^{ES}$ , the corresponding integer error is also taken one index later. Its published hypotheses are those of Erdős–Straus Theorem 3 [1]. Reindexing relates it to an LCM-cleared error, not to $E_{n}$ with the unchanged product factor $q Q_{n}$ .

A comparison with $B$ -free integers.

For a fixed family $B = {m_{i}}$ , the integers divisible by none of the $m_{i}$ are called $B$ -free integers. With pairwise coprime moduli and $\sum_{i} 1 / m_{i} < \infty$ , this is the standard setting of [21]. The next proposition is an elementary interval count in that setting. It tests what can follow from avoiding whole multiples alone. Unlike the reciprocal-tail argument, it imposes all the moduli from the outset and has no denominator recurrence or cancellation factors.

Proposition 7.15 (an elementary interval bound). Let $m_{0} < m_{1} < \dots$ be pairwise coprime integers at least $2$ with $θ = \sum_{i} 1 / m_{i} < 1$ . For all integers $x \geq 1$ and $L \geq 1$ satisfying $L > k / (1 - θ)$ , where $k = # {i : m_{i} \leq x + L}$ , the interval $[x, x + L)$ contains an integer divisible by no $m_{i}$ . If also $ℓ (m_{i}) = i + O (1)$ , then for every $ϵ > 0$ there are an index $T$ and a strictly increasing sequence of positive integers $(u_{n})$ such that

m_{i} ∤ u_{n} for every i \geq T and every n, u_{n + 1} - u_{n} \leq (1 + ϵ) ℓ (u_{n}) eventually .

Proof. The interval $[x, x + L)$ contains exactly $L$ integers. Each lies in $[1, \infty)$ and is smaller than $x + L$ , so a modulus exceeding $x + L$ divides none of them. Each of the $k$ remaining moduli divides at most $L / m_{i} + 1$ of them, so the covered count is at most $L θ + k < L$ . This interval count itself does not use pairwise coprimality; that condition is needed for the exact CRT proportions in the later gap theorem.

For the second assertion, choose a tail of the family and reindex it so that $θ < ϵ / (1 + ϵ)$ . If $k (z) = # {i : m_{i} \leq z}$ , the hypothesis $ℓ (m_{i}) = i + O (1)$ gives $k (z) \leq ℓ (z) + C$ for all large $z$ and some constant $C$ . Choose

(1 - θ)^{- 1} < ρ < 1 + ϵ, L (y) = ⌈ ρ ℓ (y) ⌉ .

Then $L (y) = O (ℓ (y)) = o (y)$ , and the definition of $ℓ$ gives $ℓ (y + 1 + L (y)) = ℓ (y) + o (1)$ . Consequently, for all large integers $y$ ,

\frac{k (y + 1 + L (y))}{1 - θ} \leq \frac{ℓ (y) + C + o (1)}{1 - θ} < ρ ℓ (y) \leq L (y),

while $L (y) \leq (1 + ϵ) ℓ (y)$ . The first part also supplies an admissible $u_{0}$ beyond this threshold. Apply it successively with $x = u_{n} + 1$ and length $L (u_{n})$ , and choose $u_{n + 1}$ in the resulting window. The sequence is strictly increasing, avoids every retained modulus, and has the required rise bound. ◻

The small-increment sequence avoids only the retained moduli $m_{i}$ , $i \geq T$ . Discarding the prefix makes their reciprocal sum small. For the full family, Theorem 14.7 instead gives the coefficient $\prod_{i} (1 - 1 / m_{i})^{- 1} > 1$ for the increasing enumeration of integers avoiding all the moduli.

Proposition 7.15 concerns avoidance of whole multiples, not coprimality to a composite modulus. The distinction matters: no integer in $[2, 5)$ is coprime to $30$ , although none is divisible by $30$ . Thus this proposition alone does not disprove a coprime-walk extension of Theorem 11.3. Proposition 14.6 below gives a separate counterexample using sparse prime moduli. Under the additional scale $ℓ (m_{j}) = j + O (1)$ , Theorem 14.7 determines the exact maximal-gap coefficient for these $B$ -free integers. Its proof uses a finite sieve estimate and the Chinese remainder theorem, not an orbit construction. Neither static construction supplies an exact reciprocal-tail orbit.

Conditions on a possible counterexample.

Together, these criteria give necessary conditions on a counterexample. For every fixed $δ \in (0, 1)$ , it must have

(1 - δ) ℓ (C_{n}) \leq - E_{n} = o (C_{n}) at infinitely many n .

It must also have a divergent sum of relative increases, unbounded negative error scaled by the previous maximum, and infinitely many record jumps of the reduced numerator of size at least three, with $h_{n} = 1$ . These are necessary conditions, not a construction of a counterexample. The residue-saturation lemma shows precisely one limitation of the fixed-old-modulus method; it is not an impossibility theorem about every future approach. A useful next target is interaction between new prime support, three consecutive numerators and the global bound on numerator growth.

Descent when the error is nonnegative

We return to zero-based indexing for the exact recurrences. If $E_{n} \geq 0$ , the update $C_{n + 1} = C_{n} - E_{n}$ makes $C_{n}$ nonincreasing. A nonincreasing sequence of natural numbers stabilises. The next theorem records this elementary case before we turn to negative errors.

Theorem 8.1 (descent). Let $C, E : N \to N$ satisfy $C_{n + 1} + E_{n} = C_{n}$ for every $n$ . Then $E_{n} = 0$ for all sufficiently large $n$ .

Proof. The recurrence gives $C_{n + 1} \leq C_{n}$ . Choose an index at which the natural-number sequence reaches its minimum. Every later value equals that minimum, and $C_{n + 1} + E_{n} = C_{n}$ then gives $E_{n} = 0$ . ◻

The result is formalised as the stabilisation of the nonnegative error, using the eventual constancy of a nonincreasing sequence.

The hypothesis is exactly one-sidedness: $C$ and $E$ take values in $N$ . If $E_{n} < 0$ infinitely often, the numerator rises at those indices and this descent argument no longer applies. The next two sections first treat constant and periodic negative errors.

When the negative error is constant

The exclusions in this section and the next concern infinite constant or periodic negative magnitudes, and they do not bound the length of a finite transient. Arbitrarily long constant transients occur on genuine rational orbits, by the flat-transient theorem of the working report on Problem #243 [9].

Suppose the error is negative with a constant magnitude, $E_{n} = - m$ for a fixed $m > 0$ and every $n$ . By Proposition 4.1 the numerator increases by $m$ at each step, so $C_{n} = c + n m$ with $c = C_{0}$ , and the definition of the error becomes a shape equation

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

Together with $D_{n + 1} = a_{n} D_{n}$ this is a closed system in $(a, D)$ . It has no infinite natural-number solution with every $a_{n} \geq 2$ . The following instance shows how the failure happens; the theorem then shows that it cannot be avoided.

Example 9.1 (the shape equation running until it fails). Take $m = c = 1$ , so that $C_{n} = 1 + n$ and the shape equation (5.1) reads $D_{n} + 1 = (a_{n} - 1) (1 + n)$ , and take $D_{0} = 1$ . Each step is now determined: at $n = 0$ the equation reads $2 = (a_{0} - 1) \cdot 1$ , so $a_{0} = 3$ , and $D_{1} = a_{0} D_{0} = 3$ ; at $n = 1$ it reads $4 = (a_{1} - 1) \cdot 2$ , so $a_{1} = 3$ , and $D_{2} = a_{1} D_{1} = 9$ ; at $n = 2$ it reads $10 = (a_{2} - 1) \cdot 3$ , which has no integer solution, and the orbit stops. Longer prefixes occur for other starting values. For $2 \leq a_{0} < 5000$ , the exact residue search in Appendix B gives a maximum of $17$ successful updates, hence $18$ multiplier values including $a_{0}$ .

Theorem 9.2 (no constant negative magnitude). For any $m, c \in N$ with $m > 0$ , there is no pair of sequences $a, D : N \to N$ with $a_{n} \geq 2$ for all $n$ satisfying $D_{n + 1} = a_{n} D_{n}$ and (5.1). The same holds if the shape equation only begins at some index.

Proof when $c$ and $m$ are coprime. Assume first $gcd (c, m) = 1$ . Every multiplier must share a prime with $m$ , but each such prime can occur in at most one multiplier.

Every $a_{j}$ shares a prime with $m$ . Suppose $gcd (a_{j}, m) = 1$ . Then $m$ is invertible modulo $a_{j}$ , so some $n$ has $c + n m \equiv 0$ , that is $a_{j} ∣ C_{n}$ ; and $a_{j} ∣ D_{n}$ for every $n > j$ , since $D$ is multiplicative with $a_{j}$ among its factors. Choosing such an $n$ beyond $j$ and reading (5.1) modulo $a_{j}$ gives $a_{j} ∣ m$ , contradicting $gcd (a_{j}, m) = 1$ and $a_{j} \geq 2$ .

A prime divisor of $m$ occurs in at most one $a_{j}$ . Suppose $p ∣ m$ and $p ∣ a_{j}$ . For $n > j$ we have $p ∣ D_{n}$ , so (5.1) gives $(a_{n} - 1) C_{n} \equiv 0 (\mod p)$ . Now $C_{n} = c + n m \equiv c$ , and $p ∤ c$ because $p ∣ m$ and $gcd (c, m) = 1$ ; hence $p ∣ a_{n} - 1$ , so $p ∤ a_{n}$ . Thus $p$ cannot divide any later multiplier.

This injects infinitely many multipliers into the finite set of prime divisors of $m$ , a contradiction. ◻

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

Removing the scale. For general $c$ , put $g = gcd (c, m)$ . Equation (5.1) shows $g ∣ 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. ◻

The formal statements are the exclusion at every scale and the eventual exclusion. The latter follows by shifting the orbit to the first index of constant error.

Theorem 9.2 excludes an error that is eventually constant and negative, at every magnitude and every scale. Constancy fixes both the possible prime divisors and the congruence used at later indices. For varying magnitudes, even when their prime divisors belong to a fixed finite set, this argument does not supply the same later congruence. It therefore does not settle that case.

When the negative error is periodic

The next case allows the magnitude to vary, provided it repeats. Write $e_{n} = - E_{n} > 0$ for the magnitude, as in Section 4, 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 numerator gains a fixed drift $M > 0$ over one period, meaning $C_{n + h} = C_{n} + M$ for every $n$ . In fact the update forces $M = \sum_{j = 0}^{h - 1} e_{j}$ : periodicity makes the sum over any $h$ consecutive indices the same. Thus $M > 0$ follows from the positive magnitudes; it is not an independent growth assumption.

At $h = 1$ this says that the magnitude is constant and that $M$ is its value, which is the situation of Section 9; Theorem 9.2 already excludes it without using the pointwise bound $e_{n} < a_{n}$ in the proof below. The new case is $h \geq 2$ .

For a constant error, the proof used the finitely many prime divisors of its magnitude. For a periodic error we use the prime divisors of the increase $M$ over one period. The required divisibility facts are as follows. Every multiplier $a_{j}$ divides each later denominator, by persistence of a multiplier. If a prime divides both $D_{n}$ and $a_{n}$ , the numerator update makes it divide $C_{n + 1}$ , the one-step divisibility implication. Once it divides both numerator and denominator, it divides every later numerator, denominator and error, by persistence of a common divisor.

Periodicity carries this divisibility back to every phase. Suppose $d ∣ M$ and $d ∣ a_{i}, a_{j}$ with $i < j$ . Then $d ∣ D_{j}$ , and $C_{j + 1} = a_{j} C_{j} - D_{j}$ gives $d ∣ C_{j + 1}$ . The common divisor persists in both sequences and in every later error. For any phase $r$ , choose $k$ with $r + k h \geq j + 1$ ; periodicity gives $d ∣ e_{r + k h} = e_{r}$ . Taking $k h \geq j + 1$ also gives $d ∣ C_{k h} = C_{0} + k M$ , hence $d ∣ C_{0}$ . This is the repeated-divisor implication; it uses the period relation and the increase over successive periods, each iterated through whole periods. A repeated prime can therefore be divided out of the entire system. This explains the induction on $M$ in the proof.

Theorem 10.1 (no periodic negative magnitude). Let $a, D, C, e : N \to N$ with $a_{n} \geq 2$ , $e_{n} > 0$ and $e_{n} < a_{n}$ for every $n$ , satisfying

D_{n + 1} = a_{n} D_{n}, C_{n + 1} = C_{n} + e_{n}, D_{n} + e_{n} = (a_{n} - 1) C_{n},

and suppose $e_{n + h} = e_{n}$ and $C_{n + h} = C_{n} + M$ for some $h > 0$ and $M > 0$ . This is impossible.

Proof. We use strong induction on the drift $M$ . A prime divisor of $M$ that recurs among the multipliers need not give an immediate contradiction. It instead divides the whole orbit, allowing us to reduce $M$ by that prime and apply the induction hypothesis.

Suppose first that no prime divisor of $M$ is a common divisor of $C_{0}$ and of every magnitude. The repeated-divisor implication 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. On the other hand, every multiplier shares a prime with $M$ . Indeed, if $gcd (a_{j}, M) = 1$ , choose $k \geq 1$ so that $a_{j} ∣ C_{j} + k M = C_{j + k h}$ . The same multiplier divides $D_{j + k h}$ , and periodicity gives $e_{j + k h} = e_{j}$ . The shape equation at $j + k h$ therefore implies $a_{j} ∣ e_{j}$ , contrary to $0 < e_{j} < a_{j}$ . Thus infinitely many multipliers would require distinct prime divisors of the fixed integer $M$ , a contradiction.

Otherwise some prime $p$ divides $M$ , divides $C_{0}$ , and divides every magnitude. Then $p ∣ 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 ∣ D_{n}$ for every $n$ . Divide $D$ , $C$ and $e$ by $p$ . The multipliers are untouched, so $a_{n} \geq 2$ 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 exclusion when no prime of $M$ divides all phases, the induction is the exclusion at every scale, and the eventual form is the eventual exclusion.

The phase-by-phase proof uses $e_{n} < a_{n}$ to prevent a multiplier from dividing its own nonzero phase magnitude. This is not a rescaling of the orbit. Nevertheless, for an infinite exact orbit with periodic positive magnitudes, the bound follows eventually from the other assumptions. The shape equation gives $C_{n} > 0$ , and periodicity gives

C_{n} = \frac{M}{h} n + O (1), sup_{n} e_{n} < \infty,

and $D_{0}$ cannot be zero: otherwise all $D_{n}$ vanish and the shape equation gives $e_{n} = (a_{n} - 1) C_{n} \geq C_{n}$ , contradicting these bounds. Thus $D_{n} \geq 2^{n} D_{0}$ , and

a_{n} - 1 = \frac{D_{n} + e_{n}}{C_{n}} ⟶ \infty .

Consequently $e_{n} < a_{n}$ eventually. Applying the eventual exclusion therefore rules out periodic positive magnitudes without an independent smallness assumption. The numbered theorem retains the pointwise bound used by its checked phase-by-phase proof. The later bounded-negative theorem also excludes this case.

Remark. On the rational-tail orbit of , the absolute error satisfies $| E_{n} | < a_{n}$ eventually. Indeed, under the dictionary in Section 3, Lemma 4(2) gives $- C_{n} / 2 \leq E_{n} < C_{n} / 2$ , hence $| E_{n} | \leq C_{n} / 2$ . The proof of Lemma 4(3) gives $C_{n + 1} \leq \frac{3}{2} C_{n}$ , hence $C_{n} \leq C_{N} (3 / 2)^{n - N}$ beyond a pseudo-greedy starting index $N$ . On the other hand, convergence of $\sum 1 / a_{n}$ gives $a_{n} \to \infty$ , and $a_{n + 1} / a_{n}^{2} \to 1$ then gives $a_{n + 1} \geq 2 a_{n}$ eventually. Thus $| E_{n} | / a_{n} \to 0$ . On a negative-error tail this gives $e_{n} < a_{n}$ .

For an abstract exact orbit, the same conclusion follows when $a_{n} > 1$ , $C_{n} > 0$ and $E_{n} / C_{n} \to 0$ hold: the calculation in Section 4 already derives the reciprocal series and its growth from these hypotheses. Summability is not an independent assumption in that setting. The bound $e_{n} < a_{n}$ is still only eventual, whereas Theorem 10.1 states it at every index; its eventual form, cited above, is therefore the applicable one. For a periodic magnitude, boundedness of $e_{n}$ and divergence of $a_{n}$ already suffice.

Bounded increases and coprimality to earlier 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.

Lemma 11.1 (shifted blocks of consecutive multiples). Let $m_{0}, \dots, m_{B - 1}$ be pairwise coprime and at least $2$ . For every bound there is a $t$ beyond it with $m_{i} ∣ t + i$ for each $i < B$ .

Proof. Standard Chinese remaindering: solve $t \equiv - i (\mod m_{i})$ simultaneously, then add multiples of $\prod_{i} m_{i}$ to pass the bound. ◻

The lemma is formalised as the shifted consecutive multiples.

Lemma 11.1 matches each modulus $m_{i}$ to its own multiple $t + i$ inside a window of $B$ consecutive integers. Matchings of a set of integers to distinct multiples in an interval are the subject of Erdős Problem #650, solved by van Doorn, Li and Tang: for every set $S$ of $k$ positive integers, every open interval of length $2 max S$ contains distinct multiples of at least $min (k, ⌈ 2 \sqrt{k} ⌉)$ elements of $S$ , and this count is optimal . Their extremal construction uses the same Chinese remaindering for moduli that need not be pairwise coprime, with their Claim 3.2 supplying the divisibility of residue differences by greatest common divisors that the generalised theorem requires [11]. The first-crossing argument below needs only the pairwise coprime case.

Example 11.2 (a block of three consecutive multiples). Take $B = 3$ and $(m_{0}, m_{1}, m_{2}) = (3, 4, 5)$ . The congruences $t \equiv 0 (\mod 3)$ , $t \equiv 3 (\mod 4)$ and $t \equiv 3 (\mod 5)$ hold exactly when $t \equiv 3 (\mod 60)$ . At $t = 3$ the block is $3, 4, 5$ with $3 ∣ 3$ , $4 ∣ 4$ and $5 ∣ 5$ ; at $t = 63$ it is $63, 64, 65$ with $3 ∣ 63$ , $4 ∣ 64$ and $5 ∣ 65$ . A sequence of natural numbers that starts at $0$ , tends to infinity and rises by at most $3$ at each step cannot step over the block ${3, 4, 5}$ : it has a first value at least $3$ , that value is at most $5$ , and every member of ${3, 4, 5}$ is divisible by one of the three moduli.

Theorem 11.3 (bounded increases and coprimality to earlier moduli). Let $u : N \to N$ tend to infinity with $u_{n + 1} \leq u_{n} + B$ for a fixed integer $B \geq 1$ . Then $u$ cannot remain coprime to infinitely many fresh pairwise coprime moduli: there is no family of pairwise coprime $m_{i} \geq 2$ , one for each index, such that $gcd (m_{i}, u_{t}) = 1$ whenever $i < t$ .

The CRT block must lie above the initial segment where some moduli are not yet available. No monotonicity of $u$ is assumed.

Proof. Choose $m_{0}, \dots, m_{B - 1}$ and use Lemma 11.1 to find $t > max (u_{0}, \dots, u_{B})$ with $m_{i} ∣ t + i$ for $0 \leq i < B$ . Since $u_{n} \to \infty$ , there is a first $n > B$ with $u_{n} \geq t$ . Minimality and the rise bound give

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

Hence $u_{n} = t + i$ for some $0 \leq i < B < n$ , so $m_{i} ∣ u_{n}$ . The inequality $i < n$ now permits the avoidance hypothesis, which says $gcd (m_{i}, u_{n}) = 1$ ; this contradicts $m_{i} \geq 2$ . The argument uses the first crossing of the CRT block, not monotonicity of $u$ . ◻

Only unboundedness above is used to obtain this first crossing. Divergence is stated because it holds for the reduced rational tail in the application. This distinction also explains why the weighted proof in Section 6 works with an unbounded running maximum, without assuming that its numerator tends to infinity.

The argument is formalised as the Chinese-remainder first-crossing consequence. Divergence forces $u$ to reach the forbidden block, and the uniform rise bound prevents it from jumping over the block. A bound only along a subsequence would leave the intervening steps unrestricted. Without a scale restriction on the moduli, Proposition 14.6 gives an unbounded coprime walk with rises $o (\log \log u_{n})$ . The same forbidden-block crossing, under a two-sided bound on the error, appears in the proof of Bado’s Theorem 5.1 , posted in September 2026.

In the application, $m_{i}$ is the $i$ th multiplier. Its coprimality is known only for later numerators, which explains the condition $i < t$ .

The barrier applies once reduction removes no further common factor. Call $(u, v)$ a reduced exact tail with multipliers $a$ when $gcd (u_{n}, v_{n}) = 1$ and

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

Here $u$ is the numerator and $v$ the denominator: the two recurrences are those of Section 4, with $u$ in the role of the numerator $C$ and $v$ in that of the denominator state $D$ , and with coprimality imposed at every index.

Proposition 11.4 (reduced tails are pairwise coprime). In a reduced exact tail, $a_{n}$ is coprime to $v_{n}$ ; the multipliers at distinct indices are pairwise coprime; and every earlier multiplier is coprime to every later numerator.

Proof. A common prime divisor of $a_{n}$ and $v_{n}$ would divide both $u_{n + 1} = a_{n} u_{n} - v_{n}$ and $v_{n + 1} = a_{n} v_{n}$ , contradicting their coprimality. Hence $gcd (a_{n}, v_{n}) = 1$ . For $i < t$ , the denominator recurrence gives $a_{i} ∣ v_{t}$ . Combining this with $gcd (a_{t}, v_{t}) = 1$ proves that $a_{i}$ and $a_{t}$ are coprime; combining it with $gcd (u_{t}, v_{t}) = 1$ proves that $a_{i}$ and $u_{t}$ are coprime. ◻

These are the step coprimality, the pairwise coprimality, and the coprimality to each earlier multiplier. Feeding them to Theorem 11.3 gives the form used later: there is no reduced exact tail whose numerator tends to infinity with a uniformly bounded upward increment, the reduced exclusion under bounded upward increments, together with its eventual form, the version with an eventual increment bound.

Example 11.5 (Sylvester’s sequence as a reduced exact tail). Put $u_{n} = 1$ and $v_{n} = D_{n} = 1, 2, 6, 42, 1806, \dots$ as in Example 4.2, with multipliers $a_{n} = v_{n} + 1 = 2, 3, 7, 43, 1807, \dots$ . Then $gcd (u_{n}, v_{n}) = 1$ , $u_{n + 1} + v_{n} = 1 + v_{n} = a_{n} u_{n}$ and $v_{n + 1} = a_{n} v_{n}$ , so this is a reduced exact tail, and Proposition 11.4 returns the classical fact that Sylvester’s numbers are pairwise coprime. Its numerator is constant, so it satisfies every hypothesis of the exclusion just stated except divergence; since the tail exists, that hypothesis cannot be dropped.

An arbitrary orbit of Section 4 need not be reduced. To use the preceding argument, we must show that the common factor stops changing. One uniform bound on the negative magnitudes at arbitrarily late indices suffices: each gcd divides every later gcd, and at a negative index it also divides the nonzero magnitude. Thus a bound at arbitrarily late negative indices bounds the entire gcd sequence. The next proposition justifies dividing by its eventual value.

Proposition 11.6 (the tail gcd stabilises). Let $(a, D, C)$ be an exact orbit of natural numbers, that is, a triple of $N$ -valued sequences with $C_{n + 1} + D_{n} = a_{n} C_{n}$ and $D_{n + 1} = a_{n} D_{n}$ , whose error is $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ . Suppose some fixed integer $B \geq 1$ satisfies $- B \leq E_{n} < 0$ at infinitely many indices. Then $gcd (C_{n}, D_{n})$ is eventually constant, and beyond that index the orbit divided by the stable gcd is a reduced exact tail.

Proof. First, $C_{n} > 0$ at every index. If $C_{n} = 0$ , the nonnegative recurrence forces $C_{n + 1} = D_{n} = 0$ , and both sequences then vanish at all later indices. This contradicts the existence of arbitrarily late negative errors.

The two recurrences give $G_{n} ∣ G_{n + 1}$ for $G_{n} = gcd (C_{n}, D_{n})$ , as in the gcd divisibility relation. Also $G_{n} = gcd (C_{n}, | E_{n} |)$ , since $D_{n} = E_{n} + (a_{n} - 1) C_{n}$ ; at a negative index this is the gcd identity with the negative magnitude. For any $n$ , choose $t \geq n$ with $- B \leq E_{t} < 0$ . Then

G_{n} \leq G_{t} \leq | E_{t} | \leq B .

The entire positive divisibility chain is therefore bounded and eventually constant, by stabilisation of a bounded divisibility chain. This is the supplied gcd stabilisation result. Dividing both sequences by the eventual value preserves the recurrences and gives coprime numerator and denominator at every later index. ◻

Other negative errors may exceed $B$ in magnitude. Gcd stabilisation uses the bounded witnesses, whereas the CRT application needs a bound on every upward increment. The supplied declaration proves stabilisation; division by the stable gcd gives the reduced tail.

Vanishing relative error also gives sparsity of the strict gcd increases. The next proposition asserts long finite intervals of constancy, not constancy on an infinite tail. For an exact orbit of natural numbers with $C_{n} > 0$ , put

G_{n} = gcd (C_{n}, D_{n}), Γ (N) = # {0 \leq j < N : G_{j} < G_{j + 1}} .

Proposition 11.7 (vanishing relative error makes strict gcd changes sparse). Let $a, C, D : N \to N$ satisfy $C_{n + 1} + D_{n} = a_{n} C_{n}$ and $D_{n + 1} = a_{n} D_{n}$ with $C_{n} > 0$ , and put $E_{n} = D_{n} - (a_{n} - 1) C_{n}$ , $G_{n} = gcd (C_{n}, D_{n})$ and $Γ (N) = # {0 \leq j < N : G_{j} < G_{j + 1}}$ . If $| E_{n} | / C_{n} \to 0$ , then $Γ (N) = o (N)$ . Moreover, for every starting bound $B$ and block length $L$ , some $n \geq B$ satisfies

G_{n} = G_{n + 1} = \dots = G_{n + L} .

The first assertion is the sublinear strict-growth theorem; the second is the arbitrarily late constant-block theorem. The proof first converts vanishing relative error into subexponential growth of $C_{n}$ . Each strict divisibility increase of $G_{n}$ contributes a factor of at least $2$ , so $2^{Γ (N)} G_{0} \leq G_{N} \leq C_{N}$ . Taking logarithms gives $Γ (N) = o (N)$ . For $L = 0$ the second assertion is immediate. For $L \geq 1$ , if every block of $L$ successive transitions beyond $B$ contained a strict increase, disjoint such blocks would give $Γ (N) \geq (N - B) / L - O (1)$ , a contradiction.

The quantifiers matter. Proposition 11.6 uses a bound on negative magnitudes at arbitrarily late indices and yields eventual constancy. Proposition 11.7 uses only vanishing relative error and yields arbitrarily late constant blocks of each prescribed finite length. This proof does not establish eventual constancy under that hypothesis, nor does it bound the negative magnitudes.

A lower bound on the error forces eventual zero

The lower bound $E_{n} \geq - B$ has two uses in the proof: it bounds negative errors at arbitrarily late indices to stabilise the gcd, and it bounds every upward increment to apply Theorem 11.3.

The denominator recurrence is essential. For a scalar sequence, $C_{n} = c + b n$ and $E_{n} = - b$ , with positive integers $b, c$ , satisfy both the lower bound and vanishing relative error but never stabilise. Theorem 9.2 excludes this as an exact orbit. The different, summability-based argument of the next section needs only the scalar update. On exact positive integer orbits with vanishing relative error, both sufficient conditions are equivalent to eventual zero error; neither is established from the unrestricted hypotheses.

Theorem 12.1 (bounded negative part). Let $a, C, D : N \to N$ and $E : N \to Z$ satisfy

$a_{n} > 1$ and $C_{n} > 0$ for every $n$ ;
the exact dynamics $C_{n + 1} + D_{n} = a_{n} C_{n}$ and $D_{n + 1} = a_{n} D_{n}$ ;
$E_{n} = D_{n} - (a_{n} - 1) C_{n}$ for every $n$ ;
eventual strict centring: $| E_{n} | < C_{n}$ for all large $n$ ;
eventually bounded negative part: $- B \leq E_{n}$ for all large $n$ , for some integer $B \geq 0$ ;
vanishing relative error: for every integer $K \geq 1$ there is an $N$ with $K | E_{n} | < C_{n}$ for all $n \geq N$ .

Then $E_{n} = 0$ for all sufficiently large $n$ .

Proof. Suppose the error is not eventually zero. Absorption implies that $| E_{n} | \geq 1$ after a sufficiently late centring threshold. Condition (6) therefore gives $C_{n} \to \infty$ .

If negative indices were finite, Theorem 8.1 would give eventual zero. Thus negative indices occur infinitely often, and their magnitudes are bounded by $B$ ; in particular $B \geq 1$ . Proposition 11.6 makes $G_{n} = gcd (C_{n}, D_{n})$ stabilise to an integer $g > 0$ . The divided sequences $u_{n} = C_{n} / g$ , $v_{n} = D_{n} / g$ form a reduced exact tail, with $u_{n} \to \infty$ and $u_{n + 1} - u_{n} = - E_{n} / g \leq B$ . Their coprimality properties from Proposition 11.4 now contradict Theorem 11.3. ◻

The theorem is formalised with hypotheses (4) and (5) holding eventually. The Lean proof shifts past both thresholds and applies the version with centring and the lower bound at every index. It uses divergence from vanishing relative error and the exclusion for bounded upward increments and arbitrarily late bounded negative magnitudes, via its formulation with divergence as a hypothesis. Both exclusion statements require a uniform bound on all upward increments. Bounded negative magnitudes at arbitrarily late indices suffice for gcd stabilisation, but not for the jump bound in the CRT argument.

Corollary 12.2. Under the hypotheses of Theorem 12.1, together with $C_{n + 1} \neq 0$ for all large $n$ , the multipliers satisfy $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ for all sufficiently large $n$ .

Proof. Theorem 12.1 gives eventual zero error. Theorem 5.7 then gives the Sylvester recurrence. ◻

Hypotheses (1)–(3) specify the positive integer recurrences. Condition (6) says $| E_{n} | / C_{n} \to 0$ and implies (4) by taking $K = 1$ . The abstract theorem lists the latter separately to expose its use in propagating a zero error. For a rational reciprocal sum, the analytic construction supplies these conditions. The only additional assumption is (5), the lower bound on the error. The constant and periodic exclusions proved earlier apply in their own stated regimes; they do not supply that bound for a general sequence.

Here is the precise comparison with [12], which also shows how Theorem 12.1 applies to Problem 1.1. Let $(a_{n})$ satisfy the hypotheses of Problem 1.1. After deleting a finite prefix, Corollary 3 of [12] makes the sequence the pseudo-greedy expansion of its own reciprocal sum, and Lemma 4 there supplies the integers $c_{n}, d_{n}, e_{n}$ of Section 3. Hypothesis (1) then holds: $c_{n}$ is a positive integer by Lemma 4(1), and $a_{n} > 1$ after a further finite shift, because summability of $\sum 1 / a_{n}$ forces $a_{n} \to \infty$ . Hypothesis (2) is the pair of recurrences $c_{n + 1} = a_{n} c_{n} - d_{n}$ and $d_{n + 1} = a_{n} d_{n}$ of Lemma 4(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 error $E_{n}$ . The centring range $- c_{n} / 2 \leq e_{n} < c_{n} / 2$ in the same lemma gives hypothesis (4) at every index, which is stronger than the eventual form used here. Hypothesis (6) is the vanishing of the gap sequence in Corollary 3, since $ε_{n} = e_{n} / c_{n}$ . The sole hypothesis not supplied is (5), the eventual bound on the negative part. Neither the cited construction [12] nor the argument here derives that bound from growth and rationality alone. This proves the conditional result, not Problem #243.

Finite total relative increase

Theorem 12.1 bounds individual upward increments of $C_{n}$ . Here we instead assume that the sum of those increments divided by $C_{n}$ converges. A Sylvester tail satisfies this because its numerator is eventually constant. The integer sequences $C_{n} = n + 1$ and $C_{n} = (n + 1)^{2}$ do not satisfy it: their relative increases have a divergent harmonic sum, although each tends to zero. Unlike the preceding argument, this proof needs no denominator or growth hypothesis.

Theorem 13.1 (finite sum of relative increases). Let $C_{n} \in N_{> 0}$ and $E_{n} \in Z$ satisfy $C_{n + 1} = C_{n} - E_{n}$ . If

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

then $E_{n} = 0$ eventually. For an exact reciprocal-tail orbit this implies $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ eventually. No hypothesis $| E_{n} | / C_{n} \to 0$ is required.

Proof. Put $δ_{n} = (- E_{n})_{+} / C_{n}$ . The update gives $C_{n + 1} \leq C_{n} (1 + δ_{n})$ , so

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

Choose an integer upper bound $K$ for $C_{n}$ . Each strict rise of the integer sequence contributes at least $1 / K$ to $\sum_{n} δ_{n}$ , so there are only finitely many rises. The remaining positive integer sequence is nonincreasing and therefore stabilises, forcing $E_{n} = 0$ . The recurrence follows from Theorem 5.7, since $C_{n} > 0$ . ◻

The same proof allows any positive real $C_{0}$ , provided $E_{n} \in Z$ : after the finitely many rises, the bounded positive values lie in the finite set $(C_{0} + Z) \cap (0, K]$ , so they stabilise. The linked formal statement retains integer-valued $C_{n}$ .

The two indispensable features of this argument are positivity and discrete increments. With $C_{n} = 1 + 1 / (n + 1)$ and $E_{n} = 1 / ((n + 1) (n + 2))$ , the numerator decreases forever with zero relative-increase sum, but the errors are not integers. With $C_{n} = - n - 1$ and $E_{n} = 1$ , the increments are integers but positivity fails.

The scalar conclusion is the eventual vanishing for a positive integer sequence; its exact-orbit consequence is the scalar recurrence from a convergent sum. The separate release contains a formulation for the rational-tail numerators using a convergent sum, outside the main-repository build identified here. Summability remains an assumption; the elementary scalar implication needs neither growth nor vanishing relative error.

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 [9]. Bado’s Theorem 11.1 also accounts for the factors removed in LCM clearing [8]. In the notation of Section 6, the update gives

\log U_{N} \leq \log U_{0} + \sum_{n < N} \frac{(- E_{n})_{+}}{C_{n}} - \sum_{n < N} \log ρ_{n} .

His sufficient condition is an upper bound on the difference of these two sums. The subtractive term records the decrease caused by a repeated factor in the denominator. It may offset some relative increases; the hypothesis does not require either sum to converge separately. Unlike the scalar criterion above, this argument also uses the pseudo-greedy limit: bounded $U_{n}$ and $V_{n} / U_{n} = E_{n} / C_{n} \to 0$ make the integer $V_{n}$ eventually zero, after which $ρ_{n} U_{n + 1} = U_{n}$ gives eventual constancy.

Corollary 3 [12] and Lemma 4 [12] supply the same positive integer update after a finite restart. Theorem 13.1 therefore applies if the relative-increase sum converges. This is the sole additional hypothesis, asked for in Problem 14.5; the cited construction does not establish it.

Example 13.2 (the product bound at a geometric rate). Suppose $C_{0} = 100$ and $(- E_{n})_{+} / C_{n} \leq 2^{- n - 1}$ for every $n$ , so that the sum of relative increases is at most $1$ ; the constraint at $n = 0$ still permits $E_{0}$ as negative as $- 50$ . Since $1 + x \leq e^{x}$ ,

C_{N} \leq 100 \prod_{n < N} (1 + 2^{- n - 1}) \leq 100 e < 272

for every $N$ . For all sufficiently large $n$ , we have $2^{- n - 1} < 1 / 272$ . A strict rise would then force $(- E_{n})_{+} / C_{n} \geq 1 / C_{n} > 1 / 272$ , a contradiction. Thus $C_{n}$ is eventually nonincreasing; as a positive integer sequence it stabilises, and $E_{n} = 0$ thereafter. The constant $272$ comes from the total mass and not from any single magnitude, which is why the hypothesis of Theorem 13.1 is summability of $(- E_{n})_{+} / C_{n}$ and not a bound on it.

Complements and further questions

Absorption, descent and the two finiteness criteria give the following necessary conditions. Constant or periodic patterns only along the negative indices of a mixed-sign sequence are not covered by the all-negative exclusions. None of these results resolves Problem #243.

Proposition 14.1 (necessary conditions on a counterexample). For the integer tail attached to any counterexample to Problem 1.1,

E_{n} \neq 0 eventually, \frac{| E_{n} |}{C_{n}} ⟶ 0,

and

\underset{\begin{matrix} n \to \infty \\ E_{n} < 0 \end{matrix}}{lim sup} (- E_{n}) = \infty, \sum_{n = 0}^{\infty} \frac{(- E_{n})_{+}}{C_{n}} = \infty .

In particular, negative indices occur infinitely often. Thus the remaining regime consists of unbounded negative errors along exact reciprocal tails for which the sum of relative increases diverges.

Proof. Koizumi’s construction from a rational reciprocal tail gives strict centring and vanishing relative error after a finite shift; the strict-centring hypothesis of Theorem 12.1 also follows from vanishing relative error with $K = 1$ . Absorption then makes $E_{n} \neq 0$ eventually, since eventual zero would give the Sylvester recurrence. Descent excludes an eventually nonnegative error. Theorem 12.1 excludes a bounded negative part, and Theorem 13.1 excludes convergence of the sum of relative increases. These statements are unchanged by deleting a finite prefix. ◻

Lean checks Proposition 14.1 as the necessary conditions on a counterexample, from the rational reciprocal sum, the quadratic growth limit, and the failure of eventual Sylvester behaviour. The divergent sum of relative increases is recorded there as divergence of the partial sums.

Proposition 14.1 does not assert infinitely many prime divisors of the error magnitudes. Nor are its numerical conditions alone a reformulation of the problem: the numerator and denominator must satisfy the exact recurrences. With those recurrences, positivity and vanishing relative error, Section 4 supplies the reciprocal-series realisation. The following exact-orbit question is therefore equivalent to the original problem.

Problem 14.2 (unbounded negative errors with divergent relative sum). Exclude, or construct, an exact orbit of natural numbers $(a, D, C)$ with $a_{n} > 1$ and $C_{n} > 0$ , whose multipliers satisfy $lim_{n} a_{n + 1} / a_{n}^{2} = 1$ and whose error satisfies vanishing relative error, and which is negative infinitely often with magnitudes unbounded along that infinite set and

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

Such an orbit fails the bounded-negative-part and summable-relative-increase hypotheses. By Proposition 14.1 the integer tail of a counterexample is such an orbit after deletion of a finite prefix, so an exclusion would settle Problem #243. Conversely, a global orbit with the displayed properties has $C_{n} / D_{n} \to 0$ by Section 4. The reciprocal-series realisation then identifies its reciprocal sum as $C_{0} / D_{0}$ . After deletion of a finite prefix the multipliers are strictly increasing, and the infinitely many negative errors rule out a Sylvester tail. It is therefore a counterexample to Problem #243. Finite admissible prefixes alone do not provide such a construction.

Remark. The hypotheses in Problem 14.2 beyond the state recurrence are not decorative: the recurrence alone admits unbounded divergent-mass excursions. Put

C_{n} = 2^{n}, b_{0} = 2, b_{n + 1} = \frac{1}{2} b_{n} (b_{n} + 2), a_{n} = b_{n} + 2, D_{n} = b_{n} C_{n},

so that $(b_{n}) = 2, 4, 12, 84, 3612, \dots$ and $(a_{n}) = 4, 6, 14, 86, 3614, \dots$ . Every $b_{n}$ is a positive even integer, since $b_{n} = 2 k$ gives $b_{n + 1} = 2 k (k + 1)$ , so all four sequences are $N$ -valued. The orbit is exact: $C_{n + 1} + D_{n} = 2^{n} (2 + b_{n}) = a_{n} C_{n}$ and $D_{n + 1} = b_{n + 1} 2^{n + 1} = b_{n} (b_{n} + 2) 2^{n} = a_{n} D_{n}$ . Its error is

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

so the negative magnitudes $2^{n}$ are unbounded and $\sum_{n} (- E_{n})_{+} / C_{n}$ diverges. What fails is the centring: $| E_{n} | = C_{n}$ at every index, so strict centring fails at the boundary and vanishing relative error fails outright. The multipliers satisfy $a_{n + 1} = \frac{1}{2} (a_{n}^{2} - 2 a_{n} + 4)$ , so $a_{n + 1} / a_{n}^{2} \to \frac{1}{2}$ and the growth hypothesis fails as well. The example therefore says nothing about Problem 1.1, and it does not isolate the centring hypotheses: $E_{n} = - C_{n}$ at every index forces that multiplier recurrence, so growth fails with them. It is recorded only to show that the state recurrence alone is not enough.

A scalar profile need not satisfy the recurrences.

The example $C_{n} = n^{2} + 1$ , $E_{n} = - (2 n + 1)$ satisfies the numerator update, $| E_{n} | / C_{n} \to 0$ , $\log C_{n} = o (n)$ and $\sum_{n} (E_{n} / C_{n})^{2} < \infty$ . It is not an exact reciprocal-tail orbit. Indeed, $C_{2} = 5$ , $C_{3} = 10$ and $C_{4} = 17$ . The first numerator update forces $5 ∣ D_{2}$ ; the multiplicative denominator update gives $5 ∣ D_{3}$ ; the next numerator update then forces $5 ∣ C_{4}$ , a contradiction. This is the failed-route example referred to at the end of the short note: subexponential size and a small relative error do not supply arithmetic compatibility.

Growth of the factors repeated in the denominator

To compare repeated prime factors in the denominator with its total size, define

L_{0} = D_{0}, L_{n + 1} = lcm (L_{n}, a_{n}), M_{n} = \frac{D_{n}}{L_{n}} .

Since $D_{n} = D_{0} \prod_{j < n} a_{j}$ , the quotient is integral and $M_{n} L_{n} = D_{n}$ . The product counts every occurrence of a prime, whereas the least common multiple keeps only its largest exponent. The quotient $M_{n}$ records the remaining factors. Problem 14.3 below asks whether failure of the Sylvester recurrence would force this quotient to grow exponentially, contradicting its known subexponential upper bound. We first record a local estimate for cancellation during a recovery interval; it does not by itself give that global lower bound.

Cancellation before a numerator regains its former value

The LCM quotient $M_{n}$ need not equal the common divisor $G_{n}$ removed by reduction to lowest terms. Since $M_{n}$ divides both $C_{n}$ and $D_{n}$ , we have $M_{n} ∣ G_{n}$ , but equality is not assumed. The following estimate concerns the successive reduction factors, over an interval where the reduced numerator regains its starting value. In the calculation below, $h_{n}$ is the factor removed at step $n$ , $c_{n}$ is a positive integer with $c_{n}^{2} ∣ h_{n}$ , and ${\tilde{e}}_{n}$ denotes the signed reduced error, as in Section 7. For the estimate itself, let $u, h, c : N \to N$ and $\tilde{e} : N \to Z$ satisfy

h_{n} u_{n + 1} = u_{n} - {\tilde{e}}_{n}, u_{n} > 0, h_{n} > 0.

Fix $K, r, L \in N$ with $K, L > 0$ , assume

K | {\tilde{e}}_{r + i} | < u_{r + i} (0 \leq i < L), u_{r} \leq u_{r + L},

and let $R$ be a finite family of moduli. Suppose every $m_{q}$ , $q \in R$ , divides $\prod_{r \leq n < r + L} c_{n}$ , and that $c_{n}^{2} ∣ h_{n}$ throughout the interval. Then

\begin{matrix} (22) & K^{L} lcm (m_{q} : q \in R)^{2} < (K + 1)^{L} . \end{matrix}

To see this, each relative-error bound gives $h_{n} u_{n + 1} < (1 + 1 / K) u_{n}$ . Multiplication over the interval and $u_{r} \leq u_{r + L}$ yield

\prod_{r \leq n < r + L} h_{n} < (1 + 1 / K)^{L} .

The least common multiple of the $m_{q}$ divides the product of the $c_{n}$ , and $c_{n}^{2} ∣ h_{n}$ at every step. Its square therefore divides, and is at most, the positive product on the left. Multiplying by $K^{L}$ proves the claimed bound. This is the bound on cancellation over a recovery interval.

The square in (22) comes from the assumption $c_{n}^{2} ∣ h_{n}$ . If the least common multiple of the chosen moduli is at least $2^{| R |}$ , then

K^{L} 4^{| R |} < (K + 1)^{L} .

The formal consequence is the bound on the number of independent moduli. Taking logarithms gives the explicit bound

\frac{| R |}{L} < \frac{\log (1 + 1 / K)}{\log 4} \leq \frac{1}{K \log 4} .

Thus the number of these moduli is small relative to the recovery length when the relative-error bound is small. This statement requires the lower bound $2^{| R |}$ on their least common multiple; it does not apply to an arbitrary family with repeated prime factors.

For a fixed number of steps, the same estimate has a simpler consequence: a sufficiently late recovery cannot include any cancellation. If $K | {\tilde{e}}_{n} | < u_{n}$ eventually for every $K$ , then for each fixed $L > 0$ there is an $N$ such that every recovery $u_{r} \leq u_{r + L}$ with $r \geq N$ satisfies

\prod_{0 \leq i < L} h_{r + i} = 1.

Indeed, choose $K$ so large that $(1 + 1 / K)^{L} < 2$ and apply the same product estimate beyond its error threshold. The positive integer product is then smaller than $2$ , so it equals $1$ . The same $K$ works for every length $1 \leq j \leq L$ , since $(1 + 1 / K)^{j} \leq (1 + 1 / K)^{L} < 2$ . Thus, after a sufficiently late step with $h_{n} > 1$ , the numerator cannot regain its starting value at any of the next $L$ indices. This includes a recovery followed by another fall before the last endpoint. The fixed-length conclusion is formalised as absence of late cancellation during recovery intervals of fixed length. The theorem does not bound a recovery length that varies with $r$ , nor does it supply a lower bound for the least common multiple of the chosen moduli. Those are the missing inputs needed to turn (22) into a global contradiction.

Problem 14.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?

The two displayed formulations are equivalent up to changing the positive constant; the second is not a weaker target. Section 6 already gives $1 \leq M_{n} \leq C_{n}$ , hence $\log M_{n} / n \to 0$ on every orbit under consideration. A positive answer would therefore be a contradiction, not a further compatible necessary condition. It would prove Problem #243. The missing step is to force exponential growth of $M_{n}$ from failure of the Sylvester recurrence.

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_{0} A_{n}$ . From

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

one immediately obtains

gcd (A_{n}, a_{n} - 1) ∣ E_{n} .

The checked tail-height estimate and vanishing relative error make $| E_{n} |$ subexponential in $n$ .

Problem 14.4 (common factors of the prefix and $a_{n} - 1$ ). In every rational-tail orbit satisfying the hypotheses but not the conclusion of Problem 1.1, is

\underset{n \to \infty}{lim sup} \frac{\log gcd (A_{n}, a_{n} - 1)}{n} > 0 ?

Equivalently, do there exist $η > 0$ and infinitely many $n$ such that $gcd (A_{n}, a_{n} - 1) \geq e^{η n}$ ?

By Proposition 14.1, the error is nonzero eventually. The displayed divisibility therefore bounds $gcd (A_{n}, a_{n} - 1)$ by $| E_{n} |$ at every sufficiently late index. A positive answer contradicts the subexponential bound on that error. Arbitrarily long locally admissible blocks do not answer this question: the gcd uses the complete prefix.

The direct analytic question

Problem 14.5 (summability from rationality). Let $(a_{n})$ satisfy the hypotheses of Problem 1.1, and let $(D_{n}, C_{n}, E_{n})$ be its integer tail. Must

\sum_{n = 0}^{\infty} \frac{(- E_{n})_{+}}{C_{n}} < \infty ?

An affirmative answer closes Problem #243 by Theorem 13.1. The summands are nonnegative and tend to zero, so $\log (1 + t)$ is comparable to $t$ at their values. Convergence is therefore equivalent to boundedness of the partial products $\prod_{n < N} (1 + (- E_{n})_{+} / C_{n})$ , the same criterion in multiplicative form. A negative answer requires a sequence satisfying the full growth and rationality hypotheses. A locally admissible state orbit is insufficient. By Theorem 6.2, it is enough to establish the finiteness of (20) for one nonincreasing weight with divergent integral and one fixed $B \geq 0$ . The equivalent sum in Theorem 6.2 uses only steps where the LCM numerator exceeds its previous maximum. It subtracts $B$ from each upward jump, takes the positive part and weights it by $f (U_{n})$ .

Remark. One further question is not left open here, since it is answered in [12]: whether vanishing relative error follows from $a_{n + 1} / a_{n}^{2} \to 1$ and rationality. It does. After deleting a finite prefix, Koizumi’s Corollary 3 [12] makes the sequence the pseudo-greedy expansion of its own reciprocal sum and gives $ε_{n} \to 0$ under exactly the hypotheses of Problem 1.1; rationality is not needed for that step, only summability of $\sum 1 / a_{n}$ . The matched-index dictionary in Section 3 gives $ε_{n} = E_{n} / C_{n}$ on the restarted tail. For a rational sum, Lemma 4(2) [12] also gives $- c_{n} / 2 \leq e_{n} < c_{n} / 2$ at every index of that expansion. Thus $| E_{n} | < C_{n}$ holds beyond the restart, as required by Theorem 12.1; it need not hold at every original index. Eventual strict centring also follows directly from vanishing relative error with $K = 1$ . What remains unsupplied is hypothesis (5), the bound on the negative part, which is why the theorem is still conditional.

What changes when upward increments are not bounded

Proposition 14.6 (small increases when the prime moduli are sparse). There exist strictly increasing primes $p_{i}$ and a strictly increasing positive integer sequence $u_{n} \to \infty$ such that $gcd (u_{n}, p_{i}) = 1$ for all $i, n$ and

u_{n + 1} - u_{n} = O (\sqrt{\log \log (u_{n} + e^{e})}) = o (\log \log (u_{n} + 3)) .

Thus the bounded-increment hypothesis of Theorem 11.3 cannot be replaced by an $o (\log \log u_{n})$ bound without a quantitative restriction on the moduli.

Proof. Choose increasing primes $p_{i} > max {\exp (\exp ((i + 2)^{2})), 2^{i + 3}}$ , for $i \geq 0$ . Primes of arbitrarily large size suffice; no distribution theorem is used. Then $θ = \sum_{i} 1 / p_{i} < 1 / 4$ and $k (z) = # {i : p_{i} \leq z} \leq \sqrt{\log \log z}$ whenever $z$ is large. For integer $x$ put $L (x) = ⌈ 4 \sqrt{\log \log (x + e^{e})} + 8 ⌉$ . Since $L (x) = o (x)$ , eventually $L (x) > k (x + L (x)) / (1 - θ)$ . The elementary window bound of Proposition 7.15 leaves an integer in $[x, x + L (x))$ divisible by no $p_{i}$ . The set of such integers is therefore unbounded. Enumerate it increasingly as $(u_{n})$ and apply the same bound with $x = u_{n} + 1$ to obtain $u_{n + 1} - u_{n} \leq L (u_{n} + 1)$ . For prime moduli nondivisibility is exactly coprimality, proving every claim. The moduli are deliberately much sparser than the scale used in the next theorem. ◻

We now keep the full family of moduli, rather than discarding a prefix as in Proposition 7.15. The resulting coefficient depends on $σ = \prod_{j} (1 - 1 / m_{j})$ . For a finite prefix, the corresponding product is exactly the proportion of admissible residue classes by the Chinese remainder theorem. This explains the constant in the statement before the limiting argument is made.

Theorem 14.7 (largest gaps between integers avoiding given multiples). Let $m_{0} < m_{1} < \dots$ be pairwise coprime integers at least $2$ with $ℓ (m_{j}) = j + O (1)$ , where $ℓ (x) = \log_{2} \log_{2} max (4, x)$ . Let $σ = \prod_{j} (1 - 1 / m_{j}) > 0$ and enumerate the positive integers divisible by no $m_{j}$ in increasing order as $(u_{n})$ . Then

\underset{n \to \infty}{lim sup} \frac{u_{n + 1} - u_{n}}{ℓ (u_{n})} = σ^{- 1} .

This is a statement about avoidance of multiples of whole moduli. It is not a statement about coprimality to composite $m_{j}$ , or about integer tail orbits.

Proof. Write $k (z) = # {j : m_{j} \leq z} = ℓ (z) + O (1)$ . For a fixed prefix length $T$ , set

M_{T} = \prod_{j < T} m_{j}, σ_{T} = \prod_{j < T} (1 - 1 / m_{j}), θ_{T} = \sum_{j \geq T} 1 / m_{j} .

Here $θ_{T} \to 0$ . By the Chinese remainder theorem, avoiding the first $T$ whole moduli selects precisely the fraction $σ_{T}$ of the residues modulo $M_{T}$ .

For the upper bound, an integer interval $[x, x + L)$ contains at least $σ_{T} L - M_{T}$ integers avoiding that prefix. The remaining moduli cover at most $L θ_{T} + k (x + L)$ integers. Choose $T$ large enough that $σ_{T} > θ_{T}$ , and then any $c > (σ_{T} - θ_{T})^{- 1}$ . For $L = ⌈ c ℓ (x) ⌉$ , the number left is positive for all sufficiently large $x$ , since $k (x + L) = ℓ (x) + O (1)$ . Thus the set being enumerated is unbounded, and every sufficiently late such interval meets it. Applying this at $x = u_{n} + 1$ gives

\underset{n}{lim sup} \frac{u_{n + 1} - u_{n}}{ℓ (u_{n})} \leq (σ_{T} - θ_{T})^{- 1} .

Letting $T \to \infty$ gives the upper bound $σ^{- 1}$ .

For the lower bound, fix $T$ and let the integer length $L$ tend to infinity. Among the offsets $0 \leq j < L$ , precisely $K_{L} = σ_{T} L + O (M_{T})$ avoid the first $T$ moduli. Assign to these offsets distinct moduli $m_{T}, \dots, m_{T + K_{L} - 1}$ . Solve simultaneously $x \equiv 0 (\mod M_{T})$ and $x \equiv - j$ modulo the modulus assigned to $j$ . Put $Q_{L} = \prod_{i < T + K_{L}} m_{i}$ and choose this solution in $[Q_{L}, 2 Q_{L})$ . Every integer of $[x, x + L)$ is then divisible by a modulus: either an old one or its assigned new one. Let $u$ be the greatest admissible integer below $x$ ; its successor is at least $x + L$ , so the gap is at least $L$ . The scale assumption gives

ℓ (2 Q_{L}) \leq T + K_{L} + O (1),

because $\log_{2} m_{i} = 2^{i + O (1)}$ and these upper bounds sum geometrically. Since $u < 2 Q_{L}$ , the ratio for this gap is at least $L / (T + K_{L} + O (1))$ , tending to $σ_{T}^{- 1}$ . These $u$ tend to infinity: $x \geq Q_{L} \to \infty$ and admissible integers are unbounded. Hence the limsup is at least $σ_{T}^{- 1}$ for every $T$ . Let $T \to \infty$ to finish. ◻

For the Fermat moduli $m_{j} = 2^{2^{j}} + 1$ , pairwise coprimality and the finite-product identity

\prod_{j = 0}^{N} (1 - \frac{1}{2^{2^{j}} + 1}) = \frac{2^{2^{N + 1} - 1}}{2^{2^{N + 1}} - 1}

give $σ = 1 / 2$ , so the coefficient is exactly $2$ . These results describe gaps between integers avoiding fixed moduli. They do not construct multipliers or numerator and denominator sequences satisfying the exact recurrences. In particular, the static proportion $σ$ must not be substituted for $φ (v_{T}) / v_{T}$ : the first excludes multiples of the whole moduli, while the second excludes every prime factor of the reduced denominator.

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 the absolute-convergence form of Corollary 3.2 of , including its signed numerators, and recover the all-positive specialisation used for comparison here. For the printed condition interpreted as mere signed convergence, first justify the nonvanishing-product step discussed in Section 3. That interpretation is not treated as an already verified formalisation target.

Statements and declarations

Artefact and data availability.

The pinned formal-source revision contains the Lean sources, the fixed toolchain and library manifest for the formalised results. Each declaration establishes its stated implication. Results that also need written arguments are identified separately in the manuscript.

The supplied source index records a successful build of the listed main-repository modules at revision 6b78209ab63a, using the identical-file evidence described there. The links in this manuscript retain their original pins, including 3d6d938d696f; this build record is not a new verification of every linked revision. No new Lean run or transitive-axiom audit is claimed here, and the separate release is not covered as a whole. A source link is not a build receipt. The external formal-conjecture entry states the problem rather than proving it. The ordinary proofs and their exposition require mathematical review independently of the recorded checks.

Funding and competing interests.

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

Acknowledgements.

I thank Wouter van Doorn for advice on exposition, including the explanation of restrictive hypotheses and the removal of unnecessary terminology. The problem numbering follows the supplied Erdős Problems catalogue snapshot [13].

Guide to the formal sources

The main-repository links retain revision 3d6d938d696f; other links specify their repository and revision. The supplied source index records a main-repository build at 6b78209ab63a and sixty theorem-specific Comparator checks in the separate release. The label release only distinguishes the repositories and build records; it does not deny those sixty checks. The principal state theorem is in ReciprocalTailRigidity.lean. The scalar convergence theorem is in SparseResetRecovery.lean, and the bounds on cancelled factors are in RepairEntropy.lean. The rational-tail estimates are separate checked declarations in PaperCompleteR7, not consequences of the abstract state module alone. The checked periodic statement assumes $e_{n} < a_{n}$ ; Section 10 derives this bound eventually for a periodic positive error magnitude. The bounded-negative statement lists strict centring and vanishing relative error separately; the latter implies the former eventually by taking $K = 1$ . Sections 3 and 12 give the construction from a rational reciprocal sum.

A factorial residue reduction for forced orbits

In the case $m = c = 1$ of Section 9, where the shape equation (5.1) reads $D_{n} + 1 = (a_{n} - 1) (n + 1)$ , each multiplier is determined by its predecessor; we call such an orbit forced. At index $n$ the numerator of the next multiplier is

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

the forced numerator, and the divisor is $n + 2$ . The orbit continues for another step exactly when this division is exact. The formal survival predicate requires exact division at each step. Example 9.1 is the forced orbit from $a = 3$ read this way: $num (0, 3) = 6$ is divisible by $2$ and gives $a_{1} = 3$ , while $num (1, 3) = 13$ is not divisible by $3$ , so the orbit stops there. 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 [12]; for the forced numerator that product is a factorial.

Theorem B.1 (factorial residue reduction). For all $h$ and all integers $a \equiv b (\mod (h + 1)!)$ , the orbit from $a$ survives $h$ forced updates exactly when the orbit from $b$ does.

Proof. Define $M (0, i) = 1$ and $M (h + 1, i) = (i + 2) M (h, i + 1)$ . Thus $M (h, 0) = (h + 1)!$ . We prove the stronger statement that, at index $i$ , congruent inputs modulo $M (h, i)$ survive the same $h$ updates. There is nothing to prove for $h = 0$ .

For the inductive step, suppose $a \equiv b (\mod (i + 2) M (h, i + 1))$ . Since $num (i, \cdot)$ is an integer polynomial, its values at $a$ and $b$ are congruent modulo that product. In particular, one is divisible by $i + 2$ if and only if the other is. If neither is divisible, both orbits stop. Otherwise their quotients are congruent modulo $M (h, i + 1)$ , so the induction hypothesis applies to the remaining $h$ updates at index $i + 1$ . Taking $i = 0$ proves the claim. ◻

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.

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

Exact enumeration for $2 \leq a_{0} < 5000$ gives a maximum of $17$ successful updates, or $18$ multiplier values including $a_{0}$ . Nine seeds attain it, the least being $1501$ . The seed $a_{0} = 1$ is excluded: it gives $a_{n} = 1$ at every step and violates the hypothesis $a_{n} \geq 2$ . Survival here counts exact divisions, not all the conditions on a positive integer orbit. The finite search does not prove the infinite exclusion; Theorem 9.2 does so under its stated hypotheses. The reduction remains useful because its shrinking-modulus argument applies to other recurrences defined by polynomial division.

Result map and proof dependencies

The following map records proof dependencies. A checked component does not confer that status on an assembled ordinary theorem. The short note contains its bounded-increment proof in Sections 2–4. Details kept here rather than repeated there are the signed-series comparison in Section 3, the integer-coefficient extension at the end of Section 6, the general $1 + c / n$ comparison in Section 7, and the scalar failed-divisibility example in Section 14. The cubic and double-logarithmic arguments retain their separate proofs in Section 2 and Theorem 7.3, respectively.

Bounded upward increments.

Vanishing relative error gives eventual absorption. Bounded negative values at arbitrarily late indices give a stable gcd; CRT then excludes the unbounded reduced tail with bounded upward increments. The state theorem and rational-tail construction have supplied main-repository build evidence. The increment bound is an extra hypothesis.

A convergent sum of relative increases.

The inequality $C_{n + 1} \leq C_{n} (1 + (- E_{n})_{+} / C_{n})$ turns summability into a uniform bound on $C_{n}$ . Integrality then permits only finitely many rises, after which the numerator stabilises. No vanishing relative error is needed. The scalar and exact-orbit results have cited main-repository declarations; the linked rational-tail formulation is outside that build record.

New maxima and prime-power persistence.

A bound on the negative reduced error scaled by the previous maximum also bounds every cancellation factor. Primes larger than that bound persist in the reduced denominator, giving the CRT contradiction in Theorem 7.5. The double-logarithmic argument uses the density-one coprimality count to obtain enough moduli, then controls the height of the CRT block. The LCM numerator gives weighted first-crossing estimates. A prime power dividing the reduced denominator persists while the unreduced next numerator stays below the threshold in Corollary 7.2. Crossings can be counted before that threshold is reached. The large odd prime powers and convergence equivalences have written proofs. Separate-release integer lemmas and main-repository conditional record declarations establish only their stated conclusions.

Cubic rate.

The tail estimate and finite differences of the Gamma ratio force an eventual cubic polynomial for the integer numerator. The recurrence and Chebotarëv then force a square in the cubic field. The trace calculation leaves $m = 12$ , and both possible signs are excluded modulo seven. This is an ordinary proof. Finite checks and component sources do not constitute a formal proof of the complete cubic-rate theorem.

Static barriers.

For sufficiently sparse prime moduli, a coprime integer sequence can have unbounded but very small increments. At the specified double-exponential scale, counting residue classes and applying CRT give the largest gaps between integers divisible by none of the whole moduli. These auxiliary results do not construct reciprocal-tail examples.

What remains.

For the unrestricted problem, one still needs the stated summability or record bound, or a contradiction to the necessary conditions on a counterexample. The static examples and local identities supply neither.

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.
V. Kovač and T. Tao, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), no. 2, 572–608, doi:10.1007/s10474-025-01528-0; arXiv:2406.17593v4. Page references are to arXiv:2406.17593v4.
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.
W. van Doorn, Y. Li and Q. Tang, Optimal bounds for an Erdős problem on matching integers to distinct multiples, preprint arXiv:2603.28636v1, 2026.
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, supplied snapshot of 28 July 2026; not a live status verification.
The Formal Conjectures Authors, FormalConjectures.ErdosProblems.243, Lean source at commit f776d2f, 2025. Formal problem statement, not a proof.
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.
E. H. el Abdalaoui, M. Lemańczyk and T. de la Rue, A dynamical point of view on the set of $B$ -free integers, Int. Math. Res. Not. IMRN (2015), no. 16, 7258–7286, doi:10.1093/imrn/rnu164. The cited definition is also in §1.2 of arXiv:1311.3752v3.

Introduction

Irrationality at the cubic rate

The integer tail.

Reduction under the zero lower-density assumption

A square condition from three consecutive numerators

The square condition forces 𝑚 =12m=12

The two remaining cubics fail modulo seven

From an asymptotic ratio to an exact polynomial

Prior work and formalisation

Classical criteria and pseudo-greedy expansions.

Results and proof status.

Integer numerators, denominators and errors

Construction from the reciprocal sum.

When a zero error forces the Sylvester recurrence

Relations among three consecutive numerators

A criterion using new maxima of an LCM numerator

Formalisation.

Integer coefficients.

New maxima of reduced numerators

Fractions in lowest terms.

Comparison with Duverney’s reduced parameters.

How fast the running maximum must increase

Formalisation.

Bounds that allow for cancellation and earlier decreases

Counting jumps before a prime power can be lost

Formalisation.

Bounds on the error and on the original sequence

Formalisation.

Attribution.

Signs of the error and of the growth ratio

A comparison with BB-free integers.

Conditions on a possible counterexample.

Descent when the error is nonnegative

When the negative error is constant

When the negative error is periodic

Bounded increases and coprimality to earlier moduli

A lower bound on the error forces eventual zero

Finite total relative increase

Complements and further questions

A scalar profile need not satisfy the recurrences.

Growth of the factors repeated in the denominator

Cancellation before a numerator regains its former value

The direct analytic question

What changes when upward increments are not bounded

Formalisation targets

Erdős–Straus.

Duverney.

Statements and declarations

Artefact and data availability.

Funding and competing interests.

Acknowledgements.

Guide to the formal sources

A factorial residue reduction for forced orbits

Result map and proof dependencies

Bounded upward increments.

A convergent sum of relative increases.

New maxima and prime-power persistence.

Cubic rate.

Static barriers.

What remains.

References

The square condition forces $m = 12$

A comparison with $B$ -free integers.