diff --git a/RealRooted.lean b/RealRooted.lean
index 12887667e..f106efa4b 100644
--- a/RealRooted.lean
+++ b/RealRooted.lean
@@ -2058,3 +2058,8 @@ import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.CanonicalProduct
 import RealRooted.Tactic.Row.ThresholdOrbit
 import RealRooted.ThresholdMatrix.Orbit
 import RealRooted.NarayanaInterpolation
+import RealRooted.Mathlib.Algebra.LinearRecurrence.Operator
+import RealRooted.RecurrenceSpace.Defect
+import RealRooted.RecurrenceSpace.Filtered
+import RealRooted.RecurrenceSpace.Operators
+import RealRooted.Tactic.Examples.A049325RecurrenceSpace
diff --git a/RealRooted/Mathlib/Algebra/LinearRecurrence/Operator.lean b/RealRooted/Mathlib/Algebra/LinearRecurrence/Operator.lean
new file mode 100644
index 000000000..ce658a4ce
--- /dev/null
+++ b/RealRooted/Mathlib/Algebra/LinearRecurrence/Operator.lean
@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2026 Per Alexandersson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Per Alexandersson
+-/
+import Mathlib.Algebra.Polynomial.Derivative
+import Mathlib.Algebra.Polynomial.Monic
+import Mathlib.Tactic.LinearCombination
+import Mathlib.Tactic.Ring
+import RealRooted.Mathlib.Algebra.LinearRecurrence.Annihilator
+
+/-!
+# Polynomial actions on recurrence sequences
+
+A polynomial acts on a sequence by evaluating it at the forward shift.  We also prove that a
+monic annihilator is determined by its initial values and compute its commutator with
+multiplication by the sequence index.
+-/
+
+open Finset Polynomial
+
+namespace LinearRecurrence
+
+variable {R : Type*}
+
+noncomputable section
+
+section CommRing
+
+variable [CommRing R]
+
+/-- The action of a polynomial on a sequence, obtained by evaluating at the forward shift. -/
+def shiftAction (p : R[X]) : (ℕ → R) →ₗ[R] ℕ → R :=
+  Polynomial.aeval forwardShift p
+
+@[simp]
+theorem shiftAction_zero : shiftAction (0 : R[X]) = 0 := by
+  simp [shiftAction]
+
+@[simp]
+theorem shiftAction_one : shiftAction (1 : R[X]) = LinearMap.id := by
+  ext u
+  simp [shiftAction]
+
+/-- Products of shift polynomials act by composition. -/
+theorem shiftAction_mul_apply (p q : R[X]) (u : ℕ → R) :
+    shiftAction (p * q) u = shiftAction p (shiftAction q u) := by
+  simp [shiftAction, Polynomial.aeval_mul, Module.End.mul_apply]
+
+/-- Powers of a shift polynomial act by iterating its action. -/
+theorem shiftAction_pow_apply (p : R[X]) (q : ℕ) (u : ℕ → R) :
+    shiftAction (p ^ q) u = (shiftAction p ^ q) u := by
+  induction q generalizing u with
+  | zero => simp
+  | succ q ih => simp [pow_succ, shiftAction_mul_apply, ih]
+
+private def recurrenceOfMonic (p : R[X]) : LinearRecurrence R where
+  order := p.natDegree
+  coeffs i := -p.coeff i
+
+private theorem charPoly_recurrenceOfMonic {p : R[X]} (hp : p.Monic) :
+    (recurrenceOfMonic p).charPoly = p := by
+  rw [LinearRecurrence.charPoly]
+  dsimp only [recurrenceOfMonic]
+  rw [monomial_one_right_eq_X_pow]
+  change X ^ p.natDegree - ∑ i : Fin p.natDegree, monomial i (-p.coeff i) = p
+  calc
+    _ = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i := by
+      rw [Fin.sum_univ_eq_sum_range (fun i ↦ monomial i (-p.coeff i)) p.natDegree]
+      simp [← C_mul_X_pow_eq_monomial]
+    _ = p := hp.as_sum.symm
+
+/-- A sequence annihilated by a monic shift polynomial is zero when its first
+`p.natDegree` entries are zero. -/
+theorem eq_zero_of_monic_of_shiftAction_eq_zero {p : R[X]} (hp : p.Monic)
+    {u : ℕ → R} (hann : shiftAction p u = 0)
+    (hinit : ∀ n < p.natDegree, u n = 0) : u = 0 := by
+  let E := recurrenceOfMonic p
+  have hsol : E.IsSolution u := by
+    rw [isSolution_iff_aeval_charPoly_eq_zero, charPoly_recurrenceOfMonic hp]
+    exact hann
+  rw [E.eq_iff_eqOn_range_order u 0 hsol E.solSpace.zero_mem]
+  intro n hn
+  exact hinit n (mem_range.mp hn)
+
+/-- Multiplication of a sequence by its index. -/
+def indexMul : (ℕ → R) →ₗ[R] ℕ → R where
+  toFun u n := (n : R) * u n
+  map_add' u v := by ext n; simp [mul_add]
+  map_smul' a u := by ext n; simp [mul_left_comm]
+
+@[simp]
+theorem indexMul_apply (u : ℕ → R) (n : ℕ) : indexMul u n = (n : R) * u n :=
+  rfl
+
+/-- A monomial in the shift acts by a scalar times an iterated forward shift. -/
+theorem shiftAction_monomial_apply (a : R) (k : ℕ) (u : ℕ → R) :
+    shiftAction (monomial k a) u = a • (forwardShift ^ k) u := by
+  simp [shiftAction, ← C_mul_X_pow_eq_monomial, Polynomial.aeval_mul,
+    Module.End.mul_apply]
+
+/-- The commutator of a shift polynomial with index multiplication is the action of
+`X * p.derivative`. -/
+theorem shiftAction_indexMul_sub (p : R[X]) (u : ℕ → R) :
+    shiftAction p (indexMul u) - indexMul (shiftAction p u) =
+      shiftAction (X * p.derivative) u := by
+  induction p using Polynomial.induction_on' with
+  | add p q hp hq =>
+      simp only [shiftAction, map_add, mul_add]
+      ext n
+      have hp' := congr_fun hp n
+      have hq' := congr_fun hq n
+      simp only [shiftAction, LinearMap.add_apply, Pi.add_apply, Pi.sub_apply,
+        indexMul_apply] at hp' hq' ⊢
+      linear_combination hp' + hq'
+  | monomial k a =>
+      ext n
+      simp only [shiftAction_monomial_apply, Pi.smul_apply, smul_eq_mul,
+        forwardShift_pow_apply, indexMul_apply, Pi.sub_apply, derivative_monomial]
+      by_cases hk : k = 0
+      · simp only [hk, add_zero, zero_tsub, Nat.cast_zero, mul_zero, monomial_zero_right,
+          shiftAction_zero, LinearMap.zero_apply, Pi.zero_apply]
+        ring
+      · rw [X_mul_monomial, Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hk),
+          shiftAction_monomial_apply]
+        simp only [Pi.smul_apply, smul_eq_mul, forwardShift_pow_apply]
+        simp only [Nat.cast_add]
+        ring
+
+/-- The commutator form of `shiftAction_indexMul_sub`. -/
+theorem shiftAction_indexMul (p : R[X]) (u : ℕ → R) :
+    shiftAction p (indexMul u) =
+      indexMul (shiftAction p u) + shiftAction (X * p.derivative) u := by
+  have h := shiftAction_indexMul_sub p u
+  rw [sub_eq_iff_eq_add] at h
+  simpa only [add_comm] using h
+
+end CommRing
+
+end
+
+end LinearRecurrence
diff --git a/RealRooted/Production.lean b/RealRooted/Production.lean
index f1ff10639..248f88df8 100644
--- a/RealRooted/Production.lean
+++ b/RealRooted/Production.lean
@@ -1878,6 +1878,10 @@ import RealRooted.MultiplierSequence.PolyaSchur.LaguerrePolya.CanonicalProduct
 import RealRooted.Tactic.Row.ThresholdOrbit
 import RealRooted.ThresholdMatrix.Orbit
 import RealRooted.NarayanaInterpolation
