[formalization] Certified recurrence spaces and lag–derivative trade-offs #1978

Purpose and proof status

Formalize an algebraic theory of alternative recurrence representations for
a specified polynomial sequence, then use checked derivative lifts in the
row tactics. Real-rootedness is a downstream application, not a hypothesis
of the recurrence theory.

Related: #555 (sequence annihilators), #1235 (higher-order pure-lag families),
#1234 (derivatives of several lagged rows), and #1061 (promotion/tactics).
This is distinct from #1908, which concerns a universal PF operator comparison.

The statements below have paper proofs and exact research audits. They are
not yet Lean theorems. The external Polytool implementation is a separate
workstream: the representation menu reports finite fits, and a separate opt-in
backend now computes complete bounded coefficient spaces and certificates
conditional on a supplied source recurrence. Finite fitting alone does not
prove an identity for the intended infinite sequence.

1. First target: the complete bounded recurrence space

Polytool implementation contract (updated 2026-10-21)

Implemented and pushed in Polytool ec48a23,
on feat/recurrence-representations-20261020. The API documentation
and checked example
are included. This is external exact verification, not a Lean proof. The opt-in CLI mode is
polytool recurrence --space, accepting a JSON request on stdin, with
--verify-space for independent certificate replay. The library and MCP
expose find_recurrence_spaces and verify_recurrence_spaces; the existing
finite-fit finder and --representations retain their meanings.

Requests declare exact coefficient support (or degree-box shapes), original
index/domain, and either a monic source plus seeds or finite rows alone.
Constant-index sources use h*k residuals, counting the target coefficient's
index degree in h. The new indexed_source form accepts Q[n,X] coefficients
and supplies an explicit common residual propagator and sufficient prefix
instead. Finite-row positives are labeled as fits. Complete nullspaces include zero-leading relations; successor
existence requires nonzero target projection. Absence uses dual witnesses
y_i^T C=e_i^T, valid from the supplied rows alone. Basis completeness uses
exact null vectors, an independent basis minor and a rank lower-bound minor.

Outputs distinguish bounded coverage, evidence, singular indices, exact
polynomial division and resource exhaustion. A zero kernel after a completed
exact calculation is different from an interrupted calculation. This first
release does not claim spectral or unrestricted-order classification.
The schema is polytool.recurrence-spaces.v1. The browser Complete spaces
mode and WASM adapter share that exact contract and export the full report.
No live website publication or installed-MCP replacement occurred in this
checkpoint. Existing finite-fit schemas remain unchanged.

Verification passed: all 360 library tests and existing integration suites;
25 complete-space and three CLI regressions; 34 MCP library tests plus
binary/stdio, 13 native web tests, five doctests; strict
Clippy/Rustdoc; and all 50 Node checks against optimized WASM. The regressions
cover A049325, A171608, A111049's exceptional initial row, finite support,
nonminimal sources, sparse tails in the original index, a high-degree leader,
all-zero matrices, singular ranks outside the checked prefix, inconsistent
source initial rows, and corrupted basis/minor/dual witnesses. Returned
A049325/A171608 representatives also replay independently in the old evaluator.

The exact singularity diagnostic reports all nonnegative integer base ranks
where the entire leader vanishes, or explicitly unknown beyond degree 8 or
128-bit coefficient bounds. For indexed-source propagation, a proved Cauchy
root bound supplies a safe cutoff when the exact exceptional-rank list is
unknown. Inhomogeneous/nonmonic sources and automatic subsequence transforms
are not part of this backend. Constant sources retain source+h for
reconstructing chi^h; indexed sources include explicit polynomial propagation
coefficients. Lean scripts remain a consumer task.
The source-bound replay checks a kernel and rank certificate by multiplication,
reducing only the small leader projection. Its expected-request argument binds
independently supplied assumptions; CLI replay checks the embedded assumptions.

