{"chains":[{"edge":{"id":"e-3333a9756ae82eb9","operation":{"index_shift":0,"operation":"preserver_image","operator":"{\"shape\":\"affine\",\"slope\":\"1\",\"intercept\":\"1\"}"},"operation_detail":"affine, shift 0","conclusion_id":"n-f6bd524925313b17","premise_count":1,"theorem":"a real affine substitution x -> a x + b (a != 0), the reversal x^d p(1/x) (d >= deg p) and a real Mobius map (c x + e)^d p((a x + b)/(c x + e)) (a e - b c != 0, d >= deg p) map real roots to real roots: a root r of p gives the root (r - b)/a, 1/r (and 0) or (e r - b)/(a - c r) (and -e/c); for an input row that is a polynomial the degree condition holds automatically","lean_route":null,"lean_declarations":["Polynomial.Splits.comp_of_degree_le_one"],"certificate_hash":"c1ad73d399d6239d6f406174b942195bd89c6d36e2e1f25b923c76360cf803b7","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"-1"}}}],"premises":[{"position":0,"node_id":"n-b8808e9caf8dcf35","role":"sequence","name":"Triangle read by rows, (2, 3)-Lah numbers.","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-b8808e9caf8dcf35","role":"sequence","name":"Triangle read by rows, (2, 3)-Lah numbers.","uses":{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 0, is zero or real-rooted with all roots in (-inf, 0]"},"chains":[{"edge":{"id":"e-66440ab2a9214737","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-b8808e9caf8dcf35","premise_count":0,"theorem":"Iterated real-rootedness preservers (induction on n): if P_m is nonzero and real-rooted with every root in a closed region R and, for every n > m, P_n = a_n(x) S_n(P_(n-1)) where S_n maps every polynomial that is zero or real-rooted with every root in R to zero or a real-rooted polynomial with every root in R and a_n is real-rooted with every root in R, then every P_n is real-rooted with every root in R (the roots of a product are the roots of its factors); an exact degree step keeps every row nonzero; S_n = kappa (theta + a)(theta + b) + x (u + v theta) with kappa (t + a)(t + b) = 25 + 10 n + n^2 + (10 + 2 n) t + (1) t^2 and u + v theta = 1: The degree-local Euler step: T = kappa (theta + a)(theta + b) + x (u + v theta), theta = x D, with kappa, a, b > 0, u + v k > 0 for every k <= d and a negative comparison defect kappa (a b - (a + b + 1)^2/4) + (u - (a + b + 1) v/2) s - v^2 s^2/(4 kappa) < 0 for every s <= 0, maps every polynomial of degree <= d with nonnegative coefficients and only real roots to such a polynomial (RealRooted IsPFPolynomial.generalStep_of_natDegree_le, a half-line theorem: the symbol of T has discriminant -4 kappa s^2 times the comparison defect at s, so its real-rootedness is required for s <= 0 only, and the hypothesis (i) of P. Branden, Linear transformations preserving the Polya frequency property, Trans. Amer. Math. Soc. 358 (2006), Corollary 3.5, for every real s, is not needed); here d = deg P_(n-1), so u(n) + v(n) k > 0 is required for 0 <= k <= deg P_(n-1) only (both ends, the condition being linear in k); by linearity a row with nonpositive coefficients is handled through its negative","lean_route":null,"lean_declarations":["RealRooted.IsPFPolynomial.generalStep_of_natDegree_le","RealRooted.EulerBidiagonal.generalStep","RealRooted.EulerBidiagonal.comparisonDefect","RealRooted.EulerBidiagonal.generalRowsDep_spec"],"certificate_hash":"6001c2791d322bad5792cf2399cd0fb7462836cf2e7440aefe3781eed1b9d50a","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[]},"premises":[]}]}]}],"truncated":false,"expanded":2}