Metadata

slug: fokkink-joshi-2025-continued-fraction-tail-beatty
bibkey: fokkinkjoshi2025hiccup
doi: 10.1007/s11139-025-01305-1
url: https://arxiv.org/abs/2507.16956v4
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/ContinuedFractionTailBeattyRefutation.result

Continued-fraction tails with u = 2 and v = 1 miss the Beatty sequence

Problem

R. Fokkink and G. Joshi, On Cloitre’s hiccup sequences, arXiv:2507.16956v4, Section 4 after Equation (14), state the two-parameter family

$s_{n} = n u + v + \frac{n ^{2}}{s _{n + 1}}$

and its asymptotic line

$α = \frac{u + u ^{2} + 4}{2}, β = \frac{v α ^{2} - α}{α ^{2} + 1} .$

They state that positive tails satisfying $s_{n} = α n + β + O (1/ n)$ round down to the Beatty sequence with slope $α$ and offset $β$ . The settling declaration is D5.S1.Recurrence.ContinuedFractionTailBeattyRefutation.result.

Statement echo

The Lean beta, IsTail and claim definitions retain the source’s radical slope, offset, positive-tail recurrence, uniform $C / n$ error bound, and floor equality. The claim body is displayed in the Scribe and the result proves its negation.

Motivation

The source’s generalization would transfer an asymptotic estimate into an exact floor identity. The settlement supplies a positive-tail counterexample at $u = 2$ , $v = 1$ .

Gap

The preregistration is issue #18586. The source’s Section 4 statement and Theorem 24 were read. The recorded literature screen found no settlement of this generalization in its searched scope; completeness remains ASSUMED-UNVERIFIED.

Route

Set $α = 1 + 2$ and $β = 1/2$ . On the closed set of bounded real sequences with $0 \leq e_{k} \leq 1/ (k + 1)$ , the error operator induced by the recurrence preserves the set and is a contraction with factor $1/4$ . Its fixed point gives positive tails with

$\frac{1}{8 n} < s_{n} - (α n + 1/2) < \frac{α}{4 n} .$

At $n = 1$ , the Beatty line has floor $2$ , while the recurrence gives $s_{1} = 3 + 1/ s_{2} > 3$ . Therefore the universal rounding assertion is false. The module uses the existing frozen metallicValue owner for the metallic mean while keeping the source radical literal in claim.

Pell-index comparison

The following derivation is mathematical exposition, proved in prose. The kernel-checked settlement is the index-one case; the quantified Pell-index conclusion is not a Lean declaration in this delivery.

For $r \in N$ , define integer sequences by

$p_{0} = 3, n_{0} = 1, p_{r + 1} = 3 p_{r} + 8 n_{r}, n_{r + 1} = p_{r} + 3 n_{r} .$

Induction shows that $p_{r}$ is odd and $p_{r}, n_{r} \geq 1$ . The Pell invariant is preserved because

$p_{r + 1}^{2} - 8 n_{r + 1}^{2} = (3 p_{r} + 8 n_{r})^{2} - 8 (p_{r} + 3 n_{r})^{2} = p_{r}^{2} - 8 n_{r}^{2} = 1.$

Both sequences strictly increase, since $p_{r + 1} - p_{r} = 2 p_{r} + 8 n_{r} > 0$ and $n_{r + 1} - n_{r} = p_{r} + 2 n_{r} > 0$ . Eliminating $p_{r}$ gives

$n_{r + 2} = p_{r + 1} + 3 n_{r + 1} = 6 p_{r} + 17 n_{r} = 6 n_{r + 1} - n_{r} .$

Define the integer $m_{r}$ and the asymptotic line value $x_{r}$ by

$m_{r} = n_{r} + \frac{p _{r} + 1}{2}, x_{r} = α n_{r} + \frac{1}{2}, α = 1 + 2 .$

The positive Pell invariant implies $p_{r} > 2 n_{r} 2$ , and rationalization gives the exact gap

$0 < m_{r} - x_{r} = \frac{p _{r} - 2 n _{r} 2}{2} = \frac{1}{2 ( p _{r} + 2 n _{r} 2 )} < \frac{1}{8 n _{r}} .$

The final inequality uses $p_{r} + 2 n_{r} 2 > 4 n_{r} 2 > 4 n_{r}$ . Combining this gap with the sharp error bounds for the constructed tails gives

$m_{r} - 1 < x_{r} < m_{r} < x_{r} + \frac{1}{8 n _{r}} < s_{n_{r}} < x_{r} + \frac{α}{4 n _{r}} < m_{r} + 1.$

Here $m_{r} - x_{r} < 1$ gives the left endpoint, and $α / (4 n_{r}) < 1$ gives the right endpoint because $n_{r} \geq 1$ and $α < 4$ . Thus

$⌊ s_{n_{r}} ⌋ = m_{r}, ⌊ α n_{r} + 1/2 ⌋ = m_{r} - 1.$