+import RealRooted.Mathlib.Algebra.LinearRecurrence.Operator
+import RealRooted.RecurrenceSpace.Defect
+import RealRooted.RecurrenceSpace.Filtered
+import RealRooted.RecurrenceSpace.Operators
 
 /-!
 # RealRooted production umbrella
diff --git a/RealRooted/RecurrenceSpace/Defect.lean b/RealRooted/RecurrenceSpace/Defect.lean
new file mode 100644
index 000000000..23fcfa3d1
--- /dev/null
+++ b/RealRooted/RecurrenceSpace/Defect.lean
@@ -0,0 +1,224 @@
+import Mathlib.Tactic.Abel
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
+import RealRooted.RecurrenceSpace.Filtered
+
+/-!
+# Universal source-and-lift defect identity
+
+This module formalizes the universal defect identity and its two propagation corollaries
+from RealRooted issue #1978.  The identity is valid for arbitrary polynomial-valued
+sequences; recurrence and lift assumptions enter only in the corollaries.
+-/
+
+open Finset Polynomial
+
+namespace RealRooted
+
+noncomputable section
+
+variable {K : Type*} [Field K]
+
+/-- An affine polynomial-valued function of a natural-number index. -/
+def affineIndex (c₁ c₀ : K[X]) (n : ℕ) : K[X] :=
+  (n : K[X]) * c₁ + c₀
+
+/-- The defect in a constant-coefficient pure-lag recurrence. -/
+def lagDefect {k : ℕ} (a : Fin k → K[X]) (P : ℕ → K[X]) (n : ℕ) : K[X] :=
+  P (n + k) - ∑ i, a i * P (n + i)
+
+/-- The defect in an affine-index first-order differential lift. -/
+def liftDefect (d₁ d₀ A₁ A₀ B : K[X]) (P : ℕ → K[X]) (n : ℕ) : K[X] :=
+  affineIndex d₁ d₀ n * P (n + 1) - affineIndex A₁ A₀ n * P n -
+    B * (P n).derivative
+
+/-- The monic characteristic polynomial of a pure-lag recurrence. -/
+def lagCharacteristic {k : ℕ} (a : Fin k → K[X]) : Polynomial K[X] :=
+  (LinearRecurrence.mk k a).charPoly
+
+/-- The correction polynomial `J` in the universal defect identity. -/
+def defectCorrection {k : ℕ} (a : Fin k → K[X]) (d₁ A₁ B : K[X]) :
+    Polynomial K[X] :=
+  ∑ i : Fin k, (monomial (i + 1) ((k - i : ℕ) * a i * d₁) -
+    monomial i ((k - i : ℕ) * a i * A₁ + B * (a i).derivative))
+
+private def correctionSummand {k : ℕ} (a : Fin k → K[X])
+    (d₁ A₁ B : K[X]) (P : ℕ → K[X]) (n : ℕ) (i : Fin k) : K[X] :=
+  (k - i : ℕ) * a i * d₁ * P (n + i + 1) -
+    ((k - i : ℕ) * a i * A₁ + B * (a i).derivative) * P (n + i)
+
+private def correctionAction {k : ℕ} (a : Fin k → K[X])
+    (d₁ A₁ B : K[X]) (P : ℕ → K[X]) (n : ℕ) : K[X] :=
+  ∑ i, correctionSummand a d₁ A₁ B P n i
+
+private theorem shiftAction_defectCorrection_apply {k : ℕ} (a : Fin k → K[X])
+    (d₁ A₁ B : K[X]) (P : ℕ → K[X]) (n : ℕ) :
+    LinearRecurrence.shiftAction (defectCorrection a d₁ A₁ B) P n =
+      correctionAction a d₁ A₁ B P n := by
+  have shiftAction_sum (g : Fin k → Polynomial K[X]) :
+      LinearRecurrence.shiftAction (∑ i, g i) =
+        ∑ i, LinearRecurrence.shiftAction (g i) := by
+    simp [LinearRecurrence.shiftAction]
+  have shiftAction_sub (p q : Polynomial K[X]) :
+      LinearRecurrence.shiftAction (p - q) =
+        LinearRecurrence.shiftAction p - LinearRecurrence.shiftAction q := by
+    simp [LinearRecurrence.shiftAction]
+  rw [defectCorrection]
+  rw [shiftAction_sum]
+  simp only [LinearMap.sum_apply, Finset.sum_apply, correctionAction]
+  apply Fintype.sum_congr
+  intro i
+  rw [shiftAction_sub, LinearMap.sub_apply,
+    LinearRecurrence.shiftAction_monomial_apply,
+    LinearRecurrence.shiftAction_monomial_apply]
+  simp [correctionSummand, Nat.add_assoc]
+
+private theorem derivative_lagDefect {k : ℕ} (a : Fin k → K[X])
+    (P : ℕ → K[X]) (n : ℕ) :
+    (lagDefect a P n).derivative = (P (n + k)).derivative -
+      ∑ i : Fin k, ((a i).derivative * P (n + i) +
+        a i * (P (n + i)).derivative) := by
+  rw [lagDefect, map_sub, map_sum]
+  apply congrArg₂ (fun x y ↦ x - y) rfl
+  apply sum_congr rfl
+  intro i _
+  exact derivative_mul
+
+private theorem affineIndex_sub {k : ℕ} (c₁ c₀ : K[X]) (n : ℕ)
+    (i : Fin k) :
+    affineIndex c₁ c₀ (n + k) - affineIndex c₁ c₀ (n + i) =
+      (k - i : ℕ) * c₁ := by
+  have hi : (i : ℕ) + (k - i) = k := Nat.add_sub_of_le i.isLt.le
+  have hi' : (k : K[X]) = (i : ℕ) + (k - i : ℕ) := by
+    rw [← Nat.cast_add, hi]
+  simp only [affineIndex, Nat.cast_add]
+  rw [hi']
+  ring
+
+private theorem correction_summand_identity {k : ℕ} (a : Fin k → K[X])
+    (d₁ d₀ A₁ A₀ B : K[X]) (P : ℕ → K[X]) (n : ℕ) (i : Fin k) :
+    -affineIndex d₁ d₀ (n + k) * a i * P (n + i + 1) +
+        affineIndex A₁ A₀ (n + k) * a i * P (n + i) +
+        B * ((a i).derivative * P (n + i) + a i * (P (n + i)).derivative) +
+        correctionSummand a d₁ A₁ B P n i =
+      -a i * liftDefect d₁ d₀ A₁ A₀ B P (n + i) := by
+  have hd := affineIndex_sub d₁ d₀ n i
+  have hA := affineIndex_sub A₁ A₀ n i
+  have hd' := sub_eq_iff_eq_add.mp hd
+  have hA' := sub_eq_iff_eq_add.mp hA
+  simp only [liftDefect, correctionSummand]
+  rw [hd', hA']
+  ring
+
+/-- The universal source-and-lift defect identity, valid for every polynomial sequence: the
+lag defect of the lift defect is a combination of lag defects plus the correction action. -/
+theorem lagDefect_liftDefect {k : ℕ} (a : Fin k → K[X])
+    (d₁ d₀ A₁ A₀ B : K[X]) (P : ℕ → K[X]) (n : ℕ) :
+    lagDefect a (liftDefect d₁ d₀ A₁ A₀ B P) n =
+      affineIndex d₁ d₀ (n + k) * lagDefect a P (n + 1) -
+        affineIndex A₁ A₀ (n + k) * lagDefect a P n -
+        B * (lagDefect a P n).derivative +
+        LinearRecurrence.shiftAction (defectCorrection a d₁ A₁ B) P n := by
+  change liftDefect d₁ d₀ A₁ A₀ B P (n + k) -
+      ∑ i, a i * liftDefect d₁ d₀ A₁ A₀ B P (n + i) = _
+  rw [shiftAction_defectCorrection_apply, derivative_lagDefect]
+  have hs :
+      ∑ i,
+          (-affineIndex d₁ d₀ (n + k) * a i * P (n + i + 1) +
+            affineIndex A₁ A₀ (n + k) * a i * P (n + i) +
+            B * ((a i).derivative * P (n + i) + a i * (P (n + i)).derivative) +
+            correctionSummand a d₁ A₁ B P n i) =
+        ∑ i, -(a i * liftDefect d₁ d₀ A₁ A₀ B P (n + i)) := by
+    apply sum_congr rfl
+    intro i _
+    simpa only [neg_mul] using
+      correction_summand_identity a d₁ d₀ A₁ A₀ B P n i
+  rw [sub_eq_add_neg, ← sum_neg_distrib, ← hs]
+  simp only [lagDefect, liftDefect, correctionAction]
+  simp_rw [mul_sub, mul_sum]
+  simp_rw [Finset.sum_add_distrib]
+  simp only [Nat.add_assoc, Nat.add_comm 1 k]
+  ring_nf
+  rw [Finset.sum_neg_distrib]
+  ring
+
+/-- Evaluating the lag characteristic polynomial at the shift gives the lag defect. -/
+theorem shiftAction_lagCharacteristic_apply {k : ℕ} (a : Fin k → K[X])
+    (P : ℕ → K[X]) (n : ℕ) :
+    LinearRecurrence.shiftAction (lagCharacteristic a) P n = lagDefect a P n := by
+  simp [LinearRecurrence.shiftAction, lagCharacteristic, LinearRecurrence.charPoly,
+    lagDefect, ← C_mul_X_pow_eq_monomial, LinearRecurrence.forwardShift_pow_apply]
+
+private theorem shiftAction_defectCorrection_eq_smul_lagDefect {k : ℕ}
+    (a : Fin k → K[X]) (d₁ A₁ B gamma : K[X]) (P : ℕ → K[X])
+    (hfactor : defectCorrection a d₁ A₁ B = C gamma * lagCharacteristic a) :
+    LinearRecurrence.shiftAction (defectCorrection a d₁ A₁ B) P =
+      gamma • lagDefect a P := by
+  rw [hfactor, LinearRecurrence.shiftAction_mul_apply]
+  calc
+    LinearRecurrence.shiftAction (C gamma)
+        (LinearRecurrence.shiftAction (lagCharacteristic a) P) =
+      gamma • LinearRecurrence.shiftAction (lagCharacteristic a) P := by
+        ext n
+        simp [LinearRecurrence.shiftAction]
+    _ = gamma • lagDefect a P := by
+      congr 1
+      funext n
+      exact shiftAction_lagCharacteristic_apply a P n
+
+/-- A source recurrence and `k` zero lift-defect seeds imply the differential lift when
+the correction polynomial is a multiple of the source characteristic polynomial. -/
+theorem liftDefect_eq_zero_of_lagDefect_eq_zero {k : ℕ} (a : Fin k → K[X])
+    (d₁ d₀ A₁ A₀ B gamma : K[X]) (P : ℕ → K[X])
+    (hsource : ∀ n, lagDefect a P n = 0)
+    (hfactor : defectCorrection a d₁ A₁ B = C gamma * lagCharacteristic a)
+    (hseed : ∀ n < k, liftDefect d₁ d₀ A₁ A₀ B P n = 0) :
+    liftDefect d₁ d₀ A₁ A₀ B P = 0 := by
+  let E : LinearRecurrence K[X] := LinearRecurrence.mk k a
+  have hcorr := shiftAction_defectCorrection_eq_smul_lagDefect a d₁ A₁ B gamma P hfactor
+  have hsol : E.IsSolution (liftDefect d₁ d₀ A₁ A₀ B P) := by
+    intro n
+    have hid :
+        liftDefect d₁ d₀ A₁ A₀ B P (n + k) -
+          ∑ i, a i * liftDefect d₁ d₀ A₁ A₀ B P (n + i) = _ :=
+      lagDefect_liftDefect a d₁ d₀ A₁ A₀ B P n
+    have hc := congr_fun hcorr n
+    simp only [Pi.smul_apply, smul_eq_mul, hsource, map_zero, mul_zero, sub_zero,
+      zero_add] at hid hc
+    rw [hc] at hid
+    simpa [E] using sub_eq_zero.mp hid
+  rw [E.eq_iff_eqOn_range_order _ 0 hsol E.solSpace.zero_mem]
+  intro n hn
+  exact hseed n (mem_range.mp hn)
+
+/-- Conversely, a differential lift, one zero source-defect seed, and nonvanishing affine
+leaders imply the pure-lag recurrence when the same factor certificate holds. -/
+theorem lagDefect_eq_zero_of_liftDefect_eq_zero {k : ℕ} (a : Fin k → K[X])
+    (d₁ d₀ A₁ A₀ B gamma : K[X]) (P : ℕ → K[X])
+    (hlift : ∀ n, liftDefect d₁ d₀ A₁ A₀ B P n = 0)
+    (hfactor : defectCorrection a d₁ A₁ B = C gamma * lagCharacteristic a)
+    (hseed : lagDefect a P 0 = 0)
+    (hleader : ∀ n, affineIndex d₁ d₀ (n + k) ≠ 0) :
+    lagDefect a P = 0 := by
+  have hcorr := shiftAction_defectCorrection_eq_smul_lagDefect a d₁ A₁ B gamma P hfactor
+  apply funext
+  intro m
+  change lagDefect a P m = 0
+  induction m with
+  | zero => exact hseed
+  | succ n ih =>
+      have hid :
+          liftDefect d₁ d₀ A₁ A₀ B P (n + k) -
+            ∑ i, a i * liftDefect d₁ d₀ A₁ A₀ B P (n + i) = _ :=
+        lagDefect_liftDefect a d₁ d₀ A₁ A₀ B P n
+      have hc : LinearRecurrence.shiftAction (defectCorrection a d₁ A₁ B) P n = 0 := by
+        rw [congr_fun hcorr n, Pi.smul_apply, smul_eq_mul, ih, mul_zero]
+      simp only [hlift, mul_zero, sum_const_zero, sub_zero, ih, derivative_zero,
+        hc] at hid
+      have hmul : affineIndex d₁ d₀ (n + k) * lagDefect a P (n + 1) = 0 := by
+        simpa only [add_zero] using hid.symm
+      exact (mul_eq_zero.mp hmul).resolve_left (hleader n)
+
+end
+
+end RealRooted
diff --git a/RealRooted/RecurrenceSpace/Filtered.lean b/RealRooted/RecurrenceSpace/Filtered.lean
new file mode 100644
index 000000000..8b5d9c1db
--- /dev/null
+++ b/RealRooted/RecurrenceSpace/Filtered.lean
@@ -0,0 +1,140 @@
+import Mathlib.Tactic.Linarith
+import RealRooted.RecurrenceSpace.Operators
+
+/-!
+# Finite certificates for filtered recurrence operators
+
+This module proves the filtered finite-check theorem proposed in RealRooted issue #1978.
+Operators are finite `K[X]`-linear combinations of words in the forward shift, sequence
+index multiplication, and coefficientwise differentiation.
+-/
+
+open Finset Polynomial
+
+namespace RealRooted
+
+noncomputable section
+
+variable {K : Type*} [Field K]
+
+/-- Exponents specifying the word `N^u S^j D^s`. -/
+structure RecurrenceWord where
+  /-- Exponent of the forward shift. -/
+  shiftOrder : ℕ
+  /-- Exponent of coefficientwise differentiation. -/
+  derivativeOrder : ℕ
+  /-- Exponent of index multiplication. -/
+  indexOrder : ℕ
+  deriving DecidableEq
+
+/-- Apply a recurrence word in the order `N^u S^j D^s`. -/
+def RecurrenceWord.apply (w : RecurrenceWord) (f : ℕ → K[X]) : ℕ → K[X] :=
+  (LinearRecurrence.indexMul ^ w.indexOrder)
+    ((LinearRecurrence.forwardShift ^ w.shiftOrder)
+      ((sequenceDerivative ^ w.derivativeOrder) f))
+
+/-- A finite polynomial-coefficient combination of recurrence words. -/
+structure FilteredOperator where
+  /-- The finite collection of words used by the operator. -/
+  support : Finset RecurrenceWord
+  /-- The polynomial coefficient multiplying each word. -/
+  coeff : RecurrenceWord → K[X]
+
+/-- Apply a filtered operator to a polynomial-valued sequence. -/
+def FilteredOperator.apply (L : FilteredOperator (K := K))
+    (f : ℕ → K[X]) : ℕ → K[X] :=
+  ∑ w ∈ L.support, L.coeff w • w.apply f
+
+private theorem shiftAction_pow_le {p : Polynomial K[X]} {a b : ℕ} (hab : a ≤ b)
+    {f : ℕ → K[X]} (hf : LinearRecurrence.shiftAction (p ^ a) f = 0) :
+    LinearRecurrence.shiftAction (p ^ b) f = 0 := by
+  obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le hab
+  rw [pow_add, mul_comm (p ^ a), LinearRecurrence.shiftAction_mul_apply, hf, map_zero]
+
+private theorem shiftAction_pow_iterate_derivative {p : Polynomial K[X]} (q s : ℕ)
+    (f : ℕ → K[X]) (hf : LinearRecurrence.shiftAction (p ^ q) f = 0) :
+    LinearRecurrence.shiftAction (p ^ (q + s)) ((sequenceDerivative ^ s) f) = 0 := by
+  induction s generalizing f q with
+  | zero => simpa using hf
+  | succ s ih =>
+      rw [pow_succ', Module.End.mul_apply]
+      have hs := ih q f hf
+      have hc := shiftAction_pow_succ_sequenceDerivative_eq_zero p (q + s)
+        ((sequenceDerivative ^ s) f) hs
+      simpa only [Nat.add_assoc, Nat.add_comm s 1] using hc
+
+private theorem shiftAction_pow_iterate_index {p : Polynomial K[X]} (q u : ℕ)
+    (f : ℕ → K[X]) (hf : LinearRecurrence.shiftAction (p ^ q) f = 0) :
+    LinearRecurrence.shiftAction (p ^ (q + u))
+      ((LinearRecurrence.indexMul ^ u) f) = 0 := by
+  induction u generalizing f q with
+  | zero => simpa using hf
+  | succ u ih =>
+      rw [pow_succ', Module.End.mul_apply]
+      have hu := ih q f hf
+      have hc := shiftAction_pow_succ_indexMul_eq_zero p (q + u)
+        ((LinearRecurrence.indexMul ^ u) f) hu
+      simpa only [Nat.add_assoc, Nat.add_comm u 1] using hc
+
+private theorem shiftAction_pow_forwardShift {p : Polynomial K[X]} (q j : ℕ)
+    (f : ℕ → K[X]) (hf : LinearRecurrence.shiftAction (p ^ q) f = 0) :
+    LinearRecurrence.shiftAction (p ^ q) ((LinearRecurrence.forwardShift ^ j) f) = 0 := by
+  have hcomm := shiftAction_commute (p ^ q) (X ^ j) f
+  have hshift : LinearRecurrence.shiftAction (X ^ j) f =
+      (LinearRecurrence.forwardShift ^ j) f := by
+    rw [LinearRecurrence.shiftAction_pow_apply]
+    congr 1
+    ext g n
+    simp [LinearRecurrence.shiftAction]
+  rw [hshift] at hcomm
+  rw [hcomm, hf, map_zero]
+
+private theorem shiftAction_pow_word {p : Polynomial K[X]} (h : ℕ)
+    (f : ℕ → K[X]) (hf : LinearRecurrence.shiftAction p f = 0)
+    (w : RecurrenceWord) (hw : w.indexOrder + w.derivativeOrder < h) :
+    LinearRecurrence.shiftAction (p ^ h) (w.apply f) = 0 := by
+  have hbase : LinearRecurrence.shiftAction (p ^ 1) f = 0 := by simpa using hf
+  have hd := shiftAction_pow_iterate_derivative 1 w.derivativeOrder f hbase
+  have hs := shiftAction_pow_forwardShift (1 + w.derivativeOrder) w.shiftOrder
+    ((sequenceDerivative ^ w.derivativeOrder) f) hd
+  have hi := shiftAction_pow_iterate_index (1 + w.derivativeOrder) w.indexOrder
+    ((LinearRecurrence.forwardShift ^ w.shiftOrder)
+      ((sequenceDerivative ^ w.derivativeOrder) f)) hs
+  apply shiftAction_pow_le (p := p) (a := 1 + w.derivativeOrder + w.indexOrder)
+    (b := h) (by lia)
+  exact hi
+
+/-- Every filtered operator of weight below `h` sends a sequence annihilated by `p(S)`
+to a sequence annihilated by `p(S)^h`. -/
+theorem FilteredOperator.shiftAction_pow_apply_eq_zero
+    (L : FilteredOperator (K := K))
+    (p : Polynomial K[X]) (h : ℕ) (f : ℕ → K[X])
+    (hf : LinearRecurrence.shiftAction p f = 0)
+    (hweight : ∀ w ∈ L.support, w.indexOrder + w.derivativeOrder < h) :
+    LinearRecurrence.shiftAction (p ^ h) (L.apply f) = 0 := by
+  rw [FilteredOperator.apply, map_sum]
+  apply sum_eq_zero
+  intro w hw
+  rw [map_smul, shiftAction_pow_word h f hf w (hweight w hw), smul_zero]
+
+/-- Filtered finite check: under a monic degree-`k` source recurrence, a filtered
+residual of weight below `h` vanishes identically exactly when its first `h * k`
+entries vanish. -/
+theorem FilteredOperator.apply_eq_zero_iff (L : FilteredOperator (K := K))
+    (p : Polynomial K[X]) (h k : ℕ) (f : ℕ → K[X]) (hp : p.Monic)
+    (hdegree : p.natDegree = k) (hf : LinearRecurrence.shiftAction p f = 0)
+    (hweight : ∀ w ∈ L.support, w.indexOrder + w.derivativeOrder < h) :
+    L.apply f = 0 ↔ ∀ n < h * k, L.apply f n = 0 := by
+  constructor
+  · intro hzero n _
+    rw [hzero]
+    rfl
+  · intro hinit
+    apply LinearRecurrence.eq_zero_of_monic_of_shiftAction_eq_zero (hp.pow h)
+      (L.shiftAction_pow_apply_eq_zero p h f hf hweight)
+    rw [hp.natDegree_pow, hdegree]
+    exact hinit
+
+end
+
+end RealRooted
diff --git a/RealRooted/RecurrenceSpace/Operators.lean b/RealRooted/RecurrenceSpace/Operators.lean
new file mode 100644
index 000000000..d19897852
--- /dev/null
+++ b/RealRooted/RecurrenceSpace/Operators.lean
@@ -0,0 +1,198 @@
+import Mathlib.Algebra.Module.LinearMap.End
+import Mathlib.Algebra.Polynomial.Derivative
+import Mathlib.Tactic.Abel
+import Mathlib.Tactic.LinearCombination
+import Mathlib.Tactic.Ring
+import RealRooted.Mathlib.Algebra.LinearRecurrence.Operator
+
+/-!
+# Differential operators on recurrence spaces
+
+This module proves the coefficient-derivative product rule and the elementary closure
+theorems underlying the finite recurrence certificates of RealRooted issue #1978.
+-/
+
+open Finset Polynomial
+
+namespace RealRooted
+
+noncomputable section
+
+variable {K : Type*} [Field K]
+
+/-- Differentiate every coefficient of a polynomial whose coefficients lie in `K[X]`. -/
+def coefficientDerivative (p : Polynomial K[X]) : Polynomial K[X] :=
+  p.sum fun n a ↦ monomial n a.derivative
+
+@[simp]
+theorem coefficientDerivative_zero : coefficientDerivative (0 : Polynomial K[X]) = 0 := by
+  simp [coefficientDerivative]
+
+@[simp]
+theorem coefficientDerivative_add (p q : Polynomial K[X]) :
+    coefficientDerivative (p + q) = coefficientDerivative p + coefficientDerivative q := by
+  simp [coefficientDerivative, Polynomial.sum_add_index, derivative_add]
+
+@[simp]
+theorem coefficientDerivative_monomial (n : ℕ) (a : K[X]) :
+    coefficientDerivative (monomial n a) = monomial n a.derivative := by
+  simp [coefficientDerivative]
+
+/-- Differentiate each entry of a polynomial-valued sequence. -/
+def sequenceDerivative : (ℕ → K[X]) →ₗ[K] ℕ → K[X] where
+  toFun f n := (f n).derivative
+  map_add' f g := by ext n; simp
+  map_smul' a f := by ext n; simp
+
+@[simp]
+theorem sequenceDerivative_apply (f : ℕ → K[X]) (n : ℕ) :
+    sequenceDerivative f n = (f n).derivative :=
+  rfl
+
+/-- Differentiating the result of a shift-polynomial action differentiates both the
+operator coefficients and the sequence entries. -/
+theorem sequenceDerivative_shiftAction (p : Polynomial K[X]) (f : ℕ → K[X]) :
+    sequenceDerivative (LinearRecurrence.shiftAction p f) =
+      LinearRecurrence.shiftAction (coefficientDerivative p) f +
+        LinearRecurrence.shiftAction p (sequenceDerivative f) := by
+  induction p using Polynomial.induction_on' with
+  | add p q hp hq =>
+      rw [show LinearRecurrence.shiftAction (p + q) f =
+        LinearRecurrence.shiftAction p f + LinearRecurrence.shiftAction q f by
+          simp [LinearRecurrence.shiftAction]]
+      rw [sequenceDerivative.map_add, hp, hq, coefficientDerivative_add]
+      simp only [LinearRecurrence.shiftAction, map_add, LinearMap.add_apply]
+      abel
+  | monomial j a =>
+      ext n
+      simp [LinearRecurrence.shiftAction_monomial_apply, sequenceDerivative,
+        LinearRecurrence.forwardShift_pow_apply, derivative_mul]
+
+/-- A shift-polynomial action commutes with multiplication of every sequence entry by a
+fixed coefficient polynomial. -/
+theorem shiftAction_smul (p : Polynomial K[X]) (a : K[X]) (f : ℕ → K[X]) :
+    LinearRecurrence.shiftAction p (a • f) =
+      a • LinearRecurrence.shiftAction p f := by
+  exact (LinearRecurrence.shiftAction p).map_smul a f
+
+/-- Two shift-polynomial actions commute. -/
+theorem shiftAction_commute (p q : Polynomial K[X]) (f : ℕ → K[X]) :
+    LinearRecurrence.shiftAction p (LinearRecurrence.shiftAction q f) =
+      LinearRecurrence.shiftAction q (LinearRecurrence.shiftAction p f) := by
+  rw [← LinearRecurrence.shiftAction_mul_apply,
+    ← LinearRecurrence.shiftAction_mul_apply, mul_comm]
+
+private theorem pow_succ_apply_eq_zero_of_commutator
+    {M : Type*} [AddCommGroup M] [Module K M]
+    (T N C : Module.End K M) (hcomm : T * N = N * T + C)
+    (hTC : Commute T C) {q : ℕ} {x : M} (hx : (T ^ q) x = 0) :
+    (T ^ (q + 1)) (N x) = 0 := by
+  induction q generalizing x with
+  | zero =>
+      simp only [pow_zero, Module.End.one_apply] at hx
+      subst x
+      simp
+  | succ q ih =>
+      have hTx : (T ^ q) (T x) = 0 := by
+        simpa only [pow_succ, Module.End.mul_apply] using hx
+      have hN : (T ^ (q + 1)) (N (T x)) = 0 := ih hTx
+      have hC : (T ^ (q + 1)) (C x) = 0 := by
+        have hc := LinearMap.congr_fun (hTC.pow_left (q + 1)).eq x
+        simp only [Module.End.mul_apply] at hc
+        rw [hc, hx, map_zero]
+      rw [show q + 1 + 1 = (q + 1) + 1 by rfl, pow_succ, Module.End.mul_apply,
+        show T (N x) = N (T x) + C x by
+          simpa only [Module.End.mul_apply, LinearMap.add_apply] using
+            LinearMap.congr_fun hcomm x,
+        map_add, hN, hC, add_zero]
+
+private def polynomialShiftEnd (p : Polynomial K[X]) : Module.End K (ℕ → K[X]) :=
+  (LinearRecurrence.shiftAction p).restrictScalars K
+
+private theorem polynomialShiftEnd_pow_apply (p : Polynomial K[X]) (q : ℕ)
+    (f : ℕ → K[X]) :
+    (polynomialShiftEnd p ^ q) f = LinearRecurrence.shiftAction (p ^ q) f := by
+  induction q generalizing f with
+  | zero => simp [polynomialShiftEnd]
+  | succ q ih =>
+      rw [pow_succ, Module.End.mul_apply, ih]
+      exact (LinearRecurrence.shiftAction_mul_apply (p ^ q) p f).symm
+
+private def polynomialIndexEnd : Module.End K (ℕ → K[X]) :=
+  (LinearRecurrence.indexMul (R := K[X])).restrictScalars K
+
+/-- If `p(S)^q` annihilates a polynomial sequence, then `p(S)^(q+1)` annihilates its
+index multiple. -/
+theorem shiftAction_pow_succ_indexMul_eq_zero (p : Polynomial K[X]) (q : ℕ)
+    (f : ℕ → K[X]) (hf : LinearRecurrence.shiftAction (p ^ q) f = 0) :
+    LinearRecurrence.shiftAction (p ^ (q + 1))
+      (LinearRecurrence.indexMul f) = 0 := by
+  let T := polynomialShiftEnd p
+  let N := polynomialIndexEnd (K := K)
+  let C := polynomialShiftEnd (X * p.derivative)
+  have hcomm : T * N = N * T + C := by
+    apply LinearMap.ext
+    intro f
+    simpa [T, N, C, polynomialShiftEnd, polynomialIndexEnd, Module.End.mul_apply]
+      using LinearRecurrence.shiftAction_indexMul p f
+  have hTC : Commute T C := by
+    change T * C = C * T
+    apply LinearMap.ext
+    intro f
+    change LinearRecurrence.shiftAction p
+        (LinearRecurrence.shiftAction (X * p.derivative) f) =
+      LinearRecurrence.shiftAction (X * p.derivative)
+        (LinearRecurrence.shiftAction p f)
+    exact shiftAction_commute p (X * p.derivative) f
+  have hpow : (T ^ q) f = 0 := by
+    dsimp only [T]
+    rw [polynomialShiftEnd_pow_apply]
+    exact hf
+  have h := pow_succ_apply_eq_zero_of_commutator T N C hcomm hTC hpow
+  dsimp only [T] at h
+  rw [polynomialShiftEnd_pow_apply] at h
+  exact h
+
+private def polynomialDerivativeEnd : Module.End K (ℕ → K[X]) :=
+  sequenceDerivative
+
+/-- If `p(S)^q` annihilates a polynomial sequence, then `p(S)^(q+1)` annihilates its
+coefficientwise derivative. -/
+theorem shiftAction_pow_succ_sequenceDerivative_eq_zero (p : Polynomial K[X]) (q : ℕ)
+    (f : ℕ → K[X]) (hf : LinearRecurrence.shiftAction (p ^ q) f = 0) :
+    LinearRecurrence.shiftAction (p ^ (q + 1)) (sequenceDerivative f) = 0 := by
+  let T := polynomialShiftEnd p
+  let N := polynomialDerivativeEnd (K := K)
+  let C := -polynomialShiftEnd (coefficientDerivative p)
+  have hcomm : T * N = N * T + C := by
+    apply LinearMap.ext
+    intro f
+    have h := sequenceDerivative_shiftAction p f
+    change LinearRecurrence.shiftAction p (sequenceDerivative f) =
+      sequenceDerivative (LinearRecurrence.shiftAction p f) -
+        LinearRecurrence.shiftAction (coefficientDerivative p) f
+    rw [h]
+    abel
+  have hTC : Commute T C := by
+    change T * C = C * T
+    apply LinearMap.ext
+    intro f
+    change LinearRecurrence.shiftAction p
+        (-LinearRecurrence.shiftAction (coefficientDerivative p) f) =
+      -LinearRecurrence.shiftAction (coefficientDerivative p)
+        (LinearRecurrence.shiftAction p f)
+    rw [map_neg]
+    congr 1
+    exact shiftAction_commute p (coefficientDerivative p) f
+  have hpow : (T ^ q) f = 0 := by
+    dsimp only [T]
+    rw [polynomialShiftEnd_pow_apply]
+    exact hf
+  have h := pow_succ_apply_eq_zero_of_commutator T N C hcomm hTC hpow
+  dsimp only [T] at h
+  rw [polynomialShiftEnd_pow_apply] at h
+  exact h
+
+end
+
+end RealRooted
diff --git a/RealRooted/Tactic/Examples.lean b/RealRooted/Tactic/Examples.lean
index 2775e6ad9..8d1aa2a09 100644
--- a/RealRooted/Tactic/Examples.lean
+++ b/RealRooted/Tactic/Examples.lean
@@ -1,3 +1,4 @@
+import RealRooted.Tactic.Examples.A049325RecurrenceSpace
 import RealRooted.Tactic.Examples.AffineDerivative
 import RealRooted.Tactic.Examples.AissenSchoenbergWhitney
 import RealRooted.Tactic.Examples.AllCombo
diff --git a/RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean b/RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean
new file mode 100644
index 000000000..9d38db32d
--- /dev/null
+++ b/RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean
@@ -0,0 +1,49 @@
+import Mathlib.Tactic.NormNum
+import RealRooted.RecurrenceSpace.Defect
+
+/-!
+# A049325 recurrence-space certificate
+
+This regression module instantiates the universal defect certificate from RealRooted
+issue #1978 for the pure-lag recurrence and first-order lift associated with A049325.
+-/
+
+open Polynomial
+
+namespace RealRooted
+
+noncomputable section
+
+/-- The four pure-lag coefficients for the A049325 certificate. -/
+def a049325Coeffs : Fin 4 → ℚ[X] :=
+  ![16 * X, 16 * X, 6 * X, X]
+
+/-- The A049325 correction polynomial is `X` times its lag characteristic polynomial. -/
+theorem a049325_defectCorrection :
+    defectCorrection a049325Coeffs 1 (-4) (X * (X + 16)) =
+      C X * lagCharacteristic a049325Coeffs := by
+  norm_num [defectCorrection, lagCharacteristic, LinearRecurrence.charPoly,
+    a049325Coeffs, Fin.sum_univ_succ]
+  simp only [← C_mul_X_pow_eq_monomial]
+  simp only [map_add, map_mul, map_one, map_ofNat]
+  ring
+
+/-- The A049325 pure-lag recurrence and four lift-defect seeds certify its first-order
+differential lift. -/
+theorem a049325_first_order_of_recurrence (P : ℕ → ℚ[X])
+    (hsource : ∀ n, lagDefect a049325Coeffs P n = 0)
+    (hseed : ∀ n < 4,
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0) (n : ℕ) :
+    (n + 4 : ℚ[X]) * P (n + 1) =
+      X * (X + 16) * (P n).derivative +
+        (4 - 4 * (n : ℚ[X]) + 2 * X) * P n := by
+  have h := liftDefect_eq_zero_of_lagDefect_eq_zero a049325Coeffs
+    1 4 (-4) (4 + 2 * X) (X * (X + 16)) X P hsource
+    a049325_defectCorrection hseed
+  have hn := congr_fun h n
+  simp only [liftDefect, affineIndex, Pi.zero_apply] at hn
+  linear_combination hn
+
+end
+
+end RealRooted
diff --git a/RealRooted/Tactic/OEIS_COVERAGE.md b/RealRooted/Tactic/OEIS_COVERAGE.md
index 24f9757d6..8e95213be 100644
--- a/RealRooted/Tactic/OEIS_COVERAGE.md
+++ b/RealRooted/Tactic/OEIS_COVERAGE.md
@@ -63,7 +63,7 @@ Current totals: **308 IDs**; **34 formalized**, **261 shells**, **3 fragments**,
 | A049020 | `shell` | Distinguished-block set partitions: `v_n(t) = 1 + t` ().<br>def : ℕ → ℝ[X]<br>+4 additional test intents | `rr_row_interlaces`, `rr_row_splits`, `rr_sign_at_roots_upper` | implicit/local certificates resolved by the route | concrete row definition and proofs of the listed certificates |
 | A049218 | `shell` | active scalar-lag Favard shell `P_m=tP_{m-1}-m(m+1)P_{m-2}`. | `rr_favard_param_auto` | `alpha`, `base_one`, `base_zero`, `beta`, `step` | concrete row definition and proofs of the listed certificates |
 | A049310 | `shell` | OEIS shape `/`: `P_{n+2}=tP_{n+1}-P_n`.<br>OEIS shapes `//`: real-rootedness consequence of<br>+2 additional test intents | `rr_favard`, `rr_favard_const`, `rr_favard_const_unit` | `alpha`, `base_one`, `base_zero`, `step` | concrete row definition and proofs of the listed certificates |
-| A049325 | `shell` | namespace H<br>The OEIS polynomial sequence, given by a literal fourth-order recurrence.<br>+10 additional test intents | `rr_row_interlaces`, `rr_row_splits` | implicit/local certificates resolved by the route | concrete row definition and proofs of the listed certificates |
+| A049325 | `shell` | # recurrence-space certificate<br>issue #1978 for the pure-lag recurrence and first-order lift associated with .<br>+15 additional test intents | `rr_row_interlaces`, `rr_row_splits` | implicit/local certificates resolved by the route | concrete row definition and proofs of the listed certificates |
 | A049347 | `shell` | -style sequence shell: repeated lag `-(t^2-t+1)`. | `rr_lw_negative_quadratic_sequence_realrooted_auto` | `base`, `degree_succ`, `no_common_roots`, `pos_lc`, `recurrence` | concrete row definition and proofs of the listed certificates |
 | A049403 | `shell` | OEIS shape : `P_n = t P_{n-1} + c_n t P_{n-2}`.<br>after reindexing, `P_{n+2}=tP_{n+1}+(n+1)tP_n`.<br>+3 additional test intents | `rr_lw_current_X_sequence_auto`, `rr_lw_current_X_sequence_realrooted`, `rr_lw_positive_t`, `rr_sign`, `rr_sign_at_roots` | `base`, `coeff_nonneg`, `degree_lower`, `degree_succ`, `degree_upper`, `interlacer`, `interlacer_pos_lc`, `no_common_roots`, `nonneg_coeffs`, `pos_lc`, `recurrence`, `roots_nonpos`, `target_pos_lc` | concrete row definition and proofs of the listed certificates |
 | A052553 | `shell` | OEIS shapes `//`:<br>Full sequence shell for `//`: | `rr_strict_interl_pos_X_lag_combo`, `rr_strict_interl_pos_X_lag_sequence_auto`, `rr_wagner_pos_term` | `base`, `current_coeff_pos`, `lag_coeff_pos`, `left_nonneg`, `nonneg_coeffs`, `proper`, `recurrence`, `right_nonneg` | concrete row definition and proofs of the listed certificates |
diff --git a/scripts/import_architecture.json b/scripts/import_architecture.json
index 2a68d604c..fb4d36acd 100644
--- a/scripts/import_architecture.json
+++ b/scripts/import_architecture.json
@@ -16,13 +16,13 @@
   ],
   "budgets": {
     "RealRooted": {
-      "max_modules": 2052
+      "max_modules": 2056
     },
     "RealRooted.Production": {
-      "max_modules": 1874
+      "max_modules": 1877
     },
     "RealRooted.Tactic.Examples": {
-      "max_modules": 927
+      "max_modules": 931
     },
     "RealRooted.ParkingFunctions.Descents.Words": {
       "max_modules": 137
diff --git a/scripts/mathlib_shims.json b/scripts/mathlib_shims.json
index 414f5b041..bca8aa72d 100644
--- a/scripts/mathlib_shims.json
+++ b/scripts/mathlib_shims.json
@@ -63,6 +63,16 @@
       "note": "Speculative target module generated from the shim tree; no upstream PR or attribution has been recorded yet.",
       "speculative": true
     },
+    {
+      "sources": [
+        "RealRooted/Mathlib/Algebra/LinearRecurrence/Operator.lean"
+      ],
+      "modules": [
+        "Mathlib.Algebra.LinearRecurrence.Operator"
+      ],
+      "note": "Speculative target module generated from the shim tree; no upstream PR or attribution has been recorded yet.",
+      "speculative": true
+    },
     {
       "sources": [
         "RealRooted/Mathlib/Algebra/LinearRecurrence/Quadratic.lean"