Reciprocal Sums and the Sylvester Recurrence: Further Results and Proofs

Will Cook

Long paper

Reciprocal Sums and the Sylvester Recurrence: Further Results and Proofs

Erdős #243 By Will Cook September 2026 Authorship, AI use and citation

PDFOpen the PDF, 61 pages TeXLaTeX source Source on GitHub Problem page

Summary. Integer finite differences exclude nonintegral regular rates and reduce the cubic rate to a polynomial. A square condition in the cubic field and congruences modulo seven then prove irrationality. For rational reciprocal sums with $a_{n + 1} / a_{n}^{2}$ tending to one, the record derives sufficient Sylvester-recurrence criteria from persistent divisors, bounded numerator increases and weighted crossings of new maxima. The arithmetic estimates needed to apply these criteria to every rational reciprocal sum remain open.

This paper covers cubic and nonintegral regular-rate irrationality, integer-tail arithmetic and sufficient Sylvester-recurrence criteria, with their separate hypotheses and remaining estimates.

It does not establish the validity of claims tagged Lean, which belongs to the cited kernel-checked source, or a solution to Erdős #243, which remains open.

Start here, by the editorial route

In this paper

Verification and reproducibility

The fixed toolchain, library manifest and Lean sources are in the public repository. The evidence record identifies the exact declarations, source versions and Comparator status, including source-pin and index gaps. The external formal-conjecture entry states the problem without proving it. The printed square-specialisation proof uses Chebotarev, while the formal proof uses a Dedekind-zeta pole comparison; the shared conclusion does not check every step of the printed argument. No new Lean build, Comparator replay or independent review was performed for this revision.

The recurrence identities and arithmetic exclusions are in ReciprocalTailRigidity.lean, the scalar convergence theorem is in SparseResetRecovery.lean, and the bounds on cancelled factors are in RepairEntropy.lean. The Lean statement excluding a periodic error assumes $e_{n} < a_{n}$ ; Section 10 derives this bound eventually for a periodic positive error magnitude. The printed bounded-negative theorem uses $E_{n} / C_{n} \to 0$ . The formal statement uses its division-free form, $K | E_{n} | < C_{n}$ eventually for each natural $K$ ; the bound $| E_{n} | < C_{n}$ is its $K = 1$ case. Sections 3 and 12 give the construction from a rational reciprocal sum.

Indexing of the regular-rate theorems

Index translation for the Lean statements. Both Lean declarations use $b : N \to N$ , including a positive $b_{0}$ , whereas the theorems above start at $a_{1}$ . A simple shift changes $λ / n$ by order $n^{- 2}$ and may lose the stated $o (n^{- λ})$ precision. Instead choose a large $N$ with $a_{N} > N$ . Such an $N$ exists: strict increase gives $a_{n} \geq n$ and the rate gives $a_{n}^{2} / a_{n + 1} < 2$ eventually, hence $a_{n + 1} > a_{n}^{2} / 2 \geq n^{2} / 2 > n + 1$ for large $n$ . Define

b_{n} = {\begin{cases} n + 1, & 0 \leq n < N, \\ a_{n}, & n \geq N . \end{cases}

Then $b$ is positive and strictly increasing, with the same indexed rate for every $n \geq N$ . Moreover

\sum_{n \geq 0} \frac{1}{b_{n}} - \sum_{n \geq 1} \frac{1}{a_{n}} = \sum_{n = 0}^{N - 1} \frac{1}{n + 1} - \sum_{n = 1}^{N - 1} \frac{1}{a_{n}} \in Q .

The series converge by the stated rapid-growth rate. If the original sum were rational, so would be the sum for $b$ , contradicting the corresponding zero-indexed Lean theorem. This finite-prefix implication is proved here in ordinary mathematics; the Lean declarations check the zero-indexed theorems themselves.

The square-specialisation proofs

Lemma 2.7 and its consequences, Proposition 2.8, Theorem 2.3 and Theorem 2.1, are formalised without Chebotarev. The printed proof of Lemma 2.7 uses that theorem; its Lean proof instead uses the simple pole of the Dedekind zeta function. The zero-indexed Lean statement of Theorem 2.1 requires the finite-prefix bridge above.

The nonintegral-rate formal proof uses the real-parameter extraction theorem and a quantitative canonical-tail estimate. Convergence of the reciprocal series is derived from the rate.

Recurrence declarations

Proposition 4.1. update law.

Proposition 4.3. denominator, numerator and error.

Theorem 5.1. defect identity.

Theorem 5.3. local rigidity step.

Theorem 5.7. eventual Sylvester recurrence.

Theorem 5.8. absorption of a vanishing error, with the companion contrapositive along a tail.

Theorem 8.1. stabilisation of the nonnegative error, using the eventual constancy of a nonincreasing sequence.

Lemma 11.1. shifted consecutive multiples.

Theorem 11.3. the Chinese-remainder first-crossing consequence.

Theorem 12.1. The theorem is stated with an eventual lower bound and division-free vanishing relative error. The Lean proof shifts past both thresholds and applies the version with $| E_{n} | < C_{n}$ 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.

Theorem 13.1. The scalar conclusion is the eventual vanishing for a positive integer sequence; its exact-orbit consequence is the scalar recurrence from a convergent sum. A separate exact-orbit formulation retains the denominator and tail update equations, positivity, the centered-step identity and division-free normalized vanishing. Under $\sum_{n} (- E_{n})_{+} / C_{n} < \infty$ , the checked results give a bound on numerator growth, eventual zero error, and the Sylvester recurrence. These are conditional hypotheses, not properties proved here for the original orbit. The plectis-erdos-lean repository contains a formulation for the rational-tail numerators using a convergent sum, not covered by the evidence record. Summability remains an assumption; the elementary scalar implication needs neither growth nor vanishing relative error.

Proposition 14.1. In the Lean statement of Proposition 14.1, the divergent sum of relative increases is recorded as divergence of the partial sums.

About this paper

Authorship and AI use. Will Cook built and directed the research infrastructure and maintains the public release. He reviewed claims when he could. AI agents did most of the research and drafting. Cook did not independently verify every claim.

Cite and contact. Cite this paper by its title, author and date above, with its PDF; cite the earlier sources it uses for a mathematical result. For software, use the release citation and give the commit used. Contact Will with questions or corrections.

Prefer the manuscript?

PDFOpen the PDF, 61 pages TeXOpen the LaTeX source Problem page

Equations typeset from the exact TeX. Rendered from the LaTeX manuscript source with file fingerprint sha256:92512a9aa35a79c5. Its file fingerprint matched the published source record, so the PDF above, the LaTeX, and this page are one manuscript. Redeploying the site regenerates this page from whatever the public repository holds at that moment.