Generalized snake posets

A generalized snake poset $P(w)$ is a width-two poset built from a word $w$ in the letters $L$ and $R$. By Braun and Jal, the $h^*$-polynomial of its order polytope is the non-nesting rook polynomial $M_w$ of a skew board whose cells are the incomparable cross-chain pairs of $P(w)$.

Theorem (Braun–Jal, Theorem 4.1). Each $M_w$ is real-rooted, and deleting the last letter of $w$ gives a polynomial interlacing $M_w$.

The Lean proof covers the concrete snake board (theorem41_generalizedSnakeRookModel).

The proof runs through the modified Narayana polynomials $P_n = t^{-1} N_{n+1}$, which are the rook polynomials of the full truncated staircase boards, and $G_n = \sum_{i<n} R(n,i)$, a sum of truncated-staircase rook polynomials.

Analytic core. Every $P_n$ is a PF polynomial and $P_n \ll P_{n+1}$. Lemma 3.4: for $m \geq 2$, $\lambda \geq 0$ and $\nu \geq -1$, $(\lambda x+\nu) P_{m-1} + P_m \ll (\lambda x+\nu) P_m + P_{m+1}$. Claim (7) and a matrix induction then give Theorem 4.1 for any family satisfying the combinatorial inputs below.
Theorem 3.5 (generalizedSnakeTheorem35). If $k$ is the last position where $w$ differs from its final letter and $s = |w| - k - 1$, then $M_w = M_{w[:k+1]}\, P_s + x\, M_{w[:k]}\, G_s$.
Staircase inputs. $x\, G_{n-1} = P_n - (1+x) P_{n-1}$, and $G_n - G_{n-1}$ has nonnegative coefficients, both from a column recurrence for truncated-staircase rook polynomials. Constant words give $P_{n+1}$.

For Theorem 3.5, the incomparable pairs $(i,j)$ of $P(w)$ are the cells whose gaps between $i$ and $j$ all carry one letter: $R$ above the diagonal, $L$ below it. The Braun–Jal board reverses the column order, which turns non-nesting placements into chains that increase in both coordinates. The final constant block cuts this band into a staircase, one column of cells, and the band of the prefix, and the recurrence follows by expanding along that column.

The reversed column orientation matters. The non-nesting rook polynomial of the reversed board agrees with an independent $h^*$-polynomial computation for every word of length at most 11. The non-nesting rook polynomial of the unreversed board does not.

References

Braun and Jal, “Order polytopes of generalized snake posets are h*-real-rooted,” arXiv:2607.00922 (2026).

Definitions

Letters L and R of a snake word
RealRooted.GeneralizedSnakePosets.SnakeLettersource
```
inductive SnakeLetter where
  | L
  | R
  deriving DecidableEq, Repr
```

Board of a generalized snake poset

RealRooted.GeneralizedSnakePosets.generalizedSnakeBoardsource

def generalizedSnakeBoard (w : SnakeWord) : FiniteSkewBoard where
  cells := (snakeIncomparableBoard w).cells.image fun cell => (cell.1, w.length - cell.2)

Non-nesting rook polynomial of a board

RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.rookPolynomialsource

def rookPolynomial (B : FiniteSkewBoard) : ℝ[X] := by
  classical
  exact (B.cells.powerset.filter (fun P => B.IsNonNestingPlacement P)).sum
    (fun P => X ^ P.card)

Modified Narayana polynomials Pₙ
RealRooted.GeneralizedSnakePosets.modifiedNarayanaPolynomialsource
```
def modifiedNarayanaPolynomial (n : ℕ) : ℝ[X] :=
  narayanaQuot (n + 1)
```

Auxiliary polynomials Gₙ

RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.auxiliaryGsource

def auxiliaryG : ℕ → ℝ[X] :=
  fun n => ((List.range n).map fun i => truncatedStaircaseRookPolynomial n i).sum

Theorems

Modified Narayana polynomials are Pólya-frequency
RealRooted.GeneralizedSnakePosets.modifiedNarayanaPolynomial_isPFPolynomialsource
```
theorem modifiedNarayanaPolynomial_isPFPolynomial (n : ℕ) :
    IsPFPolynomial (modifiedNarayanaPolynomial n)
```