Additional opt-in controls are automatic_variable_degree shapes and
include_leader_coverage: true. The former removes the RHS X-degree guess,
retaining explicit index/derivative/leader bounds. The latter combines
representatives into one identity regular at every rank where the returned
space can generate, possibly increasing coefficient degrees. Section 4a
states the proofs and certificate contract. Both are available in the browser
Complete spaces view, with Hermite and automatic-degree examples.
The source-conditional status and declared domain apply to combined identities
unchanged. Budget failures remain incomplete. General spectral/localization
and unrestricted index-degree/order algorithms are still future work.

The Lean consumer should initially check defect propagation and finite seeds.
External Rust results are certificates to replay, never trusted axioms.

Mathematical statement

Work over K = Q initially. Let k > 0 and let the specified sequence satisfy

P[n+k] = sum(i < k) a[i](X) P[n+i],

where a[i] belongs to K[X] and is independent of n, with k given initial
rows. Write F = N/D, where D(0) = 1, deg_t N < k and deg_t D <= k.
Cancellation is optional. For j >= 0, the shifted generating function
F_j = sum(n >= 0) P[n+j] t^n has the form N_j/D with deg_t N_j < k.

Fix any finite nonempty allowed support of operators

L = sum(j,s,u,v) c[j,s,u,v] X^v n^u S^j derivative_X^s,

with coefficients on the left, nonnegative exponents, and S P[n] = P[n+1].
Put h = 1 + max(u+s) on this support, including the target coefficient
at derivative order zero, and theta = t derivative_t.

Filtered iff. All identities in this support are precisely the kernel
of the K-linear map

C(L) = D^h sum(j,s,u,v) c[j,s,u,v] X^v theta^u derivative_X^s F_j.

C(L) is a polynomial in X,t of t-degree at most h*k-1. Consequently,

(L P)[n] = 0 for all n >= 0
iff
(L P)[n] = 0 for 0 <= n < h*k.

Proof: each derivative or theta raises the necessary denominator power by
at most one and the numerator t-degree by at most k. Multiplication by
D^h clears all denominators. Since D(0)=1, the first h*k zero coefficients
force this numerator to vanish. This also covers nonminimal source
recurrences, zero rows and finite-support sequences. Empty support is the
trivial zero operator and can be handled separately.

For a successor rule

delta(n) P[n+r] = sum(j < r, s <= m) C[j,s](n,X) derivative_X^s P[n+j],

restrict the target coefficient to the requested support in K[n]. Such a
rule exists iff the kernel has nonzero projection onto those target
coordinates. Zero-leading differential identities must not be mistaken for
successor rules. Arbitrary distinct coefficient-degree caps and selected
lag/derivative pairs are supported by the same theorem.

Finite negative certificate without a source recurrence. For the residual
matrix C built from any finite set of supplied rows in the claimed domain,
zero projection of ker(C) onto the target coordinates already rules out a
successor identity in this shape for every sequence agreeing with the rows.
It has a compact dual certificate: for each target coordinate i, return
y_i with y_i^T C = e_i^T. Applying this equality to a null vector proves
its i-th coordinate zero. Conversely these witnesses exist whenever that
projection is zero, by row-space/nullspace orthogonality. Source assumptions
and the finite-check theorem are needed for positive all-index identities,
not for these negative obstructions.

The theorem also holds on a declared tail by replacing P[n] with P[n+N].
Evaluate coefficient monomials at the original index, or transform their
entire allowed support when reindexing. Sparse support {n^2} does not remain
{n^2} after a nonzero index shift. The source must hold from its seed origin;
a delayed source with earlier prefix rows must be normalized explicitly.
It does not give this bound for n-dependent source coefficients. A shape
with largest forward shift j needs source rows through hk-1+j, not merely
hk rows in total. Exact elimination with M unknowns and R scalar equations
costs O(R M^2 + M^3) rational field operations; this is not a bit bound.

2. Practical Lean certificate first

Define the source and lift defects

R[n] = P[n+k] - sum(i < k) a[i] P[n+i],
E[n] = delta(n) P[n+1] - A(n,X) P[n] - B(X) derivative(P[n]),
delta(n) = d1*n+d0,   A(n,X) = A1(X)*n+A0(X).

