From f39c37e6d8bfe323404cd03888db600afca764b5 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Thu, 22 Oct 2026 09:35:52 +0000 Subject: [PATCH 1/2] Recurrence spaces, phase B: certificate replay and row-tactic adapter Worker-drafted (Codex), integrated unverified: the worker reports a passing full default build and guards; strict runLinter/audit not yet run by the integrator. See the PR for the per-target summary. Co-Authored-By: Claude Opus 5.5 --- RealRooted/RecurrenceSpace/Defect.lean | 107 ++++++++++++++++ .../Examples/A049325RecurrenceSpace.lean | 116 ++++++++++++++++-- RealRooted/Tactic/OEIS_COVERAGE.md | 2 +- RealRooted/Tactic/Recurrence.lean | 95 +++++++++++++- scripts/import_architecture.json | 4 +- 5 files changed, 313 insertions(+), 11 deletions(-) diff --git a/RealRooted/RecurrenceSpace/Defect.lean b/RealRooted/RecurrenceSpace/Defect.lean index 23fcfa3d1..11917dfb0 100644 --- a/RealRooted/RecurrenceSpace/Defect.lean +++ b/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 diff --git a/RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean b/RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean index 9d38db32d..aa82dcf4a 100644 --- a/RealRooted/Tactic/Examples/A049325RecurrenceSpace.lean +++ b/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 diff --git a/RealRooted/Tactic/OEIS_COVERAGE.md b/RealRooted/Tactic/OEIS_COVERAGE.md index 8e95213be..124de8705 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` | # 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 | +| A049325 | `shell` | # recurrence-space certificate
issue #1978 for the pure-lag recurrence and first-order lift associated with .
+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}`.
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/RealRooted/Tactic/Recurrence.lean b/RealRooted/Tactic/Recurrence.lean index eadce1fbe..56bdc83e2 100644 --- a/RealRooted/Tactic/Recurrence.lean +++ b/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 "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)) diff --git a/scripts/import_architecture.json b/scripts/import_architecture.json index fb4d36acd..4760a00be 100644 --- a/scripts/import_architecture.json +++ b/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 From ffee623521fb96acaf3d9d086c6e9cf57362f41e Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Sun, 25 Oct 2026 07:17:18 +0000 Subject: [PATCH 2/2] Name the rr_replay_factor macro for runLinter Co-Authored-By: Claude Opus 5.5 --- RealRooted/Tactic/Recurrence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RealRooted/Tactic/Recurrence.lean b/RealRooted/Tactic/Recurrence.lean index 56bdc83e2..055e97b8e 100644 --- a/RealRooted/Tactic/Recurrence.lean +++ b/RealRooted/Tactic/Recurrence.lean @@ -26,7 +26,7 @@ on these. /-- Normalize the concrete rational-polynomial factor identity generated by certificate replay. The final `done` makes a corrupted certificate fail atomically. -/ -macro "rr_replay_factor" : tactic => `(tactic| ( +macro (name := rrReplayFactor) "rr_replay_factor" : tactic => `(tactic| ( first | decide | (norm_num [RealRooted.defectCorrection, RealRooted.lagCharacteristic,