Zero-preserving integer normalization

Exact statement

If (Q) clears the recurrence-coefficient denominators and (E) clears the initial-value denominators, then (g_k=EQ^k f_k) is an integer LRS of polynomial description size and (f_n=0) exactly when (g_n=0).

StatusProved by an index-dependent scaling

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

Context

Clearing denominators only once changes the recurrence. The power Q^k is the necessary correction.

Hypotheses and scope

Q and E are positive common multiples of the relevant denominators.

Proof or evidence

Substitution gives $g_{k+d}=\sum_i c_iQ^{d-i}g_{k+i}$ ; every coefficient is integral, the new description has polynomial bit length, and the nonzero scale (EQ^n) preserves zeroness.

Rational-to-integer normalization →

Verification notes

The exponent d−i, integrality, bit-length bound, and zero-preservation step were checked independently.

Limitations

The scaling preserves zero tests, not the literal numerical values.

Open work

Include the scaling explicitly in every later reduction from rational LRS input.