This proves the Pell-index floor comparison in prose for the constructed tails. Formalizing that quantified corollary remains open; this argument assumes neither uniqueness of positive tails nor their identification with finite truncations.

Falsifier

A positive tail for $u = 2$ , $v = 1$ satisfying the stated error bound and having $⌊ s_{1} ⌋ = 2$ would falsify the refutation. The formal result uses the exact index-one contradiction. Positive-tail uniqueness, ordinary finite-truncation identification and the quantified Pell-index family are outside the kernel-checked declaration.

Evidence

Kernel-checked settling: D5.S1.Recurrence.ContinuedFractionTailBeattyRefutation.result : ¬ claim.
The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.
The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).
The Scribe attaches one OpenProblemResolutionClaim with resolution Refuted to result.
The source is documented by the Library note.

Experiment

The pinned numerical check is in the experiment directory, from commit cd9d66a5f5ff37b01ef63b93f24d14b8ca3278c3; check.py has SHA-256 4b86cbed203000b36f11ff68c34641aae75a3c1b172ee05d539477002567ee9b. Command python3 docs/reports/fokkink-joshi-2025-continued-fraction-tail-beatty/check.py in that repository exits 0 with RESULT PASS. It checks $u = 2, v = 1$ through $1 \leq n \leq 1300$ , the Theorem 24 control through $1 \leq n \leq 3000$ , and the $v = - 1$ , $u \in {1, 2, 3}$ control through $1 \leq n \leq 3000$ .

Triage

item	status	evidence and scope
Pell family definition $(p_{0}, n_{0}) = (3, 1)$ , $p_{r + 1} = 3 p_{r} + 8 n_{r}$ , $n_{r + 1} = p_{r} + 3 n_{r}$	proved in prose	Recursive construction in the Pell-index comparison above; not a kernel-checked declaration.
Pell invariants, monotonicity and $n_{r + 2} = 6 n_{r + 1} - n_{r}$	proved in prose	Induction, invariant expansion and elimination in the Pell-index comparison above.
Pell gap $0 < m_{r} - (α n_{r} + 1/2) = 1/ (2 (p_{r} + 2 n_{r} 2)) < 1/ (8 n_{r})$	proved in prose	Rationalization of the Pell invariant above, with $m_{r} = n_{r} + (p_{r} + 1) /2$ .
Pell-index floor comparison	proved in prose	The displayed comparison chain gives $⌊ s_{n_{r}} ⌋ = m_{r}$ and $⌊ α n_{r} + 1/2 ⌋ = m_{r} - 1$ for the constructed tails.
Lean formalization of the Pell-family corollary	open	No declaration states the quantified Pell-index comparison.
Numerical failures at indices $1, 6, 35, 204, 1189$	computed	Pinned experiment above, exact tested scope $n \leq 1300$ , exit 0, script SHA-256 above.
Theorem 24 control failures through $n \leq 3000$	computed	Pinned experiment above, exact tested scope $n \leq 3000$ , exit 0, script SHA-256 above; zero failures.
Original Conjecture 20 with $v = - 1$ , $u = 1, 2, 3$	computed	Pinned experiment above, exact tested scope $n \leq 3000$ , exit 0, script SHA-256 above; no failures.
Failure mechanism: analytic positive $1/ n$ correction crosses a Beatty integer at $n = 1$	proved	Kernel-checked by `result`, through `tail_exists`, `error_bounds`, `beta_value` and the floor contradiction.
Positive-tail uniqueness and identification with ordinary finite truncations	open	Not assumed by or encoded in `result`.
Equation (11) family	open	A neighbouring source question outside this claim.
Parameter pairs $(u, v)$ for which the generalized rounding assertion holds	open	The source’s $u = 1, v = φ - 1$ case survives; no classification is asserted.

What the settlement shows

Refuted by result: the universal two-parameter rounding assertion after Equation (14), because a positive tail at $u = 2$ , $v = 1$ satisfies the required $O (1/ n)$ bound but fails the floor equality at $n = 1$ .

Mechanism: the fixed-point error is strictly positive and of order $1/ n$ , while the index-one Beatty line lies below the next integer. The Pell-index comparison above proves the extension in prose for the constructed tails. The kernel-checked settlement is the index-one case and does not identify all positive tails.

Nearest statements that survive: the source’s Theorem 24 case $u = 1$ , $v = φ - 1$ and the original Conjecture 20 specialization $v = - 1$ are outside the refuted parameter choice. Their finite numerical controls are computed only over the scopes recorded above.

Follow-up questions: Lean formalization of the Pell-family corollary, positive-tail uniqueness, finite-truncation convergence, the Equation (11) family and the set of valid $(u, v)$ remain open.

ASSUMED-UNVERIFIED

Literature completeness and priority remain ASSUMED-UNVERIFIED; the recorded source and citation screen is bounded. The Pell-family generalization, positive-tail uniqueness, finite-truncation convergence and all parameter classifications beyond the kernel-checked counterexample are not formalized here.

Keyboard shortcuts

trureturing — Discovering truth