Recurrence spaces, phase B: certificate replay, exceptional indices, row-tactic adapter (#1978)

RealRooted/RecurrenceSpace/Defect.lean

@@ -191,6 +191,45 @@ theorem liftDefect_eq_zero_of_lagDefect_eq_zero {k : ℕ} (a : Fin k → K[X])
   intro n hn
   exact hseed n (mem_range.mp hn)
 
+/-- A source recurrence valid from `n₀` and `k` consecutive lift-defect seeds imply
+the differential lift from `n₀` onward. -/
+theorem liftDefect_eq_zero_from_of_lagDefect_eq_zero_from {k : ℕ}
+    (a : Fin k → K[X]) (d₁ d₀ A₁ A₀ B gamma : K[X]) (P : ℕ → K[X]) (n₀ : ℕ)
+    (hsource : ∀ n, n₀ ≤ n → lagDefect a P n = 0)
+    (hfactor : defectCorrection a d₁ A₁ B = C gamma * lagCharacteristic a)
+    (hseed : ∀ n, n₀ ≤ n → n < n₀ + k → liftDefect d₁ d₀ A₁ A₀ B P n = 0) :
+    ∀ n, n₀ ≤ n → liftDefect d₁ d₀ A₁ A₀ B P n = 0 := by
+  let E := liftDefect d₁ d₀ A₁ A₀ B P
+  have hcorr := shiftAction_defectCorrection_eq_smul_lagDefect a d₁ A₁ B gamma P hfactor
+  intro m hm
+  induction m using Nat.strong_induction_on with
+  | h m ih =>
+      by_cases hmk : m < n₀ + k
+      · exact hseed m hm hmk
+      · let n := m - k
+        have hn : n₀ ≤ n := by
+          dsimp only [n]
+          lia
+        have hnk : n + k = m := by
+          dsimp only [n]
+          lia
+        have hid := lagDefect_liftDefect a d₁ d₀ A₁ A₀ B P n
+        have hc := congr_fun hcorr n
+        have hRn := hsource n hn
+        have hRn1 := hsource (n + 1) (by lia)
+        simp only [Pi.smul_apply, smul_eq_mul, hRn, hRn1, map_zero, mul_zero,
+          sub_zero, zero_add] at hid hc
+        rw [hc] at hid
+        change E (n + k) - ∑ i, a i * E (n + i) = 0 at hid
+        have hrec : E (n + k) = ∑ i, a i * E (n + i) := by
+          exact sub_eq_zero.mp hid
+        change E m = 0
+        rw [← hnk, hrec]
+        apply sum_eq_zero
+        intro i _
+        have hi : E (n + i) = 0 := ih (n + i) (by have := i.isLt; lia) (by lia)
+        rw [hi, mul_zero]
+
 /-- 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])
@@ -219,6 +258,74 @@ theorem lagDefect_eq_zero_of_liftDefect_eq_zero {k : ℕ} (a : Fin k → K[X])
         simpa only [add_zero] using hid.symm
       exact (mul_eq_zero.mp hmul).resolve_left (hleader n)
 