Let chi(z) = z^k - sum(i < k) a[i] z^i and

J(z) = sum(i < k) ((k-i)*a[i]*(d1*z-A1) - B*derivative(a[i]))*z^i.

Universal defect identity, valid for arbitrary polynomial rows:

E[n+k] - sum(i < k) a[i]*E[n+i]
  = delta(n+k)*R[n+1] - A(n+k,X)*R[n]
    - B*derivative(R[n]) + (J(S) P)[n].

This is just the product rule and the two affine coefficient differences.
If J = gamma*chi, it becomes

E[n+k] = sum(i < k) a[i]*E[n+i]
  + delta(n+k)*R[n+1] - (A(n+k,X)-gamma)*R[n]
  - B*derivative(R[n]).

For the source-defined sequence, k zero lift-defect seeds prove the lift
by induction. The multipliers of earlier lift defects are exactly the
source recurrence coefficients. For A049325, J = X*chi. Conversely, if the
lift is given, R[0]=0 and delta(n+k) != 0 let the same identity prove the
pure-lag recurrence by induction. Exceptional zeros require extra seeds.
This converse uses the derivative of an already proved R[n]=0; it is not
an elimination from unrelated lift instances alone.

Export the product-rule identity and its induction corollaries first.
Use congrArg Polynomial.derivative on recurrence equalities,
linear_combination with the displayed multipliers, and exact polynomial
normalization. No division by B or a variable polynomial is needed.

General certificate when the short identity does not apply

We can prove the finite-residual theorem without formal power series.
Let T=chi(S), let N multiply a sequence by n, and let D_X differentiate X.
On arbitrary polynomial sequences,

[T,N] = (z*chi_z)(S),     [D_X,T] = chi_X(S).

Both right sides commute with T. Hence T^q f=0 implies
T^(q+1)(N f)=0 and T^(q+1)(D_X f)=0. Shifts and multiplication by X
commute with T. Induction proves that every residual in the support of
section 1 satisfies chi(S)^h E=0, before checking its seeds. This is a
monic recurrence of order hk; its first hk zero rows prove E=0.
This is the preferred first implementation of the general checker:
small operator/product-rule lemmas plus monic recurrence extensionality.
The coefficients of chi^h and the finite seeds are explicit certificate data.

Alternatively, export the operator identity chi(S)^h L = Q chi(S).
The two elementary identities

chi^2 D_X = (chi D_X - chi_X) chi,
chi^2 N   = (chi N + (z*chi_z)(S)) chi

give this membership constructively. Exact right division by the monic
source operator retains Q. Expanding Q gives multipliers of shifted
derivatives of the source defect for linear_combination. This offers an
instance checker before the general closure theorem is available.

For a filtered residual E, Q=D^h annihilates E after the first h*k rows.
Writing Q=sum(q[j]*t^j), q[0]=1, gives explicit multipliers -q[j] for
the homogeneous defect recurrence beyond that initial range. The finite
seeds then prove E=0. Formalize this propagation or the filtered iff above.

A more general certificate also handles index-dependent source coefficients.
For a sufficiently large companion jet state, retain the exact identity

Z[n+1] = T[n] Z[n] + sum(u <= s) e[u] derivative^u R[n],
E[n] = v[n] Z[n].

Here e[u] injects into the last coordinate of jet block u, and if C[n]
is the source companion matrix, its lower jet blocks are
T[n]_(u,v) = binomial(u,v)*derivative^(u-v) C[n] for v <= u.
Choose a verified row dependence

sum(j=0..r) c[j] v[n+j] T[n+j-1] ... T[n] = 0.

With empty products equal to the identity, define

m[u,l] = sum(j=l+1..r) c[j] v[n+j] T[n+j-1] ... T[n+l+1] e[u].

Then for arbitrary rows,

c[r] E[n+r] = -sum(j < r) c[j] E[n+j]
  + sum(l < r, u <= s) m[u,l] derivative^u R[n+l].

