Real-rooted atlas

Proof step

Gamma criterion

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

Concludes
Triangle read by rows: T(n,k) (n >= 1, 0 <= k <= ceiling(n/2)-1) = number of permutations of [n] with k peaks.
Premises
  • eulerian
    sequence: Every row P_n, n >= 1, 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-ed4df29580db3bff · JSON
Operation
Gamma polynomial of a palindromic parent
{
  "index_shift": 1,
  "operation": "gamma_polynomial",
  "scale": "1/4"
}
Claims
{
  "claim": "real_rooted",
  "from_index": 0,
  "region": {
    "upper": {
      "closed": true,
      "value": "0"
    }
  }
}
Certificate
gamma_polynomial, SHA-256 737290ad36b92d3d209fab3273e64a3eb27748f334955e25ceb2376e5c571593, 7,401 bytes (2,120 compressed); download
polytool replayed the certificate when the step was written.
Cited by