{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013610 of Triangle of coefficients of polynomials v(n,x) jointly generated with A207606; see Formula section."},"identifying_rows":1,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["-270","-1728","-2592","0","0"],["90","1071","4725","5751","972"],["0","45","756","648","-486"],["0","0","-81","-567","-486"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["50","750","4536","11340","9558","1944"],["0","90","1251","4833","4131","0"],["0","0","-45","-108","-1458","-1458"],["0","0","0","-81","-567","-486"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","25","510","3132","6966","4779","972"],["0","0","0","90","54","-810","-486"],["0","0","0","-45","-432","-1053","-486"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["90","216","0","0"],["-60","-684","-1755","-324"],["0","0","-243","0"],["0","0","54","324"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["0","90","216","0","0"],["0","-60","-684","-1755","-324"],["0","0","0","-243","0"],["0","0","0","54","324"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["1"]],"recurrence":{"denominator":{"coeffs":[["150","900","1458","0"],["-60","-684","-1107","648"],["0","0","-405","-972"],["0","0","54","324"]]},"terms":[{"coeff":{"coeffs":[["360","2754","6480","4536","972"],["-90","-981","-2970","-2754","-486"],["0","-45","-999","-2349","-972"],["0","0","81","567","486"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["-25","-510","-2997","-6480","-4536","-972"],["0","0","-180","-918","-1296","-486"],["0","0","45","432","1053","486"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":0,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_leader_shift":2,"parent_valid_from_base":0,"quotients":[],"row_annihilation":{"kind":"system","system":{"generators":[{"annihilator":{"terms":[{"coeff":{"coeffs":[["-162","-324","0"],["-27","-162","0"],["9","108","324"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["18","126","54","-324"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-5","-78","-405","-756","-324"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["54"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["1093500","10497600","37004040","57631824","37555164","8503056","0","0","0","0"],["-2187000","-36304200","-226551330","-677410128","-1002652020","-680244480","-188130114","-12754584","0","0"],["1458000","34408800","319761270","1521574632","3958881156","5511397464","3744533286","1113900336","102036672","0"],["-324000","-9914400","-120824460","-788912136","-3059892936","-7141937184","-9510904332","-6452402328","-1989715104","-204073344"],["0","0","-2187000","-41990400","-303905520","-1029814560","-1651010040","-1105397280","-255091680","0"],["0","0","291600","7348320","74113056","380433024","1043986320","1468194336","918330048","204073344"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","1093500","10497600","37004040","57631824","37555164","8503056","0","0","0","0"],["0","-2187000","-36304200","-226551330","-677410128","-1002652020","-680244480","-188130114","-12754584","0","0"],["0","1458000","34408800","319761270","1521574632","3958881156","5511397464","3744533286","1113900336","102036672","0"],["0","-324000","-9914400","-120824460","-788912136","-3059892936","-7141937184","-9510904332","-6452402328","-1989715104","-204073344"],["0","0","0","-2187000","-41990400","-303905520","-1029814560","-1651010040","-1105397280","-255091680","0"],["0","0","0","291600","7348320","74113056","380433024","1043986320","1468194336","918330048","204073344"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-531441000","-5739562800","-23532207480","-45457337376","-42357973464","-18596183472","-3099363912","0","0","0"],["1062882000","17856417600","115939168560","373301164512","630203995440","545488048512","229352929488","37192366944","0","0"],["-708588000","-16155806400","-148718449440","-712624117248","-1913340655008","-2884474680768","-2334854147040","-942206629248","-148769467776","0"],["157464000","4534963200","54589619520","356652180864","1375352301888","3192115246848","4364822718144","3322518113664","1289335387392","198359290368"]]},"step_quotients":[[{"coeff":{"coeffs":[["177147000","4038951600","27613674360","74843898912","54755429112","-97113402576","-178729985592","-99179645184","-18596183472","0","0","0"],["-265720500","-9778514400","-111889588140","-565882628328","-1328421810060","-1047585002256","996445497708","2116865551896","1190155742208","223154201664","0","0"],["-29524500","4286957400","102642514740","914401636128","4016335596804","8997453436536","8613993245868","-1002127664880","-7419877205328","-4611853501056","-892616806656","0"],["242757000","4944369600","26149259160","-132616495728","-2188605835368","-10818489167136","-26516282707224","-32467788429552","-15016073779872","3479552551872","5157341549568","1190155742208"],["-144342000","-4708173600","-64023287760","-463575275712","-1853946808848","-3460012529184","1330736767056","19982861844480","39567168448128","35175714158592","14777767132416","2380311484416"],["26244000","1070755200","19112980320","195831048384","1270067462496","5422636896768","15363814758048","28436089936320","33048861767424","22546839338496","8132730905088","1190155742208"]]},"deriv_order":0},{"coeff":{"coeffs":[["-177147000","-3153216600","-21767823360","-72611846712","-109281275712","-9298091736","185961834720","228319808184","108477736920","18596183472","0","0","0"],["354294000","8432197200","81374245920","406437573744","1089904711968","1329971492016","-260346568608","-2688181633008","-2956793172048","-1338925209984","-223154201664","0","0"],["-236196000","-7038640800","-87978286080","-596455366176","-2352353436288","-5246266509216","-5146321588992","2833507363104","12723921980064","12719789494848","5504470307712","892616806656","0"],["52488000","1879070400","28935584640","249850018368","1318019029632","4302308250432","8138649032064","6232093815744","-6605548035264","-19791849194496","-18182934950400","-7537653033984","-1190155742208"]]},"deriv_order":1},{"coeff":{"coeffs":[["49207500","1299078000","14455195200","88686874080","329616714312","767723920128","1122428901168","1009703887776","537739638732","154968195600","18596183472","0","0","0"],["-98415000","-3188646000","-44499326400","-350836090560","-1723475917584","-5490848412000","-11457544843872","-15488554589568","-13191925930776","-6762812055984","-1896810714144","-223154201664","0","0"],["65610000","2519424000","42420801600","411888032640","2552328307296","10554469278336","29601756877248","56155882435200","70748835645456","57276245093760","28315788700032","7736012324352","892616806656","0"],["-14580000","-647352000","-12786076800","-148091742720","-1116368111808","-5748542027136","-20650793899392","-51948094155264","-90596473390368","-107059835325888","-82660724280576","-39473498783232","-10513042389504","-1190155742208"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-118098000","-3401222400","-40942214640","-267489135648","-1031514226416","-2394086435136","-3273617038608","-2491888585248","-967001540544","-148769467776","0","0","0"],["29524500","2090334600","45948388860","496765537632","3066514480908","11429420986152","25956311828580","34995951051696","26406580530240","10190708542656","1562079411648","0","0"],["82012500","2106081000","16575054300","-32198238720","-1419034626324","-10736974620792","-42111382714236","-96337643267952","-129125010554208","-96683624113536","-37068392387520","-5653239775488","0"],["-52488000","-1984046400","-31801429440","-276984214848","-1365148634688","-3224869018560","1808191864512","35310708675648","104518816083072","153199491927552","119015574220800","46416073946112","7140934453248"],["13122000","614109600","12768755760","155254465152","1222526876400","6521520835872","23949818069328","60309489242304","101832700692672","110420004971520","71706883468032","24993270586368","3570467226624"]]},"deriv_order":0},{"coeff":{"coeffs":[["-236196000","-7806277800","-111503407680","-903394430136","-4582339393680","-15160978608696","-33086054134368","-47174040609480","-42756758287344","-23468383541664","-7066549719360","-892616806656","0","0"],["249318000","9778514400","168700631040","1684665135648","10784612992032","46318884016032","135800810838144","271431271452384","363652500280176","316068999260544","168853345925760","49986541172736","6248317646592","0"],["-61236000","-2787112800","-56611457280","-676818693216","-5289649100928","-28386040948704","-106928514129024","-284156570927520","-528185332912608","-672071580658368","-564431360742144","-295158624067584","-86286291310080","-10711401679872"]]},"deriv_order":1},{"coeff":{"coeffs":[["-16402500","-629856000","-10605200400","-102972008160","-638082076824","-2638617319584","-7400439219312","-14038970608800","-17687208911364","-14319061273440","-7078947175008","-1934003081088","-223154201664","0","0"],["21870000","971028000","19179115200","222137614080","1674552167712","8622813040704","30976190849088","77922141232896","135894710085552","160589752988832","123991086420864","59210248174848","15769563584256","1785233613312","0"],["-7290000","-367416000","-8335094400","-112404101760","-1002459284064","-6223375348992","-27571023031104","-87926428775808","-201142519160976","-325319337834048","-362509868117952","-267718922233344","-123677017544448","-32134205039616","-3570467226624"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0"],["81","0"],["81","0"],["-18","-108"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-36","-54","0"],["-36","-36","108"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["-15","-54","-27","0"],["10","96","234","108"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["-364500","-11153700","-127808280","-712445868","-2084429700","-3163845420","-2295825120","-733388580","-76527504","0","0"],["486000","17787600","259749990","1968588684","8451486540","20847603744","28377886518","19380590388","5981899896","612220032","0"],["-162000","-6901200","-121210830","-1147877568","-6496938396","-22848183864","-49436649486","-62104903848","-40563828648","-12193382304","-1224440064"],["0","0","-874800","-28605960","-348310368","-2053015632","-6221402640","-9357613128","-6071181984","-1377495072","0"],["0","0","145800","5423760","81146448","634894848","2804591304","6998015088","9268331040","5612016960","1224440064"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","-364500","-7873200","-67447080","-293197968","-687094164","-844636896","-484674192","-102036672","0","0","0"],["0","486000","14142600","170520390","1102405464","4131619164","9054809856","11113848486","6912984528","1900433016","153055008","0"],["0","-162000","-5929200","-91467630","-782123688","-4079026188","-13368536136","-27171869742","-32422152528","-20505119544","-6071181984","-612220032"],["0","0","0","-874800","-22044960","-222339168","-1141299072","-3131958960","-4404583008","-2754990144","-612220032","0"],["0","0","0","145800","4548960","59101488","412555680","1663292232","3866056128","4863748032","2857026816","612220032"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["-531441000","-5739562800","-23532207480","-45457337376","-42357973464","-18596183472","-3099363912","0","0","0"],["1062882000","17856417600","115939168560","373301164512","630203995440","545488048512","229352929488","37192366944","0","0"],["-708588000","-16155806400","-148718449440","-712624117248","-1913340655008","-2884474680768","-2334854147040","-942206629248","-148769467776","0"],["157464000","4534963200","54589619520","356652180864","1375352301888","3192115246848","4364822718144","3322518113664","1289335387392","198359290368"]]},"step_quotients":[[{"coeff":{"coeffs":[["-1417176000","-14242618800","-51273427680","-74155151376","-22039921152","35126124336","28927396512","6198727824","0","0","0"],["974308500","28591525800","225532931580","745683998976","1058432775948","383288003784","-378638957916","-340930030320","-74384733888","0","0"],["1564798500","14774059800","-42951061620","-873510439824","-3459521477700","-5492417225832","-2817493982892","929809173600","1264540476096","297538935552","0"],["-1351566000","-34988500800","-316923068880","-1206748038816","-1286316802512","3728419994880","11270128986576","9490481881056","1702583908992","-1157095860480","-396718580736"],["-157464000","3023308800","112070278080","1100431495296","5036224019904","11515858801920","11096181969984","-1493204658048","-9917964518400","-6149138001408","-1190155742208"],["314928000","8125142400","81969459840","385766644608","610791518592","-1867883317632","-10423046044800","-19543900081536","-17356437907200","-7339293743616","-1190155742208"],["-52488000","-1826582400","-27266466240","-228063299328","-1171755129024","-3814743019392","-7839171399744","-9837151474176","-7074814689792","-2644790538240","-396718580736"]]},"deriv_order":0},{"coeff":{"coeffs":[["708588000","8538485400","39879332640","88351003368","85175111952","4476858984","-49589822592","-32026760424","-6198727824","0","0","0"],["-1062882000","-21399357600","-163768858560","-620740094112","-1219083138720","-1081333631520","-24794911296","624005267616","390519852912","74384733888","0","0"],["236196000","10109188800","136729140480","875270572416","3004265733696","5572426731264","4837762692864","292028955264","-2467093673952","-1562079411648","-297538935552","0"],["262440000","4933872000","28469491200","-15532248960","-865837848960","-4061807814528","-8736379856640","-8904740365440","-2469389499072","2446431247872","1950533021952","396718580736"],["-104976000","-3128284800","-39101460480","-265091273856","-1045490416128","-2331674004096","-2287254039552","1259336605824","5655076435584","5653239775488","2446431247872","396718580736"]]},"deriv_order":1},{"coeff":{"coeffs":[["49207500","118098000","-4322386800","-37158354720","-133119593208","-252540763200","-267463626480","-158411933280","-49073261940","-6198727824","0","0","0"],["-196830000","-2834352000","-9636796800","49997969280","510030304992","1779723633024","3257316680256","3355577995392","1948466779344","595077871104","74384733888","0","0"],["262440000","6141096000","56309126400","241713538560","338965824384","-1179339854976","-6297295249152","-12573775017216","-13287317464512","-7777337176512","-2380311484416","-297538935552","0"],["-145800000","-4548960000","-60256224000","-440647257600","-1929589050240","-5070633053184","-7212632221440","-2577038188032","7991614187712","13433331942144","9212687041536","3041509118976","396718580736"],["29160000","1119744000","18853689600","183061347840","1134368136576","4690875234816","13156336389888","24958169971200","31443926953536","25456108930560","12584794977792","3438227699712","396718580736"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["-1358127000","-15022065600","-55461182760","-40023884592","237962273688","651555169056","657409523112","295472692944","49589822592","0","0","0"],["2450533500","45420490800","323849516580","1074433401576","1323026621028","-1447747320672","-6112117821348","-6633671892984","-3062171545056","-520693137216","0","0"],["-1236748500","-33591007800","-373556964780","-2171065448016","-6879582398268","-10570552808760","-1793594243124","17121345414912","22143922029936","10802316354624","1884413258496","0"],["19683000","3086294400","77493545640","863595876528","5223278497320","18124825065696","35115219166680","31947095292336","943584124320","-19216056254400","-12298276002816","-2380311484416"],["118098000","3637418400","44910307440","267744227328","583879346352","-1962624367584","-16694551525104","-48418951780800","-72616030215552","-57722553497088","-22910498037504","-3570467226624"],["-26244000","-1070755200","-19112980320","-195831048384","-1270067462496","-5422636896768","-15363814758048","-28436089936320","-33048861767424","-22546839338496","-8132730905088","-1190155742208"]]},"deriv_order":0},{"coeff":{"coeffs":[["-531441000","-8160571800","-34267315680","87126563304","1276070620032","4905145160136","9672770395584","10734474722328","6722520325128","2212945833168","297538935552","0","0"],["1115370000","26965710000","258823576800","1199767029840","2173160034144","-3729159760752","-27795248617824","-62069698361808","-71962408803888","-46027620335808","-15348050092224","-2082772548864","0"],["-691092000","-22134189600","-302494642560","-2297278197792","-10543199894784","-29479840060320","-46268120771712","-24527830307040","41831311181472","87672051352512","67954586891904","24894090941184","3570467226624"],["122472000","4839393600","84186552960","848518068672","5488189789824","23842943158464","70799369307264","143516926011456","195269109756480","172528502777856","93691704817152","28167019232256","3570467226624"]]},"deriv_order":1},{"coeff":{"coeffs":[["-16402500","-236196000","377913600","28258489440","244875258216","1062558883872","2696752713456","4153147642080","3859569004860","2099302489728","613674054576","74384733888","0","0"],["54675000","1509030000","16218792000","76244068800","21923712720","-1545464440224","-8276959740960","-21948700367232","-33973964499528","-31421351339856","-16980381752544","-4934187347904","-595077871104","0"],["-51030000","-1872072000","-29634724800","-263796289920","-1435960195488","-4805927251200","-8950962977856","-4207788279936","19847637744912","49783590232128","54344935580544","31737486458880","9620425582848","1190155742208"],["14580000","647352000","12786076800","148091742720","1116368111808","5748542027136","20650793899392","51948094155264","90596473390368","107059835325888","82660724280576","39473498783232","10513042389504","1190155742208"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["656100","4723920","10865016","8503056","2125764","0","0"],["-874800","-11547360","-52278048","-98257536","-70858800","-17006112","0"],["291600","5598720","40520736","137308608","220134672","147386304","34012224"]]},"start_base":0}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-3","-3"]]},"deriv_order":0,"shift":1},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":2}]},"statement":"w(n) E = sum_nu H_nu S^nu L' (with any remainder removed by row annihilators of the parent), where L' is the parent rule at P'_n = P_(n+0) (valid from base 0) and E the input rule gauged by lambda(n)/delta(n) and composed with (or conjugated through) T = f(n, theta) = 1 + (1) theta; so the candidate rows satisfy the input rule at every base n >= 0 (the exceptional bases checked exactly), and agreement on the 1 identifying rows gives Q_n = lambda(n) T_n(P_(n+0)) for every n >= 0"},"method":"operator_division"},"status":"certified"},"input_first_index":0,"interlacing":{"from_index":1,"justification":"the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = f(n, theta) = 1 + (1) theta is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1","kind":"weak","orientation":"unordered","status":"claimed"},"lean_declarations":["RealRooted.isMultiplierSequence_eval_of_roots_nonpos","RealRooted.isPFMultiplierSequence_eval_of_roots_nonpos","RealRooted.isMultiplierSequence_iff_preserves"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [1, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"euler_polynomial_roots_nonpositive","statement":"the polynomial in theta is real-rooted with every root <= 0 for every n >= n0","status":{"kind":"verified"}},{"evidence":"lambda(n) = 1","name":"gauge_finite_nonzero","statement":"lambda(n) is finite and nonzero for every n >= n0","status":{"kind":"verified"}},{"evidence":"delta(n) != 0 for every integer n in [0, +inf) (exact; Taylor shift: the coefficients of delta(n) at n = 0 + u have one sign)","name":"operator_coefficients_defined","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1"]},"numerator":["1"],"range":{"first":"0","last":null}},"decision":"holds"},"statement":"the operator coefficients are finite at every n >= n0 (their denominators do not vanish)","status":{"kind":"verified"}}],"identity":{"method":"forward_division","status":"certified"},"input_first_index":0,"input_interlacing":{"interlacing":{"from_index":1,"justification":{"premises":["the parent theorem (ThreeTermRecurrence) proves P_(m-1) strictly interlacing P_m for every m >= 1; T = f(n, theta) = 1 + (1) theta is independent of n and maps every real-rooted polynomial to a real-rooted polynomial or zero, so by the Hermite--Kakeya--Obreschkoff theorem (both directions) T(P_(m-1)) and T(P_m) have weakly interlacing zeros; the nonzero gauge does not move zeros, so Q_(n-1) and Q_n interlace weakly (orientation not determined) for every n >= 1"],"theorem":"Hermite--Kakeya--Obreschkoff theorem (N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, 1963; see S. Fisk, Polynomials, Roots, and Interlacing, arXiv:math/0612833): real polynomials f, g have weakly interlacing zeros iff alpha f + beta g is real-rooted or zero for all real alpha, beta; a linear T independent of n that maps every real-rooted polynomial to a real-rooted polynomial or zero therefore maps interlacing pairs to pairs with weakly interlacing zeros (orientation not determined)"},"kind":"weak","orientation":"unordered"},"status":"proved"},"lean_replay":"not_attempted","operation":{"description":"f(n, theta) = 1 + (1) theta","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["1"]},{"denominator":["1"],"numerator":["1"]}],"shape":"euler_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (1) theta, for every n >= 0"},"parent_proof":{"route":"three_term_recurrence","statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"root_transfer":{"input_conclusion":"every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]","input_root_region":{"upper":{"closed":true,"value":"0"}},"parent_hypothesis":"every parent row used is zero or real-rooted with all roots in (-inf, 0] (coefficients of one sign)","parent_root_region":{"upper":{"closed":true,"value":"0"}},"theorem":"Laguerre's theorem on multiplier sequences: if f is a real polynomial whose roots are all real and <= 0, then (f(k))_(k >= 0) is a multiplier sequence, so x^k -> f(k) x^k maps every real-rooted polynomial to a real-rooted polynomial or zero (Laguerre; see T. Craven and G. Csordas, Multiplier sequences for fields, Illinois J. Math. 21 (1977); Polya--Schur, Theorem 40 of P. Branden, arXiv:1410.6601: sum_k f(k) x^k / k! = f(theta) e^x = C e^x x^m prod (1 + x/a_j), a_j > 0); f(k) has one sign for k >= 0, so coefficients of one sign stay of one sign; applied to f(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"parent_interlacing_report":{"conclusion":{"first_index":0,"interlacing":"strict","interlacing_from":1,"root_region":{"upper":{"closed":false,"value":"0"}},"simple_roots":true,"statement":"every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"},"hypotheses":[{"evidence":"f(n) a_n = 3 != 0 for every integer n in [2, +inf) (exact; Taylor shift: the coefficients of f(n) a_n = 3 at n = 2 + u have one sign)","name":"leading_coefficient_nonzero","sign_decision":{"certificate":{"condition":"nonzero","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["3"]},"numerator":["3"],"range":{"first":"2","last":null}},"decision":"holds"},"statement":"a_n != 0 for every n >= 2","status":{"kind":"verified"}},{"evidence":"Q_0 has degree 0, Q_1 degree 1; simple real roots and strict interlacing checked exactly","name":"seeds_interlace","statement":"Q_0 and Q_1 have simple real roots, degrees e and e + 1, and Q_0 strictly interlaces Q_1","status":{"kind":"verified"}},{"evidence":"beta_2 = 1/18 (exact)","name":"first_coefficient_positive","statement":"beta_2 = c_2 L_0 / (a_2 L_1) > 0","status":{"kind":"verified"}},{"evidence":"beta_n = 1/9 > 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of beta_n = 1/9 at n = 3 + u have one sign)","name":"recurrence_coefficient_positive","sign_decision":{"certificate":{"condition":"positive","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["1/9"]},"numerator":["1/9"],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"beta_n = c_n / (a_n a_(n-1)) > 0 for every n >= 3","status":{"kind":"verified"}},{"evidence":"seeds checked exactly; positive-ratio induction at t = 0 with g(n) = 1/2 ((t - alpha_n)/2): g(n) > 0 for n >= 2, r_2 >= g(2) exactly, and (t - alpha_n) - beta_n/g(n-1) - g(n) >= 0 for every integer n in [3, +inf) (exact; Taylor shift: the coefficients of (t - alpha_n) - beta_n/g(n-1) - g(n) at n = 3 + u have one sign)","name":"root_upper_bound","sign_decision":{"certificate":{"condition":"nonnegative","denominator":["1"],"method":{"kind":"taylor_shift","shifted_denominator":["1"],"shifted_numerator":["5/18"]},"numerator":["5/18"],"range":{"first":"3","last":null}},"decision":"holds"},"statement":"every root of P_n is < 0 for every n >= 0 (region (-inf, 0) for P)","status":{"kind":"verified"}}],"lean_replay":"not_attempted","normal_form":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 3, b_n = 3, c_n = 1","recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","6"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["-1"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["3","3"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"reference":"three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction","requested_root_region":{"upper":{"closed":false,"value":"0"}},"schema":"polytool.recurrence-real-rootedness-theorem.v1","status":"proved","theorem":"three_term_recurrence"},"parent_proof":{"attempts":[{"detail":"the rule is not P_(n+k) = c(x) P_n with c free of n","route":"periodic_product","success":false,"variant":"P_(n+k) = c(x) P_n"},{"detail":"not applicable: expected one nonzero lag term","route":"product_recurrence","success":false,"variant":"product_recurrence"},{"detail":"no theorem matched (weighted_renewal_window: coefficient of P_(n-1) must be 1 after normalization; fixed_delay_predecessor_window: coefficient of P_(n-1) must be 1 (+ w(n) t) after normalization)","route":"paper_theorem","success":false,"variant":"match_recurrence_theorems"},{"detail":"P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 3, b_n = 3, c_n = 1: every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)","route":"three_term_recurrence","success":true,"variant":"three_term_recurrence"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = (a_n x + b_n) P_(n-1) - c_n P_(n-2) for n >= 2, with a_n = 3, b_n = 3, c_n = 1","every P_n, n >= 0, is nonzero and real-rooted, with simple roots from n = 0 on; P_(n-1) strictly interlaces P_n for n >= 1; every root lies in (-inf, 0)"],"theorem":"three_term_recurrence: three-term recurrence Q_n = (a_n y + b_n) Q_(n-1) - c_n Q_(n-2) with a_n != 0 and beta_n = c_n / (a_n a_(n-1)) > 0: simple real roots and strict interlacing of consecutive rows (zero separation for orthogonal polynomials: G. Szeg\u0151, Orthogonal Polynomials, \u00a73.3; Favard, C. R. Acad. Sci. Paris 200 (1935)); root regions by a positive-ratio (chain-sequence) induction"},"kind":"strict","orientation":"previous_interlaces_next"},"route":"three_term_recurrence","rows_checked":10,"statement":"every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign","status":"proved"},"rows_compared":16,"schema":"polytool.recurrence-preserver-image.v1","statement":"proved: Q_n = lambda(n) T_n(P_(n+0)) with T = f(n, theta) = 1 + (1) theta for every n >= 0, the side conditions hold for every n, and every parent row P_n, n >= 0, is zero or real-rooted with coefficients of one sign; so every Q_n, n >= 0, is zero or real-rooted with roots in (-inf, 0]"},"kind":"preserver_image"}