Proof: iterate the inhomogeneous state equation and cancel its initial-state
coefficient using the checked row dependence. Retaining row operations
produces the multipliers, not just an assertion that they exist. Clear a
common denominator in the whole identity, prove any cancelled leading
factor nonzero, and discharge its exceptional integer indices separately.

3. Structural theory: repeated poles and a first-order iff

These are subsequent formalization targets, not prerequisites for checking
a particular certificate. Decompose the reduced rational F into a finite
polynomial part U(t) and a proper tail. In a splitting field,

P_tail[n] = sum(i=1..d) a_i(n,X) lambda_i(X)^n,
deg_n a_i = multiplicity_i - 1,

where the d distinct nonzero bases are active. Repeated poles change the
polynomial amplitudes; d counts distinct bases, not pole multiplicities.
Put

q_i = derivative_X(a_i)/a_i + n*lambda_i'/lambda_i,
h_i = lambda_i*a_i(n+1,X)/a_i(n,X).

First-order iff and uniqueness. For d >= 2, a rational-coefficient
eventual rule P[n+1]=A P[n]+B P'[n] exists iff q is nonconstant across
components and h belongs to span{1,q}. The normalized A,B are unique:
B=(h_i-h_j)/(q_i-q_j), A=h_i-B*q_i for any unequal pair.
Existence and the unique answer descend to K(n,X).

Proof: independence of exponential-polynomial sequences gives h=A+Bq
componentwise. The h_i are not all equal since their limits at n=infinity
are the distinct lambda_i. For d=1 a pure-lag one-row rule already exists;
the uniqueness assertion is omitted. Finite support d=0 is a boundary case.

If M=max(multiplicity_i-1), a lift for the proper tail has a polynomial
representative Delta P[n+1]=C P[n]+E P'[n] with n-degrees bounded by
(2M+1,2M+1,2M). In an n-independent basis, the amplitude, derivative
and shift columns have degrees M,M+1,M, so 2x2 minors give these bounds.
Primitive gcd reduction gives the same bounds for an index-only leader
whenever such a leader exists. Finite boundary masking may raise them.

Finite model and rational length/order trade-offs

Let p(z) be the squarefree nonzero characteristic polynomial,
E=K(X)[z]/p(z), and V=E(n), of dimension d over K(n,X). Define

