Real-rooted atlas

Proof step

Gamma criterion

Gamma polynomial of a palindromic parent scale 1/4, shift 0

Concludes
Triangle read by rows: T(n,k) is the number of permutations of [n] with k increasing runs of length at least 2.
Premises
  • type_b_eulerian
    sequence: Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]
Theorem
RealRooted IsGammaExpansion.isRealRooted_and_hasRootsNonpos_iff ?
Checked
polytool replayed · Lean not attempted
Technical details
Step id
e-16125ab4d60fcfd7 · JSON
Operation
Gamma polynomial of a palindromic parent
{
  "index_shift": 0,
  "operation": "gamma_polynomial",
  "scale": "1/4"
}
Claims
{
  "claim": "real_rooted",
  "from_index": 0,
  "region": {
    "upper": {
      "closed": true,
      "value": "0"
    }
  }
}
Certificate
gamma_polynomial, SHA-256 fafbfab63c2d005f9c6d4ee81b46c65ac61bc4983bb90c279a2f33985ab1de7c, 10,238 bytes (2,311 compressed); download
polytool replayed the certificate when the step was written.
Cited by