Skip to content

Add generalized-Laguerre sequence interlacing - #521

Merged
PerAlexandersson merged 2 commits into
mainfrom
feat/issue-365-generalized-laguerre-sequence
Sep 5, 2026
Merged

Add generalized-Laguerre sequence interlacing#521
PerAlexandersson merged 2 commits into
mainfrom
feat/issue-365-generalized-laguerre-sequence

Conversation

@PerAlexandersson

Copy link
Copy Markdown
Owner

Closes #365

Summary:

  • extend the bilinear derivative-recurrence backend with nonnegative-coefficient and adjacent Prec results
  • package the generalized-Laguerre reduction as degree, Prec, Interlaces, and rowwise real-rootedness theorems
  • add rr_generalized_laguerre_second_derivative_sequence with numeral normalization
  • add smoke tests for (m,c) = (1,2), (2,2), and (4,6)

Verification:

  • lake-workspace build RealRooted.DerivativeRecurrence.GeneralizedLaguerreInterlacing RealRooted.Tactic.Examples.GeneralizedLaguerre
  • lake-workspace build RealRooted.Tactic.Examples.OEISTestbed
  • lake-workspace build RealRooted.Tactic RealRooted.Tactic.Examples RealRooted
  • axiom audit: only propext, Classical.choice, and Quot.sound

@PerAlexandersson
PerAlexandersson merged commit 231b411 into main Sep 5, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add a generalized-Laguerre ODE reduction for second-derivative sequences

1 participant