[PerAlexandersson]

Phase A of #1978: the operator algebra behind turning a long linear recurrence into a shorter
recurrence that involves derivatives (a "derivative lift"), and back.

Shift operators (RealRooted/Mathlib/Algebra/LinearRecurrence/Operator.lean, upstream-shaped)

• LinearRecurrence.shiftAction p acts on a sequence by evaluating p at the shift, i.e. p(S).
  The action is multiplicative and respects powers.
• eq_zero_of_monic_of_shiftAction_eq_zero: if a monic p(S) annihilates a sequence whose
  first p.natDegree values are zero, the sequence is zero.
• shiftAction_indexMul: commuting p(S) past multiplication by the index produces
  (X * p.derivative)(S).

Operators on polynomial-valued sequences (RealRooted/RecurrenceSpace/)

• sequenceDerivative_shiftAction: a product rule, D(p(S) f) = p_X(S) f + p(S)(D f), where
  p_X differentiates the coefficients of p.
• FilteredOperator represents combinations of the words N^u S^j D^s.
  FilteredOperator.apply_eq_zero_iff reduces "the residual vanishes for all n" to
  "it vanishes for n < h * k", for a monic source recurrence of degree k.
• lagDefect_liftDefect is the universal source-and-lift defect identity.
  liftDefect_eq_zero_of_lagDefect_eq_zero and lagDefect_eq_zero_of_liftDefect_eq_zero give
  the two propagation directions under the factor certificate J = C γ * χ.
• Example (Tactic/Examples/A049325RecurrenceSpace.lean): the fourth-order lag recurrence of
  A049325 certifies the first-order lift
  (n+4) P[n+1] = X(X+16) P'[n] + (4 - 4n + 2X) P[n].

Phase B (a certificate-replay tactic) and phase C (structure theory) remain open in #1978.

Checks (local)

• Full default build passes.
• runLinter passes against the committed nolints.json, with the baseline unchanged.
• lake exe lint-style and all guards pass.
• The shim registry check passes, with the new shim registered.
• OEIS_COVERAGE.md is regenerated and passes --check.
• The catalog axiom audit passes.

🤖 Generated with Claude Code