z' = -p_X/p_z,
S(v) = z*v(n+1),
nabla(v) = total_derivative_X(v) + n*(z'/z)*v.

The amplitude a belongs to V. Then L annihilates the tail iff
L(S,nabla)a=0. The vectors a,Sa,...,S^(d-1)a form a basis: their
determinant's highest n-coefficient is a nonzero amplitude product times
the Vandermonde determinant of the bases. Consequently the full rational
eventual annihilator is generated by

S^d - sum(j < d) r[j] S^j,
derivative_X - sum(j < d) b[j] S^j,

with coefficients obtained from this basis. These are identities for the
specified sequence, not arbitrary consequences of its one displayed
pure-lag operator with unspecified seeds.

For 1 <= r <= d, a rational length-r, derivative-order-at-most-s rule
exists iff S^r a lies in the span of
{nabla^u S^j a : j<r, u<=s}. If any order works, s <= d-r works:
the spans start with dimension r; equality at successive orders gives
differential closure, otherwise dimension increases. This computes a full
frontier over K(n,X), for eventual identities.

For polynomial-coefficient L, the all-index condition adds exactly
(L U)[n]=0 for 0<=n<=deg_t U. Boundary factors must not be cancelled
using tail information alone.

4. Polynomial restrictions and unavoidable singular ranks

The rational bound d-r does not hold when the leading coefficient must lie
in K[n]. At fixed (r,s), form the matrix with columns

[ S^r a | -nabla^u S^j a ],  j<r, u<=s,

and clear a common denominator to obtain T over A=K[n,X]. Its polynomial
kernel is exactly the eventual coefficient module. To impose initial rows,
each finite-part residual is a row R_k with the condition
R_k v = 0 mod (n-k). Thus the all-index module is the projection of

kernel [[T,0],[R,-diag(n,n-1,...,n-deg_t U)]].

It is finitely generated by polynomial syzygies. If G_i are generators,
the possible leaders form the ideal I generated by their first coordinates.
The index-only leaders are exactly

I intersect K[n] = (g(n)), with g monic or zero.

Existence is equivalent to g != 0. If g(k)=0 then every such identity is
singular at k at this fixed support; if g has no nonnegative integer zeros,
a witness with leader g generates regularly there. Retaining an elimination
witness gives a vector v0 with leader g. All index-only identities are
f(n)*v0 + sum H_i(n,X)*Z_i, where Z_i generate the zero-leading module.
Use ideal elimination, not gcd: (n,X) intersect K[n]=(n) although
gcd(n,X)=1. Equality of the projected ideals at two adjacent derivative
orders does not prove permanent stabilization.

Essential counterexample. For every m>=1,
P[n]=1+(2+X^m)^n has two simple poles, but its least derivative order in
a one-row polynomial-coefficient rule with nonzero leader in K[n] is m.
For order <m, evaluate at X=0 after separating the two bases: every positive
derivative coordinate vanishes there, whereas the shift contrast is 1.
For order m, Bezout applied to the first and mth derivative numerators over
K(n)[X] supplies a witness; clear denominators in n. Thus there is no
replacement bound depending only on d in this coefficient class.

With unrestricted coefficient degrees and singular initial indices allowed,
existence at any derivative order reduces to membership of S^r a in the
K(n)[X]-module generated by the first r shifts. Holonomic localization
and Weyl-module algorithms decide this problem. This is a long-term theory
target, not a request to implement a D-module package before the useful
certificate lemmas. It does not solve a fixed-degree or everywhere-nonsingular
variant merely by invoking the rational-field stopping bound.

4a. Automatic RHS degree, regular leaders and indexed-source propagation

These statements have direct paper proofs and are implemented by the linked
Polytool checkpoint; they are additional Lean targets, not formalized facts.

Polynomial solution degree bound

Let H be an E-by-M matrix over Q[X] of rank rho>=1, with entry degrees
at most D>=0. Let b have degree at most B>=0. If Hp=b has a polynomial
solution, it has one with

deg p <= max(B+(rho-1)D, rho D-1, 0).

Choose a nonsingular rank minor K=H[I,J], Delta=det K, d=deg Delta.
The identity Delta H_l=H_J adj(K) H[I,l] lets us divide every nonpivot
coordinate by Delta and transfer its quotient into the pivot coordinates.
Nonpivot remainders have degree below d and vanish if d=0. Cramer's rule
gives pivot coordinates of degree at most
(rho-1)D+max(B,D+d-1)-d; if d=0 omit the second term. This proves
the bound. When H=0, solvability is b=0, with p=0.
We can replace rho by the safe upper bound min(E,M).

Fix lag, derivative, index-degree and leader-degree bounds, leaving RHS
X-degree free. A finite residual criterion uniform under X-multiplication
gives H(X)p=b(X). The bound above preserves every allowed leader.
Thus the kernel computed at that cap has exactly the leader projection for
arbitrary RHS X-degree. A completed absence is correspondingly stronger;
the bounded kernel itself is not the whole polynomial module.
Large caps may exceed resource limits. Index degree and derivative order
are not made unrestricted by this construction.

A single identity covering the regular ranks

For identities L_i with the same target and real polynomial leaders delta_i,
form the left combination

L_* = sum_i delta_i L_i,     delta_* = sum_i delta_i^2.

At a real rank a, delta_(a,X) is identically zero iff every delta_i(a,X)
is identically zero: evaluate at real X and use the sum-of-squares property.
These are precisely the ranks where every polynomial combination of the
supplied identities has identically zero leader. Lag and derivative bounds
are preserved; coefficient degrees may grow by the leader degrees.
For index-only leaders, delta_ is positive at every regular rank.

The certificate is the displayed list of left polynomial multipliers, which
is directly suitable for linear_combination. No derivative acts on a
multiplier. Common integer singular ranks come from the gcd of all
X-coefficients of all leaders, regarded as polynomials in n. The scope is
the polynomial module generated by the supplied space, not every possible
larger-support recurrence. X-dependent leaders still require exact division.

Finite certificates for monic polynomial-index sources

Suppose P[n+k]=sum(i<k) a_i(n,X)P[n+i], a_i in Q[n,X], valid from
the declared source origin. For derivative order s, the jet state
Z_n=(D^d P[n+i])_(d<=s,i<k) has dimension q=k(s+1) and a polynomial
transition Z[n+1]=T(n,X)Z[n]. Its last derivative-block row uses
binom(d,e) D^(d-e)a_i; other rows shift.

Deduplicate the requested (lag,derivative,index-power) triples after removing
X-powers. Express their m columns as V(n,X)Z[n]. Put
W_0=V and W_(j+1)=W_j(n+1)T(n). Flatten these m-by-q matrices over
Q(n,X). Linear dependence gives polynomial coefficients, after clearing
denominators, with

sum(j=0..r) c_j(n,X) W_j(n,X)=0,   c_r != 0,   r <= mq.

Consequently every shaped residual E satisfies sum_j c_j E[n+j]=0,
including arbitrary Q[X]-multiples. The identity holds at every rank even
where an intermediate elimination pivot vanished: it is a polynomial
identity, rather than a pointwise division certificate.

Choose N at least the domain start and beyond all nonnegative integer ranks
where c_r specializes to the zero polynomial. A residual is identically zero
on the domain iff it vanishes through N+r-1. Induction cancels nonzero c_r
in Q[X] on the tail; the finite prefix covers earlier ranks. For r=0 and
N equal to the domain start, no seed residual is needed.

The exceptional ranks are roots of the gcd of c_r's X-coefficients. If
exact enumeration is unavailable, any nonzero coefficient polynomial
g(n)=a_d n^d+...+a_0 gives the sufficient cutoff
floor(max(i<d)|a_i/a_d|)+2 by Cauchy's root bound. The report marks the
root list unknown in that case. A bound on order alone does not bound N.

Replay reconstructs W_j, checks the polynomial dependence, nonzero leader,
cutoff and finite kernel/rank witnesses. It does not repeat dependence search.
Search uses at most mq+1 state matrices and O((mq)^3) polynomial operations
for elimination; degree/bit growth and prefix length remain separately
bounded. This also supplies the uniform residual criterion needed by the
automatic X-degree theorem. Nonmonic source denominators are outside this
implementation's contract.

Useful added regressions are Hermite's H[n+1]=2XH[n]-H[n]' (four residuals,
order-four propagator), P[n]=n!X^n (automatic cap 3, order-two propagator),
P[n+1]=(n-17)XP[n] (late exception beyond h*k), degree-nine propagation
leaders using the Cauchy fallback, leaders n and n-1 combining to
2n^2-2n+1, and altered dependence/cutoff/combination certificates.

5. Tactic integration and regressions

At revision 1b2a3184aad604ac7110627d5f6e3f39743b1d0b, existing infrastructure
includes Tactic/Recurrence/{Shape,Eval,Degree,ODE}.lean,
Tactic/RowInterlacing.lean, and
DerivativeRecurrence/RootWindow.lean. In particular reuse
RealRooted.derivRec_interlaces_of_window,
RealRooted.derivRec_interlaces_of_roots_mem_Icc and
RealRooted.derivRec_interlaces_of_roots_le where their hypotheses apply.
Current Lean uses AP'+BP; this issue uses AP+BP'. Prefer descriptive
coefficient names in any certificate structure.

The proposed route is: parse source and seeds; probe for a useful lift;
verify its certificate; then apply the existing derivative/window theorem
and discharge degree, leading-sign, normalization, root-sign and seed goals.
In particular delta(n)>0 is a separate condition when dividing an identity
for a sign-sensitive root theorem. A lift by itself proves no root property.
Second derivatives and several derivative-bearing lags belong to the
algebraic search even when no root theorem applies to that representation.

Use exact fixtures pinned to OEIS-proofs revision
9bb3970e5ba7877b77572c066bd56fbf8f63f05c:

These structural negatives should become formal regression theorems when
the required layer exists. A bounded probe may only claim absence within
its specified support. Finite exact audits are useful tests, not proofs of
all-index nonexistence or real-rootedness.

Acceptance and staging

• Algebraic defect identity and induction corollaries, with A049325 client. (Recurrence spaces, phase A: shift operators, filtered finite check, defect identity (#1978) #1997)
• General finite-residual theorem with explicit bound and arbitrary support. (Recurrence spaces, phase A: shift operators, filtered finite check, defect identity (#1978) #1997)
• Checked certificate import/replay and exceptional-index handling. (draft Recurrence spaces, phase B: certificate replay, exceptional indices, row-tactic adapter (#1978) #1998, unverified)
• Proof-producing row-tactic adapter reusing existing root-window theory. (draft Recurrence spaces, phase B: certificate replay, exceptional indices, row-tactic adapter (#1978) #1998, unverified)
• Full bounded-kernel iff, including nonzero successor projection.
• Finite-row dual obstruction lemma, independent of a source recurrence.
• Repeated-pole first-order iff, uniqueness and degree bounds.
• Finite spectral model and rational trade-off stopping theorem.
• Fixed-support polynomial-module and leading-ideal statements.
• Counterexample separating rational and index-only coefficient classes.
• Polynomial-matrix preimage degree bound and complete unbounded-X leader projection.
• Sum-of-squares leader combination, common singular ranks and left-multiplier replay.
• Polynomial-index jet transition, common propagator and exceptional-rank zero induction.
• Evaluate unrestricted-order formalization separately after useful layers land.

The first four items are the first practical milestone. Later items can be
split into linked issues. Keep recurrence algebra independent of real-rootedness
and avoid forcing a full Ore algebra implementation into the first milestone.
Use generic Mathlib-shaped names and types where practical. Completion needs
checked declarations and tactic tests, focused/default builds, repository
guards and axiom audits; no admissions or trusted external search results.

Primary references and attribution

This is a specialization of established annihilator/module methods; no
novelty claim is intended. Creative telescoping concerns elimination from
annihilating ideals, but a supplied annihilating ideal can be strictly smaller
than the full annihilator of the sequence with its specified initial data.
A nonzero remainder modulo such an ideal is not a nonexistence proof.

• Chyzak–Salvy (1998), §2, especially §2.2.2, for Ore algebra and effective
  operator manipulation: primary paper.
• Hyun–Neiger–Schost (ISSAC 2019), for implemented polynomial-matrix kernels,
  system solving and basis reduction over prime fields (an optimization
  reference, not an attribution of our precise degree bound):
  authors' preprint.
• Koutschan, HolonomicFunctions, for implemented holonomic operations:
  author's software page.
• Zhang (ISSAC 2016), Theorem 4.2 and Algorithms 4.6/5.5, for fixed-order
  syzygies, contraction and desingularization:
  author's paper.
• Oaku–Takayama, Algorithm 6.4, and Oaku–Takayama–Walther, §1, for effective
  localization: primary paper,
  preprint.
• Chen–Jaroschek–Kauers–Singer, Theorem 9, for order-degree trade-offs:
  primary preprint.

These references motivate algorithms; they do not replace proving the precise
sequence, coefficient-class and boundary statements above.

External review

A requested read-only Claude Opus 5.5 review found no definite mathematical
errors in the supplied core arguments; it ran no computations or Lean builds.
It recommended the finite-row dual obstruction, strict index/domain handling,
and a small defect-certificate checker before spectral or module machinery.
Those recommendations are reflected above. The broader structural statements
remain later proof targets, not requirements for the first useful tactic.