Recurrence spaces, phase A: shift operators, filtered finite check, defect identity (#1978)

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

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

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

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