Consecutive modified Narayana polynomials interlace

RealRooted.GeneralizedSnakePosets.modifiedNarayanaPolynomial_strictInterl_succsource

theorem modifiedNarayanaPolynomial_strictInterl_succ (n : ℕ) :
    StrictInterl (modifiedNarayanaPolynomial n) (modifiedNarayanaPolynomial (n + 1))

Braun–Jal, Lemma 3.4

RealRooted.GeneralizedSnakePosets.lemma34ModifiedNarayanaInterlacing_modifiedsource

theorem lemma34ModifiedNarayanaInterlacing_modified :
    Lemma34ModifiedNarayanaInterlacingStatement modifiedNarayanaPolynomial

Full truncated staircases have rook polynomial Pₙ

RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.truncatedStaircaseRookPolynomial_full_eq_modifiedNarayanaPolynomialsource

theorem FiniteSkewBoard.truncatedStaircaseRookPolynomial_full_eq_modifiedNarayanaPolynomial
    (n : ℕ) :
    FiniteSkewBoard.truncatedStaircaseRookPolynomial n n =
      modifiedNarayanaPolynomial n

Theorem 4.1 from the combinatorial inputs

RealRooted.GeneralizedSnakePosets.theorem41NonNestingRook_modified_of_sourceInputssource

theorem theorem41NonNestingRook_modified_of_sourceInputs
    {M : SnakeWord → ℝ[X]}
    (hrec2 : NarayanaAuxiliaryGRecurrenceStatement
      modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG)
    (hH_nonneg : ∀ n : ℕ, 1 ≤ n →
      HasNonnegCoeffs
        (FiniteSkewBoard.auxiliaryG n -
          FiniteSkewBoard.auxiliaryG (n - 1)))
    (hrec : Theorem35GeneralizedSnakeRecurrenceStatement M
      modifiedNarayanaPolynomial FiniteSkewBoard.auxiliaryG)
    (hM_nonneg : ∀ w : SnakeWord, HasNonnegCoeffs (M w))
    (hdeg : ∀ {w : SnakeWord}, 1 ≤ w.length →
      (M w.deleteFinal).natDegree + 1 = (M w).natDegree)
    (hM_const : ∀ {w : SnakeWord}, w.IsConstant →
      M w = modifiedNarayanaPolynomial (w.length + 1)) :
    Theorem41NonNestingRookStatement M

Column recurrence for the auxiliary polynomials Gₙ
RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.narayanaAuxiliaryGRecurrence_modifiedsource
```
theorem narayanaAuxiliaryGRecurrence_modified :
    NarayanaAuxiliaryGRecurrenceStatement modifiedNarayanaPolynomial auxiliaryG
```

Constant words give modified Narayana polynomials

RealRooted.GeneralizedSnakePosets.generalizedSnakeRookModel_snakePolynomial_of_isConstantsource

theorem generalizedSnakeRookModel_snakePolynomial_of_isConstant {w : SnakeWord}
    (hw : w.IsConstant) :
    generalizedSnakeRookModel.snakePolynomial w = modifiedNarayanaPolynomial (w.length + 1)

Braun–Jal, Theorem 3.5: the snake recurrenceMain result
RealRooted.GeneralizedSnakePosets.generalizedSnakeTheorem35source
```
theorem generalizedSnakeTheorem35 : GeneralizedSnakeTheorem35
```
Braun–Jal, Theorem 4.1: snake polynomials are real-rooted and interlaceMain result
RealRooted.GeneralizedSnakePosets.theorem41_generalizedSnakeRookModelsource
```
theorem theorem41_generalizedSnakeRookModel :
    Theorem41NonNestingRookStatement generalizedSnakeRookModel.snakePolynomial
```

Lean source RealRooted/Challenges/GeneralizedSnakePosets.lean at revision 5827550b.

Generalized snake posets

References

≔ Definitions

⊢ Theorems

Definitions

Theorems