From f3f61abef7b3512ab8e1de54b61123ad3ecfb8c4 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 21 Oct 2026 16:57:47 +0000 Subject: [PATCH 1/2] Recurrence spaces, phase A: shift operators, filtered check, defect identity Formalizes phase A of #1978. - `LinearRecurrence.shiftAction p` acts on sequences by `p(S)`. It is multiplicative, and a monic annihilator with zero initial values forces zero. - The commutator with index multiplication is `(X * p.derivative)(S)`. - `sequenceDerivative_shiftAction`: coefficient-derivative product rule. - `FilteredOperator.apply_eq_zero_iff`: a filtered residual vanishes iff it vanishes for `n < h * 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 both propagation directions. - Example: the A049325 lag recurrence certifies its first-order lift. Co-Authored-By: Claude Opus 5.5 --- RealRooted.lean | 5 + .../Algebra/LinearRecurrence/Operator.lean | 142 +++++++++++ RealRooted/Production.lean | 4 + RealRooted/RecurrenceSpace/Defect.lean | 224 ++++++++++++++++++ RealRooted/RecurrenceSpace/Filtered.lean | 140 +++++++++++ RealRooted/RecurrenceSpace/Operators.lean | 198 ++++++++++++++++ RealRooted/Tactic/Examples.lean | 1 + .../Examples/A049325RecurrenceSpace.lean | 49 ++++ scripts/import_architecture.json | 6 +- 9 files changed, 766 insertions(+), 3 deletions(-) create mode 100644 RealRooted/Mathlib/Algebra/LinearRecurrence/Operator.lean create mode 100644 RealRooted/RecurrenceSpace/Defect.lean create mode 100644 RealRooted/RecurrenceSpace/Filtered.lean create mode 100644 RealRooted/RecurrenceSpace/Operators.lean create mode 100644 RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean 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/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 From 0ed8d32f1cc3d63381b39ca3f66bf1bac9ae98b5 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Wed, 21 Oct 2026 17:41:31 +0000 Subject: [PATCH 2/2] Register the LinearRecurrence.Operator shim; regenerate OEIS tactic coverage Co-Authored-By: Claude Opus 5.5 --- RealRooted/Tactic/OEIS_COVERAGE.md | 2 +- scripts/mathlib_shims.json | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/RealRooted/Tactic/OEIS_COVERAGE.md b/RealRooted/Tactic/OEIS_COVERAGE.md index 839c50024..d569d26f6 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` ().
def : ℕ → ℝ[X]
+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`.
OEIS shapes `//`: real-rootedness consequence of
+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
The OEIS polynomial sequence, given by a literal fourth-order recurrence.
+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
issue #1978 for the pure-lag recurrence and first-order lift associated with .
+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}`.
after reindexing, `P_{n+2}=tP_{n+1}+(n+1)tP_n`.
+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 `//`:
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/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"