Explicit indexed LRS zeroness

Exact statement

An order-(d) rational linear recurrence sequence is given by binary-encoded initial values $f_0,\ldots,f_{d-1}$ , recurrence coefficients $c_0,\ldots,c_{d-1}$ , and a binary index (n); the decision question is whether (f_n=0).

StatusPrecisely stated for explicit rational recurrence input

External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

The bit model and input encoding are essential because a term at a binary index can have exponentially many output bits.

Definitions

The recurrence has the form $f_{k+d}=\sum_{i=0}^{d-1}c_i f_{k+i}$ .

Hypotheses and scope

All numerators, denominators, and n are encoded in binary.

Proof or evidence

The definition fixes the model for the normalization, matrix-power equivalence, and complexity bounds below.

Input model and normalization →

Verification notes

The source question states a rational LRS and binary index but does not spell out a representation; the site therefore labels this assumption explicitly.

Limitations

Rational generating functions, weighted automata, closed forms, and succinctly encoded recurrence order require separate conversion analyses.

Open work

Maintain this as the exact public input model; analyze other succinct representations separately.