+/-- A differential lift valid from `n₀`, one source-defect seed, and explicit
+source-defect seeds at every exceptional leader rank imply the source recurrence
+from `n₀` onward.  A finite exceptional set can discharge `hexception` by cases. -/
+theorem lagDefect_eq_zero_from_of_liftDefect_eq_zero_from_of_exceptional {k : ℕ}
+    (a : Fin k → K[X]) (d₁ d₀ A₁ A₀ B gamma : K[X]) (P : ℕ → K[X]) (n₀ : ℕ)
+    (hlift : ∀ n, n₀ ≤ n → liftDefect d₁ d₀ A₁ A₀ B P n = 0)
+    (hfactor : defectCorrection a d₁ A₁ B = C gamma * lagCharacteristic a)
+    (hseed : lagDefect a P n₀ = 0)
+    (hexception : ∀ n, n₀ ≤ n → affineIndex d₁ d₀ (n + k) = 0 →
+      lagDefect a P (n + 1) = 0) :
+    ∀ n, n₀ ≤ n → lagDefect a P n = 0 := by
+  have hcorr := shiftAction_defectCorrection_eq_smul_lagDefect a d₁ A₁ B gamma P hfactor
+  intro m hm
+  obtain ⟨r, rfl⟩ := Nat.exists_eq_add_of_le hm
+  induction r with
+  | zero => simpa using hseed
+  | succ r ih =>
+      let n := n₀ + r
+      have hn : n₀ ≤ n := by simp [n]
+      have hRn : lagDefect a P n = 0 := by simpa [n] using ih
+      by_cases hleader : affineIndex d₁ d₀ (n + k) = 0
+      · simpa [n, Nat.add_assoc] using hexception n hn hleader
+      · have hid := lagDefect_liftDefect a d₁ d₀ A₁ A₀ B P n
+        change liftDefect d₁ d₀ A₁ A₀ B P (n + k) -
+          ∑ i, a i * liftDefect d₁ d₀ A₁ A₀ B P (n + i) = _ at hid
+        have hc : LinearRecurrence.shiftAction (defectCorrection a d₁ A₁ B) P n = 0 := by
+          rw [congr_fun hcorr n, Pi.smul_apply, smul_eq_mul, hRn, mul_zero]
+        have hEnk := hlift (n + k) (by lia)
+        have hEi : ∀ i : Fin k, liftDefect d₁ d₀ A₁ A₀ B P (n + i) = 0 :=
+          fun i ↦ hlift (n + i) (by lia)
+        simp only [hEnk, hEi, mul_zero, sum_const_zero, sub_zero, hRn,
+          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
+        have := (mul_eq_zero.mp hmul).resolve_left hleader
+        simpa [n, Nat.add_assoc] using this
+
+/-- The regular-leader specialization of
+`lagDefect_eq_zero_from_of_liftDefect_eq_zero_from_of_exceptional`. -/
+theorem lagDefect_eq_zero_from_of_liftDefect_eq_zero_from {k : ℕ}
+    (a : Fin k → K[X]) (d₁ d₀ A₁ A₀ B gamma : K[X]) (P : ℕ → K[X]) (n₀ : ℕ)
+    (hlift : ∀ n, n₀ ≤ n → liftDefect d₁ d₀ A₁ A₀ B P n = 0)
+    (hfactor : defectCorrection a d₁ A₁ B = C gamma * lagCharacteristic a)
+    (hseed : lagDefect a P n₀ = 0)
+    (hleader : ∀ n, n₀ ≤ n → affineIndex d₁ d₀ (n + k) ≠ 0) :
+    ∀ n, n₀ ≤ n → lagDefect a P n = 0 := by
+  apply lagDefect_eq_zero_from_of_liftDefect_eq_zero_from_of_exceptional a
+    d₁ d₀ A₁ A₀ B gamma P n₀ hlift hfactor hseed
+  intro n hn hzero
+  exact absurd hzero (hleader n hn)
+
+/-- A zero lift defect with a nonzero scalar leader is the derivative recurrence in
+the coefficient order used by the root-window theorems. -/
+theorem derivativeRecurrence_of_liftDefect_eq_zero
+    (d₁ d₀ A₁ A₀ B : K[X]) (P : ℕ → K[X]) (delta : ℕ → K)
+    (hlift : ∀ n, liftDefect d₁ d₀ A₁ A₀ B P n = 0)
+    (hdelta : ∀ n, affineIndex d₁ d₀ n = C (delta n))
+    (hdelta_ne : ∀ n, delta n ≠ 0) (n : ℕ) :
+    P (n + 1) = C (delta n)⁻¹ * B * (P n).derivative +
+      C (delta n)⁻¹ * affineIndex A₁ A₀ n * P n := by
+  have h := hlift n
+  rw [liftDefect, hdelta n] at h
+  have hc : C (delta n) ≠ 0 := C_ne_zero.mpr (hdelta_ne n)
+  apply mul_left_cancel₀ hc
+  rw [mul_add]
+  simp only [← mul_assoc, ← C_mul, mul_inv_cancel₀ (hdelta_ne n), C_1, one_mul]
+  linear_combination h
+
 end
 
 end RealRooted

RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean

@@ -1,5 +1,6 @@
 import Mathlib.Tactic.NormNum
-import RealRooted.RecurrenceSpace.Defect
+import RealRooted.DerivativeRecurrence.RootWindow
+import RealRooted.Tactic.Recurrence
 
 /-!
 # A049325 recurrence-space certificate
@@ -15,7 +16,7 @@ namespace RealRooted
 noncomputable section
 
 /-- The four pure-lag coefficients for the A049325 certificate. -/
-def a049325Coeffs : Fin 4 → ℚ[X] :=
+@[simp] def a049325Coeffs : Fin 4 → ℚ[X] :=
   ![16 * X, 16 * X, 6 * X, X]
 
 /-- The A049325 correction polynomial is `X` times its lag characteristic polynomial. -/
@@ -37,13 +38,114 @@ theorem a049325_first_order_of_recurrence (P : ℕ → ℚ[X])
     (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
+  have hlift : ∀ m,
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P m = 0 := by
+    rr_replay_lift (hsource) (X) (hseed)
+  have hn := hlift n
+  simp only [liftDefect, affineIndex] at hn
   linear_combination hn
 
+/-- The monic physicists' Hermite recurrence, used to regress the lift-to-row adapter. -/
+def hermiteReplay : ℕ → ℚ[X]
+  | 0 => 1
+  | n + 1 => 2 * X * hermiteReplay n - (hermiteReplay n).derivative
+
+/-- The row adapter changes `A * P + B * P'` into the root-window convention
+`B * P' + A * P`; for Hermite it recovers `H[n+1] = 2X H[n] - H[n]'`. -/
+theorem hermiteReplay_succ (n : ℕ) :
+    hermiteReplay (n + 1) =
+      2 * X * hermiteReplay n - (hermiteReplay n).derivative := by
+  have hlift : ∀ m, liftDefect 0 1 0 (2 * X) (-1) hermiteReplay m = 0 := by
+    intro m
+    simp [liftDefect, affineIndex, hermiteReplay]
+  have hrec : ∀ m,
+      hermiteReplay (m + 1) =
+        C ((1 : ℚ))⁻¹ * (-1) * (hermiteReplay m).derivative +
+          C ((1 : ℚ))⁻¹ * affineIndex 0 (2 * X) m * hermiteReplay m := by
+    rr_lift_recurrence (hlift) (fun _ => (1 : ℚ))
+      (by simp [affineIndex]) (by simp)
+  simpa [affineIndex, sub_eq_add_neg, add_comm] using hrec n
+
+/-- The lift adapter supplies the recurrence premise of the existing root-window theorem;
+degree, leading-sign, window propagation, and base-row facts remain explicit. -/
+example {P : ℕ → ℝ[X]} {d₁ d₀ A₁ A₀ B : ℝ[X]} {delta : ℕ → ℝ}
+    {D₀ : ℕ} (W : ℝ → Prop)
+    (hlift : ∀ n, liftDefect d₁ d₀ A₁ A₀ B P n = 0)
+    (hdelta : ∀ n, affineIndex d₁ d₀ n = C (delta n))
+    (hdelta_ne : ∀ n, delta n ≠ 0)
+    (hdeg : ∀ n, (P n).natDegree = D₀ + n)
+    (hpos : ∀ n, 0 < (P n).leadingCoeff)
+    (hB : ∀ n x, W x → (C (delta n)⁻¹ * B).eval x ≤ 0)
+    (hW : ∀ n, (P n).Splits → (∀ t ∈ (P n).roots, W t) →
+      ∀ t ∈ (P (n + 1)).roots, W t)
+    (h₀ : (P 0).Splits) (hW₀ : ∀ t ∈ (P 0).roots, W t)
+    (h₀₁ : D₀ = 0 → Interlaces (P 0) (P 1)) :
+    ∀ n, Interlaces (P n) (P (n + 1)) := by
+  apply derivativeRecurrence_interlaces_of_window W
+  · rr_lift_recurrence (hlift) (delta) (hdelta) (hdelta_ne)
+  · exact hdeg
+  · exact hpos
+  · exact hB
+  · exact hW
+  · exact h₀
+  · exact hW₀
+  · exact h₀₁
+
+/-- Replay also works when the source recurrence and seeds begin at a later index. -/
+example (P : ℕ → ℚ[X])
+    (hsource : ∀ n, 3 ≤ n → lagDefect a049325Coeffs P n = 0)
+    (hseed : ∀ n, 3 ≤ n → n < 3 + 4 →
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0) :
+    ∀ n, 3 ≤ n →
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0 := by
+  rr_replay_lift_from (3) (hsource) (X) (a049325_defectCorrection) (hseed)
+
+/-- Converse replay uses the affine-leader nonvanishing side condition. -/
+example (P : ℕ → ℚ[X])
+    (hlift : ∀ n,
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0)
+    (hseed : lagDefect a049325Coeffs P 0 = 0)
+    (hleader : ∀ n, affineIndex (1 : ℚ[X]) 4 (n + 4) ≠ 0) :
+    ∀ n, lagDefect a049325Coeffs P n = 0 := by
+  rr_replay_source (hlift) (X) (hseed) (hleader)
+
+/-- Converse replay accepts explicit extra source seeds at singular affine leaders. -/
+example (P : ℕ → ℚ[X])
+    (hlift : ∀ n, 2 ≤ n →
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0)
+    (hseed : lagDefect a049325Coeffs P 2 = 0)
+    (hexception : ∀ n, 2 ≤ n →
+      affineIndex (1 : ℚ[X]) (4 : ℚ[X]) (n + 4) = 0 →
+      lagDefect a049325Coeffs P (n + 1) = 0) :
+    ∀ n, 2 ≤ n → lagDefect a049325Coeffs P n = 0 := by
+  rr_replay_source_from (2) (hlift) (X) (a049325_defectCorrection)
+    (hseed) (hexception)
+
+/-- A changed factor is rejected by certificate replay. -/
+example (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, liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0 := by
+  fail_if_success
+    rr_replay_lift (hsource) (X + 1) (hseed)
+  rr_replay_lift (hsource) (X) (hseed)
+
+/-- A seed certificate for a changed derivative coefficient is rejected. -/
+example (P : ℕ → ℚ[X])
+    (hsource : ∀ n, lagDefect a049325Coeffs P n = 0)
+    (hseed : ∀ n < 4,
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 15)) P n = 0)
+    (hgood : ∀ n < 4,
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0) :
+    (∀ n, liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 16)) P n = 0) ∧
+      liftDefect 1 4 (-4) (4 + 2 * X) (X * (X + 15)) P 0 = 0 := by
+  constructor
+  · fail_if_success
+      rr_replay_lift (hsource) (X) (hseed)
+    rr_replay_lift (hsource) (X) (hgood)
+  · exact hseed 0 (by norm_num)
+
 end
 
 end RealRooted

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` | # 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 |
+| 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_lift_recurrence`, `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 |

RealRooted/Tactic/Recurrence.lean

@@ -2,6 +2,7 @@ import RealRooted.Tactic.Recurrence.Shape
 import RealRooted.Tactic.Recurrence.Eval
 import RealRooted.Tactic.Recurrence.Degree
 import RealRooted.Tactic.Recurrence.ODE
+import RealRooted.RecurrenceSpace.Defect
 
 /-!
 # Recurrence tactics
@@ -14,8 +15,100 @@ real-rootedness:
 * `RealRooted.Tactic.Recurrence.Degree`: `rr_row_natDegree`, `rr_row_ne_zero`,
   `rr_row_leadingCoeff_pos`;
 * `RealRooted.Tactic.Recurrence.ODE`: `rr_find_ode` and `rr_row_ode`, eigen-ODEs of
-  second-order recurrences.
+  second-order recurrences;
+* `rr_replay_lift` and `rr_replay_source`: replay short recurrence-space certificates;
+* `rr_lift_recurrence`: adapt a checked lift to the coefficient convention used by the
+  derivative-recurrence theorems.
 
 The real-rootedness and interlacing tactics (`rr_row_interlaces`, `rr_product_*`) build
 on these.
 -/
+
+/-- Normalize the concrete rational-polynomial factor identity generated by certificate
+replay.  The final `done` makes a corrupted certificate fail atomically. -/
+macro (name := rrReplayFactor) "rr_replay_factor" : tactic => `(tactic| (
+  first
+  | decide
+  | (norm_num [RealRooted.defectCorrection, RealRooted.lagCharacteristic,
+      LinearRecurrence.charPoly, Fin.sum_univ_succ]
+     simp only [← Polynomial.C_mul_X_pow_eq_monomial, map_add, map_mul, map_one,
+       map_ofNat]
+     ring)
+  done))
+
+/-- Replay a short factor certificate from a pure-lag recurrence and its lift seeds. -/
+syntax (name := rrReplayLift) "rr_replay_lift" "(" term ")" "(" term ")" "(" term ")" : tactic
+
+macro_rules
+  | `(tactic|
+      rr_replay_lift ($hsource:term) ($factor:term) ($hseeds:term)) =>
+      `(tactic| first
+        | (refine RealRooted.liftDefect_eq_zero_of_lagDefect_eq_zero
+              (gamma := $factor) (hsource := $hsource) (hfactor := ?_)
+              (hseed := $hseeds)
+           rr_replay_factor)
+        | (intro n
+           refine congrFun (RealRooted.liftDefect_eq_zero_of_lagDefect_eq_zero
+             (gamma := $factor) (hsource := $hsource) (hfactor := ?_)
+             (hseed := $hseeds)) n
+           rr_replay_factor))
+
+/-- Replay a short factor certificate on a tail beginning at an exceptional index. -/
+syntax (name := rrReplayLiftFrom) "rr_replay_lift_from" "(" term ")" "(" term ")"
+  "(" term ")" "(" term ")" "(" term ")" : tactic
+
+macro_rules
+  | `(tactic|
+      rr_replay_lift_from ($origin:term) ($hsource:term) ($factor:term)
+        ($hfactor:term) ($hseeds:term)) =>
+      `(tactic| exact RealRooted.liftDefect_eq_zero_from_of_lagDefect_eq_zero_from
+        (n₀ := $origin) (gamma := $factor) (hsource := $hsource) (hfactor := $hfactor)
+        (hseed := $hseeds))
+
+/-- Replay the converse short certificate when every affine leader is nonzero. -/
+syntax (name := rrReplaySource) "rr_replay_source" "(" term ")" "(" term ")"
+  "(" term ")" "(" term ")" : tactic
+
+macro_rules
+  | `(tactic|
+      rr_replay_source ($hlift:term) ($factor:term) ($hseed:term) ($hleader:term)) =>
+      `(tactic| first
+        | (refine RealRooted.lagDefect_eq_zero_of_liftDefect_eq_zero
+              (gamma := $factor) (hlift := $hlift) (hfactor := ?_)
+              (hseed := $hseed) (hleader := $hleader)
+           rr_replay_factor)
+        | (intro n
+           refine congrFun (RealRooted.lagDefect_eq_zero_of_liftDefect_eq_zero
+             (gamma := $factor) (hlift := $hlift) (hfactor := ?_)
+             (hseed := $hseed) (hleader := $hleader)) n
+           rr_replay_factor))
+
+/-- Replay the converse certificate on a tail, using extra source seeds at singular leaders. -/
+syntax (name := rrReplaySourceFrom) "rr_replay_source_from" "(" term ")" "(" term ")"
+  "(" term ")" "(" term ")" "(" term ")" "(" term ")" : tactic
+
+macro_rules
+  | `(tactic|
+      rr_replay_source_from ($origin:term) ($hlift:term) ($factor:term)
+        ($hfactor:term) ($hseed:term) ($hexceptions:term)) =>
+      `(tactic| exact
+        RealRooted.lagDefect_eq_zero_from_of_liftDefect_eq_zero_from_of_exceptional
+          (n₀ := $origin) (gamma := $factor) (hlift := $hlift) (hfactor := $hfactor)
+          (hseed := $hseed) (hexception := $hexceptions))
+
+/-- Convert a checked lift to the `A * P' + B * P` convention of the
+derivative-recurrence and root-window theorems. -/
+syntax (name := rrLiftRecurrence) "rr_lift_recurrence" "(" term ")" "(" term ")"
+  "(" term ")" "(" term ")" : tactic
+
+macro_rules
+  | `(tactic|
+      rr_lift_recurrence ($hlift:term) ($scalar:term) ($scalarEq:term) ($scalarNe:term)) =>
+      `(tactic| first
+        | exact RealRooted.derivativeRecurrence_of_liftDefect_eq_zero
+            (delta := $scalar) (hlift := $hlift) (hdelta := $scalarEq)
+            (hdelta_ne := $scalarNe) _
+        | (intro n
+           exact RealRooted.derivativeRecurrence_of_liftDefect_eq_zero
+             (delta := $scalar) (hlift := $hlift) (hdelta := $scalarEq)
+             (hdelta_ne := $scalarNe) n))

scripts/import_architecture.json

@@ -1483,7 +1483,7 @@
       "max_modules": 112
     },
     "RealRooted.Tactic.OEIS": {
-      "max_modules": 558
+      "max_modules": 561
    },
     "RealRooted.SequenceClosure": {
       "max_modules": 16
@@ -1576,7 +1576,7 @@
       "max_modules": 104
     },
     "RealRooted.Tactic": {
-      "max_modules": 588
+      "max_modules": 591
    },
     "RealRooted.Tactic.CommonInterleaver.Core": {
       "max_modules": 182