{"chains":[{"edge":{"id":"e-e5594dfd8f34b1b6","operation":{"index_shift":1,"operation":"preserver_image","operator":"{\"shape\":\"reversal\",\"schedule\":{\"first_index\":0,\"first_degree\":0,\"step\":3}}"},"operation_detail":"reversal, shift 1","conclusion_id":"n-73781d44d680ea54","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":"reversed","lean_declarations":["RealRooted.X_pow_mul_reverse_eq_zero_or_splits","RealRooted.reflect_eq_zero_or_splits"],"certificate_hash":"a131f5fd435ba24a31bf691fe6de6adbae32980fdecec2c7e6329e4c7eb83e34","verification_polytool":"replayed","verification_lean":"not_attempted","claims":[{"claim":"real_rooted","from_index":0,"region":{"upper":{"closed":true,"value":"0"}}}],"premises":[{"position":0,"node_id":"n-ddd13fb19530ec39","role":"sequence","name":"An interpolation operator, companion to A133080.","uses":{"claim":"real_rooted","from_index":1,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 1, is zero or real-rooted with all roots in (-inf, 0]"}]},"premises":[{"premise":{"position":0,"node_id":"n-ddd13fb19530ec39","role":"sequence","name":"An interpolation operator, companion to A133080.","uses":{"claim":"real_rooted","from_index":1,"region":{"upper":{"closed":true,"value":"0"}}},"uses_text":"Every row P_n, n >= 1, is zero or real-rooted with all roots in (-inf, 0]"},"chains":[{"edge":{"id":"e-97c604120024b828","operation":{"operation":"theorem_check","theorem":"iterated_preserver"},"operation_detail":"iterated_preserver","conclusion_id":"n-ddd13fb19530ec39","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; here S_n is the identity; with lag L = 2, the induction runs in each residue class of n modulo L from its start row","lean_route":null,"lean_declarations":[],"certificate_hash":"7758212977d07716a2002f4953b417d2325324b62f31ee3516994fa1d26fd0e0","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}