Theorems
Real-rooted Eulerian variations
Three Eulerian-type families, coming from permutations, words and paths, are real-rooted.
- Cyclic path descents: the polynomial with coefficients $2\binom{n}{k}\binom{n-1}{k-1}$ equals $\tfrac{2}{n}\, x N_n'(x)$, where $N_n$ is the Narayana polynomial. Its zeros are simple: $0$, together with $n - 1$ negative zeros.
- Peak values: the multivariate peak-value polynomial is real stable. For every choice of positive weights, consecutive weighted diagonals strictly interlace.
- Ternary runs: the ternary run polynomials are PF polynomials, and consecutive ones strictly interlace.
The combinatorial interpretations are taken from the paper; the Lean statements are about the polynomials themselves.
References
P. Alexandersson, “Real-rooted Eulerian polynomials from permutations, words, and paths,” arXiv:2609.07325 (2026).
≔ Definitions
Cyclic path descent polynomial
def cyclicPathDescentPolynomial (n : ℕ) : ℝ[X] :=
∑ k ∈ Finset.Icc 1 n,
monomial k (2 * (Nat.choose n k : ℝ) * Nat.choose (n - 1) (k - 1))
Ternary run polynomial
def ternaryRunPolynomial : ℕ → ℝ[X]
| 0 => 1
| n + 1 =>
(C (3 / ((n : ℝ) + 1)) * X + C (-3 / ((n : ℝ) + 1)) * X ^ 2) *
(ternaryRunPolynomial n).derivative +
(C (-(n : ℝ) / ((n : ℝ) + 1)) +
C ((4 * (n : ℝ) + 3) / ((n : ℝ) + 1)) * X) *
ternaryRunPolynomial n
Multivariate peak-value polynomial
def peakValuePolynomial (n : ℕ) : MvPolynomial (Fin n) ℝ :=
∑ π : Equiv.Perm (Fin n), peakValueMonomial π
⊢ Theorems
Zeros of the cyclic path descent polynomial
theorem cyclicPathDescentPolynomial_simple_root_description
(n : ℕ) (hn : 0 < n) :
HasSimpleRoots (cyclicPathDescentPolynomial n) ∧
(cyclicPathDescentPolynomial n).IsRoot 0 ∧
(∀ r ∈ (cyclicPathDescentPolynomial n).roots.erase 0, r < 0) ∧
((cyclicPathDescentPolynomial n).roots.erase 0).card = n - 1
Cyclic path descents via the Narayana derivative
theorem cyclicPathDescentPolynomial_eq_derivative (n : ℕ) (hn : 0 < n) :
cyclicPathDescentPolynomial n =
C (2 / (n : ℝ)) * X * (narayanaPolynomial 0 n).derivative
The peak-value polynomial is real stable
theorem peakValuePolynomial_stable (n : ℕ) (_hn : 1 ≤ n) :
MvRealStable (peakValuePolynomial n)
Weighted peak-value diagonals interlace
theorem peakValueWeightedDiagonal_consecutive_strictInterl
(n : ℕ) (hn : 1 ≤ n) (wt : Fin (n + 1) → ℝ)
(hwt : ∀ j, 0 < wt j) :
StrictInterl
(peakValueWeightedDiagonal (fun j : Fin n => wt j.castSucc))
(peakValueWeightedDiagonal wt)
Ternary run polynomials are PF
theorem ternaryRunPolynomial_isPF (n : ℕ) :
IsPFPolynomial (ternaryRunPolynomial n)
Consecutive ternary run polynomials interlace
theorem ternaryRunPolynomial_strictInterl (n : ℕ) :
StrictInterl (ternaryRunPolynomial n) (ternaryRunPolynomial (n + 1))
Lean source RealRooted/Challenges/EulerianVariations.lean at revision 5827550b.