A positive constant-recursive sequence with nonquasipolynomial power ranks

Dev D. Goyal

A positive constant-recursive sequence with nonquasipolynomial power ranks

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Power ranks of constant-recursive sequences: Rowland–Sistos Barrón finiteness conjecture
Posed in: Rowland and Sistos Barrón, 'Complexity of powers of a constant-recursive sequence' (arXiv:2501.14643), unnumbered fixed-rank finiteness conjecture on page 2 of the author-hosted preprint
Status: Counterexample
Result: s(n) = 1 + 2^n + 3^n(1 − 2^n)² + n9^n(1 + 2^n)³ has rank 13 and power ranks P(M) − 2Q(M), not eventually quasipolynomial; a companion family gives infinitely many power-rank sequences at each rank r ≥ 3.

Abstract

Exact minimal recurrences for every power of a rank-thirteen sequence, nonquasipolynomial ranks, and infinitely many power-rank profiles at each rank at least three.

Details

Year: 2026
Discipline: Mathematics
Area: Integer sequences
Subject: Integer sequences and combinatorics
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: power-rank
Keywords: C-finite sequences, constant-recursive sequences, linear recurrences, power ranks, quasipolynomial, recurrence order of powers

Statement and scope

Formal scope. The main and arbitrary-rank companion theorems are formalized. Generating-function and polynomial corollaries retain conventional proofs.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 296 KB
PDF on GitHub: papers/mathematics/power-rank/manuscript.pdf
LaTeX source: papers/mathematics/power-rank/manuscript.tex
Bibliography: papers/mathematics/power-rank/references.bib

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/power-rank/

Lean project

papers/mathematics/power-rank/formalization/ 35 Lean files

Lakefile

papers/mathematics/power-rank/formalization/lakefile.toml

Toolchain

leanprover/lean4:v4.35.0

Library roots

formalization/src/CompleteAudit.lean

Reproduce

The commands below are quoted from papers/mathematics/power-rank/README.md, which gives their context and working directory.

Build and reproduce

mkdir -p .build
latexmk -pdf -interaction=nonstopmode -halt-on-error -outdir=.build manuscript.tex
cp .build/manuscript.pdf manuscript.pdf

Build and reproduce

mkdir -p .build
python3 -B supplement/test_optimization_guard.py
python3 supplement/check_revision.py --max-power 14 --max-bm 3 --output .build/revision-checks.json

README: papers/mathematics/power-rank/README.md
Proof map: papers/mathematics/power-rank/PROOF_MAP.md
Authorship: papers/mathematics/power-rank/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Priority and subsequent correspondence. On 29 October 2026, through correspondence with Professor Eric Rowland, I learned that he had independently obtained an infinite family of rank sequences for rank-three recurrences while experimenting with an LLM. The constructions have not been compared. Priority and novelty record.

Questions and answers

What does this paper prove about power ranks of constant-recursive sequences?

It determines the minimal characteristic polynomial of every power of an explicit positive integer sequence of rank 13, whose power ranks equal P(M) − 2Q(M) with P cubic and Q a parity-restricted square count, so they are not eventually quasipolynomial. A companion family gives infinitely many distinct power-rank sequences at each initial rank r ≥ 3. Rank 13 is not claimed minimal.

Does this contradict a conjecture of Rowland and Sistos Barrón?

The companion family contradicts, as written, the unnumbered fixed-rank finiteness conjecture on page 2 of their author-hosted preprint, for every r ≥ 3. Eric Rowland has independently obtained an infinite family of rank sequences for rank-three recurrences; the constructions have not been compared. Their Conjecture 5.3 is not claimed refuted, since its term 'pseudo-polynomial' is undefined there.

Is the proof formally verified?

The main rank-13 theorem and the companion family theorem for all r ≥ 3, d ≥ 2 and M ≥ 0 are formalized in Lean 4. The generating function, eventual polynomial degree and leading coefficient, and rank-three examples keep conventional proofs, and the paper is an unrefereed preprint.

Cite

Citation file papers/mathematics/power-rank/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{Goyal2026PowerRanks,
  author = {Goyal, Dev D.},
  title = {A positive constant-recursive sequence with nonquasipolynomial power ranks},
  year = {2026},
  note = {Unpublished manuscript. Historical priority remains provisional}
}