Irrationality of Lacunary Fibonacci Reciprocal Sums

The problem and why it is difficult

Let $F_1=F_2=1$, $F_{n+1}=F_n+F_{n-1}$, and let $n_1<n_2<\cdots$ be any infinite index sequence with a uniform ratio gap $n_{k+1}/n_k\ge c$ for some $c>1$. Erdős asked whether

$$\sum_k \frac{1}{F_{n_k}}$$

must be irrational.

For fast-growing gaps this is classical territory: when $c\ge 2$ the series is covered by known irrationality criteria for lacunary series (Badea, 1993). The genuinely open range was $1<c<2$, where the terms shrink too slowly for size-based criteria — the tail of the series is not small enough compared with its leading term to force a contradiction from a single denominator. Any proof must instead exploit the precise arithmetic of Fibonacci numbers, not just their growth.

Where the natural approaches stalled

• Pure size arguments fail. Below $c=2$, the tail $\sum_{j>k}1/F_{n_j}$ can be comparable to $1/F_{n_k}$, so the classical "the fractional part cannot be that small" argument does not close.
• Working modulo one denominator loses the structure. Individual $F_n$ share deep divisibility relations (periods, gcd identities); rationality forces global coherence conditions across all selected indices simultaneously, which no single modulus sees.
• Golden-ratio expansions need exactness. The identity $1/F_n=\sqrt5\sum_j(-1)^{nj}\varphi^{-(2j+1)n}$ converts the series into a Lambert-type series in $\varphi^{-1}$, but making "the coefficients cannot all cancel" rigorous requires controlling a lattice of quadratic integers, not an archimedean estimate.

The proof architecture

The formal proof assumes a rational (more generally, a scaled-golden) total and derives a contradiction in three stages.

1. Exact Lambert and quadratic-norm infrastructure. The reciprocal Fibonacci expansion is collected into a locally finite integer coefficient word over $\mathbb Z[\varphi]$. A rational total forces normalized residuals to lie in a fixed lattice, and a sufficiently long equal / mismatch / equal comparison between two windows of the word produces a nonzero quadratic integer whose norm lies strictly between $0$ and $1$ — impossible. The rest of the proof engineers such a comparison.

2. Reduction to bounded two-adic order. If the selected indices contain arbitrarily deep dyadic structure (unbounded two-adic order), they must contain a complete selected dyadic tail; such tails can be deleted exactly, preserving both the ratio gap and the scaled-golden total, and only finitely many disjoint tails can exist. This reduces any putative rational counterexample to one with uniformly bounded selected two-adic order.

3. The reverse-window contradiction. For the bounded-order remainder, the proof selects arbitrarily late "genuinely new" prefix periods, makes the reduced period quotient odd, and controls compatibility conditions with an exact offset count on a linear-width budget. Protecting two affine window centers by a polynomial CRT density argument isolates a singleton target inside a short radius; a protected sieve plus the norm gate from stage 1 then contradicts the assumed total. The cutoff at which this happens is explicit — polynomial in the period data — so the argument closes without any unproved case.

Combining the two branches eliminates every rational value, for every sequence with any uniform ratio gap $c>1$.

Verification

The faithful statement quantifies over all index sequences with the exact quotient condition from the problem:

theorem erdos_problem_267
    (n : ℕ → ℕ) (hpos : ∀ k, 0 < n k) (hmono : StrictMono n)
    (hgap : HasRatioGap n) :
    Irrational (reciprocalFibSeries n)

where reciprocalFibSeries is the real tsum of (Nat.fib (n k))⁻¹ and HasRatioGap asserts one real $c>1$ with $c\le n_{k+1}/n_k$ for all $k$. The pinned project builds with warnings promoted to errors (lake --wfail build), a source scan finds no proof placeholders, and #print axioms reports exactly [propext, Classical.choice, Quot.sound]. The download bundle contains the pinned statement project, the self-contained standalone artifact, and the checker documentation with the line-by-line fidelity audit.