{"certification":{"candidate":{"gauge":{"kind":"none"},"index_shift":0,"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"parent_name":"basis_map_A013611 of A Riordan array of coordination sequences."},"identifying_rows":2,"identity":{"certificate":{"certificate":{"dividend_relation":{"terms":[{"coeff":{"coeffs":[["6","54","144","96"],["2","28","104","96"],["-10","-52","-56","0"],["2","6","0","0"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["1","12","50","80","32"],["1","12","50","80","32"],["-1","-8","-18","-8","0"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["0","0","0"],["-2","-10","-16"],["2","2","-8"],["0","2","0"]]},"deriv_order":1,"shift":1}]},"exceptional_bases":[],"gauge":{"kind":"none"},"identifying_indices":[0,1],"index_shift":0,"input":{"first_index":0,"initial_polynomials":[["0"],["4"]],"recurrence":{"denominator":{"coeffs":[["4","10","8"],["-6","-8","0"],["2","-4","-8"],["0","2","0"]]},"terms":[{"coeff":{"coeffs":[["8","32","16","0"],["-28","-150","-216","-96"],["16","70","56","0"],["-2","-6","0","0"]]},"deriv_order":0,"offset":1,"sign":"none"},{"coeff":{"coeffs":[["1","8","18","8","0"],["-3","-28","-86","-96","-32"],["1","8","18","8","0"]]},"deriv_order":1,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"input_valid_from_base":1,"multiplier":["1"],"operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"},"parent":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","4"]]},"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":[["-3","-4","0"],["2","-4","-16"],["0","4","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-1","2","28","24"],["0","-4","-16","-8"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["0","1","8","18","8"]]},"deriv_order":2,"shift":0},{"coeff":{"coeffs":[["1"]]},"deriv_order":0,"shift":1}]},"quotient":[{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["-2","-58","-744","-5544","-26472","-84136","-178624","-246528","-206848","-92160","-16384"],["2","42","328","840","-3736","-36376","-127680","-241024","-249344","-126976","-24576"],["0","10","208","1760","7520","15240","2944","-47520","-86016","-55808","-12288"],["0","0","16","296","2208","8352","16192","12960","-1920","-6656","-2048"],["0","0","0","8","128","800","2432","3616","2304","512","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["1","36","582","5568","34956","150864","455624","960960","1387392","1316864","768000","245760","32768"],["0","6","192","2724","22512","119688","426432","1028016","1653696","1709568","1062912","356352","49152"],["0","0","12","336","4104","28608","124944","353088","643680","732672","488448","172032","24576"],["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"]]},"step_quotients":[[{"coeff":{"coeffs":[["1","36","566","4992","25644","61776","-103672","-1452864","-5902592","-14058496","-21430272","-20824064","-12255232","-3932160","-524288"],["2","82","1484","15516","102312","428568","1021648","443600","-5840576","-21930752","-40791040","-44503040","-28196864","-9502720","-1310720"],["0","16","564","8784","79032","448896","1634160","3564608","3084960","-5781504","-22038016","-30867456","-22290432","-8126464","-1179648"],["0","0","48","1496","20448","160144","785536","2460960","4714880","4492992","-781056","-6801408","-6840320","-2899968","-458752"],["0","0","0","64","1760","20992","141632","590080","1549952","2491392","2191104","651264","-385024","-327680","-65536"],["0","0","0","0","32","768","7872","44800","153984","325632","413952","297984","110592","16384","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1","-38","-642","-6284","-38532","-144648","-248792","497456","4572000","14729856","28622336","36218880","29761536","15171584","4325376","524288"],["0","-10","-364","-5948","-57432","-362520","-1559376","-4600400","-9018272","-10427776","-3342848","9250816","15540224","10977280","3801088","524288"],["0","0","-36","-1224","-18648","-167760","-988272","-3994848","-11285280","-22258368","-30101760","-26892288","-14893056","-4571136","-589824","0"],["0","0","0","-56","-1744","-24144","-195488","-1024544","-3632832","-8848832","-14742912","-16458240","-11874304","-5242880","-1277952","-131072"],["0","0","0","0","-32","-896","-11008","-77824","-348928","-1031168","-2024448","-2605056","-2130432","-1054720","-286720","-32768"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","1","44","888","10880","90264","535392","2336288","7601152","18483216","33358272","43963648","41192448","26357760","10829824","2555904","262144"],["0","0","6","240","4368","47808","350352","1810944","6773952","18511104","36854880","52730112","52861440","35708928","15310848","3735552","393216"],["0","0","0","12","432","7008","67584","430368","1900416","5946240","13237248","20760768","22417152","16054272","7200768","1818624","196608"],["0","0","0","0","8","256","3648","30464","165056","606720","1537280","2675712","3137664","2394112","1126400","294912","32768"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["0","0","2","80","1420","14768","99928","461312","1479824","3292608","4979712","4913152","2953216","966656","131072"],["0","0","-4","-100","-904","-1848","30736","312400","1471264","4165728","7435776","8246272","5373952","1859584","262144"],["0","0","-8","-256","-3552","-27776","-132224","-377856","-537728","148992","2011776","3467264","2781184","1081344","163840"],["0","0","0","-24","-656","-7760","-51744","-211744","-539584","-816576","-607104","0","307200","180224","32768"],["0","0","0","0","-16","-384","-3936","-22400","-76992","-162816","-206976","-148992","-55296","-8192","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","-2","-78","-1372","-14372","-99688","-481448","-1656848","-4087088","-7169856","-8753152","-7157760","-3682304","-1064960","-131072"],["0","0","6","200","2968","25776","144704","546464","1395360","2338112","2329248","893184","-668672","-950272","-417792","-65536"],["0","0","0","20","616","8424","67280","347216","1209696","2887136","4695744","5091456","3543040","1495040","344064","32768"],["0","0","0","0","16","448","5504","38912","174464","515584","1012224","1302528","1065216","527360","143360","16384"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","0","-1","-40","-728","-7968","-58392","-301824","-1128992","-3085184","-6142480","-8788352","-8810240","-5951488","-2551808","-622592","-65536"],["0","0","0","-4","-144","-2336","-22528","-143456","-633472","-1982080","-4412416","-6920256","-7472384","-5351424","-2400256","-606208","-65536"],["0","0","0","0","-4","-128","-1824","-15232","-82528","-303360","-768640","-1337856","-1568832","-1197056","-563200","-147456","-16384"]]},"deriv_order":2}]]},{"annihilator":{"terms":[{"coeff":{"coeffs":[["0","0","0"],["-8","-40","-64"],["8","8","-32"],["0","8","0"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["6","54","144","96"],["-6","-28","-16","16"],["0","-8","-32","-16"]]},"deriv_order":1,"shift":0},{"coeff":{"coeffs":[["1","12","50","80","32"],["0","2","16","36","16"]]},"deriv_order":2,"shift":0}]},"quotient":[{"coeff":{"coeffs":[["1","24","244","1360","4484","8768","9600","5120","1024"],["1","26","284","1688","5892","12104","13792","7552","1536"],["-1","-18","-124","-376","-260","1240","2976","2176","512"],["0","-2","-32","-200","-608","-904","-576","-128","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","0","0","0","0","0","0","0","0","0","0"],["0","2","50","544","3368","13000","32136","50080","46208","22016","4096"],["0","-2","-38","-276","-824","296","9192","26640","34304","19712","4096"],["0","0","-6","-108","-776","-2768","-4760","-2288","3392","3840","1024"],["0","0","0","-4","-64","-400","-1216","-1808","-1152","-256","0"]]},"deriv_order":1}],"step_multiplier":{"coeffs":[["1","36","582","5568","34956","150864","455624","960960","1387392","1316864","768000","245760","32768"],["0","6","192","2724","22512","119688","426432","1028016","1653696","1709568","1062912","356352","49152"],["0","0","12","336","4104","28608","124944","353088","643680","732672","488448","172032","24576"],["0","0","0","8","192","1968","11200","38496","81408","103488","74496","27648","4096"]]},"step_quotients":[[{"coeff":{"coeffs":[["0","-24","-960","-17424","-189504","-1373472","-6976512","-25417920","-66802944","-125549568","-164794368","-144850944","-79626240","-24379392","-3145728"],["8","288","4384","34752","121344","-307584","-5863040","-33347328","-112830592","-250846208","-371226624","-356220928","-208633856","-66846720","-8912896"],["8","368","7312","82752","585504","2625408","6803392","4599040","-34552576","-143073536","-278660096","-313630720","-203128832","-69533696","-9699328"],["0","56","2112","35088","336768","2050848","8136576","20390080","27325440","-185856","-67956224","-115826688","-90390528","-34340864","-5111808"],["0","0","144","4672","66528","544256","2806208","9374976","19891840","24290304","10607616","-10960896","-16580608","-7864320","-1310720"],["0","0","0","160","4480","54464","375296","1602944","4349440","7350528","7163904","3201024","-90112","-557056","-131072"],["0","0","0","0","64","1536","15744","89600","307968","651264","827904","595968","221184","32768","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["0","18","744","14028","159552","1219608","6605856","26039952","75520128","160965120","249145344","273432576","204570624","97910784","26738688","3145728"],["-6","-260","-5048","-57880","-433824","-2212848","-7680288","-17114656","-18538528","16280320","99299840","179191808","179052544","103743488","32374784","4194304"],["0","-44","-1736","-30880","-326928","-2289504","-11142816","-38508928","-94769344","-163746752","-191771392","-141690880","-55648256","-4243456","4259840","1048576"],["0","0","-120","-4272","-68256","-645408","-4008960","-17163072","-51679104","-109676928","-161981568","-162014208","-105148416","-41582592","-8945664","-786432"],["0","0","0","-144","-4576","-64672","-534848","-2864960","-10390400","-25909120","-44237568","-50677248","-37585920","-17100800","-4308992","-458752"],["0","0","0","0","-64","-1792","-22016","-155648","-697856","-2062336","-4048896","-5210112","-4260864","-2109440","-573440","-65536"]]},"deriv_order":1},{"coeff":{"coeffs":[["1","50","1152","16208","155544","1076976","5548640","21618880","64090128","144257568","244113280","304974336","273512448","168976384","67534848","15597568","1572864"],["0","8","364","7584","95776","817728","4983840","22312192","74357120","184887936","340575936","457169408","435262464","282279936","117260288","27918336","2883584"],["0","0","24","984","18336","205248","1536576","8104512","30896640","85936896","173894016","252441984","256280064","174944256","75644928","18579456","1966080"],["0","0","0","32","1168","19200","187520","1208576","5397888","17070080","38373888","60713472","66054400","47599616","21454848","5439488","589824"],["0","0","0","0","16","512","7296","60928","330112","1213440","3074560","5351424","6275328","4788224","2252800","589824","65536"]]},"deriv_order":2}],[{"coeff":{"coeffs":[["1","40","746","8632","69380","409312","1818232","6119904","15480864","28827008","38193152","34213888","19210240","5996544","786432"],["2","74","1252","13028","95256","530632","2353520","8355376","23122816","47768512","69978112","68360192","41074688","13484032","1835008"],["0","0","-44","-1280","-15656","-100704","-320848","-39808","3890720","16394880","34757376","42352640","29179904","10452992","1507328"],["0","0","-32","-1080","-15840","-132048","-684288","-2247072","-4465024","-4291008","1195008","7682048","7716864","3293184","524288"],["0","0","0","-64","-1792","-21760","-149504","-634880","-1703936","-2817024","-2605056","-949248","274432","311296","65536"],["0","0","0","0","-32","-768","-7872","-44800","-153984","-325632","-413952","-297984","-110592","-16384","0"]]},"deriv_order":0},{"coeff":{"coeffs":[["-1","-42","-818","-9808","-80996","-487744","-2208568","-7630720","-20170656","-40480736","-60582528","-65628160","-49180672","-23781376","-6586368","-786432"],["0","2","88","1676","18312","127160","581840","1729168","2984160","1263488","-6943424","-18167296","-21678080","-14090240","-4767744","-655360"],["0","0","28","1008","16232","154144","957776","4082560","12167392","25356928","36355584","34681088","20852736","7266304","1245184","65536"],["0","0","0","56","1776","25040","206496","1102368","3981760","9880000","16767360","19063296","14004736","6297600","1564672","163840"],["0","0","0","0","32","896","11008","77824","348928","1031168","2024448","2605056","2130432","1054720","286720","32768"]]},"deriv_order":1},{"coeff":{"coeffs":[["0","-1","-46","-968","-12336","-106200","-652176","-2939936","-9859136","-24653584","-45643232","-61540352","-58812928","-38260736","-15933440","-3801088","-393216"],["0","0","-6","-248","-4656","-52480","-395408","-2097856","-8040896","-22475264","-45679712","-66570624","-67806208","-46411776","-20111360","-4947968","-524288"],["0","0","0","-12","-440","-7264","-71232","-460832","-2065472","-6552960","-14774528","-23436480","-25554816","-18448384","-8327168","-2113536","-229376"],["0","0","0","0","-8","-256","-3648","-30464","-165056","-606720","-1537280","-2675712","-3137664","-2394112","-1126400","-294912","-32768"]]},"deriv_order":2}]]}],"restart_bases":[],"row_multiplier":{"coeffs":[["1","24","244","1360","4484","8768","9600","5120","1024"],["0","4","80","656","2816","6672","8384","4864","1024"],["0","0","4","64","400","1216","1808","1152","256"]]},"start_base":1}},"shifted_parent_relation":{"terms":[{"coeff":{"coeffs":[["-1","-4"]]},"deriv_order":0,"shift":0},{"coeff":{"coeffs":[["-2","-4"]]},"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 = phi(n, D) = (1) D; so the candidate rows satisfy the input rule at every base n >= 1 (the exceptional bases checked exactly), and agreement on the 2 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"none"},"lean_declarations":["RealRooted.splits_add_C_mul_derivative_all","RealRooted.splits_C_mul_add_derivative","Polynomial.Splits.derivative"],"lift_summary":{"hypotheses":[{"evidence":"the polynomial with ascending coefficients [0, 1] is fixed; exact check: real-rooted = true, coefficients of one sign = true","name":"derivative_polynomial_real_rooted","statement":"the polynomial in D is real-rooted 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":{"reason":"no parent theorem report with an interlacing conclusion","status":"not_proved"},"lean_replay":"not_attempted","operation":{"description":"phi(n, D) = (1) D","kind":"preserver_image","operator":{"coefficients":[{"denominator":["1"],"numerator":["0"]},{"denominator":["1"],"numerator":["1"]}],"shape":"derivative_polynomial"}},"parent":{"gauge":{"kind":"none"},"index_shift":0,"recurrence":{"first_index":0,"initial_polynomials":[["1"],["3","4"]],"recurrence":{"terms":[{"coeff":{"coeffs":[["1","4"]]},"deriv_order":0,"offset":2,"sign":"none"},{"coeff":{"coeffs":[["2","4"]]},"deriv_order":0,"offset":1,"sign":"none"}]},"schema":"polytool.recurrence.v1"},"relation":"Q_n = lambda(n) T_n(P_(n+0)) with T = phi(n, D) = (1) D, for every n >= 0"},"parent_proof":{"route":"liu_wang_three_term","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 differential operators: if phi is a real polynomial with only real roots, then phi(D) maps every real-rooted polynomial to a real-rooted polynomial or zero (write phi(D) = C D^j prod (1 + c_i D); D preserves real-rootedness by Rolle's theorem and p + c p' is real-rooted for every real c by Rolle's theorem applied to e^(x/c) p; Polya--Schur 1914); when the coefficients of phi have one sign, coefficients of one sign stay of one sign; applied to phi(n, .) for each n"},"verdict":"proved"},"notes":["the division remainder is removed by row annihilators of the shifted parent"],"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":"not applicable: c_2(n, x) = gamma(n) w(x) with w neither constant nor a constant times a square (x + v_0)^2","route":"three_term_recurrence","success":false,"variant":"three_term_recurrence"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + c_1(n, x) P'_(n-1)","route":"liu_wang","success":false,"variant":"liu_wang"},{"detail":"HypothesisFailed: P_n = A_n(x) P_(n-1) + V_n(x) P'_(n-1) + W_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (4) x, V_n(x) = 0, W_n(x) = (1) + (4) x; open hypotheses: multipliers_vanish_at_zero: [x^0] c_2(n, x) = 1 is not the zero polynomial; lag_coefficient_nonpositive: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 there (exact); derivative_or_lag_coefficient_negative: W_n is not separable with a factor of one sign on (-inf, 0), and the sufficient monomial test (-1)^k [x^k] W_n <= 0 fails for k = 0 (not a disproof): fails at n = 2: [x^0] W_n = 1 there (exact)","route":"liu_wang_derivative_lag","success":false,"variant":"liu_wang_derivative_lag"},{"detail":"not applicable: the rule is not f(n) P_n = c_0(n, x) P_(n-1) + gamma(n) (x - L)(x - U) P'_(n-1)","route":"ma_wang_interval","success":false,"variant":"ma_wang_interval"},{"detail":"P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (4) x, B_n(x) = (1) + (4) x: every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2","route":"liu_wang_three_term","success":true,"variant":"liu_wang_three_term"}],"conditional_on":[],"interlacing":{"from_index":1,"justification":{"premises":["every hypothesis of the theorem is verified exactly for every index: P_n = A_n(x) P_(n-1) + B_n(x) P_(n-2) for n >= 2, with A_n(x) = (2) + (4) x, B_n(x) = (1) + (4) x","every P_n, n >= 0, is nonzero and real-rooted with every root in (-inf, -1/4] (so its coefficients have one sign); for n >= 1, P_(n-1) interlaces P_n (weakly, in the sense of Liu and Wang), and deg P_n - deg P_(n-1) is 0 or 1 for n >= 2"],"theorem":"liu_wang_three_term: L. L. Liu and Y. Wang, Adv. Appl. Math. 38 (2007) 542-560, Theorem 2.1 and Corollary 2.4 (A unified approach to polynomial sequences with only real zeros; the lag row as the interlacer, b_n = 0), weak interlacing of consecutive rows, with nonnegativity of the coefficients replaced, where a root region is certified, by an exact root-location induction"},"kind":"weak","orientation":"previous_interlaces_next"},"route":"liu_wang_three_term","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 = phi(n, D) = (1) D 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"}